Vampire---5.0.1.SAT-Sat.s

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

% Computer : n007.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:09 PM UTC 2026

% Result   : Satisfiable 7.31s 3.62s
% Output   : Saturation 0.23s
% Verified : 
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)

% Comments : 
%------------------------------------------------------------------------------
cnf(u1816,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdf_Property,X0),true,icext(X0,uri_rdf_predicate),true) ).

cnf(u3325,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_first),true,ifeq(iext(X0,sK4_testcase_premise_fullish_022_List_Member_Access_BNODE_l22,uri_rdf_rest),true,true,true),true) ).

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

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

cnf(u2445,axiom,
    true = icext(uri_rdf_List,sK5_testcase_premise_fullish_022_List_Member_Access_BNODE_l12) ).

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

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

cnf(u3327,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_rest),true,ifeq(iext(X0,sK7_testcase_premise_fullish_022_List_Member_Access_BNODE_l21,sK4_testcase_premise_fullish_022_List_Member_Access_BNODE_l22),true,true,true),true) ).

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

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

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

cnf(u3360,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(u4007,axiom,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdfs_Class),true,ifeq(iext(X0,uri_skos_OrderedCollection,X1),true,true,true),true) ).

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

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

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

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

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

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

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

cnf(u2691,axiom,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdf_List),true,ifeq(iext(X0,X1,sK2_testcase_premise_fullish_022_List_Member_Access_BNODE_l31),true,true,true),true) ).

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

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

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

cnf(u5905,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_skos_member,uri_rdfs_Resource),true,ifeq(sF1,true,true,true),true) ).

cnf(u3429,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_skos_member),true,ifeq(iext(X0,uri_ex_MyOrderedCollection,uri_ex_Z),true,sF3,true),true) ).

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

cnf(u933,axiom,
    true = icext(uri_rdf_Property,sK6_testcase_premise_fullish_022_List_Member_Access_BNODE_pL) ).

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

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

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

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

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

cnf(u931,axiom,
    true = icext(uri_skos_OrderedCollection,uri_ex_MyOrderedCollection) ).

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

cnf(u2717,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdf_List,X0),true,icext(X0,sK8_testcase_premise_fullish_022_List_Member_Access_BNODE_l11),true) ).

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

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

cnf(u3377,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(u316,axiom,
    true = ifeq(sF2,true,ip(uri_skos_member),true) ).

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

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

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

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

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

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

cnf(u2475,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdf_List,X0),true,icext(X0,sK4_testcase_premise_fullish_022_List_Member_Access_BNODE_l22),true) ).

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

cnf(u189,axiom,
    true = iext(uri_rdf_rest,sK2_testcase_premise_fullish_022_List_Member_Access_BNODE_l31,sK3_testcase_premise_fullish_022_List_Member_Access_BNODE_l32) ).

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

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

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

cnf(u3378,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(u3509,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_domain,X0),true,iext(X0,uri_rdfs_subClassOf,uri_rdfs_Class),true) ).

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

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

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

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

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

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

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

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

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

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

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

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

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

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

cnf(u3399,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(u1865,axiom,
    true = iext(uri_rdfs_subPropertyOf,uri_rdfs_label,uri_rdfs_label) ).

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

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

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

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

cnf(u5826,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_skos_member,uri_rdfs_Resource),true,ifeq(sF3,true,true,true),true) ).

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

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

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

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

cnf(u3403,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(u3527,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_rest,X0),true,iext(X0,sK3_testcase_premise_fullish_022_List_Member_Access_BNODE_l32,sK1_testcase_premise_fullish_022_List_Member_Access_BNODE_l33),true) ).

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

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

cnf(u3539,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,sK5_testcase_premise_fullish_022_List_Member_Access_BNODE_l12,uri_rdf_List),true) ).

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

cnf(u2263,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdf_first,X0),true,icext(X0,uri_ex_Z),true) ).

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

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

cnf(u5068,axiom,
    true = iext(sK6_testcase_premise_fullish_022_List_Member_Access_BNODE_pL,uri_ex_MyOrderedCollection,sK2_testcase_premise_fullish_022_List_Member_Access_BNODE_l31) ).

cnf(u3531,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_rest,X0),true,iext(X0,sK7_testcase_premise_fullish_022_List_Member_Access_BNODE_l21,sK4_testcase_premise_fullish_022_List_Member_Access_BNODE_l22),true) ).

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

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

cnf(u3410,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(u89,axiom,
    true = iext(uri_rdfs_range,uri_rdf__3,uri_rdfs_Resource) ).

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

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

cnf(u3409,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(u6596,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_skos_member,uri_skos_member),true,ifeq(sF2,true,sF2,true),true) ).

cnf(u3368,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(u3534,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_first,X0),true,iext(X0,sK3_testcase_premise_fullish_022_List_Member_Access_BNODE_l32,uri_ex_Y),true) ).

cnf(u2261,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdf_first,X0),true,icext(X0,uri_rdf_rest),true) ).

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

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

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

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

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

cnf(u3430,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_skos_memberList),true,ifeq(iext(X0,uri_ex_MyOrderedCollection,sK2_testcase_premise_fullish_022_List_Member_Access_BNODE_l31),true,true,true),true) ).

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

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

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

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

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

cnf(u3538,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_first,X0),true,iext(X0,sK7_testcase_premise_fullish_022_List_Member_Access_BNODE_l21,sK6_testcase_premise_fullish_022_List_Member_Access_BNODE_pL),true) ).

cnf(u217,axiom,
    true = iext(uri_rdfs_subPropertyOf,uri_skos_memberList,sK6_testcase_premise_fullish_022_List_Member_Access_BNODE_pL) ).

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

cnf(u3385,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(u2262,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdf_first,X0),true,icext(X0,uri_ex_Y),true) ).

cnf(u2671,axiom,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdf_List),true,ifeq(iext(X0,X1,sK1_testcase_premise_fullish_022_List_Member_Access_BNODE_l33),true,true,true),true) ).

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

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

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

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

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

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

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

cnf(u2129,axiom,
    true = ifeq(iext(uri_rdfs_range,X0,uri_skos_OrderedCollection),true,ifeq(iext(X0,X1,uri_ex_MyOrderedCollection),true,true,true),true) ).

cnf(u3405,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(u5629,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_skos_member,uri_skos_OrderedCollection),true,ifeq(sF2,true,true,true),true) ).

cnf(u234,axiom,
    tuple(true,true,true) = sF5 ).

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

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

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

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

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

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

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

cnf(u3411,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(u201,axiom,
    true = iext(uri_rdf_first,sK1_testcase_premise_fullish_022_List_Member_Access_BNODE_l33,uri_ex_Z) ).

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

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

cnf(u3321,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_first),true,ifeq(iext(X0,sK8_testcase_premise_fullish_022_List_Member_Access_BNODE_l11,sK6_testcase_premise_fullish_022_List_Member_Access_BNODE_pL),true,true,true),true) ).

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

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

cnf(u3318,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_type),true,ifeq(iext(X0,sK4_testcase_premise_fullish_022_List_Member_Access_BNODE_l22,uri_rdf_List),true,true,true),true) ).

cnf(u3333,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_rest),true,ifeq(iext(X0,sK5_testcase_premise_fullish_022_List_Member_Access_BNODE_l12,uri_rdf_nil),true,true,true),true) ).

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

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

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

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

cnf(u3375,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(u3344,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(u961,axiom,
    true = icext(uri_rdf_Property,uri_rdf_rest) ).

cnf(u3322,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_first),true,ifeq(iext(X0,sK2_testcase_premise_fullish_022_List_Member_Access_BNODE_l31,uri_ex_X),true,true,true),true) ).

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

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

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

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

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

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

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

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

cnf(u3285,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(u802,axiom,
    true = iext(uri_rdfs_subPropertyOf,uri_owl_propertyChainAxiom,uri_owl_propertyChainAxiom) ).

cnf(u3331,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_rest),true,ifeq(iext(X0,sK3_testcase_premise_fullish_022_List_Member_Access_BNODE_l32,sK1_testcase_premise_fullish_022_List_Member_Access_BNODE_l33),true,true,true),true) ).

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

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

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

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

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

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

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

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

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

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

cnf(u3396,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_subPropertyOf),true,ifeq(iext(X0,uri_skos_memberList,sK6_testcase_premise_fullish_022_List_Member_Access_BNODE_pL),true,true,true),true) ).

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

cnf(u2088,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_skos_member,X0),true,ifeq(sF3,true,icext(X0,uri_ex_Z),true),true) ).

cnf(u3383,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(u562,axiom,
    true = ic(uri_rdfs_Class) ).

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

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

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

cnf(u317,axiom,
    true = ifeq(sF3,true,ip(uri_skos_member),true) ).

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

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

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

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

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

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

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

cnf(u3738,axiom,
    true = iext(uri_rdfs_subClassOf,uri_rdfs_Statement,uri_rdfs_Resource) ).

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

cnf(u3543,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,sK2_testcase_premise_fullish_022_List_Member_Access_BNODE_l31,uri_rdf_List),true) ).

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

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

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

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

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

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

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

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

cnf(u3535,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_first,X0),true,iext(X0,sK1_testcase_premise_fullish_022_List_Member_Access_BNODE_l33,uri_ex_Z),true) ).

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

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

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

cnf(u3414,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(u4036,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdfs_subClassOf),true,ifeq(iext(X0,uri_skos_OrderedCollection,uri_rdfs_Resource),true,true,true),true) ).

cnf(u3372,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(u3352,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(u79,axiom,
    true = iext(uri_rdfs_domain,uri_rdf__1,uri_rdfs_Resource) ).

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

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

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

cnf(u3365,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(u5978,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_skos_member,uri_rdfs_Resource),true,ifeq(sF3,true,true,true),true) ).

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

cnf(u2448,axiom,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdf_List),true,ifeq(iext(X0,sK5_testcase_premise_fullish_022_List_Member_Access_BNODE_l12,X1),true,true,true),true) ).

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

cnf(u3542,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,sK1_testcase_premise_fullish_022_List_Member_Access_BNODE_l33,uri_rdf_List),true) ).

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

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

cnf(u3369,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(u207,axiom,
    true = iext(uri_rdf_first,sK4_testcase_premise_fullish_022_List_Member_Access_BNODE_l22,uri_rdf_rest) ).

cnf(u3428,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_skos_member),true,ifeq(iext(X0,uri_ex_MyOrderedCollection,uri_ex_X),true,sF2,true),true) ).

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

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

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

cnf(u3546,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,sK8_testcase_premise_fullish_022_List_Member_Access_BNODE_l11,uri_rdf_List),true) ).

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

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

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

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

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

cnf(u3301,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(u3432,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_owl_propertyChainAxiom,X0),true,iext(X0,uri_skos_member,sK8_testcase_premise_fullish_022_List_Member_Access_BNODE_l11),true) ).

cnf(u3282,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(u740,axiom,
    true = ip(sK6_testcase_premise_fullish_022_List_Member_Access_BNODE_pL) ).

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

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

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

cnf(u3305,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(u3452,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0),true,iext(X0,uri_rdfs_ContainerMembershipProperty,uri_rdfs_Resource),true) ).

cnf(u2257,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdf_rest,X0),true,icext(X0,sK3_testcase_premise_fullish_022_List_Member_Access_BNODE_l32),true) ).

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

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

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

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

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

cnf(u6597,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_skos_member,uri_skos_member),true,ifeq(sF3,true,sF3,true),true) ).

cnf(u3328,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_rest),true,ifeq(iext(X0,sK8_testcase_premise_fullish_022_List_Member_Access_BNODE_l11,sK5_testcase_premise_fullish_022_List_Member_Access_BNODE_l12),true,true,true),true) ).

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

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

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

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

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

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

cnf(u745,axiom,
    true = ifeq(iext(sK6_testcase_premise_fullish_022_List_Member_Access_BNODE_pL,X1,X0),true,true,true) ).

cnf(u3316,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_type),true,ifeq(iext(X0,sK1_testcase_premise_fullish_022_List_Member_Access_BNODE_l33,uri_rdf_List),true,true,true),true) ).

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

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

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

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

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

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

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

cnf(u3320,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_first),true,ifeq(iext(X0,sK7_testcase_premise_fullish_022_List_Member_Access_BNODE_l21,sK6_testcase_premise_fullish_022_List_Member_Access_BNODE_pL),true,true,true),true) ).

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

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

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

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

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

cnf(u1580,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_skos_member,X0),true,ifeq(sF3,true,icext(X0,uri_ex_MyOrderedCollection),true),true) ).

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

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

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

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

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

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

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

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

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

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

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

cnf(u2718,axiom,
    true = iext(uri_rdf_type,sK8_testcase_premise_fullish_022_List_Member_Access_BNODE_l11,uri_rdf_List) ).

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

cnf(u1183,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_skos_OrderedCollection,X0),true,icext(X0,uri_ex_MyOrderedCollection),true) ).

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

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

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

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

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

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

cnf(u187,axiom,
    true = iext(uri_rdf_rest,sK1_testcase_premise_fullish_022_List_Member_Access_BNODE_l33,uri_rdf_nil) ).

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

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

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

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

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

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

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

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

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

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

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

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

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

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

cnf(u185,axiom,
    true = iext(uri_skos_memberList,uri_ex_MyOrderedCollection,sK2_testcase_premise_fullish_022_List_Member_Access_BNODE_l31) ).

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

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

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

cnf(u2730,axiom,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdf_List),true,ifeq(iext(X0,sK7_testcase_premise_fullish_022_List_Member_Access_BNODE_l21,X1),true,true,true),true) ).

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

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

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

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

cnf(u191,axiom,
    true = iext(uri_rdf_rest,sK3_testcase_premise_fullish_022_List_Member_Access_BNODE_l32,sK1_testcase_premise_fullish_022_List_Member_Access_BNODE_l33) ).

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

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

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

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

cnf(u5076,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,sK6_testcase_premise_fullish_022_List_Member_Access_BNODE_pL,X0),true,iext(X0,uri_ex_MyOrderedCollection,sK2_testcase_premise_fullish_022_List_Member_Access_BNODE_l31),true) ).

cnf(u3957,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_skos_memberList),true,iext(uri_rdfs_subPropertyOf,X0,sK6_testcase_premise_fullish_022_List_Member_Access_BNODE_pL),true) ).

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

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

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

cnf(u3526,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_rest,X0),true,iext(X0,sK4_testcase_premise_fullish_022_List_Member_Access_BNODE_l22,uri_rdf_nil),true) ).

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

cnf(u3349,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(u3281,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(u2650,axiom,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdf_List),true,ifeq(iext(X0,sK3_testcase_premise_fullish_022_List_Member_Access_BNODE_l32,X1),true,true,true),true) ).

cnf(u3530,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_rest,X0),true,iext(X0,sK8_testcase_premise_fullish_022_List_Member_Access_BNODE_l11,sK5_testcase_premise_fullish_022_List_Member_Access_BNODE_l12),true) ).

cnf(u3353,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(u2113,axiom,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdfs_Resource),true,ifeq(iext(X0,X2,X1),true,true,true),true) ).

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

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

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

cnf(u2658,axiom,
    true = iext(uri_rdf_type,sK3_testcase_premise_fullish_022_List_Member_Access_BNODE_l32,uri_rdf_List) ).

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

cnf(u3540,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,sK4_testcase_premise_fullish_022_List_Member_Access_BNODE_l22,uri_rdf_List),true) ).

cnf(u2259,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdf_rest,X0),true,icext(X0,sK4_testcase_premise_fullish_022_List_Member_Access_BNODE_l22),true) ).

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

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

cnf(u2449,axiom,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdf_List),true,ifeq(iext(X0,X1,sK5_testcase_premise_fullish_022_List_Member_Access_BNODE_l12),true,true,true),true) ).

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

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

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

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

cnf(u3379,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(u630,axiom,
    true = ic(uri_rdf_XMLLiteral) ).

cnf(u3286,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(u101,axiom,
    true = iext(uri_rdf_type,uri_rdf_XMLLiteral,uri_rdfs_Datatype) ).

cnf(u3544,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,uri_ex_MyOrderedCollection,uri_skos_OrderedCollection),true) ).

cnf(u231,axiom,
    tuple(sF1,sF2,sF3) = sF4 ).

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

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

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

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

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

cnf(u3290,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(u3433,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_owl_propertyChainAxiom,X0),true,iext(X0,sK6_testcase_premise_fullish_022_List_Member_Access_BNODE_pL,sK7_testcase_premise_fullish_022_List_Member_Access_BNODE_l21),true) ).

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

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

cnf(u229,axiom,
    iext(uri_skos_member,uri_ex_MyOrderedCollection,uri_ex_Z) = sF3 ).

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

cnf(u3423,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(u3300,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(u2667,axiom,
    true = icext(uri_rdf_List,sK1_testcase_premise_fullish_022_List_Member_Access_BNODE_l33) ).

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

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

cnf(u4056,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subClassOf,X0),true,icext(X0,uri_skos_OrderedCollection),true) ).

cnf(u2159,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_skos_memberList,X0),true,icext(X0,sK2_testcase_premise_fullish_022_List_Member_Access_BNODE_l31),true) ).

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

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

cnf(u3315,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_type),true,ifeq(iext(X0,sK2_testcase_premise_fullish_022_List_Member_Access_BNODE_l31,uri_rdf_List),true,true,true),true) ).

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

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

cnf(u2087,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_skos_member,X0),true,ifeq(sF2,true,icext(X0,uri_ex_X),true),true) ).

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

cnf(u3329,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_rest),true,ifeq(iext(X0,sK2_testcase_premise_fullish_022_List_Member_Access_BNODE_l31,sK3_testcase_premise_fullish_022_List_Member_Access_BNODE_l32),true,true,true),true) ).

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

cnf(u746,axiom,
    true = iext(uri_rdf_type,sK6_testcase_premise_fullish_022_List_Member_Access_BNODE_pL,uri_rdf_Property) ).

cnf(u3324,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_first),true,ifeq(iext(X0,sK3_testcase_premise_fullish_022_List_Member_Access_BNODE_l32,uri_ex_Y),true,true,true),true) ).

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

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

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

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

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

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

cnf(u2258,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdf_rest,X0),true,icext(X0,sK5_testcase_premise_fullish_022_List_Member_Access_BNODE_l12),true) ).

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

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

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

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

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

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

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

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

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

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

cnf(u3312,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_type),true,ifeq(iext(X0,sK8_testcase_premise_fullish_022_List_Member_Access_BNODE_l11,uri_rdf_List),true,true,true),true) ).

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

cnf(u2086,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_skos_member,X0),true,ifeq(sF1,true,icext(X0,uri_ex_Y),true),true) ).

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

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

cnf(u3355,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(u3479,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X0),true,iext(X0,uri_rdf__3,uri_rdfs_member),true) ).

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

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

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

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

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

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

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

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

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

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

cnf(u3362,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(u41,axiom,
    true = iext(uri_rdfs_range,uri_rdfs_isDefinedBy,uri_rdfs_Resource) ).

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

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

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

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

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

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

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

cnf(u2468,axiom,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdf_List),true,ifeq(iext(X0,sK4_testcase_premise_fullish_022_List_Member_Access_BNODE_l22,X1),true,true,true),true) ).

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

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

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

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

cnf(u2727,axiom,
    true = icext(uri_rdf_List,sK7_testcase_premise_fullish_022_List_Member_Access_BNODE_l21) ).

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

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

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

cnf(u315,axiom,
    true = ifeq(sF1,true,ip(uri_skos_member),true) ).

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

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

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

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

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

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

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

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

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

cnf(u4015,axiom,
    true = iext(uri_rdf_type,uri_skos_OrderedCollection,uri_rdfs_Class) ).

cnf(u2737,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdf_List,X0),true,icext(X0,sK7_testcase_premise_fullish_022_List_Member_Access_BNODE_l21),true) ).

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

cnf(u2485,axiom,
    true = icext(uri_rdf_List,sK3_testcase_premise_fullish_022_List_Member_Access_BNODE_l32) ).

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

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

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

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

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

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

cnf(u3317,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_type),true,ifeq(iext(X0,sK3_testcase_premise_fullish_022_List_Member_Access_BNODE_l32,uri_rdf_List),true,true,true),true) ).

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

cnf(u2690,axiom,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdf_List),true,ifeq(iext(X0,sK2_testcase_premise_fullish_022_List_Member_Access_BNODE_l31,X1),true,true,true),true) ).

cnf(u3400,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(u1724,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdf_first,X0),true,icext(X0,sK8_testcase_premise_fullish_022_List_Member_Access_BNODE_l11),true) ).

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

cnf(u3269,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_skos_member,X0),true,ifeq(sF1,true,iext(X0,uri_ex_MyOrderedCollection,uri_ex_Y),true),true) ).

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

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

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

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

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

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

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

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

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

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

cnf(u3361,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(u3311,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_type),true,ifeq(iext(X0,sK7_testcase_premise_fullish_022_List_Member_Access_BNODE_l21,uri_rdf_List),true,true,true),true) ).

cnf(u3270,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_skos_member,X0),true,ifeq(sF2,true,iext(X0,uri_ex_MyOrderedCollection,uri_ex_X),true),true) ).

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

cnf(u3528,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_rest,X0),true,iext(X0,sK1_testcase_premise_fullish_022_List_Member_Access_BNODE_l33,uri_rdf_nil),true) ).

cnf(u215,axiom,
    true = iext(uri_rdf_type,uri_ex_MyOrderedCollection,uri_skos_OrderedCollection) ).

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

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

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

cnf(u3363,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(u3424,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(u1846,axiom,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdf_Property),true,ifeq(iext(X0,uri_rdfs_label,X1),true,true,true),true) ).

cnf(u3274,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(u3417,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(u1636,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_subClassOf,X0),true,icext(X0,uri_rdfs_Literal),true) ).

cnf(u2267,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdf_type,X0),true,icext(X0,uri_skos_OrderedCollection),true) ).

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

cnf(u6595,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_skos_member,uri_skos_member),true,ifeq(sF1,true,sF1,true),true) ).

cnf(u213,axiom,
    true = iext(uri_rdf_first,sK8_testcase_premise_fullish_022_List_Member_Access_BNODE_l11,sK6_testcase_premise_fullish_022_List_Member_Access_BNODE_pL) ).

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

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

cnf(u3284,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(u2651,axiom,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdf_List),true,ifeq(iext(X0,X1,sK3_testcase_premise_fullish_022_List_Member_Access_BNODE_l32),true,true,true),true) ).

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

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

cnf(u3930,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,sK6_testcase_premise_fullish_022_List_Member_Access_BNODE_pL,X0),true,iext(uri_rdfs_subPropertyOf,uri_skos_memberList,X0),true) ).

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

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

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

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

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

cnf(u203,axiom,
    true = iext(uri_rdf_first,sK2_testcase_premise_fullish_022_List_Member_Access_BNODE_l31,uri_ex_X) ).

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

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

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

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

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

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

cnf(u3319,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_type),true,ifeq(iext(X0,sK5_testcase_premise_fullish_022_List_Member_Access_BNODE_l12,uri_rdf_List),true,true,true),true) ).

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

cnf(u3667,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(u3703,axiom,
    true = ifeq(icext(uri_rdf_List,X0),true,icext(uri_rdf_List,X0),true) ).

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

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

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

cnf(u3323,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_first),true,ifeq(iext(X0,sK1_testcase_premise_fullish_022_List_Member_Access_BNODE_l33,uri_ex_Z),true,true,true),true) ).

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

cnf(u3418,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(u2168,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subClassOf,X0),true,icext(X0,uri_rdf_Bag),true) ).

cnf(u3335,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(u27,axiom,
    true = ifeq(ip(X0),true,iext(uri_rdf_type,X0,uri_rdf_Property),true) ).

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

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

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

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

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

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

cnf(u3339,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(u2110,axiom,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdf_Property),true,ifeq(iext(X0,X1,sK6_testcase_premise_fullish_022_List_Member_Access_BNODE_pL),true,true,true),true) ).

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

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

cnf(u2707,axiom,
    true = icext(uri_rdf_List,sK8_testcase_premise_fullish_022_List_Member_Access_BNODE_l11) ).

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

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

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

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

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

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

cnf(u2710,axiom,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdf_List),true,ifeq(iext(X0,sK8_testcase_premise_fullish_022_List_Member_Access_BNODE_l11,X1),true,true,true),true) ).

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

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

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

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

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

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

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

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

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

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

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

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

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

cnf(u2697,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdf_List,X0),true,icext(X0,sK2_testcase_premise_fullish_022_List_Member_Access_BNODE_l31),true) ).

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

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

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

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

cnf(u2711,axiom,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdf_List),true,ifeq(iext(X0,X1,sK8_testcase_premise_fullish_022_List_Member_Access_BNODE_l11),true,true,true),true) ).

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

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

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

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

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

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

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

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

cnf(u2698,axiom,
    true = iext(uri_rdf_type,sK2_testcase_premise_fullish_022_List_Member_Access_BNODE_l31,uri_rdf_List) ).

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

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

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

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

cnf(u3752,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(u951,axiom,
    true = icext(uri_rdf_Property,uri_rdfs_domain) ).

cnf(u5070,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,sK6_testcase_premise_fullish_022_List_Member_Access_BNODE_pL),true,ifeq(iext(X0,uri_ex_MyOrderedCollection,sK2_testcase_premise_fullish_022_List_Member_Access_BNODE_l31),true,true,true),true) ).

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

cnf(u2476,axiom,
    true = iext(uri_rdf_type,sK4_testcase_premise_fullish_022_List_Member_Access_BNODE_l22,uri_rdf_List) ).

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

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

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

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

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

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

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

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

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

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

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

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

cnf(u1578,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_skos_member,X0),true,ifeq(sF1,true,icext(X0,uri_ex_MyOrderedCollection),true),true) ).

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

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

cnf(u5555,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_skos_member,uri_skos_OrderedCollection),true,ifeq(sF1,true,true,true),true) ).

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

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

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

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

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

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

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

cnf(u3425,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_owl_propertyChainAxiom),true,ifeq(iext(X0,sK6_testcase_premise_fullish_022_List_Member_Access_BNODE_pL,sK7_testcase_premise_fullish_022_List_Member_Access_BNODE_l21),true,true,true),true) ).

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

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

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

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

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

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

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

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

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

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

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

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

cnf(u199,axiom,
    true = iext(uri_rdf_rest,sK8_testcase_premise_fullish_022_List_Member_Access_BNODE_l11,sK5_testcase_premise_fullish_022_List_Member_Access_BNODE_l12) ).

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

cnf(u5554,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_skos_member,uri_rdfs_Resource),true,ifeq(sF1,true,true,true),true) ).

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

cnf(u3999,axiom,
    true = icext(uri_rdfs_Class,uri_skos_OrderedCollection) ).

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

cnf(u3277,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(u3408,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(u1623,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_owl_propertyChainAxiom,X0),true,icext(X0,sK6_testcase_premise_fullish_022_List_Member_Access_BNODE_pL),true) ).

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

cnf(u3306,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(u2114,axiom,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdfs_ContainerMembershipProperty),true,ifeq(iext(X0,X1,uri_rdf__3),true,true,true),true) ).

cnf(u3401,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(u3532,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_first,X0),true,iext(X0,sK5_testcase_premise_fullish_022_List_Member_Access_BNODE_l12,uri_rdf_first),true) ).

cnf(u197,axiom,
    true = iext(uri_rdf_rest,sK7_testcase_premise_fullish_022_List_Member_Access_BNODE_l21,sK4_testcase_premise_fullish_022_List_Member_Access_BNODE_l22) ).

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

cnf(u3347,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(u1618,axiom,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_skos_OrderedCollection),true,ifeq(iext(X0,uri_ex_MyOrderedCollection,X1),true,true,true),true) ).

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

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

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

cnf(u3421,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(u1624,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_rdfs_subClassOf,X0),true,icext(X0,uri_rdfs_Class),true) ).

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

cnf(u586,axiom,
    true = icext(uri_rdfs_Class,uri_rdfs_Literal) ).

cnf(u3529,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_rest,X0),true,iext(X0,sK2_testcase_premise_fullish_022_List_Member_Access_BNODE_l31,sK3_testcase_premise_fullish_022_List_Member_Access_BNODE_l32),true) ).

cnf(u3283,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(u109,axiom,
    true = ifeq(iext(uri_rdfs_domain,X0,X1),true,ifeq(iext(X0,X2,X3),true,icext(X1,X2),true),true) ).

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

cnf(u3374,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(u5074,axiom,
    true = ifeq(iext(uri_rdfs_domain,sK6_testcase_premise_fullish_022_List_Member_Access_BNODE_pL,X0),true,icext(X0,uri_ex_MyOrderedCollection),true) ).

cnf(u2265,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdf_first,X0),true,icext(X0,sK6_testcase_premise_fullish_022_List_Member_Access_BNODE_pL),true) ).

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

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

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

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

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

cnf(u2161,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_owl_propertyChainAxiom,X0),true,icext(X0,sK7_testcase_premise_fullish_022_List_Member_Access_BNODE_l21),true) ).

cnf(u2255,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdf_rest,X0),true,icext(X0,sK1_testcase_premise_fullish_022_List_Member_Access_BNODE_l33),true) ).

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

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

cnf(u3292,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(u99,axiom,
    true = iext(uri_rdfs_subClassOf,uri_rdf_XMLLiteral,uri_rdfs_Literal) ).

cnf(u2670,axiom,
    true = ifeq(iext(uri_rdfs_domain,X0,uri_rdf_List),true,ifeq(iext(X0,sK1_testcase_premise_fullish_022_List_Member_Access_BNODE_l33,X1),true,true,true),true) ).

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

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

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

cnf(u3307,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(u3693,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(u3296,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(u3447,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subClassOf,X0),true,iext(X0,uri_rdf_XMLLiteral,uri_rdfs_Literal),true) ).

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

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

cnf(u227,axiom,
    iext(uri_skos_member,uri_ex_MyOrderedCollection,uri_ex_X) = sF2 ).

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

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

cnf(u3412,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(u2092,axiom,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdf_Property),true,ifeq(iext(X0,X1,uri_rdf_rest),true,true,true),true) ).

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

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

cnf(u225,axiom,
    iext(uri_skos_member,uri_ex_MyOrderedCollection,uri_ex_Y) = sF1 ).

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

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

cnf(u3343,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(u2295,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdf_type,X0),true,icext(X0,uri_rdfs_ContainerMembershipProperty),true) ).

cnf(u5628,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_skos_member,uri_rdfs_Resource),true,ifeq(sF2,true,true,true),true) ).

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

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

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

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

cnf(u3330,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_rest),true,ifeq(iext(X0,sK1_testcase_premise_fullish_022_List_Member_Access_BNODE_l33,uri_rdf_nil),true,true,true),true) ).

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

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

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

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

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

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

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

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

cnf(u3373,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(u3350,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(u3608,axiom,
    true = ifeq(iext(uri_rdf__1,X1,X0),true,iext(uri_rdfs_member,X1,X0),true) ).

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

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

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

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

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

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

cnf(u2455,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdf_List,X0),true,icext(X0,sK5_testcase_premise_fullish_022_List_Member_Access_BNODE_l12),true) ).

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

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

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

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

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

cnf(u2205,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdfs_subPropertyOf,X0),true,icext(X0,uri_rdf_value),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(u3364,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(u550,axiom,
    true = ifeq(iext(uri_rdf_subject,X1,X0),true,true,true) ).

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

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

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

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

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

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

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

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

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

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

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

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

cnf(u1579,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_skos_member,X0),true,ifeq(sF2,true,icext(X0,uri_ex_MyOrderedCollection),true),true) ).

cnf(u3314,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_type),true,ifeq(iext(X0,uri_ex_MyOrderedCollection,uri_skos_OrderedCollection),true,true,true),true) ).

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

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

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

cnf(u3388,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(u2107,axiom,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdf_Property),true,ifeq(iext(X0,X1,uri_rdfs_member),true,true,true),true) ).

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

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

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

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

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

cnf(u183,axiom,
    true = iext(uri_owl_propertyChainAxiom,uri_skos_member,sK8_testcase_premise_fullish_022_List_Member_Access_BNODE_l11) ).

cnf(u2738,axiom,
    true = iext(uri_rdf_type,sK7_testcase_premise_fullish_022_List_Member_Access_BNODE_l21,uri_rdf_List) ).

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

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

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

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

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

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

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

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

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

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

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

cnf(u181,axiom,
    true = iext(uri_owl_propertyChainAxiom,sK6_testcase_premise_fullish_022_List_Member_Access_BNODE_pL,sK7_testcase_premise_fullish_022_List_Member_Access_BNODE_l21) ).

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

cnf(u3289,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(u3392,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(u4008,axiom,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdfs_Class),true,ifeq(iext(X0,X1,uri_skos_OrderedCollection),true,true,true),true) ).

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

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

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

cnf(u1621,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_skos_memberList,X0),true,icext(X0,uri_ex_MyOrderedCollection),true) ).

cnf(u4022,axiom,
    true = iext(uri_rdfs_subClassOf,uri_skos_OrderedCollection,uri_rdfs_Resource) ).

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

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

cnf(u3279,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(u1201,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdf_Property,X0),true,icext(X0,uri_skos_memberList),true) ).

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

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

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

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

cnf(u232,negated_conjecture,
    ~ sP0(sF4) ).

cnf(u5827,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_skos_member,uri_skos_OrderedCollection),true,ifeq(sF3,true,true,true),true) ).

cnf(u3541,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,sK3_testcase_premise_fullish_022_List_Member_Access_BNODE_l32,uri_rdf_List),true) ).

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

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

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

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

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

cnf(u5075,axiom,
    true = ifeq(iext(uri_rdfs_range,sK6_testcase_premise_fullish_022_List_Member_Access_BNODE_pL,X0),true,icext(X0,sK2_testcase_premise_fullish_022_List_Member_Access_BNODE_l31),true) ).

cnf(u3294,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(u3533,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_first,X0),true,iext(X0,sK4_testcase_premise_fullish_022_List_Member_Access_BNODE_l22,uri_rdf_rest),true) ).

cnf(u2657,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdf_List,X0),true,icext(X0,sK3_testcase_premise_fullish_022_List_Member_Access_BNODE_l32),true) ).

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

cnf(u3276,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(u83,axiom,
    true = iext(uri_rdfs_domain,uri_rdf__3,uri_rdfs_Resource) ).

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

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

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

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

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

cnf(u3537,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_first,X0),true,iext(X0,sK8_testcase_premise_fullish_022_List_Member_Access_BNODE_l11,sK6_testcase_premise_fullish_022_List_Member_Access_BNODE_pL),true) ).

cnf(u3291,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(u1766,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,X1,X0),true,icext(uri_rdfs_Class,X1),true) ).

cnf(u2677,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdf_List,X0),true,icext(X0,sK1_testcase_premise_fullish_022_List_Member_Access_BNODE_l33),true) ).

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

cnf(u3280,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(u3431,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_skos_memberList,X0),true,iext(X0,uri_ex_MyOrderedCollection,sK2_testcase_premise_fullish_022_List_Member_Access_BNODE_l31),true) ).

cnf(u3741,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(u1218,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdf_Property,X0),true,icext(X0,uri_rdf_first),true) ).

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

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

cnf(u211,axiom,
    true = iext(uri_rdf_first,sK7_testcase_premise_fullish_022_List_Member_Access_BNODE_l21,sK6_testcase_premise_fullish_022_List_Member_Access_BNODE_pL) ).

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

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

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

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

cnf(u2678,axiom,
    true = iext(uri_rdf_type,sK1_testcase_premise_fullish_022_List_Member_Access_BNODE_l33,uri_rdf_List) ).

cnf(u2264,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_rdf_first,X0),true,icext(X0,uri_ex_X),true) ).

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

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

cnf(u209,axiom,
    true = iext(uri_rdf_first,sK5_testcase_premise_fullish_022_List_Member_Access_BNODE_l12,uri_rdf_first) ).

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

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

cnf(u2160,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_owl_propertyChainAxiom,X0),true,icext(X0,sK8_testcase_premise_fullish_022_List_Member_Access_BNODE_l11),true) ).

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

cnf(u2465,axiom,
    true = icext(uri_rdf_List,sK4_testcase_premise_fullish_022_List_Member_Access_BNODE_l22) ).

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

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

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

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

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

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

cnf(u3588,axiom,
    true = ifeq(iext(sK6_testcase_premise_fullish_022_List_Member_Access_BNODE_pL,X1,X0),true,iext(sK6_testcase_premise_fullish_022_List_Member_Access_BNODE_pL,X1,X0),true) ).

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

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

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

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

cnf(u3586,axiom,
    true = ifeq(iext(uri_skos_memberList,X1,X0),true,iext(uri_skos_memberList,X1,X0),true) ).

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

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

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

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

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

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

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

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

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

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

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

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

cnf(u3462,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdfs_subPropertyOf,X0),true,iext(X0,uri_skos_memberList,sK6_testcase_premise_fullish_022_List_Member_Access_BNODE_pL),true) ).

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

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

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

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

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

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

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

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

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

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

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

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

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

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

cnf(u5977,axiom,
    true = ifeq(iext(uri_rdfs_range,uri_skos_member,uri_rdfs_Resource),true,ifeq(sF2,true,true,true),true) ).

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

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

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

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

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

cnf(u37,axiom,
    true = iext(uri_rdfs_range,uri_rdfs_comment,uri_rdfs_Literal) ).

cnf(u800,axiom,
    true = iext(uri_rdfs_subPropertyOf,uri_skos_memberList,uri_skos_memberList) ).

cnf(u167,axiom,
    true = iext(uri_rdfs_range,uri_rdfs_subPropertyOf,uri_rdf_Property) ).

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

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

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

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

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

cnf(u422,axiom,
    true = iext(uri_rdf_type,uri_owl_propertyChainAxiom,uri_rdf_Property) ).

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

cnf(u3376,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(u4023,axiom,
    true = iext(uri_rdfs_subClassOf,uri_skos_OrderedCollection,uri_skos_OrderedCollection) ).

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

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

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

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

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

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

cnf(u165,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,X1),true,ifeq(iext(X0,X2,X3),true,iext(X1,X2,X3),true),true) ).

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

cnf(u2731,axiom,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdf_List),true,ifeq(iext(X0,X1,sK7_testcase_premise_fullish_022_List_Member_Access_BNODE_l21),true,true,true),true) ).

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

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

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

cnf(u3415,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(u3389,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(u682,axiom,
    true = icext(uri_rdfs_Class,uri_rdfs_ContainerMembershipProperty) ).

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

cnf(u77,axiom,
    true = iext(uri_rdfs_range,uri_rdfs_member,uri_rdfs_Resource) ).

cnf(u3299,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(u4016,axiom,
    true = ic(uri_skos_OrderedCollection) ).

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

cnf(u3393,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(u1622,axiom,
    true = ifeq(iext(uri_rdfs_domain,uri_owl_propertyChainAxiom,X0),true,icext(X0,uri_skos_member),true) ).

cnf(u3525,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_rest,X0),true,iext(X0,sK5_testcase_premise_fullish_022_List_Member_Access_BNODE_l12,uri_rdf_nil),true) ).

cnf(u3271,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_skos_member,X0),true,ifeq(sF3,true,iext(X0,uri_ex_MyOrderedCollection,uri_ex_Z),true),true) ).

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

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

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

cnf(u3359,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(u67,axiom,
    true = iext(uri_rdfs_subClassOf,uri_rdf_Alt,uri_rdfs_Container) ).

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

cnf(u205,axiom,
    true = iext(uri_rdf_first,sK3_testcase_premise_fullish_022_List_Member_Access_BNODE_l32,uri_ex_Y) ).

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

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

cnf(u3275,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(u3342,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(u587,axiom,
    true = iext(uri_rdfs_subClassOf,uri_rdfs_Literal,uri_rdfs_Resource) ).

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

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

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

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

cnf(u65,axiom,
    true = iext(uri_rdfs_range,uri_rdf_rest,uri_rdf_List) ).

cnf(u195,axiom,
    true = iext(uri_rdf_rest,sK5_testcase_premise_fullish_022_List_Member_Access_BNODE_l12,uri_rdf_nil) ).

cnf(u3346,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(u1895,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,uri_rdf_Property,X0),true,icext(X0,uri_rdfs_comment),true) ).

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

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

cnf(u3419,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(u149,axiom,
    true = ifeq(iext(uri_rdfs_subClassOf,X0,X1),true,ic(X1),true) ).

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

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

cnf(u3380,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(u107,axiom,
    true = iext(uri_rdfs_domain,uri_rdfs_domain,uri_rdf_Property) ).

cnf(u193,axiom,
    true = iext(uri_rdf_rest,sK4_testcase_premise_fullish_022_List_Member_Access_BNODE_l22,uri_rdf_nil) ).

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

cnf(u3384,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(u3547,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_type,X0),true,iext(X0,sK7_testcase_premise_fullish_022_List_Member_Access_BNODE_l21,uri_rdf_List),true) ).

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

cnf(u2456,axiom,
    true = iext(uri_rdf_type,sK5_testcase_premise_fullish_022_List_Member_Access_BNODE_l12,uri_rdf_List) ).

cnf(u3426,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_owl_propertyChainAxiom),true,ifeq(iext(X0,uri_skos_member,sK8_testcase_premise_fullish_022_List_Member_Access_BNODE_l11),true,true,true),true) ).

cnf(u105,axiom,
    true = iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,uri_rdfs_Class) ).

cnf(u235,negated_conjecture,
    sP0(sF5) ).

cnf(u3589,axiom,
    true = ifeq(iext(uri_owl_propertyChainAxiom,X1,X0),true,iext(uri_owl_propertyChainAxiom,X1,X0),true) ).

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

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

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

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

cnf(u3587,axiom,
    true = ifeq(iext(uri_skos_memberList,X1,X0),true,iext(sK6_testcase_premise_fullish_022_List_Member_Access_BNODE_pL,X1,X0),true) ).

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

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

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

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

cnf(u4061,axiom,
    true = ifeq(icext(uri_skos_OrderedCollection,X0),true,icext(uri_skos_OrderedCollection,X0),true) ).

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

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

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

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

cnf(u2469,axiom,
    true = ifeq(iext(uri_rdfs_range,X0,uri_rdf_List),true,ifeq(iext(X0,X1,sK4_testcase_premise_fullish_022_List_Member_Access_BNODE_l22),true,true,true),true) ).

cnf(u2687,axiom,
    true = icext(uri_rdf_List,sK2_testcase_premise_fullish_022_List_Member_Access_BNODE_l31) ).

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

cnf(u3536,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,uri_rdf_first,X0),true,iext(X0,sK2_testcase_premise_fullish_022_List_Member_Access_BNODE_l31,uri_ex_X),true) ).

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

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

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

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

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

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

cnf(u3332,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_rdf_rest),true,ifeq(iext(X0,sK4_testcase_premise_fullish_022_List_Member_Access_BNODE_l22,uri_rdf_nil),true,true,true),true) ).

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

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

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

cnf(u3427,axiom,
    true = ifeq(iext(uri_rdfs_subPropertyOf,X0,uri_skos_member),true,ifeq(iext(X0,uri_ex_MyOrderedCollection,uri_ex_Y),true,sF1,true),true) ).

cnf(u3391,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(u3336,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(u23,axiom,
    true = iext(uri_rdf_type,uri_rdf_value,uri_rdf_Property) ).

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

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

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

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

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


%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.03  % Problem  : SWB022-10 : TPTP v9.3.1. Released v7.3.0.
% 0.00/0.06  % Command  : run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.14/0.40  % Computer : n007.cluster.edu
% 0.14/0.40  % Model    : x86_64 x86_64
% 0.14/0.40  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.14/0.40  % Memory   : 8046.5625MB
% 0.14/0.40  % OS       : Linux 6.8.0-71-generic
% 0.14/0.40  % CPULimit : 300
% 0.14/0.40  % WCLimit  : 300
% 0.14/0.40  % DateTime : Mon Sep 28 07:02:25 UTC 2026
% 0.14/0.40  % CPUTime  : 
% 0.14/0.40  Running run_vampire /export/starexec/sandbox2/benchmark/theBenchmark.p 300 THM
% 0.14/0.46  Running first-order theorem proving
% 0.14/0.46  Running: /export/starexec/sandbox2/solver/bin/vampire --input_syntax tptp --output_axiom_names on --mode casc -m 16384 --cores 7 -t 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 7.31/3.62  % (2203227)Detected a unit-equality problem, will run specialized UEQ schedule.
% 7.31/3.62  % (2203234)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=2824556933:i=138329:kws=inv_arity_squared:fgj=on:bd=preordered_2999 on theBenchmark for (2999ds/138329Mi)
% 7.31/3.62  % (2203240)dis-1010_7_sil=8000:fde=unused:flr=on:random_seed=3450649677:i=1187:sd=4:av=off:ss=axioms:sgt=32_2999 on theBenchmark for (2999ds/1187Mi)
% 7.31/3.62  % (2203238)dis+10_14_to=lpo:sil=8000:tgt=full:drc=off:sp=const_frequency:sos=all:random_seed=2937988929:i=181:gtgl=5:bs=unit_only:fsr=off:gtg=exists_all_2999 on theBenchmark for (2999ds/181Mi)
% 7.31/3.62  % (2203239)lrs+10_3_to=lpo:sil=64000:drc=off:fde=unused:sp=reverse_frequency:acc=on:bsr=on:fd=preordered:nwc=1:random_seed=1351153178:avsq=on:i=257:avsqr=16,3:bd=preordered:fsr=off_2999 on theBenchmark for (2999ds/257Mi)
% 7.31/3.62  % (2203237)ott-1010_1_sfv=off:to=lpo:sil=8000:fdtod=off:sp=reverse_frequency:spb=goal_then_units:fd=preordered:random_seed=1818521555:i=136:bd=preordered:ins=2:av=off_2999 on theBenchmark for (2999ds/136Mi)
% 7.31/3.62  % (2203236)lrs+10_1_ncem=casc2026/models/loop5.pt:sil=128000:tgt=ground:npcc=on:spb=goal_then_units:urr=ec_only:random_seed=4273506402:i=130716:gtgl=4:add=on:doe=on:bd=all:gtg=exists_sym_2999 on theBenchmark for (2999ds/130716Mi)
% 7.31/3.62  % (2203235)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=4197149002:i=130792:sd=20:aac=none:nm=16:ss=included:sgt=10_2999 on theBenchmark for (2999ds/130792Mi)
% 7.31/3.62  % (2203237)Instruction limit reached! 
% 7.31/3.62  % (2203237)------------------------------
% 7.31/3.62  % (2203237)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.31/3.62  % (2203237)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.31/3.62  % (2203237)CaDiCaL version: 2.1.3
% 7.31/3.62  % (2203237)Termination reason: Instruction limit
% 7.31/3.62  % (2203237)Termination phase: Saturation
% 7.31/3.62  % (2203237)Time elapsed: 0.124 s
% 7.31/3.62  % (2203237)Peak memory usage: 89 MB
% 7.31/3.62  % (2203237)Instructions burned: 137 (million)
% 7.31/3.62  % (2203238)Refutation not found, incomplete strategy
% 7.31/3.62  % (2203238)------------------------------
% 7.31/3.62  % (2203238)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.31/3.62  % (2203238)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.31/3.62  % (2203238)CaDiCaL version: 2.1.3
% 7.31/3.62  % (2203238)Termination reason: Refutation not found, incomplete strategy
% 7.31/3.62  % (2203238)Time elapsed: 0.136 s
% 7.31/3.62  % (2203238)Peak memory usage: 89 MB
% 7.31/3.62  % (2203238)Instructions burned: 140 (million)
% 7.31/3.62  % (2203239)Instruction limit reached! 
% 7.31/3.62  % (2203239)------------------------------
% 7.31/3.62  % (2203239)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.31/3.62  % (2203239)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.31/3.62  % (2203239)CaDiCaL version: 2.1.3
% 7.31/3.62  % (2203239)Termination reason: Instruction limit
% 7.31/3.62  % (2203239)Termination phase: Saturation
% 7.31/3.62  % (2203239)Time elapsed: 0.238 s
% 7.31/3.62  % (2203239)Peak memory usage: 93 MB
% 7.31/3.62  % (2203239)Instructions burned: 258 (million)
% 7.31/3.62  % (2203248)lrs-1011_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:prc=on:fde=unused:lcm=predicate:bsr=on:flr=on:random_seed=1238348410:i=2051:gtgl=2:fgj=on:bd=all:gtg=exists_top_2996 on theBenchmark for (2996ds/2051Mi)
% 7.31/3.62  % (2203249)lrs-1002_1_ncem=casc2026/models/all5champsBiggishL14.pt:sil=16000:npcc=on:random_seed=2197272231:i=4948:ss=axioms:sgt=16_2994 on theBenchmark for (2994ds/4948Mi)
% 7.31/3.62  % (2203238)------------------------------
% 7.31/3.62  % (2203238)------------------------------
% 7.31/3.62  % (2203240)Refutation not found, incomplete strategy
% 7.31/3.62  % (2203240)------------------------------
% 7.31/3.62  % (2203240)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.31/3.62  % (2203240)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.31/3.62  % (2203240)CaDiCaL version: 2.1.3
% 7.31/3.62  % (2203240)Termination reason: Refutation not found, incomplete strategy
% 7.31/3.62  % (2203240)Time elapsed: 0.550 s
% 7.31/3.62  % (2203240)Peak memory usage: 94 MB
% 7.31/3.62  % (2203240)Instructions burned: 622 (million)
% 7.31/3.62  % (2203252)lrs+10_5:1_sil=8000:sos=all:urr=on:br=off:flr=on:random_seed=3820315906:i=215:ep=RSTC_2992 on theBenchmark for (2992ds/215Mi)
% 7.31/3.62  % (2203252)Instruction limit reached! 
% 7.31/3.62  % (2203252)------------------------------
% 7.31/3.62  % (2203252)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.31/3.62  % (2203252)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.31/3.62  % (2203252)CaDiCaL version: 2.1.3
% 7.31/3.62  % (2203252)Termination reason: Instruction limit
% 7.31/3.62  % (2203252)Termination phase: Saturation
% 7.31/3.62  % (2203252)Time elapsed: 0.181 s
% 7.31/3.62  % (2203252)Peak memory usage: 89 MB
% 7.31/3.62  % (2203252)Instructions burned: 215 (million)
% 7.31/3.62  % (2203240)------------------------------
% 7.31/3.62  % (2203240)------------------------------
% 7.31/3.62  % (2203254)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=1747143659:avsq=on:i=317:avsqr=1,16:kws=arity_squared:add=off:fgj=on:ins=10:fsr=off:gtg=exists_sym_2988 on theBenchmark for (2988ds/317Mi)
% 7.31/3.62  % (2203255)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=1869454858:i=12125:sd=2:fgj=on:ss=axioms:sgt=64_2987 on theBenchmark for (2987ds/12125Mi)
% 7.31/3.62  % (2203234)Refutation not found, incomplete strategy
% 7.31/3.62  % (2203234)------------------------------
% 7.31/3.62  % (2203234)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.31/3.62  % (2203234)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.31/3.62  % (2203234)CaDiCaL version: 2.1.3
% 7.31/3.62  % (2203234)Termination reason: Refutation not found, incomplete strategy
% 7.31/3.62  % (2203234)Time elapsed: 1.390 s
% 7.31/3.62  % (2203234)Peak memory usage: 145 MB
% 7.31/3.62  % (2203234)Instructions burned: 2424 (million)
% 7.31/3.62  % (2203254)Instruction limit reached! 
% 7.31/3.62  % (2203254)------------------------------
% 7.31/3.62  % (2203254)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.31/3.62  % (2203254)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.31/3.62  % (2203254)CaDiCaL version: 2.1.3
% 7.31/3.62  % (2203254)Termination reason: Instruction limit
% 7.31/3.62  % (2203254)Termination phase: Saturation
% 7.31/3.62  % (2203254)Time elapsed: 0.302 s
% 7.31/3.62  % (2203254)Peak memory usage: 95 MB
% 7.31/3.62  % (2203254)Instructions burned: 317 (million)
% 7.31/3.62  % (2203234)------------------------------
% 7.31/3.62  % (2203234)------------------------------
% 7.31/3.62  % (2203258)lrs+10_32_sil=8000:tgt=ground:prc=on:sp=reverse_arity:spb=non_intro:random_seed=776121196:i=2836:kws=inv_precedence:fgj=on:bd=preordered:ins=10_2982 on theBenchmark for (2982ds/2836Mi)
% 7.31/3.62  % (2203259)lrs+11_1_ncem=casc2026/models/loop8.pt:sil=32000:npcc=on:lma=off:kmz=on:random_seed=3076901212:i=14534:kws=arity:fgj=on:bd=preordered:ins=6:ss=axioms:sgt=30_2981 on theBenchmark for (2981ds/14534Mi)
% 7.31/3.62  % (2203258)First to succeed.
% 7.31/3.62  % (2203258)Solution written to "/export/starexec/sandbox2/tmp/vampire-proof-2203227"
% 7.31/3.62  % (2203255)Refutation not found, incomplete strategy
% 7.31/3.62  % (2203255)------------------------------
% 7.31/3.62  % (2203255)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 7.31/3.62  % (2203255)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 7.31/3.62  % (2203255)CaDiCaL version: 2.1.3
% 7.31/3.62  % (2203255)Termination reason: Refutation not found, incomplete strategy
% 7.31/3.62  % (2203255)Time elapsed: 0.956 s
% 7.31/3.62  % (2203255)Peak memory usage: 128 MB
% 7.31/3.62  % (2203255)Instructions burned: 945 (million)
% 7.31/3.62  % SZS status Satisfiable for theBenchmark
% 7.31/3.62  % SZS output start Saturation.
% See solution above
% 0.23/3.90  % SZS output start Definitions and Model Updates.
% 0.23/3.90  for all inputs,
% 0.23/3.90      define ir(X0) := true
% 0.23/3.90  % SZS output end Definitions and Model Updates.
% 0.23/3.90  % (2203258)------------------------------
% 0.23/3.90  % (2203258)Version: Vampire 5.0.1 (Release build, commit ea8961452 on 2026-07-16 15:14:34 +0200)
% 0.23/3.90  % (2203258)Linked with Z3 4.14.0.0 3c47fd96cf5645d0c42b2c819d9e9a84380aa721 z3-4.8.4-9178-g3c47fd96c
% 0.23/3.90  % (2203258)CaDiCaL version: 2.1.3
% 0.23/3.90  % (2203258)Termination reason: Satisfiable
% 0.23/3.90  % (2203258)Time elapsed: 0.374 s
% 0.23/3.90  % (2203258)Peak memory usage: 105 MB
% 0.23/3.90  % (2203258)Instructions burned: 709 (million)
% 0.23/3.90  % (2203258)------------------------------
% 0.23/3.90  % (2203258)------------------------------
% 0.23/3.90  % (2203227)Success in time 2.611 s
% 0.23/3.90  % Vampire exiting
%------------------------------------------------------------------------------