Vampire---5.0.1.SAT-Sat.s

%------------------------------------------------------------------------------
% File     : Vampire---5.0.1
% Problem  : SWB009-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 : n008.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:00 PM UTC 2026

% Result   : Satisfiable 11.49s 2.62s
% Output   : Saturation 12.94s
% Verified : 
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)

% Comments : 
%------------------------------------------------------------------------------
cnf(u3101,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_type),true,ifeq(iext(X0,uri_rdfs_Class,uri_rdfs_Class),true,true,true),true) ).

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

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

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

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

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

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

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

cnf(u3206,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_owl_someValuesFrom),true,ifeq(iext(X0,sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z,uri_ex_c),true,true,true),true) ).

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

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

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

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

cnf(u3105,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_type),true,ifeq(iext(X0,sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z,uri_owl_Restriction),true,true,true),true) ).

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

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

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

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

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

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

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

cnf(u3107,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_type),true,ifeq(iext(X0,uri_ex_c,uri_owl_Class),true,true,true),true) ).

cnf(u2862,axiom,
    true = ic(sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z) ).

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

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

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

cnf(u2868,axiom,
    true = iext(uri_rdfs_subClassOf,sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z,uri_rdfs_Resource) ).

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

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

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

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

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

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

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

cnf(u3116,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(u3235,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0),true,iext(X0,uri_rdf_Alt,uri_rdfs_Resource),true) ).

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

cnf(u189,axiom,
    true = iext(uri_rdf_type,uri_ex_s,sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z) ).

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

cnf(u3403,axiom,
    true = iext(uri_rdfs_subClassOf,uri_owl_ObjectProperty,uri_owl_ObjectProperty) ).

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

cnf(u3208,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_owl_onProperty,X0),true,iext(X0,sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z,uri_ex_p),true) ).

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

cnf(u1973,axiom,
    true = ifeq(iext(uri_rdfs_range,X0,uri_owl_Class),true,ifeq(iext(X0,X1,uri_ex_c),true,true,true),true) ).

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

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

cnf(u1971,axiom,
    true = ifeq(iext(uri_rdfs_range,X0,sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z),true,ifeq(iext(X0,X1,uri_ex_s),true,true,true),true) ).

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

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

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

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

cnf(u1101,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_owl_Restriction,X0),true,icext(X0,sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z),true) ).

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

cnf(u2000,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_owl_someValuesFrom,X0),true,icext(X0,uri_ex_c),true) ).

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

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

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

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

cnf(u3174,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(u3301,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X0),true,iext(X0,uri_rdf_first,uri_rdf_List),true) ).

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

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

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

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

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

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

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

cnf(u3305,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_ex_s,sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z),true) ).

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

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

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

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

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

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

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

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

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

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

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

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

cnf(u3306,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_ex_p,uri_owl_ObjectProperty),true) ).

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

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

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

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

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

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

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

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

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

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

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

cnf(u3095,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(u786,axiom,
    true = iext(uri_rdf_type,uri_rdf_Alt,uri_rdfs_Class) ).

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

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

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

cnf(u3209,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_owl_someValuesFrom,X0),true,iext(X0,sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z,uri_ex_c),true) ).

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

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

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

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

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

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

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

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

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

cnf(u3469,axiom,
    true = iext(uri_rdfs_subClassOf,uri_owl_Class,uri_rdfs_Resource) ).

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

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

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

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

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

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

cnf(u2590,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Resource,X0),true,iext(uri_rdfs_subClassOf,uri_rdf_Bag,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(u1935,axiom,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdf_Property),true,ifeq(iext(X0,X1,uri_rdf_rest),true,true,true),true) ).

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

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

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

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

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

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

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

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

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

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

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

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

cnf(u2842,axiom,
    true = icext(uri_rdfs_Class,sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z) ).

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

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

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

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

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

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

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

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

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

cnf(u2131,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdf_type,X1),true,icext(X1,uri_rdfs_Resource),true) ).

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

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

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

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

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

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

cnf(u187,axiom,
    true = iext(uri_rdf_type,uri_ex_c,uri_owl_Class) ).

cnf(u419,axiom,
    true = iext(uri_rdf_type,uri_owl_someValuesFrom,uri_rdf_Property) ).

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

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

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

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

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

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

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

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

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

cnf(u185,axiom,
    true = iext(uri_rdf_type,sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z,uri_owl_Restriction) ).

cnf(u1102,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z,X0),true,icext(X0,uri_ex_s),true) ).

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

cnf(u1974,axiom,
    true = ifeq(iext(uri_rdfs_range,X0,uri_owl_ObjectProperty),true,ifeq(iext(X0,X1,uri_ex_p),true,true,true),true) ).

cnf(u841,axiom,
    true = icext(uri_owl_Restriction,sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z) ).

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

cnf(u2898,axiom,
    true = ifeq(icext(sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z,X0),true,icext(sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z,X0),true) ).

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

cnf(u191,axiom,
    true = iext(uri_rdf_type,uri_ex_p,uri_owl_ObjectProperty) ).

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

cnf(u1100,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_owl_Class,X0),true,icext(X0,uri_ex_c),true) ).

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

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

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

cnf(u2894,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subClassOf,X0),true,icext(X0,sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z),true) ).

cnf(u3402,axiom,
    true = iext(uri_rdfs_subClassOf,uri_owl_ObjectProperty,uri_rdfs_Resource) ).

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

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

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

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

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

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

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

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

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

cnf(u1489,axiom,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_owl_Restriction),true,ifeq(iext(X0,sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z,X1),true,true,true),true) ).

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

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

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

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

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

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

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

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

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

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

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

cnf(u1495,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_owl_someValuesFrom,X0),true,icext(X0,sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z),true) ).

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

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

cnf(u3436,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subClassOf,X0),true,icext(X0,uri_owl_ObjectProperty),true) ).

cnf(u3379,axiom,
    true = icext(uri_rdfs_Class,uri_owl_ObjectProperty) ).

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

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

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

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

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

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

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

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

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

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

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

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

cnf(u3176,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(u1121,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdf_Property,X0),true,icext(X0,uri_owl_someValuesFrom),true) ).

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

cnf(u3207,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_owl_onProperty),true,ifeq(iext(X0,sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z,uri_ex_p),true,true,true),true) ).

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

cnf(u3069,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(u3124,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_domain),true,ifeq(iext(X0,uri_rdfs_label,uri_rdfs_Resource),true,true,true),true) ).

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

cnf(u2869,axiom,
    true = iext(uri_rdfs_subClassOf,sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z,sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z) ).

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

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

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

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

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

cnf(u3503,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subClassOf,X0),true,icext(X0,uri_owl_Class),true) ).

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

cnf(u1099,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_owl_ObjectProperty,X0),true,icext(X0,uri_ex_p),true) ).

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

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

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

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

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

cnf(u3396,axiom,
    true = ic(uri_owl_ObjectProperty) ).

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

cnf(u3145,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(u3142,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(u3269,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X0),true,iext(X0,uri_rdfs_member,uri_rdfs_Resource),true) ).

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

cnf(u1491,axiom,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_owl_ObjectProperty),true,ifeq(iext(X0,uri_ex_p,X1),true,true,true),true) ).

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

cnf(u1490,axiom,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_owl_Class),true,ifeq(iext(X0,uri_ex_c,X1),true,true,true),true) ).

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

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

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

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

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

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

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

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

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

cnf(u3441,axiom,
    true = ifeq(icext(uri_owl_ObjectProperty,X0),true,icext(uri_owl_ObjectProperty,X0),true) ).

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

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

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

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

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

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

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

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

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

cnf(u3308,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_ex_c,uri_owl_Class),true) ).

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

cnf(u3470,axiom,
    true = iext(uri_rdfs_subClassOf,uri_owl_Class,uri_owl_Class) ).

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

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

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

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

cnf(u2093,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdf_type,X0),true,icext(X0,uri_owl_Class),true) ).

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

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

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

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

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

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

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

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

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

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

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

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

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

cnf(u2735,axiom,
    true = iext(uri_rdfs_subClassOf,uri_rdf_List,uri_rdfs_Resource) ).

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

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

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

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

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

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

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

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

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

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

cnf(u3508,axiom,
    true = ifeq(icext(uri_owl_Class,X0),true,icext(uri_owl_Class,X0),true) ).

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

cnf(u197,axiom,
    tuple(true,true) = sF0 ).

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

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

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

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

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

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

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

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

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

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

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

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

cnf(u3529,axiom,
    true = iext(uri_rdf_type,uri_owl_Restriction,uri_rdfs_Class) ).

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

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

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

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

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

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

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

cnf(u3310,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z,uri_owl_Restriction),true) ).

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

cnf(u266,axiom,
    true = ip(uri_owl_onProperty) ).

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

cnf(u2861,axiom,
    true = iext(uri_rdf_type,sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z,uri_rdfs_Class) ).

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

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

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

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

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

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

cnf(u3109,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_type),true,ifeq(iext(X0,uri_ex_p,uri_owl_ObjectProperty),true,true,true),true) ).

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

cnf(u49,axiom,
    true = iext(uri_rdfs_domain,uri_rdfs_seeAlso,uri_rdfs_Resource) ).

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

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

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

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

cnf(u3113,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(u1673,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdf_Property,X0),true,icext(X0,uri_rdf_predicate),true) ).

cnf(u3110,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_type),true,ifeq(iext(X0,uri_ex_s,sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z),true,true,true),true) ).

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

cnf(u183,axiom,
    true = iext(uri_owl_onProperty,sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z,uri_ex_p) ).

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

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

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

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

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

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

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

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

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

cnf(u181,axiom,
    true = iext(uri_owl_someValuesFrom,sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z,uri_ex_c) ).

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

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

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

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

cnf(u837,axiom,
    true = icext(sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z,uri_ex_s) ).

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

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

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

cnf(u3513,axiom,
    true = icext(uri_rdfs_Class,uri_owl_Restriction) ).

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

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

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

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

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

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

cnf(u1972,axiom,
    true = ifeq(iext(uri_rdfs_range,X0,uri_owl_Restriction),true,ifeq(iext(X0,X1,sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z),true,true,true),true) ).

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

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

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

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

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

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

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

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

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

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

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

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

cnf(u198,negated_conjecture,
    tuple(iext(uri_rdf_type,X0,uri_ex_c),iext(uri_ex_p,uri_ex_s,X0)) != sF0 ).

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

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

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

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

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

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

cnf(u1494,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_owl_onProperty,X0),true,icext(X0,sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z),true) ).

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

cnf(u1999,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_owl_onProperty,X0),true,icext(X0,uri_ex_p),true) ).

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

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

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

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

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

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

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

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

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

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

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

cnf(u1488,axiom,
    true = ifeq(iext(uri_rdfs_domain,X0,sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z),true,ifeq(iext(X0,uri_ex_s,X1),true,true,true),true) ).

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

cnf(u3570,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subClassOf,X0),true,icext(X0,uri_owl_Restriction),true) ).

cnf(u267,axiom,
    true = ip(uri_owl_someValuesFrom) ).

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

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

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

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

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

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

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

cnf(u3462,axiom,
    true = iext(uri_rdf_type,uri_owl_Class,uri_rdfs_Class) ).

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

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

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

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

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

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

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

cnf(u37,axiom,
    true = iext(uri_rdfs_range,uri_rdfs_comment,uri_rdfs_Literal) ).

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

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

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

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

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

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

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

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

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

cnf(u3463,axiom,
    true = ic(uri_owl_Class) ).

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

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

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

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

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

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

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

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

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

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

cnf(u2091,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdf_type,X0),true,icext(X0,uri_owl_ObjectProperty),true) ).

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

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

cnf(u167,axiom,
    true = iext(uri_rdfs_range,uri_rdfs_subPropertyOf,uri_rdf_Property) ).

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

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

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

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

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

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

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

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

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

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

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

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

cnf(u3112,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(u67,axiom,
    true = iext(uri_rdfs_subClassOf,uri_rdf_Alt,uri_rdfs_Container) ).

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

cnf(u1074,axiom,
    true = ifeq(icext(uri_rdfs_Datatype,X0),true,icext(uri_rdfs_Class,X0),true) ).

cnf(u1969,axiom,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdfs_Class),true,ifeq(iext(X0,X1,uri_rdfs_Datatype),true,true,true),true) ).

cnf(u3260,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X0),true,iext(X0,uri_rdf__3,uri_rdf__3),true) ).

cnf(u77,axiom,
    true = iext(uri_rdfs_range,uri_rdfs_member,uri_rdfs_Resource) ).

cnf(u840,axiom,
    true = icext(uri_owl_Class,uri_ex_c) ).

cnf(u1956,axiom,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdfs_ContainerMembershipProperty),true,ifeq(iext(X0,X1,uri_rdf__3),true,true,true),true) ).

cnf(u577,axiom,
    true = iext(uri_rdfs_subClassOf,uri_rdf_Bag,uri_rdfs_Resource) ).

cnf(u332,axiom,
    true = ifeq(iext(uri_owl_someValuesFrom,X1,X0),true,true,true) ).

cnf(u3147,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_range),true,ifeq(iext(X0,uri_rdf_predicate,uri_rdfs_Resource),true,true,true),true) ).

cnf(u1622,axiom,
    true = ifeq(iext(uri_rdf_predicate,X1,X0),true,icext(uri_rdfs_Statement,X1),true) ).

cnf(u1483,axiom,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdfs_Class),true,ifeq(iext(X0,uri_rdfs_ContainerMembershipProperty,X1),true,true,true),true) ).

cnf(u2885,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,X0,sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z),true,iext(uri_rdfs_subClassOf,X0,uri_rdfs_Resource),true) ).

cnf(u3136,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_range),true,ifeq(iext(X0,uri_rdf_value,uri_rdfs_Resource),true,true,true),true) ).

cnf(u3271,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X0),true,iext(X0,uri_rdfs_label,uri_rdfs_Literal),true) ).

cnf(u1086,axiom,
    true = ifeq(icext(uri_rdf_XMLLiteral,X0),true,icext(uri_rdfs_Literal,X0),true) ).

cnf(u1960,axiom,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdfs_Class),true,ifeq(iext(X0,X1,uri_rdf_Property),true,true,true),true) ).

cnf(u3395,axiom,
    true = iext(uri_rdf_type,uri_owl_ObjectProperty,uri_rdfs_Class) ).

cnf(u1478,axiom,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdfs_Class),true,ifeq(iext(X0,uri_rdfs_Resource,X1),true,true,true),true) ).

cnf(u1079,axiom,
    true = ifeq(icext(uri_rdf_Bag,X0),true,icext(uri_rdf_Bag,X0),true) ).

cnf(u1097,axiom,
    true = ifeq(icext(uri_rdf_Property,X0),true,icext(uri_rdf_Property,X0),true) ).

cnf(u3275,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X0),true,iext(X0,uri_rdfs_range,uri_rdfs_Class),true) ).

cnf(u838,axiom,
    true = icext(uri_owl_ObjectProperty,uri_ex_p) ).

cnf(u3264,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X0),true,iext(X0,uri_rdf__1,uri_rdf__1),true) ).

cnf(u719,axiom,
    true = iext(uri_rdfs_subPropertyOf,uri_rdf__2,uri_rdf__2) ).

cnf(u1482,axiom,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdfs_Class),true,ifeq(iext(X0,uri_rdf_Bag,X1),true,true,true),true) ).

cnf(u65,axiom,
    true = iext(uri_rdfs_range,uri_rdf_rest,uri_rdf_List) ).

cnf(u1476,axiom,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdfs_Datatype),true,ifeq(iext(X0,uri_rdf_XMLLiteral,X1),true,true,true),true) ).

cnf(u3366,axiom,
    true = ifeq(iext(uri_rdf__3,X1,X0),true,iext(uri_rdfs_member,X1,X0),true) ).

cnf(u1110,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Class,X0),true,icext(X0,uri_rdf_Alt),true) ).

cnf(u2005,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subClassOf,X0),true,icext(X0,uri_rdfs_Seq),true) ).

cnf(u600,axiom,
    true = icext(uri_rdfs_Class,uri_rdfs_ContainerMembershipProperty) ).

cnf(u1103,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Class,X0),true,icext(X0,uri_rdfs_Class),true) ).

cnf(u2003,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subClassOf,X0),true,icext(X0,uri_rdfs_Datatype),true) ).

cnf(u1133,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdf_Property,X0),true,icext(X0,uri_rdf__2),true) ).

cnf(u1480,axiom,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdfs_Class),true,ifeq(iext(X0,uri_rdf_Alt,X1),true,true,true),true) ).

cnf(u863,axiom,
    true = icext(uri_rdf_Property,uri_rdf__2) ).

cnf(u722,axiom,
    true = iext(uri_rdfs_subPropertyOf,uri_rdf_first,uri_rdf_first) ).

cnf(u107,axiom,
    true = iext(uri_rdfs_domain,uri_rdfs_domain,uri_rdf_Property) ).

cnf(u193,axiom,
    true = ifeq(lv(X0),true,true,true) ).

cnf(u1108,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Class,X0),true,icext(X0,uri_rdf_Bag),true) ).

cnf(u3422,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0),true,iext(X0,uri_owl_ObjectProperty,uri_rdfs_Resource),true) ).

cnf(u2149,axiom,
    true = ifeq(iext(uri_rdf_type,X0,X1),true,icext(uri_rdfs_Class,X1),true) ).

cnf(u1123,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdf_Property,X0),true,icext(X0,uri_rdfs_subClassOf),true) ).

cnf(u707,axiom,
    true = iext(uri_rdfs_subPropertyOf,uri_owl_onProperty,uri_owl_onProperty) ).

cnf(u1112,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Class,X0),true,icext(X0,uri_rdfs_Resource),true) ).

cnf(u3198,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(u105,axiom,
    true = iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,uri_rdfs_Class) ).

cnf(u3550,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_subClassOf),true,ifeq(iext(X0,uri_owl_Restriction,uri_rdfs_Resource),true,true,true),true) ).

cnf(u621,axiom,
    true = iext(uri_rdfs_subClassOf,uri_rdfs_Class,uri_rdfs_Class) ).

cnf(u3146,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_range),true,ifeq(iext(X0,uri_rdfs_member,uri_rdfs_Resource),true,true,true),true) ).

cnf(u3191,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_subClassOf),true,ifeq(iext(X0,uri_rdfs_Literal,uri_rdfs_Literal),true,true,true),true) ).

cnf(u1559,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_range,X0),true,icext(X0,uri_rdf__1),true) ).

cnf(u3171,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_subPropertyOf),true,ifeq(iext(X0,uri_owl_someValuesFrom,uri_owl_someValuesFrom),true,true,true),true) ).

cnf(u1497,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_subClassOf,X0),true,icext(X0,uri_rdfs_Datatype),true) ).

cnf(u2051,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_rdf_first),true) ).

cnf(u3446,axiom,
    true = icext(uri_rdfs_Class,uri_owl_Class) ).

cnf(u111,axiom,
    true = iext(uri_rdfs_range,uri_rdfs_domain,uri_rdfs_Class) ).

cnf(u3554,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_subClassOf,X0),true,icext(X0,uri_owl_Restriction),true) ).

cnf(u3281,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_range,X0),true,iext(X0,uri_rdf__2,uri_rdfs_Resource),true) ).

cnf(u488,axiom,
    true = ic(uri_rdf_Property) ).

cnf(u1562,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_range,X0),true,icext(X0,uri_rdf_type),true) ).

cnf(u3536,axiom,
    true = iext(uri_rdfs_subClassOf,uri_owl_Restriction,uri_rdfs_Resource) ).

cnf(u2778,axiom,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdfs_Class),true,ifeq(iext(X0,uri_rdfs_Statement,X1),true,true,true),true) ).

cnf(u1641,axiom,
    true = ifeq(iext(uri_rdfs_label,X1,X0),true,true,true) ).

cnf(u2028,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_owl_onProperty),true) ).

cnf(u3184,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_subClassOf),true,ifeq(iext(X0,uri_rdfs_Seq,uri_rdfs_Resource),true,true,true),true) ).

cnf(u1533,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_rdf_subject),true) ).

cnf(u2090,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdf_type,X0),true,icext(X0,sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z),true) ).

cnf(u2026,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subClassOf,X0),true,icext(X0,uri_rdf_Property),true) ).

cnf(u3332,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_rdfs_comment,uri_rdf_Property),true) ).

cnf(u507,axiom,
    true = icext(uri_rdfs_Class,uri_rdfs_Literal) ).

cnf(u494,axiom,
    true = iext(uri_rdfs_subClassOf,uri_rdfs_Class,uri_rdfs_Resource) ).

cnf(u2032,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_rdfs_subClassOf),true) ).

cnf(u3081,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_type),true,ifeq(iext(X0,uri_rdf_subject,uri_rdf_Property),true,true,true),true) ).

cnf(u1523,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_owl_onProperty),true) ).

cnf(u3078,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_type),true,ifeq(iext(X0,uri_rdf__3,uri_rdfs_ContainerMembershipProperty),true,true,true),true) ).

cnf(u1549,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_range,X0),true,icext(X0,uri_rdfs_seeAlso),true) ).

cnf(u3336,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_rdf_object,uri_rdf_Property),true) ).

cnf(u23,axiom,
    true = iext(uri_rdf_type,uri_rdf_value,uri_rdf_Property) ).

cnf(u2578,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdfs_Container,X0),true,iext(uri_rdfs_subClassOf,uri_rdfs_Seq,X0),true) ).

cnf(u21,axiom,
    true = iext(uri_rdf_type,uri_rdf_object,uri_rdf_Property) ).

cnf(u3199,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_subClassOf),true,ifeq(iext(X0,uri_rdfs_Seq,uri_rdfs_Seq),true,true,true),true) ).

cnf(u3314,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_rdfs_Class,uri_rdfs_Class),true) ).

cnf(u1547,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_range,X0),true,icext(X0,uri_rdfs_subClassOf),true) ).

cnf(u1934,axiom,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdf_Property),true,ifeq(iext(X0,X1,uri_rdf_first),true,true,true),true) ).


%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02  % Problem  : SWB009-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.11/0.38  % Computer : n008.cluster.edu
% 0.11/0.38  % Model    : x86_64 x86_64
% 0.11/0.38  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.11/0.38  % Memory   : 8046.5625MB
% 0.11/0.38  % OS       : Linux 6.8.0-71-generic
% 0.11/0.38  % CPULimit : 300
% 0.11/0.38  % WCLimit  : 300
% 0.11/0.38  % DateTime : Mon Sep 28 06:57:10 UTC 2026
% 0.11/0.38  % CPUTime  : 
% 0.11/0.38  Running run_vampire /export/starexec/sandbox/benchmark/theBenchmark.p 300 THM
% 0.11/0.42  Running first-order theorem proving
% 0.11/0.42  Running: /export/starexec/sandbox/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox/benchmark/theBenchmark.p
% 11.49/2.62  % (2060621)Detected a unit-equality problem, will run specialized UEQ schedule.
% 11.49/2.62  % (2060626)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=2403672759:i=138329:kws=inv_arity_squared:fgj=on:bd=preordered_2999 on theBenchmark for (2999ds/138329Mi)
% 11.49/2.62  % (2060631)lrs+10_3_to=lpo:sil=64000:drc=off:fde=unused:sp=reverse_frequency:acc=on:bsr=on:fd=preordered:nwc=1:random_seed=2178135719:avsq=on:i=257:avsqr=16,3:bd=preordered:fsr=off_2999 on theBenchmark for (2999ds/257Mi)
% 11.49/2.62  % (2060628)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=128000:tgt=ground:npcc=on:spb=goal_then_units:urr=ec_only:random_seed=1567467747:i=130716:gtgl=4:add=on:doe=on:bd=all:gtg=exists_sym_2999 on theBenchmark for (2999ds/130716Mi)
% 11.49/2.62  % (2060629)ott-1010_1_sfv=off:to=lpo:sil=8000:fdtod=off:sp=reverse_frequency:spb=goal_then_units:fd=preordered:random_seed=650551933:i=136:bd=preordered:ins=2:av=off_2999 on theBenchmark for (2999ds/136Mi)
% 11.49/2.62  % (2060627)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=2015556190:i=130792:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/130792Mi)
% 11.49/2.62  % (2060630)dis+10_14_to=lpo:sil=8000:tgt=full:drc=off:sp=const_frequency:sos=all:random_seed=3443405775:i=181:gtgl=5:bs=unit_only:fsr=off:gtg=exists_all_2999 on theBenchmark for (2999ds/181Mi)
% 11.49/2.62  % (2060632)dis-1010_7_sil=8000:fde=unused:flr=on:random_seed=3482193385:i=1187:sd=4:av=off:ss=axioms:sgt=32_2999 on theBenchmark for (2999ds/1187Mi)
% 11.49/2.62  % (2060629)Instruction limit reached! 
% 11.49/2.62  % (2060629)------------------------------
% 11.49/2.62  % (2060629)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.49/2.62  % (2060629)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.49/2.62  % (2060629)CaDiCaL version: 2.1.3
% 11.49/2.62  % (2060629)Termination reason: Instruction limit
% 11.49/2.62  % (2060629)Termination phase: Saturation
% 11.49/2.62  % (2060629)Time elapsed: 0.067 s
% 11.49/2.62  % (2060629)Peak memory usage: 88 MB
% 11.49/2.62  % (2060629)Instructions burned: 137 (million)
% 11.49/2.62  % (2060630)Refutation not found, incomplete strategy
% 11.49/2.62  % (2060630)------------------------------
% 11.49/2.62  % (2060630)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.49/2.62  % (2060630)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.49/2.62  % (2060630)CaDiCaL version: 2.1.3
% 11.49/2.62  % (2060630)Termination reason: Refutation not found, incomplete strategy
% 11.49/2.62  % (2060630)Time elapsed: 0.072 s
% 11.49/2.62  % (2060630)Peak memory usage: 89 MB
% 11.49/2.62  % (2060630)Instructions burned: 133 (million)
% 11.49/2.62  % (2060631)Instruction limit reached! 
% 11.49/2.62  % (2060631)------------------------------
% 11.49/2.62  % (2060631)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.49/2.62  % (2060631)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.49/2.62  % (2060631)CaDiCaL version: 2.1.3
% 11.49/2.62  % (2060631)Termination reason: Instruction limit
% 11.49/2.62  % (2060631)Termination phase: Saturation
% 11.49/2.62  % (2060631)Time elapsed: 0.153 s
% 11.49/2.62  % (2060631)Peak memory usage: 92 MB
% 11.49/2.62  % (2060631)Instructions burned: 257 (million)
% 11.49/2.62  % (2060640)lrs-1011_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:prc=on:fde=unused:lcm=predicate:bsr=on:flr=on:random_seed=4087032322:i=2051:gtgl=2:fgj=on:bd=all:gtg=exists_top_2997 on theBenchmark for (2997ds/2051Mi)
% 11.49/2.62  % (2060641)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=3520563092:i=4948:ss=axioms:sgt=16_2996 on theBenchmark for (2996ds/4948Mi)
% 11.49/2.62  % (2060632)Refutation not found, incomplete strategy
% 11.49/2.62  % (2060632)------------------------------
% 11.49/2.62  % (2060632)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.49/2.62  % (2060632)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.49/2.62  % (2060632)CaDiCaL version: 2.1.3
% 11.49/2.62  % (2060632)Termination reason: Refutation not found, incomplete strategy
% 11.49/2.62  % (2060632)Time elapsed: 0.294 s
% 11.49/2.62  % (2060632)Peak memory usage: 94 MB
% 11.49/2.62  % (2060632)Instructions burned: 580 (million)
% 11.49/2.62  % (2060630)------------------------------
% 11.49/2.62  % (2060630)------------------------------
% 11.49/2.62  % (2060644)lrs+10_5:1_sil=8000:sos=all:urr=on:br=off:flr=on:random_seed=3598379727:i=215:ep=RSTC_2995 on theBenchmark for (2995ds/215Mi)
% 11.49/2.62  % (2060632)------------------------------
% 11.49/2.62  % (2060632)------------------------------
% 11.49/2.62  % (2060644)Instruction limit reached! 
% 11.49/2.62  % (2060644)------------------------------
% 11.49/2.62  % (2060644)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.49/2.62  % (2060644)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.49/2.62  % (2060644)CaDiCaL version: 2.1.3
% 11.49/2.62  % (2060644)Termination reason: Instruction limit
% 11.49/2.62  % (2060644)Termination phase: Saturation
% 11.49/2.62  % (2060644)Time elapsed: 0.114 s
% 11.49/2.62  % (2060644)Peak memory usage: 89 MB
% 11.49/2.62  % (2060644)Instructions burned: 215 (million)
% 11.49/2.62  % (2060646)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=3524976110:avsq=on:i=317:avsqr=1,16:kws=arity_squared:add=off:fgj=on:ins=10:fsr=off:gtg=exists_sym_2993 on theBenchmark for (2993ds/317Mi)
% 11.49/2.62  % (2060647)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=89685154:i=12125:sd=2:fgj=on:ss=axioms:sgt=64_2992 on theBenchmark for (2992ds/12125Mi)
% 11.49/2.62  % (2060626)Refutation not found, incomplete strategy
% 11.49/2.62  % (2060626)------------------------------
% 11.49/2.62  % (2060626)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.49/2.62  % (2060626)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.49/2.62  % (2060626)CaDiCaL version: 2.1.3
% 11.49/2.62  % (2060626)Termination reason: Refutation not found, incomplete strategy
% 11.49/2.62  % (2060626)Time elapsed: 0.866 s
% 11.49/2.62  % (2060626)Peak memory usage: 143 MB
% 11.49/2.62  % (2060626)Instructions burned: 2320 (million)
% 11.49/2.62  % (2060641)Refutation not found, incomplete strategy
% 11.49/2.62  % (2060641)------------------------------
% 11.49/2.62  % (2060641)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.49/2.62  % (2060641)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.49/2.62  % (2060641)CaDiCaL version: 2.1.3
% 11.49/2.62  % (2060641)Termination reason: Refutation not found, incomplete strategy
% 11.49/2.62  % (2060641)Time elapsed: 0.570 s
% 11.49/2.62  % (2060641)Peak memory usage: 127 MB
% 11.49/2.62  % (2060641)Instructions burned: 861 (million)
% 11.49/2.62  % (2060646)Instruction limit reached! 
% 11.49/2.62  % (2060646)------------------------------
% 11.49/2.62  % (2060646)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.49/2.62  % (2060646)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.49/2.62  % (2060646)CaDiCaL version: 2.1.3
% 11.49/2.62  % (2060646)Termination reason: Instruction limit
% 11.49/2.62  % (2060646)Termination phase: Saturation
% 11.49/2.62  % (2060646)Time elapsed: 0.171 s
% 11.49/2.62  % (2060646)Peak memory usage: 97 MB
% 11.49/2.62  % (2060646)Instructions burned: 319 (million)
% 11.49/2.62  % (2060626)------------------------------
% 11.49/2.62  % (2060626)------------------------------
% 11.49/2.62  % (2060650)lrs+10_32_sil=8000:tgt=ground:prc=on:sp=reverse_arity:spb=non_intro:random_seed=2984069275:i=2836:kws=inv_precedence:fgj=on:bd=preordered:ins=10_2989 on theBenchmark for (2989ds/2836Mi)
% 11.49/2.62  % (2060651)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=2942391499:i=14534:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2988 on theBenchmark for (2988ds/14534Mi)
% 11.49/2.62  % (2060641)------------------------------
% 11.49/2.62  % (2060641)------------------------------
% 11.49/2.62  % (2060654)lrs+10_1_ncem=casc2026/models/loop8.pt:sil=128000:tgt=full:npcc=on:sas=cadical:sp=reverse_frequency:bsr=on:alpa=false:sac=on:random_seed=722830186:i=11832:s2at=3:bs=on:bd=preordered:fsd=on_2987 on theBenchmark for (2987ds/11832Mi)
% 11.49/2.62  % (2060650)First to succeed.
% 11.49/2.62  % (2060650)Solution written to "/export/starexec/sandbox/tmp/vampire-proof-2060621"
% 11.49/2.62  % (2060628)Also succeeded, but the first one will report.
% 11.49/2.62  % (2060640)Instruction limit reached! 
% 11.49/2.62  % (2060640)------------------------------
% 11.49/2.62  % (2060640)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 11.49/2.62  % (2060640)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 11.49/2.62  % (2060640)CaDiCaL version: 2.1.3
% 11.49/2.62  % (2060640)Termination reason: Instruction limit
% 11.49/2.62  % (2060640)Termination phase: Saturation
% 11.49/2.62  % (2060640)Time elapsed: 1.372 s
% 11.49/2.62  % (2060640)Peak memory usage: 144 MB
% 11.49/2.62  % (2060640)Instructions burned: 2051 (million)
% 11.49/2.62  % SZS status Satisfiable for theBenchmark
% 11.49/2.62  % SZS output start Saturation.
% See solution above
% 12.94/2.71  % SZS output start Definitions and Model Updates.
% 12.94/2.71  for all inputs,
% 12.94/2.71      define ir(X0) := true
% 12.94/2.71  % SZS output end Definitions and Model Updates.
% 12.94/2.71  % (2060650)------------------------------
% 12.94/2.71  % (2060650)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 12.94/2.71  % (2060650)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 12.94/2.71  % (2060650)CaDiCaL version: 2.1.3
% 12.94/2.71  % (2060650)Termination reason: Satisfiable
% 12.94/2.71  % (2060650)Time elapsed: 0.357 s
% 12.94/2.71  % (2060650)Peak memory usage: 104 MB
% 12.94/2.71  % (2060650)Instructions burned: 642 (million)
% 12.94/2.71  % (2060650)------------------------------
% 12.94/2.71  % (2060650)------------------------------
% 12.94/2.71  % (2060621)Success in time 1.761 s
% 12.94/2.71  % Vampire exiting
%------------------------------------------------------------------------------