Vampire---5.0.1.SAT-Sat.s

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

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

% Result   : Satisfiable 5.12s 1.89s
% Output   : Saturation 7.73s
% Verified : 
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)

% Comments : 
%------------------------------------------------------------------------------
cnf(u661,negated_conjecture,
    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(u1553,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0),true,iext(X0,uri_rdf_XMLLiteral,uri_rdf_XMLLiteral),true) ).

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

cnf(u1938,negated_conjecture,
    true = ifeq(icext(uri_rdfs_Datatype,X0),true,icext(uri_rdfs_Datatype,X0),true) ).

cnf(u289,negated_conjecture,
    true = sF34 ).

cnf(u556,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_range,X0),true,icext(X0,uri_rdfs_comment),true) ).

cnf(u2188,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdf_Property,X0),true,icext(X0,uri_rdfs_subPropertyOf),true) ).

cnf(u2323,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Class,X0),true,icext(X0,uri_rdf_Alt),true) ).

cnf(u406,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_range,X0),true,icext(X0,uri_rdfs_seeAlso),true) ).

cnf(u1944,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdfs_Datatype),true,ifeq(iext(X0,uri_rdf_XMLLiteral,X1),true,true,true),true) ).

cnf(u535,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X0),true,iext(X0,uri_rdf__3,uri_rdfs_Resource),true) ).

cnf(u2203,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_subClassOf,X0),true,icext(X0,uri_rdfs_Literal),true) ).

cnf(u2862,negated_conjecture,
    true = ifeq(iext(uri_rdf__2,X0,X1),true,iext(uri_rdfs_member,X0,X1),true) ).

cnf(u1589,negated_conjecture,
    true = ifeq(iext(uri_rdf_subject,X0,X1),true,iext(uri_rdf_subject,X0,X1),true) ).

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

cnf(u295,negated_conjecture,
    true = sF36 ).

cnf(u2458,negated_conjecture,
    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(u277,negated_conjecture,
    true = sF30 ).

cnf(u649,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_rdf_subject,uri_rdf_Property),true) ).

cnf(u4141,negated_conjecture,
    true = ifeq(sF46,true,ifeq(iext(uri_owl_equivalentClass,uri_rdfs_Seq,uri_rdfs_Container),true,true,true),true) ).

cnf(u7218,negated_conjecture,
    true = ifeq(sF46,true,ifeq(iext(uri_owl_equivalentClass,uri_rdfs_Seq,uri_rdfs_Resource),true,true,true),true) ).

cnf(u663,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_rdf__1,uri_rdf_Property),true) ).

cnf(u1426,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,X0,X1),true,true,true) ).

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

cnf(u824,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subClassOf,X0),true,icext(X0,uri_rdfs_Class),true) ).

cnf(u7200,negated_conjecture,
    true = ifeq(sF46,true,ifeq(iext(uri_owl_equivalentClass,uri_rdf_List,uri_rdfs_Resource),true,true,true),true) ).

cnf(u423,negated_conjecture,
    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(u2090,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdfs_Class),true,ifeq(iext(X0,X1,uri_rdf_XMLLiteral),true,true,true),true) ).

cnf(u3377,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Class,X0),true,icext(X0,uri_rdf_List),true) ).

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

cnf(u3599,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdf_Property,X0),true,icext(X0,uri_rdfs_comment),true) ).

cnf(u1953,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,X0,X1),true,true,true) ).

cnf(u3379,negated_conjecture,
    true = ic(uri_rdf_List) ).

cnf(u689,negated_conjecture,
    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(u822,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0),true,iext(X0,uri_rdfs_Datatype,uri_rdfs_Class),true) ).

cnf(u3645,negated_conjecture,
    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(u2104,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_rdf_XMLLiteral,uri_rdfs_Class),true) ).

cnf(u1186,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_type),true,ifeq(iext(X0,X1,uri_rdfs_Resource),true,true,true),true) ).

cnf(u335,negated_conjecture,
    true = iext(uri_rdf_type,uri_rdf_value,uri_rdf_Property) ).

cnf(u1057,negated_conjecture,
    true = ip(uri_rdfs_seeAlso) ).

cnf(u2489,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Resource,X0),true,iext(uri_rdfs_subClassOf,uri_rdf_XMLLiteral,X0),true) ).

cnf(u1734,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_rdfs_isDefinedBy),true) ).

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

cnf(u3754,negated_conjecture,
    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(u956,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_range,X0),true,icext(X0,uri_rdfs_domain),true) ).

cnf(u2374,negated_conjecture,
    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(u1989,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,X0,X1),true,iext(uri_rdfs_subClassOf,X0,X1),true) ).

cnf(u584,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_range,X0),true,icext(X0,uri_rdfs_label),true) ).

cnf(u3760,negated_conjecture,
    true = ifeq(iext(uri_rdf_predicate,X0,X1),true,iext(uri_rdf_predicate,X0,X1),true) ).

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

cnf(u4940,negated_conjecture,
    true = ifeq(sF46,true,ifeq(iext(uri_owl_equivalentClass,uri_rdfs_Datatype,uri_rdfs_Class),true,true,true),true) ).

cnf(u2185,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdf_Property),true,ifeq(iext(X0,X1,uri_rdfs_subPropertyOf),true,true,true),true) ).

cnf(u2880,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X0),true,iext(X0,uri_rdf__3,uri_rdfs_member),true) ).

cnf(u1098,negated_conjecture,
    true = icext(uri_rdfs_Datatype,uri_rdf_XMLLiteral) ).

cnf(u636,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_domain,X0),true,icext(X0,uri_rdfs_Statement),true) ).

cnf(u323,negated_conjecture,
    true = sF45 ).

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

cnf(u712,negated_conjecture,
    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(u346,negated_conjecture,
    true = iext(uri_rdfs_domain,uri_rdf_first,uri_rdf_List) ).

cnf(u2633,negated_conjecture,
    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(u1107,negated_conjecture,
    true = icext(uri_rdfs_ContainerMembershipProperty,uri_rdf__1) ).

cnf(u862,negated_conjecture,
    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(u7208,negated_conjecture,
    true = ifeq(sF46,true,ifeq(iext(uri_owl_equivalentClass,uri_rdfs_Container,uri_rdfs_Container),true,true,true),true) ).

cnf(u975,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(u2513,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Resource,X0),true,iext(uri_rdfs_subClassOf,uri_rdfs_Seq,X0),true) ).

cnf(u868,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,X0,uri_rdfs_Seq),true,iext(uri_rdfs_subClassOf,X0,uri_rdfs_Container),true) ).

cnf(u1220,negated_conjecture,
    true = ifeq(icext(uri_rdf_XMLLiteral,X0),true,icext(uri_rdfs_Literal,X0),true) ).

cnf(u2261,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdf_Property,X0),true,icext(X0,uri_rdfs_isDefinedBy),true) ).

cnf(u344,negated_conjecture,
    true = iext(uri_rdfs_domain,uri_rdfs_seeAlso,uri_rdfs_Resource) ).

cnf(u1127,negated_conjecture,
    true = ip(uri_rdf__1) ).

cnf(u2807,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf__1),true,iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_member),true) ).

cnf(u1339,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdf_Property),true,ifeq(iext(X0,X1,uri_rdf__3),true,true,true),true) ).

cnf(u1884,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_rdf__3),true) ).

cnf(u4443,negated_conjecture,
    true = ifeq(sF46,true,ifeq(iext(uri_owl_equivalentClass,uri_rdf_XMLLiteral,uri_rdfs_Literal),true,true,true),true) ).

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

cnf(u1389,negated_conjecture,
    true = iext(uri_rdfs_subPropertyOf,uri_rdf_rest,uri_rdf_rest) ).

cnf(u3688,negated_conjecture,
    true = ip(uri_rdf_predicate) ).

cnf(u4045,negated_conjecture,
    true = ifeq(sF46,true,ifeq(iext(uri_owl_equivalentClass,uri_rdf_Bag,uri_rdfs_Container),true,true,true),true) ).

cnf(u1224,negated_conjecture,
    true = ifeq(icext(uri_rdf_Alt,X0),true,icext(uri_rdfs_Container,X0),true) ).

cnf(u1882,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X0),true,iext(X0,uri_rdf__3,uri_rdf__3),true) ).

cnf(u217,negated_conjecture,
    true = sF10 ).

cnf(u363,negated_conjecture,
    true = iext(uri_rdfs_subClassOf,uri_rdfs_Seq,uri_rdfs_Container) ).

cnf(u1262,negated_conjecture,
    true = iext(uri_rdfs_subClassOf,uri_rdfs_Container,uri_rdfs_Container) ).

cnf(u716,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,uri_rdf_type,X0),true,icext(X0,uri_rdf_List),true) ).

cnf(u350,negated_conjecture,
    true = iext(uri_rdfs_subClassOf,uri_rdf_Alt,uri_rdfs_Container) ).

cnf(u2405,negated_conjecture,
    true = iext(uri_rdf_type,uri_rdfs_Resource,uri_rdfs_Class) ).

cnf(u3708,negated_conjecture,
    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(u1379,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdf_Property),true,ifeq(iext(X0,uri_rdf__1,X1),true,true,true),true) ).

cnf(u1517,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_rdfs_domain,uri_rdf_Property),true) ).

cnf(u223,negated_conjecture,
    true = sF12 ).

cnf(u361,negated_conjecture,
    true = iext(uri_rdf_type,uri_rdf__2,uri_rdfs_ContainerMembershipProperty) ).

cnf(u628,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,uri_rdf_type,X0),true,icext(X0,uri_rdfs_Datatype),true) ).

cnf(u256,negated_conjecture,
    true = sF23 ).

cnf(u2016,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdf_Property),true,ifeq(iext(X0,uri_rdfs_subClassOf,X1),true,true,true),true) ).

cnf(u1521,negated_conjecture,
    true = icext(uri_rdf_Property,uri_rdfs_domain) ).

cnf(u515,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X0),true,iext(X0,uri_rdf_value,uri_rdfs_Resource),true) ).

cnf(u658,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,uri_rdf_type,X0),true,icext(X0,uri_rdfs_ContainerMembershipProperty),true) ).

cnf(u3448,negated_conjecture,
    true = ifeq(icext(uri_rdf_List,X0),true,icext(uri_rdf_List,X0),true) ).

cnf(u2559,negated_conjecture,
    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(u2929,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Resource,X0),true,iext(uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty,X0),true) ).

cnf(u2172,negated_conjecture,
    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(u262,negated_conjecture,
    true = sF25 ).

cnf(u232,negated_conjecture,
    true = sF15 ).

cnf(u890,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X0),true,iext(X0,uri_rdfs_isDefinedBy,uri_rdfs_seeAlso),true) ).

cnf(u1106,negated_conjecture,
    true = icext(uri_rdf_Property,uri_rdf__1) ).

cnf(u2059,negated_conjecture,
    true = iext(uri_rdfs_subClassOf,uri_rdfs_Class,uri_rdfs_Resource) ).

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

cnf(u3576,negated_conjecture,
    true = icext(uri_rdf_Property,uri_rdfs_label) ).

cnf(u1551,negated_conjecture,
    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(u2690,negated_conjecture,
    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(u495,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X0),true,iext(X0,uri_rdf__2,uri_rdfs_Resource),true) ).

cnf(u3661,negated_conjecture,
    true = iext(uri_rdfs_subPropertyOf,uri_rdfs_label,uri_rdfs_label) ).

cnf(u1311,negated_conjecture,
    true = iext(uri_rdfs_subPropertyOf,uri_rdf_first,uri_rdf_first) ).

cnf(u2050,negated_conjecture,
    true = iext(uri_rdfs_subClassOf,uri_rdfs_Literal,uri_rdfs_Resource) ).

cnf(u1665,negated_conjecture,
    true = iext(uri_rdfs_subPropertyOf,uri_rdf_value,uri_rdf_value) ).

cnf(u787,negated_conjecture,
    true = ip(uri_rdfs_domain) ).

cnf(u3461,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Class,X0),true,icext(X0,uri_rdfs_Statement),true) ).

cnf(u896,axiom,
    true = ifeq(sF46,true,ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_owl_equivalentClass),true,iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_subClassOf),true),true) ).

cnf(u1679,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_rdf_value),true) ).

cnf(u2073,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0),true,iext(X0,uri_rdfs_Class,uri_rdfs_Class),true) ).

cnf(u1571,negated_conjecture,
    true = iext(uri_rdfs_subPropertyOf,uri_rdf_subject,uri_rdf_subject) ).

cnf(u2435,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0),true,iext(X0,uri_rdfs_Resource,uri_rdfs_Resource),true) ).

cnf(u1678,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X0),true,iext(X0,uri_rdf_value,uri_rdf_value),true) ).

cnf(u3472,negated_conjecture,
    true = iext(uri_rdfs_subClassOf,uri_rdfs_Statement,uri_rdfs_Resource) ).

cnf(u1439,negated_conjecture,
    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(u647,negated_conjecture,
    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(u2178,negated_conjecture,
    true = icext(uri_rdf_Property,uri_rdfs_subPropertyOf) ).

cnf(u1180,negated_conjecture,
    true = iext(uri_rdf_type,X0,uri_rdfs_Resource) ).

cnf(u3420,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Resource,X0),true,iext(uri_rdfs_subClassOf,uri_rdf_List,X0),true) ).

cnf(u2974,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_rdfs_member),true) ).

cnf(u3462,negated_conjecture,
    true = iext(uri_rdf_type,uri_rdfs_Statement,uri_rdfs_Class) ).

cnf(u2701,negated_conjecture,
    true = iext(uri_rdfs_subPropertyOf,uri_rdf__2,uri_rdfs_member) ).

cnf(u2357,negated_conjecture,
    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(u2074,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_subClassOf,X0),true,icext(X0,uri_rdfs_Class),true) ).

cnf(u3361,negated_conjecture,
    true = icext(uri_rdfs_Class,uri_rdf_List) ).

cnf(u7212,negated_conjecture,
    true = ifeq(sF46,true,ifeq(iext(uri_owl_equivalentClass,uri_rdf_Bag,uri_rdfs_Resource),true,true,true),true) ).

cnf(u2334,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_rdf_Alt,uri_rdfs_Class),true) ).

cnf(u1061,negated_conjecture,
    true = ip(uri_rdfs_isDefinedBy) ).

cnf(u7215,axiom,
    true = ifeq(sF46,true,ifeq(iext(uri_owl_equivalentClass,uri_rdfs_ContainerMembershipProperty,uri_rdfs_Resource),true,true,true),true) ).

cnf(u1322,negated_conjecture,
    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(u1042,negated_conjecture,
    true = ic(uri_rdfs_Container) ).

cnf(u3609,negated_conjecture,
    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(u1446,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,X0,X1),true,iext(uri_rdfs_range,X0,X1),true) ).

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

cnf(u405,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X0),true,iext(X0,uri_rdfs_seeAlso,uri_rdfs_Resource),true) ).

cnf(u656,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_rdf__1,uri_rdfs_ContainerMembershipProperty),true) ).

cnf(u2202,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0),true,iext(X0,uri_rdfs_Literal,uri_rdfs_Literal),true) ).

cnf(u2345,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdfs_Class),true,ifeq(iext(X0,X1,uri_rdfs_Class),true,true,true),true) ).

cnf(u2141,negated_conjecture,
    true = iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf) ).

cnf(u3731,negated_conjecture,
    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(u1189,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_rdf_type,X0),true,icext(X0,X1),true) ).

cnf(u562,negated_conjecture,
    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(u1849,negated_conjecture,
    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(u3737,negated_conjecture,
    true = ifeq(iext(uri_rdfs_label,X0,X1),true,iext(uri_rdfs_label,X0,X1),true) ).

cnf(u2174,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_rdfs_subPropertyOf,uri_rdf_Property),true) ).

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

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

cnf(u317,negated_conjecture,
    true = sF43 ).

cnf(u2973,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X0),true,iext(X0,uri_rdfs_member,uri_rdfs_member),true) ).

cnf(u3616,negated_conjecture,
    true = ip(uri_rdfs_comment) ).

cnf(u2858,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X0),true,iext(X0,uri_rdf__2,uri_rdfs_member),true) ).

cnf(u3387,negated_conjecture,
    true = iext(uri_rdfs_subClassOf,uri_rdf_List,uri_rdf_List) ).

cnf(u190,negated_conjecture,
    true = sF1 ).

cnf(u2380,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,X0,uri_rdfs_Class),true,iext(uri_rdfs_subClassOf,X0,uri_rdfs_Resource),true) ).

cnf(u2971,negated_conjecture,
    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(u934,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_range,X0),true,icext(X0,uri_rdfs_range),true) ).

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

cnf(u2864,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_member,X0),true,iext(uri_rdfs_subPropertyOf,uri_rdf__2,X0),true) ).

cnf(u3647,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_rdfs_label,uri_rdf_Property),true) ).

cnf(u2657,negated_conjecture,
    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(u161,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,X1),true,ip(X1),true) ).

cnf(u3710,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X0),true,iext(X0,uri_rdfs_comment,uri_rdfs_comment),true) ).

cnf(u445,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X0),true,iext(X0,uri_rdfs_member,uri_rdfs_Resource),true) ).

cnf(u696,negated_conjecture,
    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(u416,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_range,X0),true,icext(X0,uri_rdfs_isDefinedBy),true) ).

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

cnf(u1101,negated_conjecture,
    true = icext(uri_rdf_Property,uri_rdf_object) ).

cnf(u1461,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_rdfs_range,uri_rdf_Property),true) ).

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

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

cnf(u1210,negated_conjecture,
    true = iext(uri_rdfs_subPropertyOf,uri_rdfs_seeAlso,uri_rdfs_seeAlso) ).

cnf(u358,negated_conjecture,
    true = iext(uri_rdfs_range,uri_rdf__2,uri_rdfs_Resource) ).

cnf(u435,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X0),true,iext(X0,uri_rdf__1,uri_rdfs_Resource),true) ).

cnf(u2117,negated_conjecture,
    true = iext(uri_rdf_type,uri_rdf_Bag,uri_rdfs_Class) ).

cnf(u2247,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_rdfs_isDefinedBy,uri_rdf_Property),true) ).

cnf(u330,negated_conjecture,
    true = iext(uri_rdf_type,uri_rdf_rest,uri_rdf_Property) ).

cnf(u2618,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_rdfs_Datatype,uri_rdfs_Class),true) ).

cnf(u1465,negated_conjecture,
    true = icext(uri_rdf_Property,uri_rdfs_range) ).

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

cnf(u7217,negated_conjecture,
    true = ifeq(sF46,true,ifeq(iext(uri_owl_equivalentClass,uri_rdfs_Seq,uri_rdfs_Seq),true,true,true),true) ).

cnf(u7226,negated_conjecture,
    true = ifeq(sF46,true,ifeq(iext(uri_owl_equivalentClass,uri_rdfs_Class,uri_rdfs_Resource),true,true,true),true) ).

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

cnf(u1484,negated_conjecture,
    true = iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,uri_rdfs_domain) ).

cnf(u2118,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Class,X0),true,icext(X0,uri_rdf_Bag),true) ).

cnf(u2245,negated_conjecture,
    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(u328,negated_conjecture,
    true = iext(uri_rdf_type,uri_rdf_first,uri_rdf_Property) ).

cnf(u1111,negated_conjecture,
    true = icext(uri_rdf_Property,uri_rdf_first) ).

cnf(u3666,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdf_Property),true,ifeq(iext(X0,X1,uri_rdf_predicate),true,true,true),true) ).

cnf(u3683,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_rdf_predicate,uri_rdf_Property),true) ).

cnf(u1219,negated_conjecture,
    true = ifeq(icext(uri_rdfs_Datatype,X0),true,icext(uri_rdfs_Class,X0),true) ).

cnf(u1373,negated_conjecture,
    true = ifeq(icext(uri_rdf_Bag,X0),true,icext(uri_rdf_Bag,X0),true) ).

cnf(u3672,negated_conjecture,
    true = iext(uri_rdf_type,uri_rdf_predicate,uri_rdf_Property) ).

cnf(u7228,negated_conjecture,
    true = ifeq(sF46,true,ifeq(iext(uri_owl_equivalentClass,uri_rdfs_Statement,uri_rdfs_Statement),true,true,true),true) ).

cnf(u2186,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdf_Property),true,ifeq(iext(X0,uri_rdfs_subPropertyOf,X1),true,true,true),true) ).

cnf(u2396,negated_conjecture,
    true = icext(uri_rdfs_Class,uri_rdfs_Resource) ).

cnf(u347,negated_conjecture,
    true = iext(uri_rdfs_range,uri_rdf_first,uri_rdfs_Resource) ).

cnf(u334,negated_conjecture,
    true = iext(uri_rdf_type,uri_rdf_object,uri_rdf_Property) ).

cnf(u456,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_domain,X0),true,icext(X0,uri_rdfs_label),true) ).

cnf(u1821,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_subClassOf,X0),true,icext(X0,uri_rdfs_Container),true) ).

cnf(u1363,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0),true,iext(X0,uri_rdf_Bag,uri_rdf_Bag),true) ).

cnf(u2269,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdfs_Class),true,ifeq(iext(X0,X1,uri_rdfs_Seq),true,true,true),true) ).

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

cnf(u345,negated_conjecture,
    true = iext(uri_rdfs_range,uri_rdfs_seeAlso,uri_rdfs_Resource) ).

cnf(u475,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X0),true,iext(X0,uri_rdfs_seeAlso,uri_rdfs_Resource),true) ).

cnf(u368,negated_conjecture,
    true = iext(uri_rdfs_range,uri_rdf_predicate,uri_rdfs_Resource) ).

cnf(u2129,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_rdf_Bag,uri_rdfs_Class),true) ).

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

cnf(u1906,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_rdfs_seeAlso),true) ).

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

cnf(u1028,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(u473,negated_conjecture,
    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(u2156,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_rdfs_subPropertyOf),true) ).

cnf(u1971,negated_conjecture,
    true = iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,uri_rdfs_subClassOf) ).

cnf(u2030,negated_conjecture,
    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(u2680,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Class,X0),true,icext(X0,uri_rdfs_Literal),true) ).

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

cnf(u1632,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_rdf__1),true) ).

cnf(u1649,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty,X0),true,icext(X0,uri_rdf__1),true) ).

cnf(u1403,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_rdf_rest),true) ).

cnf(u247,negated_conjecture,
    true = sF20 ).

cnf(u2034,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subClassOf,X0),true,icext(X0,uri_rdf_Alt),true) ).

cnf(u2512,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,X0,uri_rdfs_Seq),true,iext(uri_rdfs_subClassOf,X0,uri_rdfs_Resource),true) ).

cnf(u3625,negated_conjecture,
    true = iext(uri_rdfs_subPropertyOf,uri_rdfs_comment,uri_rdfs_comment) ).

cnf(u617,negated_conjecture,
    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(u372,negated_conjecture,
    true = iext(uri_rdfs_domain,uri_rdf_value,uri_rdfs_Resource) ).

cnf(u2808,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_member,X0),true,iext(uri_rdfs_subPropertyOf,uri_rdf__1,X0),true) ).

cnf(u1295,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdf_Property,X0),true,icext(X0,uri_rdf_rest),true) ).

cnf(u7220,negated_conjecture,
    true = ifeq(sF46,true,ifeq(iext(uri_owl_equivalentClass,uri_rdf_XMLLiteral,uri_rdf_XMLLiteral),true,true,true),true) ).

cnf(u1540,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdf_Property,X0),true,icext(X0,uri_rdf_object),true) ).

cnf(u2830,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_rdfs_member,uri_rdf_Property),true) ).

cnf(u1008,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(u1538,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdf_Property),true,ifeq(iext(X0,uri_rdf_object,X1),true,true,true),true) ).

cnf(u385,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X0),true,iext(X0,uri_rdf_first,uri_rdfs_Resource),true) ).

cnf(u1555,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subClassOf,X0),true,icext(X0,uri_rdf_XMLLiteral),true) ).

cnf(u1365,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subClassOf,X0),true,icext(X0,uri_rdf_Bag),true) ).

cnf(u3456,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdfs_Class),true,ifeq(iext(X0,X1,uri_rdfs_Statement),true,true,true),true) ).

cnf(u2841,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdf_Property),true,ifeq(iext(X0,X1,uri_rdfs_member),true,true,true),true) ).

cnf(u634,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X0),true,iext(X0,uri_rdf_subject,uri_rdfs_Statement),true) ).

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

cnf(u7207,negated_conjecture,
    true = ifeq(sF46,true,ifeq(iext(uri_owl_equivalentClass,uri_rdf_Alt,uri_rdfs_Resource),true,true,true),true) ).

cnf(u1807,negated_conjecture,
    true = ifeq(icext(uri_rdfs_Seq,X0),true,icext(uri_rdfs_Seq,X0),true) ).

cnf(u2058,negated_conjecture,
    true = iext(uri_rdfs_subClassOf,uri_rdfs_Class,uri_rdfs_Class) ).

cnf(u2297,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_rdfs_seeAlso,uri_rdf_Property),true) ).

cnf(u1683,negated_conjecture,
    true = ifeq(iext(uri_rdf_value,X0,X1),true,iext(uri_rdf_value,X0,X1),true) ).

cnf(u2754,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(u543,negated_conjecture,
    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(u7211,negated_conjecture,
    true = ifeq(sF46,true,ifeq(iext(uri_owl_equivalentClass,uri_rdf_Bag,uri_rdf_Bag),true,true,true),true) ).

cnf(u3593,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdf_Property),true,ifeq(iext(X0,uri_rdfs_comment,X1),true,true,true),true) ).

cnf(u1300,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdf_Property),true,ifeq(iext(X0,X1,uri_rdf_subject),true,true,true),true) ).

cnf(u3347,negated_conjecture,
    true = icext(uri_rdfs_Class,uri_rdfs_Statement) ).

cnf(u2590,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Resource,X0),true,iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,X0),true) ).

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

cnf(u389,negated_conjecture,
    true = ifeq(iext(uri_rdf_first,X0,X1),true,true,true) ).

cnf(u640,negated_conjecture,
    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(u274,negated_conjecture,
    true = sF29 ).

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

cnf(u2281,negated_conjecture,
    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(u2359,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_rdfs_Class,uri_rdfs_Class),true) ).

cnf(u546,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_domain,X0),true,icext(X0,uri_rdf__2),true) ).

cnf(u3594,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdf_Property),true,ifeq(iext(X0,X1,uri_rdfs_comment),true,true,true),true) ).

cnf(u1428,negated_conjecture,
    true = iext(uri_rdfs_subPropertyOf,uri_rdfs_range,uri_rdfs_range) ).

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

cnf(u301,negated_conjecture,
    true = sF38 ).

cnf(u2464,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,X0,uri_rdf_Bag),true,iext(uri_rdfs_subClassOf,X0,uri_rdfs_Resource),true) ).

cnf(u3600,negated_conjecture,
    true = iext(uri_rdf_type,uri_rdfs_comment,uri_rdf_Property) ).

cnf(u3735,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_rdfs_label),true) ).

cnf(u2842,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdf_Property),true,ifeq(iext(X0,uri_rdfs_member,X1),true,true,true),true) ).

cnf(u801,negated_conjecture,
    true = ip(uri_rdf_type) ).

cnf(u3371,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdfs_Class),true,ifeq(iext(X0,uri_rdf_List,X1),true,true,true),true) ).

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

cnf(u2583,negated_conjecture,
    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(u2200,negated_conjecture,
    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(u1340,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdf_Property),true,ifeq(iext(X0,uri_rdf__3,X1),true,true,true),true) ).

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

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

cnf(u1190,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,uri_rdf_type,X0),true,icext(X0,uri_rdfs_Resource),true) ).

cnf(u429,negated_conjecture,
    true = ifeq(iext(uri_rdfs_comment,X0,X1),true,true,true) ).

cnf(u2231,negated_conjecture,
    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(u314,negated_conjecture,
    true = sF42 ).

cnf(u3499,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0),true,iext(X0,uri_rdfs_Statement,uri_rdfs_Resource),true) ).

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

cnf(u2155,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_rdfs_subPropertyOf),true) ).

cnf(u943,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(u3378,negated_conjecture,
    true = iext(uri_rdf_type,uri_rdf_List,uri_rdfs_Class) ).

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

cnf(u187,negated_conjecture,
    true = sF0 ).

cnf(u1188,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,X1,uri_rdfs_Resource),true) ).

cnf(u419,negated_conjecture,
    true = ifeq(iext(uri_rdfs_isDefinedBy,X0,X1),true,true,true) ).

cnf(u2102,negated_conjecture,
    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(u573,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X0),true,iext(X0,uri_rdf__3,uri_rdfs_Resource),true) ).

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

cnf(u1852,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_rdf_type),true) ).

cnf(u571,negated_conjecture,
    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(u2885,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf__3),true,iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_member),true) ).

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

cnf(u1498,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_rdfs_domain),true) ).

cnf(u836,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0),true,iext(X0,uri_rdf_Bag,uri_rdfs_Container),true) ).

cnf(u1102,negated_conjecture,
    true = icext(uri_rdf_Property,uri_rdf__3) ).

cnf(u684,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_rdf__2,uri_rdf_Property),true) ).

cnf(u2863,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf__2),true,iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_member),true) ).

cnf(u841,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Container,X0),true,iext(uri_rdfs_subClassOf,uri_rdf_Bag,X0),true) ).

cnf(u7198,axiom,
    true = ifeq(sF46,true,ifeq(iext(uri_owl_equivalentClass,uri_rdf_Property,uri_rdf_Property),true,true,true),true) ).

cnf(u3665,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdf_Property),true,ifeq(iext(X0,uri_rdf_predicate,X1),true,true,true),true) ).

cnf(u3398,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_rdf_List,uri_rdfs_Class),true) ).

cnf(u855,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Literal,X0),true,iext(uri_rdfs_subClassOf,uri_rdf_XMLLiteral,X0),true) ).

cnf(u7223,negated_conjecture,
    true = ifeq(sF46,true,ifeq(iext(uri_owl_equivalentClass,uri_rdfs_Datatype,uri_rdfs_Datatype),true,true,true),true) ).

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

cnf(u964,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(u331,negated_conjecture,
    true = iext(uri_rdf_type,uri_rdf__1,uri_rdf_Property) ).

cnf(u1230,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdf_Property),true,ifeq(iext(X0,X1,uri_rdf_first),true,true,true),true) ).

cnf(u7224,negated_conjecture,
    true = ifeq(sF46,true,ifeq(iext(uri_owl_equivalentClass,uri_rdfs_Datatype,uri_rdfs_Resource),true,true,true),true) ).

cnf(u446,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_range,X0),true,icext(X0,uri_rdfs_member),true) ).

cnf(u1856,negated_conjecture,
    true = ifeq(iext(uri_rdf_type,X0,X1),true,iext(uri_rdf_type,X0,X1),true) ).

cnf(u2639,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,X0,uri_rdf_Alt),true,iext(uri_rdfs_subClassOf,X0,uri_rdfs_Resource),true) ).

cnf(u1361,negated_conjecture,
    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(u2116,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdfs_Class),true,ifeq(iext(X0,uri_rdf_Bag,X1),true,true,true),true) ).

cnf(u1347,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdf_Property),true,ifeq(iext(X0,X1,uri_rdf__2),true,true,true),true) ).

cnf(u590,negated_conjecture,
    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(u1104,negated_conjecture,
    true = icext(uri_rdf_Property,uri_rdf__2) ).

cnf(u1607,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdfs_ContainerMembershipProperty),true,ifeq(iext(X0,X1,uri_rdf__2),true,true,true),true) ).

cnf(u2800,negated_conjecture,
    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(u329,negated_conjecture,
    true = iext(uri_rdf_type,uri_rdf_nil,uri_rdf_List) ).

cnf(u2508,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0),true,iext(X0,uri_rdfs_Seq,uri_rdfs_Resource),true) ).

cnf(u459,negated_conjecture,
    true = ifeq(iext(uri_rdfs_label,X0,X1),true,true,true) ).

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

cnf(u352,negated_conjecture,
    true = iext(uri_rdfs_domain,uri_rdfs_member,uri_rdfs_Resource) ).

cnf(u2886,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_member,X0),true,iext(uri_rdfs_subPropertyOf,uri_rdf__3,X0),true) ).

cnf(u1984,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X0),true,iext(X0,uri_rdfs_subClassOf,uri_rdfs_subClassOf),true) ).

cnf(u202,negated_conjecture,
    true = sF5 ).

cnf(u611,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_range,X0),true,icext(X0,uri_rdf_predicate),true) ).

cnf(u1629,negated_conjecture,
    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(u3416,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_subClassOf,X0),true,icext(X0,uri_rdf_List),true) ).

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

cnf(u1537,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdf_Property),true,ifeq(iext(X0,X1,uri_rdf_object),true,true,true),true) ).

cnf(u1610,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty,X0),true,icext(X0,uri_rdf__2),true) ).

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

cnf(u2140,negated_conjecture,
    true = iext(uri_rdf_type,uri_rdfs_subPropertyOf,uri_rdf_Property) ).

cnf(u2259,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdf_Property),true,ifeq(iext(X0,uri_rdfs_isDefinedBy,X1),true,true,true),true) ).

cnf(u852,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subClassOf,X0),true,icext(X0,uri_rdfs_Literal),true) ).

cnf(u2664,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Resource,X0),true,iext(uri_rdfs_subClassOf,uri_rdfs_Literal,X0),true) ).

cnf(u1495,negated_conjecture,
    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(u1633,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_rdf__1),true) ).

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

cnf(u1387,negated_conjecture,
    true = ifeq(iext(uri_rdf_rest,X0,X1),true,true,true) ).

cnf(u2700,negated_conjecture,
    true = iext(uri_rdfs_subPropertyOf,uri_rdf__1,uri_rdfs_member) ).

cnf(u864,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0),true,iext(X0,uri_rdfs_Seq,uri_rdfs_Container),true) ).

cnf(u1647,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdfs_ContainerMembershipProperty),true,ifeq(iext(X0,uri_rdf__1,X1),true,true,true),true) ).

cnf(u2018,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdf_Property,X0),true,icext(X0,uri_rdfs_subClassOf),true) ).

cnf(u369,negated_conjecture,
    true = iext(uri_rdfs_domain,uri_rdf_predicate,uri_rdfs_Statement) ).

cnf(u463,negated_conjecture,
    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(u601,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X0),true,iext(X0,uri_rdf_rest,uri_rdf_List),true) ).

cnf(u356,negated_conjecture,
    true = iext(uri_rdfs_domain,uri_rdf__3,uri_rdfs_Resource) ).

cnf(u2403,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdfs_Class),true,ifeq(iext(X0,X1,uri_rdfs_Resource),true,true,true),true) ).

cnf(u486,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_domain,X0),true,icext(X0,uri_rdfs_isDefinedBy),true) ).

cnf(u865,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_subClassOf,X0),true,icext(X0,uri_rdfs_Seq),true) ).

cnf(u1737,negated_conjecture,
    true = ifeq(iext(uri_rdfs_isDefinedBy,X0,X1),true,iext(uri_rdfs_isDefinedBy,X0,X1),true) ).

cnf(u986,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(u1761,negated_conjecture,
    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(u3629,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdf_Property),true,ifeq(iext(X0,uri_rdfs_label,X1),true,true,true),true) ).

cnf(u2283,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_rdfs_Seq,uri_rdfs_Class),true) ).

cnf(u2270,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdfs_Class),true,ifeq(iext(X0,uri_rdfs_Seq,X1),true,true,true),true) ).

cnf(u1502,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,X0,X1),true,iext(uri_rdfs_domain,X0,X1),true) ).

cnf(u229,negated_conjecture,
    true = sF14 ).

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

cnf(u375,axiom,
    true = ifeq(sF46,true,ifeq(iext(uri_owl_equivalentClass,X0,X1),true,iext(uri_rdfs_subClassOf,X0,X1),true),true) ).

cnf(u3681,negated_conjecture,
    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(u729,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X0),true,iext(X0,uri_rdf_predicate,uri_rdfs_Statement),true) ).

cnf(u900,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_subClassOf),true,ifeq(iext(uri_rdfs_subPropertyOf,uri_owl_equivalentClass,X0),true,sF46,true),true) ).

cnf(u2159,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,X1),true,iext(uri_rdfs_subPropertyOf,X0,X1),true) ).

cnf(u1905,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X0),true,iext(X0,uri_rdfs_seeAlso,uri_rdfs_seeAlso),true) ).

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

cnf(u1286,negated_conjecture,
    true = icext(uri_rdfs_Class,uri_rdfs_Seq) ).

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

cnf(u373,negated_conjecture,
    true = iext(uri_rdfs_range,uri_rdf_value,uri_rdfs_Resource) ).

cnf(u624,negated_conjecture,
    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(u503,negated_conjecture,
    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(u670,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_rdf_value,uri_rdf_Property),true) ).

cnf(u513,negated_conjecture,
    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(u268,negated_conjecture,
    true = sF27 ).

cnf(u898,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0),true,ifeq(sF46,true,iext(uri_rdfs_subPropertyOf,uri_owl_equivalentClass,X0),true),true) ).

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

cnf(u1284,negated_conjecture,
    true = iext(uri_rdfs_subClassOf,uri_rdfs_Seq,uri_rdfs_Seq) ).

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

cnf(u2320,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdfs_Class),true,ifeq(iext(X0,X1,uri_rdf_Alt),true,true,true),true) ).

cnf(u2506,negated_conjecture,
    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(u396,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_range,X0),true,icext(X0,uri_rdf_subject),true) ).

cnf(u2258,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdf_Property),true,ifeq(iext(X0,X1,uri_rdfs_isDefinedBy),true,true,true),true) ).

cnf(u244,negated_conjecture,
    true = sF19 ).

cnf(u774,negated_conjecture,
    true = ip(uri_rdfs_range) ).

cnf(u1418,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdf_Property),true,ifeq(iext(X0,uri_rdf_value,X1),true,true,true),true) ).

cnf(u2321,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdfs_Class),true,ifeq(iext(X0,uri_rdf_Alt,X1),true,true,true),true) ).

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

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

cnf(u2702,negated_conjecture,
    true = iext(uri_rdfs_subPropertyOf,uri_rdf__3,uri_rdfs_member) ).

cnf(u536,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_range,X0),true,icext(X0,uri_rdf__3),true) ).

cnf(u415,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X0),true,iext(X0,uri_rdfs_isDefinedBy,uri_rdfs_Resource),true) ).

cnf(u553,negated_conjecture,
    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(u386,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_range,X0),true,icext(X0,uri_rdf_first),true) ).

cnf(u1275,negated_conjecture,
    true = icext(uri_rdfs_Class,uri_rdf_Alt) ).

cnf(u902,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_seeAlso,X0),true,iext(uri_rdfs_subPropertyOf,uri_rdfs_isDefinedBy,X0),true) ).

cnf(u1301,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdf_Property),true,ifeq(iext(X0,uri_rdf_subject,X1),true,true,true),true) ).

cnf(u2251,negated_conjecture,
    true = icext(uri_rdf_Property,uri_rdfs_isDefinedBy) ).

cnf(u1050,negated_conjecture,
    true = ic(uri_rdfs_Datatype) ).

cnf(u1324,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X0),true,iext(X0,uri_rdf_first,uri_rdf_first),true) ).

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

cnf(u908,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(u413,negated_conjecture,
    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(u298,negated_conjecture,
    true = sF37 ).

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

cnf(u2585,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0),true,iext(X0,uri_rdfs_Datatype,uri_rdfs_Resource),true) ).

cnf(u1059,axiom,
    true = ifeq(sF46,true,ip(uri_owl_equivalentClass),true) ).

cnf(u3630,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdf_Property),true,ifeq(iext(X0,X1,uri_rdfs_label),true,true,true),true) ).

cnf(u2806,negated_conjecture,
    true = ifeq(iext(uri_rdf__1,X0,X1),true,iext(uri_rdfs_member,X0,X1),true) ).

cnf(u2465,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Resource,X0),true,iext(uri_rdfs_subClassOf,uri_rdf_Bag,X0),true) ).

cnf(u820,negated_conjecture,
    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(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(u403,negated_conjecture,
    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(u1830,negated_conjecture,
    true = ifeq(icext(uri_rdfs_Container,X0),true,icext(uri_rdfs_Container,X0),true) ).

cnf(u557,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_range,X0),true,icext(X0,uri_rdfs_Literal),true) ).

cnf(u3503,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,X0,uri_rdfs_Statement),true,iext(uri_rdfs_subClassOf,X0,uri_rdfs_Resource),true) ).

cnf(u426,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_domain,X0),true,icext(X0,uri_rdfs_comment),true) ).

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

cnf(u7201,negated_conjecture,
    true = ifeq(sF46,true,ifeq(iext(uri_owl_equivalentClass,uri_rdf_List,uri_rdf_List),true,true,true),true) ).

cnf(u555,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X0),true,iext(X0,uri_rdfs_comment,uri_rdfs_Literal),true) ).

cnf(u3758,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_rdf_predicate),true) ).

cnf(u1209,negated_conjecture,
    true = iext(uri_rdf_type,uri_rdfs_seeAlso,uri_rdf_Property) ).

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

cnf(u668,negated_conjecture,
    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(u7221,negated_conjecture,
    true = ifeq(sF46,true,ifeq(iext(uri_owl_equivalentClass,uri_rdf_XMLLiteral,uri_rdfs_Resource),true,true,true),true) ).

cnf(u953,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(u3437,negated_conjecture,
    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(u2378,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subClassOf,X0),true,icext(X0,uri_rdfs_Resource),true) ).

cnf(u574,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_domain,X0),true,icext(X0,uri_rdf__3),true) ).

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

cnf(u7214,axiom,
    true = ifeq(sF46,true,ifeq(iext(uri_owl_equivalentClass,uri_rdfs_ContainerMembershipProperty,uri_rdfs_ContainerMembershipProperty),true,true,true),true) ).

cnf(u7225,negated_conjecture,
    true = ifeq(sF46,true,ifeq(iext(uri_owl_equivalentClass,uri_rdfs_Class,uri_rdfs_Class),true,true,true),true) ).

cnf(u443,negated_conjecture,
    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(u2093,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Class,X0),true,icext(X0,uri_rdf_XMLLiteral),true) ).

cnf(u1099,negated_conjecture,
    true = icext(uri_rdf_Property,uri_rdf_subject) ).

cnf(u827,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Class,X0),true,iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,X0),true) ).

cnf(u2383,negated_conjecture,
    true = ic(uri_rdfs_Resource) ).

cnf(u6578,axiom,
    true = ifeq(sF46,true,ifeq(iext(uri_rdfs_subPropertyOf,uri_owl_equivalentClass,uri_owl_equivalentClass),true,sF46,true),true) ).

cnf(u3396,negated_conjecture,
    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(u2115,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdfs_Class),true,ifeq(iext(X0,X1,uri_rdf_Bag),true,true,true),true) ).

cnf(u2677,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdfs_Class),true,ifeq(iext(X0,X1,uri_rdfs_Literal),true,true,true),true) ).

cnf(u336,negated_conjecture,
    true = iext(uri_rdf_type,uri_rdf_subject,uri_rdf_Property) ).

cnf(u1473,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdf_Property),true,ifeq(iext(X0,X1,uri_rdfs_range),true,true,true),true) ).

cnf(u595,negated_conjecture,
    true = ifeq(iext(uri_rdf_rest,X0,X1),true,icext(uri_rdf_List,X1),true) ).

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

cnf(u2381,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Resource,X0),true,iext(uri_rdfs_subClassOf,uri_rdfs_Class,X0),true) ).

cnf(u1264,negated_conjecture,
    true = icext(uri_rdfs_Class,uri_rdfs_Container) ).

cnf(u3757,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_rdf_predicate),true) ).

cnf(u1124,negated_conjecture,
    true = ip(uri_rdf_object) ).

cnf(u2678,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdfs_Class),true,ifeq(iext(X0,uri_rdfs_Literal,X1),true,true,true),true) ).

cnf(u342,negated_conjecture,
    true = iext(uri_rdfs_domain,uri_rdfs_label,uri_rdfs_Resource) ).

cnf(u1880,negated_conjecture,
    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(u1600,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdfs_ContainerMembershipProperty),true,ifeq(iext(X0,uri_rdf__3,X1),true,true,true),true) ).

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

cnf(u2640,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Resource,X0),true,iext(uri_rdfs_subClassOf,uri_rdf_Alt,X0),true) ).

cnf(u2004,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_rdfs_subClassOf,uri_rdf_Property),true) ).

cnf(u2139,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,X1),true,true,true) ).

cnf(u614,negated_conjecture,
    true = ifeq(iext(uri_rdf_predicate,X0,X1),true,true,true) ).

cnf(u3413,negated_conjecture,
    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(u848,negated_conjecture,
    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(u1631,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X0),true,iext(X0,uri_rdf__1,uri_rdf__1),true) ).

cnf(u2394,negated_conjecture,
    true = iext(uri_rdfs_subClassOf,uri_rdfs_Resource,uri_rdfs_Resource) ).

cnf(u353,negated_conjecture,
    true = iext(uri_rdfs_range,uri_rdfs_member,uri_rdfs_Resource) ).

cnf(u340,negated_conjecture,
    true = iext(uri_rdfs_range,uri_rdfs_isDefinedBy,uri_rdfs_Resource) ).

cnf(u869,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Container,X0),true,iext(uri_rdfs_subClassOf,uri_rdfs_Seq,X0),true) ).

cnf(u599,negated_conjecture,
    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(u970,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,X1),true,icext(uri_rdf_Property,X1),true) ).

cnf(u1636,negated_conjecture,
    true = ifeq(iext(uri_rdf__1,X0,X1),true,iext(uri_rdf__1,X0,X1),true) ).

cnf(u1499,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_rdfs_domain),true) ).

cnf(u359,negated_conjecture,
    true = iext(uri_rdfs_range,uri_rdf__3,uri_rdfs_Resource) ).

cnf(u1105,negated_conjecture,
    true = icext(uri_rdfs_ContainerMembershipProperty,uri_rdf__2) ).

cnf(u1883,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_rdf__3),true) ).

cnf(u2071,negated_conjecture,
    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(u997,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(u882,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,X0,uri_rdf_Alt),true,iext(uri_rdfs_subClassOf,X0,uri_rdfs_Container),true) ).

cnf(u2002,negated_conjecture,
    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(u727,negated_conjecture,
    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(u602,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_domain,X0),true,icext(X0,uri_rdf_rest),true) ).

cnf(u1764,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_rdf_object),true) ).

cnf(u3611,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_rdfs_comment,uri_rdf_Property),true) ).

cnf(u1781,negated_conjecture,
    true = iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,uri_rdfs_Datatype) ).

cnf(u888,negated_conjecture,
    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(u357,negated_conjecture,
    true = iext(uri_rdfs_range,uri_rdf__1,uri_rdfs_Resource) ).

cnf(u608,negated_conjecture,
    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(u1903,negated_conjecture,
    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(u2154,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X0),true,iext(X0,uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf),true) ).

cnf(u3441,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subClassOf,X0),true,icext(X0,uri_rdf_List),true) ).

cnf(u1233,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdf_Property,X0),true,icext(X0,uri_rdf_first),true) ).

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

cnf(u1768,negated_conjecture,
    true = ifeq(iext(uri_rdf_object,X0,X1),true,iext(uri_rdf_object,X0,X1),true) ).

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

cnf(u2049,negated_conjecture,
    true = iext(uri_rdfs_subClassOf,uri_rdfs_Literal,uri_rdfs_Literal) ).

cnf(u2271,negated_conjecture,
    true = iext(uri_rdf_type,uri_rdfs_Seq,uri_rdfs_Class) ).

cnf(u1122,negated_conjecture,
    true = ip(uri_rdf_subject) ).

cnf(u675,negated_conjecture,
    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(u115,axiom,
    true = ifeq(icext(uri_rdfs_Class,X0),true,ic(X0),true) ).

cnf(u253,negated_conjecture,
    true = sF22 ).

cnf(u271,negated_conjecture,
    true = sF28 ).

cnf(u485,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X0),true,iext(X0,uri_rdfs_isDefinedBy,uri_rdfs_Resource),true) ).

cnf(u3652,negated_conjecture,
    true = ip(uri_rdfs_label) ).

cnf(u370,negated_conjecture,
    true = iext(uri_rdfs_domain,uri_rdf_subject,uri_rdfs_Statement) ).

cnf(u1795,negated_conjecture,
    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(u1400,negated_conjecture,
    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(u1530,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdf_Property),true,ifeq(iext(X0,uri_rdfs_domain,X1),true,true,true),true) ).

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

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

cnf(u3571,negated_conjecture,
    true = icext(uri_rdf_Property,uri_rdf_predicate) ).

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

cnf(u399,negated_conjecture,
    true = ifeq(iext(uri_rdf_subject,X0,X1),true,true,true) ).

cnf(u1273,negated_conjecture,
    true = iext(uri_rdfs_subClassOf,uri_rdf_Alt,uri_rdf_Alt) ).

cnf(u2692,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_rdfs_Literal,uri_rdfs_Class),true) ).

cnf(u1053,negated_conjecture,
    true = ic(uri_rdf_Bag) ).

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

cnf(u1285,negated_conjecture,
    true = iext(uri_rdfs_subClassOf,uri_rdfs_Seq,uri_rdfs_Resource) ).

cnf(u3463,negated_conjecture,
    true = ic(uri_rdfs_Statement) ).

cnf(u642,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_rdf_rest,uri_rdf_Property),true) ).

cnf(u1928,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0),true,iext(X0,uri_rdfs_Datatype,uri_rdfs_Datatype),true) ).

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

cnf(u241,negated_conjecture,
    true = sF18 ).

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

cnf(u259,negated_conjecture,
    true = sF24 ).

cnf(u1943,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdfs_Datatype),true,ifeq(iext(X0,X1,uri_rdf_XMLLiteral),true,true,true),true) ).

cnf(u496,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_range,X0),true,icext(X0,uri_rdf__2),true) ).

cnf(u2295,negated_conjecture,
    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(u2332,negated_conjecture,
    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(u682,negated_conjecture,
    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(u2220,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdfs_Class),true,ifeq(iext(X0,uri_rdfs_Container,X1),true,true,true),true) ).

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

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

cnf(u1070,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(u387,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_range,X0),true,icext(X0,uri_rdfs_Resource),true) ).

cnf(u280,negated_conjecture,
    true = sF31 ).

cnf(u3415,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0),true,iext(X0,uri_rdf_List,uri_rdfs_Resource),true) ).

cnf(u3635,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdf_Property,X0),true,icext(X0,uri_rdfs_label),true) ).

cnf(u1417,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdf_Property),true,ifeq(iext(X0,X1,uri_rdf_value),true,true,true),true) ).

cnf(u1820,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0),true,iext(X0,uri_rdfs_Container,uri_rdfs_Container),true) ).

cnf(u539,negated_conjecture,
    true = ifeq(iext(uri_rdf__3,X0,X1),true,true,true) ).

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

cnf(u1325,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_rdf_first),true) ).

cnf(u823,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_subClassOf,X0),true,icext(X0,uri_rdfs_Datatype),true) ).

cnf(u1818,negated_conjecture,
    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(u153,axiom,
    true = iext(uri_rdfs_range,uri_rdfs_subClassOf,uri_rdfs_Class) ).

cnf(u2348,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Class,X0),true,icext(X0,uri_rdfs_Class),true) ).

cnf(u286,negated_conjecture,
    true = sF33 ).

cnf(u1329,negated_conjecture,
    true = ifeq(iext(uri_rdf_first,X0,X1),true,iext(uri_rdf_first,X0,X1),true) ).

cnf(u558,negated_conjecture,
    true = ifeq(iext(uri_rdfs_comment,X0,X1),true,icext(uri_rdfs_Literal,X1),true) ).

cnf(u2221,negated_conjecture,
    true = iext(uri_rdf_type,uri_rdfs_Container,uri_rdfs_Class) ).

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

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

cnf(u1946,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,X0),true,icext(X0,uri_rdf_XMLLiteral),true) ).

cnf(u2777,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(u564,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X0),true,iext(X0,uri_rdf_first,uri_rdf_List),true) ).

cnf(u427,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_domain,X0),true,icext(X0,uri_rdfs_Resource),true) ).

cnf(u7206,negated_conjecture,
    true = ifeq(sF46,true,ifeq(iext(uri_owl_equivalentClass,uri_rdf_Alt,uri_rdf_Alt),true,true,true),true) ).

cnf(u2604,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdfs_Class),true,ifeq(iext(X0,uri_rdfs_Datatype,X1),true,true,true),true) ).

cnf(u2212,negated_conjecture,
    true = ifeq(icext(uri_rdfs_Literal,X0),true,icext(uri_rdfs_Literal,X0),true) ).

cnf(u1443,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_rdfs_range),true) ).

cnf(u2605,negated_conjecture,
    true = iext(uri_rdf_type,uri_rdfs_Datatype,uri_rdfs_Class) ).

cnf(u920,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(u425,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X0),true,iext(X0,uri_rdfs_comment,uri_rdfs_Resource),true) ).

cnf(u1982,negated_conjecture,
    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(u581,negated_conjecture,
    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(u320,negated_conjecture,
    true = sF44 ).

cnf(u1584,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X0),true,iext(X0,uri_rdf_subject,uri_rdf_subject),true) ).

cnf(u826,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,X0,uri_rdfs_Datatype),true,iext(uri_rdfs_subClassOf,X0,uri_rdfs_Class),true) ).

cnf(u545,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X0),true,iext(X0,uri_rdf__2,uri_rdfs_Resource),true) ).

cnf(u939,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdfs_Resource),true,ifeq(iext(X0,X1,X2),true,true,true),true) ).

cnf(u1342,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdf_Property,X0),true,icext(X0,uri_rdf__3),true) ).

cnf(u3712,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_rdfs_comment),true) ).

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

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

cnf(u326,negated_conjecture,
    true != sF46 ).

cnf(u709,negated_conjecture,
    true = ifeq(iext(uri_rdf_object,X0,X1),true,icext(uri_rdfs_Statement,X0),true) ).

cnf(u2406,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Class,X0),true,icext(X0,uri_rdfs_Resource),true) ).

cnf(u199,negated_conjecture,
    true = sF4 ).

cnf(u1986,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_rdfs_subClassOf),true) ).

cnf(u337,negated_conjecture,
    true = iext(uri_rdfs_domain,uri_rdfs_comment,uri_rdfs_Resource) ).

cnf(u604,negated_conjecture,
    true = ifeq(iext(uri_rdf_rest,X0,X1),true,icext(uri_rdf_List,X0),true) ).

cnf(u1018,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(u594,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_range,X0),true,icext(X0,uri_rdf_List),true) ).

cnf(u583,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X0),true,iext(X0,uri_rdfs_label,uri_rdfs_Literal),true) ).

cnf(u3532,negated_conjecture,
    true = ifeq(icext(uri_rdfs_Statement,X0),true,icext(uri_rdfs_Statement,X0),true) ).

cnf(u851,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_subClassOf,X0),true,icext(X0,uri_rdf_XMLLiteral),true) ).

cnf(u1869,negated_conjecture,
    true = iext(uri_rdfs_subPropertyOf,uri_rdf__3,uri_rdf__3) ).

cnf(u343,negated_conjecture,
    true = iext(uri_rdfs_range,uri_rdfs_label,uri_rdfs_Literal) ).

cnf(u1618,negated_conjecture,
    true = iext(uri_rdfs_subPropertyOf,uri_rdf__1,uri_rdf__1) ).

cnf(u465,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X0),true,iext(X0,uri_rdf_value,uri_rdfs_Resource),true) ).

cnf(u2635,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0),true,iext(X0,uri_rdf_Alt,uri_rdfs_Resource),true) ).

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

cnf(u208,negated_conjecture,
    true = sF7 ).

cnf(u2127,negated_conjecture,
    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(u586,negated_conjecture,
    true = ifeq(iext(uri_rdfs_label,X0,X1),true,icext(uri_rdfs_Literal,X1),true) ).

cnf(u1748,negated_conjecture,
    true = ifeq(iext(uri_rdf_object,X0,X1),true,true,true) ).

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

cnf(u341,negated_conjecture,
    true = iext(uri_rdfs_subPropertyOf,uri_rdfs_isDefinedBy,uri_rdfs_seeAlso) ).

cnf(u592,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X0),true,iext(X0,uri_rdf_rest,uri_rdf_List),true) ).

cnf(u1887,negated_conjecture,
    true = ifeq(iext(uri_rdf__3,X0,X1),true,iext(uri_rdf__3,X0,X1),true) ).

cnf(u364,negated_conjecture,
    true = iext(uri_rdfs_subClassOf,uri_rdf_XMLLiteral,uri_rdfs_Literal) ).

cnf(u1797,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0),true,iext(X0,uri_rdfs_Seq,uri_rdfs_Seq),true) ).

cnf(u1654,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdf_List),true,ifeq(iext(X0,X1,uri_rdf_nil),true,true,true),true) ).

cnf(u214,negated_conjecture,
    true = sF9 ).

cnf(u1125,negated_conjecture,
    true = ip(uri_rdf__3) ).

cnf(u714,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_rdf_nil,uri_rdf_List),true) ).

cnf(u7202,negated_conjecture,
    true = ifeq(sF46,true,ifeq(iext(uri_owl_equivalentClass,uri_rdfs_Resource,uri_rdfs_Resource),true,true,true),true) ).

cnf(u383,negated_conjecture,
    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(u469,negated_conjecture,
    true = ifeq(iext(uri_rdf_value,X0,X1),true,true,true) ).

cnf(u2015,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdf_Property),true,ifeq(iext(X0,X1,uri_rdfs_subClassOf),true,true,true),true) ).

cnf(u354,negated_conjecture,
    true = iext(uri_rdfs_domain,uri_rdf__1,uri_rdfs_Resource) ).

cnf(u1129,negated_conjecture,
    true = ip(uri_rdf_first) ).

cnf(u1782,negated_conjecture,
    true = iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,uri_rdfs_Resource) ).

cnf(u2565,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,X0,uri_rdfs_Container),true,iext(uri_rdfs_subClassOf,X0,uri_rdfs_Resource),true) ).

cnf(u1253,negated_conjecture,
    true = iext(uri_rdfs_subClassOf,uri_rdf_Bag,uri_rdfs_Resource) ).

cnf(u2152,negated_conjecture,
    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(u626,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_rdf_XMLLiteral,uri_rdfs_Datatype),true) ).

cnf(u876,negated_conjecture,
    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(u632,negated_conjecture,
    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(u1799,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subClassOf,X0),true,icext(X0,uri_rdfs_Seq),true) ).

cnf(u2922,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(u3697,negated_conjecture,
    true = iext(uri_rdfs_subPropertyOf,uri_rdf_predicate,uri_rdf_predicate) ).

cnf(u2804,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_rdfs_member),true) ).

cnf(u2566,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Resource,X0),true,iext(uri_rdfs_subClassOf,uri_rdfs_Container,X0),true) ).

cnf(u1243,negated_conjecture,
    true = icext(uri_rdfs_Class,uri_rdf_XMLLiteral) ).

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

cnf(u895,negated_conjecture,
    true = ifeq(sF46,true,true,true) ).

cnf(u1292,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdf_Property),true,ifeq(iext(X0,X1,uri_rdf_rest),true,true,true),true) ).

cnf(u371,negated_conjecture,
    true = iext(uri_rdfs_range,uri_rdf_subject,uri_rdfs_Resource) ).

cnf(u1041,negated_conjecture,
    true = ic(uri_rdfs_Literal) ).

cnf(u1263,negated_conjecture,
    true = iext(uri_rdfs_subClassOf,uri_rdfs_Container,uri_rdfs_Resource) ).

cnf(u1407,negated_conjecture,
    true = ifeq(iext(uri_rdf_rest,X0,X1),true,iext(uri_rdf_rest,X0,X1),true) ).

cnf(u2308,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdf_Property),true,ifeq(iext(X0,X1,uri_rdfs_seeAlso),true,true,true),true) ).

cnf(u3579,negated_conjecture,
    true = icext(uri_rdf_Property,uri_rdfs_comment) ).

cnf(u2311,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdf_Property,X0),true,icext(X0,uri_rdfs_seeAlso),true) ).

cnf(u915,negated_conjecture,
    true = ifeq(iext(uri_rdf_type,X0,X1),true,true,true) ).

cnf(u1274,negated_conjecture,
    true = iext(uri_rdfs_subClassOf,uri_rdf_Alt,uri_rdfs_Resource) ).

cnf(u2433,negated_conjecture,
    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(u1420,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdf_Property,X0),true,icext(X0,uri_rdf_value),true) ).

cnf(u1054,negated_conjecture,
    true = ic(uri_rdf_Alt) ).

cnf(u499,negated_conjecture,
    true = ifeq(iext(uri_rdf__2,X0,X1),true,true,true) ).

cnf(u525,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X0),true,iext(X0,uri_rdfs_member,uri_rdfs_Resource),true) ).

cnf(u3471,negated_conjecture,
    true = iext(uri_rdfs_subClassOf,uri_rdfs_Statement,uri_rdfs_Statement) ).

cnf(u1529,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdf_Property),true,ifeq(iext(X0,X1,uri_rdfs_domain),true,true,true),true) ).

cnf(u2436,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_subClassOf,X0),true,icext(X0,uri_rdfs_Resource),true) ).

cnf(u523,negated_conjecture,
    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(u910,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X0),true,iext(X0,uri_rdf_type,uri_rdfs_Resource),true) ).

cnf(u1378,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdf_Property),true,ifeq(iext(X0,X1,uri_rdf__1),true,true,true),true) ).

cnf(u1052,negated_conjecture,
    true = ic(uri_rdfs_Seq) ).

cnf(u283,negated_conjecture,
    true = sF32 ).

cnf(u2856,negated_conjecture,
    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(u1926,negated_conjecture,
    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(u2810,negated_conjecture,
    true = ip(uri_rdfs_member) ).

cnf(u706,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X0),true,iext(X0,uri_rdf_object,uri_rdfs_Statement),true) ).

cnf(u2978,negated_conjecture,
    true = ifeq(iext(uri_rdfs_member,X0,X1),true,iext(uri_rdfs_member,X0,X1),true) ).

cnf(u1930,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subClassOf,X0),true,icext(X0,uri_rdfs_Datatype),true) ).

cnf(u2460,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0),true,iext(X0,uri_rdf_Bag,uri_rdfs_Resource),true) ).

cnf(u2083,negated_conjecture,
    true = ifeq(icext(uri_rdfs_Class,X0),true,icext(uri_rdfs_Class,X0),true) ).

cnf(u1838,negated_conjecture,
    true = iext(uri_rdfs_subPropertyOf,uri_rdf_type,uri_rdf_type) ).

cnf(u565,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_domain,X0),true,icext(X0,uri_rdf_first),true) ).

cnf(u304,negated_conjecture,
    true = sF39 ).

cnf(u3482,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_rdfs_Statement,uri_rdfs_Class),true) ).

cnf(u1441,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X0),true,iext(X0,uri_rdfs_range,uri_rdfs_range),true) ).

cnf(u3756,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X0),true,iext(X0,uri_rdf_predicate,uri_rdf_predicate),true) ).

cnf(u2844,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdf_Property,X0),true,icext(X0,uri_rdfs_member),true) ).

cnf(u1427,negated_conjecture,
    true = iext(uri_rdf_type,uri_rdfs_range,uri_rdf_Property) ).

cnf(u311,negated_conjecture,
    true = sF40 ).

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

cnf(u409,negated_conjecture,
    true = ifeq(iext(uri_rdfs_seeAlso,X0,X1),true,true,true) ).

cnf(u2092,negated_conjecture,
    true = iext(uri_rdf_type,uri_rdf_XMLLiteral,uri_rdfs_Class) ).

cnf(u310,negated_conjecture,
    true = sF41 ).

cnf(u2616,negated_conjecture,
    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(u2589,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,X0,uri_rdfs_Datatype),true,iext(uri_rdfs_subClassOf,X0,uri_rdfs_Resource),true) ).

cnf(u1585,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_rdf_subject),true) ).

cnf(u3388,negated_conjecture,
    true = iext(uri_rdfs_subClassOf,uri_rdf_List,uri_rdfs_Resource) ).

cnf(u691,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_rdf__3,uri_rdfs_ContainerMembershipProperty),true) ).

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

cnf(u1326,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_rdf_first),true) ).

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

cnf(u2482,negated_conjecture,
    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(u1599,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdfs_ContainerMembershipProperty),true,ifeq(iext(X0,X1,uri_rdf__3),true,true,true),true) ).

cnf(u1970,negated_conjecture,
    true = iext(uri_rdf_type,uri_rdfs_subClassOf,uri_rdf_Property) ).

cnf(u1223,negated_conjecture,
    true = ifeq(icext(uri_rdf_Bag,X0),true,icext(uri_rdfs_Container,X0),true) ).

cnf(u1707,negated_conjecture,
    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(u1696,negated_conjecture,
    true = iext(uri_rdfs_subPropertyOf,uri_rdf__2,uri_rdf__2) ).

cnf(u567,negated_conjecture,
    true = ifeq(iext(uri_rdf_first,X0,X1),true,icext(uri_rdf_List,X0),true) ).

cnf(u938,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdfs_Resource),true,ifeq(iext(X0,X1,X2),true,true,true),true) ).

cnf(u5114,axiom,
    true = ifeq(sF46,true,ifeq(iext(uri_owl_equivalentClass,uri_rdfs_ContainerMembershipProperty,uri_rdf_Property),true,true,true),true) ).

cnf(u1853,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_rdf_type),true) ).

cnf(u436,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_range,X0),true,icext(X0,uri_rdf__1),true) ).

cnf(u1851,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X0),true,iext(X0,uri_rdf_type,uri_rdf_type),true) ).

cnf(u837,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_subClassOf,X0),true,icext(X0,uri_rdf_Bag),true) ).

cnf(u1459,negated_conjecture,
    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(u2894,axiom,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdf_Property),true,ifeq(iext(X0,X1,uri_rdf_type),true,true,true),true) ).

cnf(u1646,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdfs_ContainerMembershipProperty),true,ifeq(iext(X0,X1,uri_rdf__1),true,true,true),true) ).

cnf(u2404,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdfs_Class),true,ifeq(iext(X0,uri_rdfs_Resource,X1),true,true,true),true) ).

cnf(u327,negated_conjecture,
    true = icext(uri_rdfs_Resource,X0) ).

cnf(u1602,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty,X0),true,icext(X0,uri_rdf__3),true) ).

cnf(u449,negated_conjecture,
    true = ifeq(iext(uri_rdfs_member,X0,X1),true,true,true) ).

cnf(u1201,negated_conjecture,
    true = iext(uri_rdf_type,uri_rdfs_isDefinedBy,uri_rdf_Property) ).

cnf(u2376,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0),true,iext(X0,uri_rdfs_Class,uri_rdfs_Resource),true) ).

cnf(u850,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0),true,iext(X0,uri_rdf_XMLLiteral,uri_rdfs_Literal),true) ).

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

cnf(u698,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_rdf__3,uri_rdf_Property),true) ).

cnf(u1732,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X0),true,iext(X0,uri_rdfs_isDefinedBy,uri_rdfs_isDefinedBy),true) ).

cnf(u2222,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Class,X0),true,icext(X0,uri_rdfs_Container),true) ).

cnf(u325,axiom,
    iext(uri_rdfs_subPropertyOf,uri_owl_equivalentClass,uri_rdfs_subClassOf) = sF46 ).

cnf(u455,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X0),true,iext(X0,uri_rdfs_label,uri_rdfs_Resource),true) ).

cnf(u1730,negated_conjecture,
    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(u593,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_range,X0),true,icext(X0,uri_rdf_rest),true) ).

cnf(u348,negated_conjecture,
    true = iext(uri_rdfs_domain,uri_rdf_rest,uri_rdf_List) ).

cnf(u1109,negated_conjecture,
    true = icext(uri_rdf_List,uri_rdf_nil) ).

cnf(u1765,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_rdf_object),true) ).

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

cnf(u1985,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_rdfs_subClassOf),true) ).

cnf(u2219,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdfs_Class),true,ifeq(iext(X0,X1,uri_rdfs_Container),true,true,true),true) ).

cnf(u367,negated_conjecture,
    true = iext(uri_rdfs_domain,uri_rdf_object,uri_rdfs_Statement) ).

cnf(u453,negated_conjecture,
    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(u704,negated_conjecture,
    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(u3671,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdf_Property,X0),true,icext(X0,uri_rdf_predicate),true) ).

cnf(u338,negated_conjecture,
    true = iext(uri_rdfs_range,uri_rdfs_comment,uri_rdfs_Literal) ).

cnf(u721,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_rdf_object,uri_rdf_Property),true) ).

cnf(u476,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_domain,X0),true,icext(X0,uri_rdfs_seeAlso),true) ).

cnf(u196,negated_conjecture,
    true = sF3 ).

cnf(u854,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,X0,uri_rdf_XMLLiteral),true,iext(uri_rdfs_subClassOf,X0,uri_rdfs_Literal),true) ).

cnf(u610,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X0),true,iext(X0,uri_rdf_predicate,uri_rdfs_Resource),true) ).

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

cnf(u211,negated_conjecture,
    true = sF8 ).

cnf(u1126,negated_conjecture,
    true = ip(uri_rdf__2) ).

cnf(u365,negated_conjecture,
    true = iext(uri_rdf_type,uri_rdf_XMLLiteral,uri_rdfs_Datatype) ).

cnf(u1100,negated_conjecture,
    true = icext(uri_rdf_Property,uri_rdf_value) ).

cnf(u466,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_range,X0),true,icext(X0,uri_rdf_value),true) ).

cnf(u1241,negated_conjecture,
    true = iext(uri_rdfs_subClassOf,uri_rdf_XMLLiteral,uri_rdf_XMLLiteral) ).

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

cnf(u238,negated_conjecture,
    true = sF17 ).

cnf(u1381,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdf_Property,X0),true,icext(X0,uri_rdf__1),true) ).

cnf(u879,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_subClassOf,X0),true,icext(X0,uri_rdf_Alt),true) ).

cnf(u2417,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_rdfs_Resource,uri_rdfs_Class),true) ).

cnf(u1404,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_rdf_rest),true) ).

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

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

cnf(u355,negated_conjecture,
    true = iext(uri_rdfs_domain,uri_rdf__2,uri_rdfs_Resource) ).

cnf(u1254,negated_conjecture,
    true = icext(uri_rdfs_Class,uri_rdf_Bag) ).

cnf(u493,negated_conjecture,
    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(u3455,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdfs_Class),true,ifeq(iext(X0,uri_rdfs_Statement,X1),true,true,true),true) ).

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

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

cnf(u894,negated_conjecture,
    true = ifeq(iext(uri_rdfs_isDefinedBy,X0,X1),true,iext(uri_rdfs_seeAlso,X0,X1),true) ).

cnf(u3949,negated_conjecture,
    true = ifeq(sF46,true,ifeq(iext(uri_owl_equivalentClass,uri_rdf_Alt,uri_rdfs_Container),true,true,true),true) ).

cnf(u1128,negated_conjecture,
    true = ip(uri_rdf_rest) ).

cnf(u2679,negated_conjecture,
    true = iext(uri_rdf_type,uri_rdfs_Literal,uri_rdfs_Class) ).

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

cnf(u1532,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdf_Property,X0),true,icext(X0,uri_rdfs_domain),true) ).

cnf(u2819,negated_conjecture,
    true = iext(uri_rdfs_subPropertyOf,uri_rdfs_member,uri_rdfs_member) ).

cnf(u1252,negated_conjecture,
    true = iext(uri_rdfs_subClassOf,uri_rdf_Bag,uri_rdf_Bag) ).

cnf(u483,negated_conjecture,
    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(u1910,negated_conjecture,
    true = ifeq(iext(uri_rdfs_seeAlso,X0,X1),true,iext(uri_rdfs_seeAlso,X0,X1),true) ).

cnf(u637,negated_conjecture,
    true = ifeq(iext(uri_rdf_subject,X0,X1),true,icext(uri_rdfs_Statement,X0),true) ).

cnf(u376,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X0),true,ifeq(sF46,true,iext(X0,uri_owl_equivalentClass,uri_rdfs_subClassOf),true),true) ).

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

cnf(u506,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_domain,X0),true,icext(X0,uri_rdf__1),true) ).

cnf(u2008,negated_conjecture,
    true = icext(uri_rdf_Property,uri_rdfs_subClassOf) ).

cnf(u226,negated_conjecture,
    true = sF13 ).

cnf(u635,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_domain,X0),true,icext(X0,uri_rdf_subject),true) ).

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

cnf(u1293,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdf_Property),true,ifeq(iext(X0,uri_rdf_rest,X1),true,true,true),true) ).

cnf(u2834,negated_conjecture,
    true = icext(uri_rdf_Property,uri_rdfs_member) ).

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

cnf(u2561,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0),true,iext(X0,uri_rdfs_Container,uri_rdfs_Resource),true) ).

cnf(u4228,axiom,
    true = ifeq(sF46,true,icext(uri_rdf_Property,uri_owl_equivalentClass),true) ).

cnf(u3733,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X0),true,iext(X0,uri_rdfs_label,uri_rdfs_label),true) ).

cnf(u2309,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdf_Property),true,ifeq(iext(X0,uri_rdfs_seeAlso,X1),true,true,true),true) ).

cnf(u2272,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Class,X0),true,icext(X0,uri_rdfs_Seq),true) ).

cnf(u3714,negated_conjecture,
    true = ifeq(iext(uri_rdfs_comment,X0,X1),true,iext(uri_rdfs_comment,X0,X1),true) ).

cnf(u2091,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdfs_Class),true,ifeq(iext(X0,uri_rdf_XMLLiteral,X1),true,true,true),true) ).

cnf(u1051,negated_conjecture,
    true = ic(uri_rdf_XMLLiteral) ).

cnf(u1657,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdf_List,X0),true,icext(X0,uri_rdf_nil),true) ).

cnf(u526,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_domain,X0),true,icext(X0,uri_rdfs_member),true) ).

cnf(u1040,negated_conjecture,
    true = ic(uri_rdfs_Class) ).

cnf(u1402,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X0),true,iext(X0,uri_rdf_rest,uri_rdf_rest),true) ).

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

cnf(u2042,negated_conjecture,
    true = ifeq(icext(uri_rdf_Alt,X0),true,icext(uri_rdf_Alt,X0),true) ).

cnf(u265,negated_conjecture,
    true = sF26 ).

cnf(u395,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X0),true,iext(X0,uri_rdf_subject,uri_rdfs_Resource),true) ).

cnf(u3734,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_rdfs_label),true) ).

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

cnf(u1303,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdf_Property,X0),true,icext(X0,uri_rdf_subject),true) ).

cnf(u2322,negated_conjecture,
    true = iext(uri_rdf_type,uri_rdf_Alt,uri_rdfs_Class) ).

cnf(u2828,negated_conjecture,
    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(u654,negated_conjecture,
    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(u7209,negated_conjecture,
    true = ifeq(sF46,true,ifeq(iext(uri_owl_equivalentClass,uri_rdfs_Container,uri_rdfs_Resource),true,true,true),true) ).

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

cnf(u393,negated_conjecture,
    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(u1563,negated_conjecture,
    true = ifeq(icext(uri_rdf_XMLLiteral,X0),true,icext(uri_rdf_XMLLiteral,X0),true) ).

cnf(u677,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_rdf__2,uri_rdfs_ContainerMembershipProperty),true) ).

cnf(u3711,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_rdfs_comment),true) ).

cnf(u7199,axiom,
    true = ifeq(sF46,true,ifeq(iext(uri_owl_equivalentClass,uri_rdf_Property,uri_rdfs_Resource),true,true,true),true) ).

cnf(u3372,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdfs_Class),true,ifeq(iext(X0,X1,uri_rdf_List),true,true,true),true) ).

cnf(u2347,negated_conjecture,
    true = iext(uri_rdf_type,uri_rdfs_Class,uri_rdfs_Class) ).

cnf(u566,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_domain,X0),true,icext(X0,uri_rdf_List),true) ).

cnf(u1676,negated_conjecture,
    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(u3480,negated_conjecture,
    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(u167,axiom,
    true = iext(uri_rdfs_range,uri_rdfs_subPropertyOf,uri_rdf_Property) ).

cnf(u2346,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdfs_Class),true,ifeq(iext(X0,uri_rdfs_Class,X1),true,true,true),true) ).

cnf(u292,negated_conjecture,
    true = sF35 ).

cnf(u7203,negated_conjecture,
    true = ifeq(sF46,true,ifeq(iext(uri_owl_equivalentClass,uri_rdfs_Literal,uri_rdfs_Literal),true,true,true),true) ).

cnf(u1582,negated_conjecture,
    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(u2728,axiom,
    true = iext(uri_rdfs_subClassOf,uri_rdf_Property,uri_rdf_Property) ).

cnf(u2802,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X0),true,iext(X0,uri_rdf__1,uri_rdfs_member),true) ).

cnf(u1680,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_rdf_value),true) ).

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

cnf(u3636,negated_conjecture,
    true = iext(uri_rdf_type,uri_rdfs_label,uri_rdf_Property) ).

cnf(u3500,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_subClassOf,X0),true,icext(X0,uri_rdfs_Statement),true) ).

cnf(u2606,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Class,X0),true,icext(X0,uri_rdfs_Datatype),true) ).

cnf(u2878,negated_conjecture,
    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(u165,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,X1),true,ifeq(iext(X0,X2,X3),true,iext(X1,X2,X3),true),true) ).

cnf(u1711,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_rdf__2),true) ).

cnf(u1586,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_rdf_subject),true) ).

cnf(u433,negated_conjecture,
    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(u2603,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdfs_Class),true,ifeq(iext(X0,X1,uri_rdfs_Datatype),true,true,true),true) ).

cnf(u1710,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_rdf__2),true) ).

cnf(u7204,negated_conjecture,
    true = ifeq(sF46,true,ifeq(iext(uri_owl_equivalentClass,uri_rdfs_Literal,uri_rdfs_Resource),true,true,true),true) ).

cnf(u3504,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Resource,X0),true,iext(uri_rdfs_subClassOf,uri_rdfs_Statement,X0),true) ).

cnf(u2484,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0),true,iext(X0,uri_rdf_XMLLiteral,uri_rdfs_Resource),true) ).

cnf(u1442,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_rdfs_range),true) ).

cnf(u3497,negated_conjecture,
    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(u7227,negated_conjecture,
    true = ifeq(sF46,true,ifeq(iext(uri_owl_equivalentClass,uri_rdfs_Statement,uri_rdfs_Resource),true,true,true),true) ).

cnf(u333,negated_conjecture,
    true = iext(uri_rdf_type,uri_rdf__3,uri_rdf_Property) ).

cnf(u1965,negated_conjecture,
    true = ifeq(icext(X0,X1),true,true,true) ).

cnf(u439,negated_conjecture,
    true = ifeq(iext(uri_rdf__1,X0,X1),true,true,true) ).

cnf(u1714,negated_conjecture,
    true = ifeq(iext(uri_rdf__2,X0,X1),true,iext(uri_rdf__2,X0,X1),true) ).

cnf(u2233,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_rdfs_Container,uri_rdfs_Class),true) ).

cnf(u2884,negated_conjecture,
    true = ifeq(iext(uri_rdf__3,X0,X1),true,iext(uri_rdfs_member,X0,X1),true) ).

cnf(u182,negated_conjecture,
    true = ifeq(lv(X0),true,true,true) ).

cnf(u1515,negated_conjecture,
    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(u2488,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,X0,uri_rdf_XMLLiteral),true,iext(uri_rdfs_subClassOf,X0,uri_rdfs_Resource),true) ).

cnf(u834,negated_conjecture,
    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(u1074,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subClassOf,X0),true,icext(X0,uri_rdf_Property),true) ).

cnf(u1350,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdf_Property,X0),true,icext(X0,uri_rdf__2),true) ).

cnf(u1709,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X0),true,iext(X0,uri_rdf__2,uri_rdf__2),true) ).

cnf(u840,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,X0,uri_rdf_Bag),true,iext(uri_rdfs_subClassOf,X0,uri_rdfs_Container),true) ).

cnf(u332,negated_conjecture,
    true = iext(uri_rdf_type,uri_rdf__2,uri_rdf_Property) ).

cnf(u1483,negated_conjecture,
    true = iext(uri_rdf_type,uri_rdfs_domain,uri_rdf_Property) ).

cnf(u3525,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subClassOf,X0),true,icext(X0,uri_rdfs_Statement),true) ).

cnf(u1202,negated_conjecture,
    true = iext(uri_rdfs_subPropertyOf,uri_rdfs_isDefinedBy,uri_rdfs_isDefinedBy) ).

cnf(u1348,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdf_Property),true,ifeq(iext(X0,uri_rdf__2,X1),true,true,true),true) ).

cnf(u205,negated_conjecture,
    true = sF6 ).

cnf(u351,negated_conjecture,
    true = iext(uri_rdfs_subClassOf,uri_rdf_Bag,uri_rdfs_Container) ).

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

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

cnf(u3521,negated_conjecture,
    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(u1750,negated_conjecture,
    true = iext(uri_rdfs_subPropertyOf,uri_rdf_object,uri_rdf_object) ).

cnf(u3003,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(u838,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subClassOf,X0),true,icext(X0,uri_rdfs_Container),true) ).

cnf(u1221,negated_conjecture,
    true = ifeq(icext(uri_rdfs_Seq,X0),true,icext(uri_rdfs_Container,X0),true) ).

cnf(u719,negated_conjecture,
    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(u1482,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,X0,X1),true,true,true) ).

cnf(u1474,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdf_Property),true,ifeq(iext(X0,uri_rdfs_range,X1),true,true,true),true) ).

cnf(u2659,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0),true,iext(X0,uri_rdfs_Literal,uri_rdfs_Resource),true) ).

cnf(u1476,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdf_Property,X0),true,icext(X0,uri_rdfs_range),true) ).

cnf(u3523,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0),true,iext(X0,uri_rdfs_Statement,uri_rdfs_Statement),true) ).

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

cnf(u349,negated_conjecture,
    true = iext(uri_rdfs_range,uri_rdf_rest,uri_rdf_List) ).

cnf(u1103,negated_conjecture,
    true = icext(uri_rdfs_ContainerMembershipProperty,uri_rdf__3) ).

cnf(u1225,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Resource,X1),true,icext(X1,X0),true) ).

cnf(u3419,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,X0,uri_rdf_List),true,iext(uri_rdfs_subClassOf,X0,uri_rdfs_Resource),true) ).

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

cnf(u6229,negated_conjecture,
    true = ifeq(sF46,true,sF46,true) ).

cnf(u107,axiom,
    true = iext(uri_rdfs_domain,uri_rdfs_domain,uri_rdf_Property) ).

cnf(u193,negated_conjecture,
    true = sF2 ).

cnf(u1108,negated_conjecture,
    true = icext(uri_rdf_Property,uri_rdf_rest) ).

cnf(u339,negated_conjecture,
    true = iext(uri_rdfs_domain,uri_rdfs_isDefinedBy,uri_rdfs_Resource) ).

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

cnf(u3439,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0),true,iext(X0,uri_rdf_List,uri_rdf_List),true) ).

cnf(u362,negated_conjecture,
    true = iext(uri_rdf_type,uri_rdf__3,uri_rdfs_ContainerMembershipProperty) ).

cnf(u1231,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdf_Property),true,ifeq(iext(X0,uri_rdf_first,X1),true,true,true),true) ).

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

cnf(u220,negated_conjecture,
    true = sF11 ).

cnf(u1123,negated_conjecture,
    true = ip(uri_rdf_value) ).

cnf(u878,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0),true,iext(X0,uri_rdf_Alt,uri_rdfs_Container),true) ).

cnf(u707,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_domain,X0),true,icext(X0,uri_rdf_object),true) ).

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

cnf(u2663,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,X0,uri_rdfs_Literal),true,iext(uri_rdfs_subClassOf,X0,uri_rdfs_Resource),true) ).

cnf(u1242,negated_conjecture,
    true = iext(uri_rdfs_subClassOf,uri_rdf_XMLLiteral,uri_rdfs_Resource) ).

cnf(u235,negated_conjecture,
    true = sF16 ).

cnf(u883,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Container,X0),true,iext(uri_rdfs_subClassOf,uri_rdf_Alt,X0),true) ).

cnf(u621,negated_conjecture,
    true = ifeq(iext(uri_rdfs_range,uri_rdf_type,X0),true,icext(X0,uri_rdf_Property),true) ).

cnf(u360,negated_conjecture,
    true = iext(uri_rdf_type,uri_rdf__1,uri_rdfs_ContainerMembershipProperty) ).

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

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

cnf(u1497,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X0),true,iext(X0,uri_rdfs_domain,uri_rdfs_domain),true) ).

cnf(u619,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_rdf_first,uri_rdf_Property),true) ).

cnf(u2818,negated_conjecture,
    true = iext(uri_rdf_type,uri_rdfs_member,uri_rdf_Property) ).

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

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

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

cnf(u732,negated_conjecture,
    true = ifeq(iext(uri_rdf_predicate,X0,X1),true,icext(uri_rdfs_Statement,X0),true) ).

cnf(u366,negated_conjecture,
    true = iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,uri_rdfs_Class) ).

cnf(u2301,negated_conjecture,
    true = icext(uri_rdf_Property,uri_rdfs_seeAlso) ).

cnf(u903,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_isDefinedBy),true,iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_seeAlso),true) ).

cnf(u2946,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(u1655,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdf_List),true,ifeq(iext(X0,uri_rdf_nil,X1),true,true,true),true) ).

cnf(u377,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_subPropertyOf),true,ifeq(iext(X0,uri_owl_equivalentClass,uri_rdfs_subClassOf),true,sF46,true),true) ).

cnf(u516,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_domain,X0),true,icext(X0,uri_rdf_value),true) ).

cnf(u2051,negated_conjecture,
    true = icext(uri_rdfs_Class,uri_rdfs_Literal) ).

cnf(u533,negated_conjecture,
    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(u1763,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X0),true,iext(X0,uri_rdf_object,uri_rdf_object),true) ).

cnf(u893,negated_conjecture,
    true = ip(uri_rdfs_subPropertyOf) ).

cnf(u2032,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0),true,iext(X0,uri_rdf_Alt,uri_rdf_Alt),true) ).

cnf(u250,negated_conjecture,
    true = sF21 ).

cnf(u891,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_rdfs_isDefinedBy),true) ).

cnf(u1608,negated_conjecture,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdfs_ContainerMembershipProperty),true,ifeq(iext(X0,uri_rdf__2,X1),true,true,true),true) ).

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

cnf(u1783,negated_conjecture,
    true = icext(uri_rdfs_Class,uri_rdfs_Datatype) ).

cnf(u505,negated_conjecture,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X0),true,iext(X0,uri_rdf__1,uri_rdfs_Resource),true) ).

cnf(u2060,negated_conjecture,
    true = icext(uri_rdfs_Class,uri_rdfs_Class) ).


%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02  % Problem  : SWB016-10 : TPTP v9.3.1. Released v7.5.0.
% 0.00/0.05  % Command  : run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.40  % Computer : n020.cluster.edu
% 0.12/0.40  % Model    : x86_64 x86_64
% 0.12/0.40  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.40  % Memory   : 8046.5625MB
% 0.12/0.40  % OS       : Linux 6.8.0-71-generic
% 0.12/0.40  % CPULimit : 300
% 0.12/0.40  % WCLimit  : 300
% 0.12/0.40  % DateTime : Mon Sep 28 07:00:50 UTC 2026
% 0.12/0.40  % CPUTime  : 
% 0.12/0.40  Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.12/0.44  Running first-order theorem proving
% 0.12/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.12/1.89  % (8094)Detected a unit-equality problem, will run specialized UEQ schedule.
% 5.12/1.89  % (8101)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=128000:tgt=ground:npcc=on:spb=goal_then_units:urr=ec_only:random_seed=2432349014:i=130716:gtgl=4:add=on:doe=on:bd=all:gtg=exists_sym_2999 on theBenchmark for (2999ds/130716Mi)
% 5.12/1.89  % (8102)ott-1010_1_sfv=off:to=lpo:sil=8000:fdtod=off:sp=reverse_frequency:spb=goal_then_units:fd=preordered:random_seed=913756818:i=136:bd=preordered:ins=2:av=off_2999 on theBenchmark for (2999ds/136Mi)
% 5.12/1.89  % (8104)lrs+10_3_to=lpo:sil=64000:drc=off:fde=unused:sp=reverse_frequency:acc=on:bsr=on:fd=preordered:nwc=1:random_seed=708386186:avsq=on:i=257:avsqr=16,3:bd=preordered:fsr=off_2999 on theBenchmark for (2999ds/257Mi)
% 5.12/1.89  % (8099)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=151066765:i=138329:kws=inv_arity_squared:fgj=on:bd=preordered_2999 on theBenchmark for (2999ds/138329Mi)
% 5.12/1.89  % (8100)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=3696360751:i=130792:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/130792Mi)
% 5.12/1.89  % (8103)dis+10_14_to=lpo:sil=8000:tgt=full:drc=off:sp=const_frequency:sos=all:random_seed=323571673:i=181:gtgl=5:bs=unit_only:fsr=off:gtg=exists_all_2999 on theBenchmark for (2999ds/181Mi)
% 5.12/1.89  % (8105)dis-1010_7_sil=8000:fde=unused:flr=on:random_seed=2245658212:i=1187:sd=4:av=off:ss=axioms:sgt=32_2999 on theBenchmark for (2999ds/1187Mi)
% 5.12/1.89  % (8102)Instruction limit reached! 
% 5.12/1.89  % (8102)------------------------------
% 5.12/1.89  % (8102)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.12/1.89  % (8102)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.12/1.89  % (8102)CaDiCaL version: 2.1.3
% 5.12/1.89  % (8102)Termination reason: Instruction limit
% 5.12/1.89  % (8102)Termination phase: Saturation
% 5.12/1.89  % (8102)Time elapsed: 0.070 s
% 5.12/1.89  % (8102)Peak memory usage: 89 MB
% 5.12/1.89  % (8102)Instructions burned: 136 (million)
% 5.12/1.89  % (8103)Refutation not found, incomplete strategy
% 5.12/1.89  % (8103)------------------------------
% 5.12/1.89  % (8103)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.12/1.89  % (8103)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.12/1.89  % (8103)CaDiCaL version: 2.1.3
% 5.12/1.89  % (8103)Termination reason: Refutation not found, incomplete strategy
% 5.12/1.89  % (8103)Time elapsed: 0.072 s
% 5.12/1.89  % (8103)Peak memory usage: 89 MB
% 5.12/1.89  % (8103)Instructions burned: 133 (million)
% 5.12/1.89  % (8104)Instruction limit reached! 
% 5.12/1.89  % (8104)------------------------------
% 5.12/1.89  % (8104)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.12/1.89  % (8104)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.12/1.89  % (8104)CaDiCaL version: 2.1.3
% 5.12/1.89  % (8104)Termination reason: Instruction limit
% 5.12/1.89  % (8104)Termination phase: Saturation
% 5.12/1.89  % (8104)Time elapsed: 0.144 s
% 5.12/1.89  % (8104)Peak memory usage: 92 MB
% 5.12/1.89  % (8104)Instructions burned: 259 (million)
% 5.12/1.89  % (8113)lrs-1011_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:prc=on:fde=unused:lcm=predicate:bsr=on:flr=on:random_seed=914381948:i=2051:gtgl=2:fgj=on:bd=all:gtg=exists_top_2997 on theBenchmark for (2997ds/2051Mi)
% 5.12/1.89  % (8105)Refutation not found, incomplete strategy
% 5.12/1.89  % (8105)------------------------------
% 5.12/1.89  % (8105)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.12/1.89  % (8105)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.12/1.89  % (8105)CaDiCaL version: 2.1.3
% 5.12/1.89  % (8105)Termination reason: Refutation not found, incomplete strategy
% 5.12/1.89  % (8105)Time elapsed: 0.236 s
% 5.12/1.89  % (8105)Peak memory usage: 92 MB
% 5.12/1.89  % (8105)Instructions burned: 466 (million)
% 5.12/1.89  % (8114)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2184951092:i=4948:ss=axioms:sgt=16_2997 on theBenchmark for (2997ds/4948Mi)
% 5.12/1.89  % (8103)------------------------------
% 5.12/1.89  % (8103)------------------------------
% 5.12/1.89  % (8117)lrs+10_5:1_sil=8000:sos=all:urr=on:br=off:flr=on:random_seed=157180749:i=215:ep=RSTC_2995 on theBenchmark for (2995ds/215Mi)
% 5.12/1.89  % (8105)------------------------------
% 5.12/1.89  % (8105)------------------------------
% 5.12/1.89  % (8117)Instruction limit reached! 
% 5.12/1.89  % (8117)------------------------------
% 5.12/1.89  % (8117)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.12/1.89  % (8117)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.12/1.89  % (8117)CaDiCaL version: 2.1.3
% 5.12/1.89  % (8117)Termination reason: Instruction limit
% 5.12/1.89  % (8117)Termination phase: Saturation
% 5.12/1.89  % (8117)Time elapsed: 0.091 s
% 5.12/1.89  % (8117)Peak memory usage: 91 MB
% 5.12/1.89  % (8117)Instructions burned: 217 (million)
% 5.12/1.89  % (8119)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=1956315435: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.12/1.89  % (8120)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=3223868422:i=12125:sd=2:fgj=on:ss=axioms:sgt=64_2993 on theBenchmark for (2993ds/12125Mi)
% 5.12/1.89  % (8101)First to succeed.
% 5.12/1.89  % (8101)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-8094"
% 5.12/1.89  % (8119)Instruction limit reached! 
% 5.12/1.89  % (8119)------------------------------
% 5.12/1.89  % (8119)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 5.12/1.89  % (8119)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 5.12/1.89  % (8119)CaDiCaL version: 2.1.3
% 5.12/1.89  % (8119)Termination reason: Instruction limit
% 5.12/1.89  % (8119)Termination phase: Saturation
% 5.12/1.89  % (8119)Time elapsed: 0.176 s
% 5.12/1.89  % (8119)Peak memory usage: 95 MB
% 5.12/1.89  % (8119)Instructions burned: 317 (million)
% 5.12/1.89  % SZS status Satisfiable for theBenchmark
% 5.12/1.89  % SZS output start Saturation.
% See solution above
% 7.73/2.08  % SZS output start Definitions and Model Updates.
% 7.73/2.08  for all inputs,
% 7.73/2.08      define ir(X0) := true
% 7.73/2.08  % SZS output end Definitions and Model Updates.
% 7.73/2.08  % (8101)------------------------------
% 7.73/2.08  % (8101)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.73/2.08  % (8101)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.73/2.08  % (8101)CaDiCaL version: 2.1.3
% 7.73/2.08  % (8101)Termination reason: Satisfiable
% 7.73/2.08  % (8101)Time elapsed: 0.737 s
% 7.73/2.08  % (8101)Peak memory usage: 138 MB
% 7.73/2.08  % (8101)Instructions burned: 2049 (million)
% 7.73/2.08  % (8101)------------------------------
% 7.73/2.08  % (8101)------------------------------
% 7.73/2.08  % (8094)Success in time 1.014 s
% 7.73/2.08  % Vampire exiting
%------------------------------------------------------------------------------