↑ Up

Toma---0.7.SAT-Ass.s

View TPTP
Problem
Process solution in
SystemOnTSTP
Download .tgz
%------------------------------------------------------------------------------
% File     : Toma---0.7
% Problem  : SWB024-10 : TPTP v9.0.0. Released v7.3.0.
% Transfm  : none
% Format   : tptp:raw
% Command  : run_Leo-III %s %d THM

% Computer : n012.cluster.edu
% Model    : x86_64 x86_64
% CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory   : 8042.1875MB
% OS       : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit  : 300s
% DateTime : Tue Jul 15 08:00:42 AM UTC 2025

% Result   : Satisfiable 25.61s 25.24s
% Output   : Assurance 0s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.01/0.11  % Problem  : SWB024-10 : TPTP v9.0.0. Released v7.3.0.
% 0.01/0.11  % Command  : run_Leo-III %s %d THM
% 0.12/0.32  % Computer : n012.cluster.edu
% 0.12/0.32  % Model    : x86_64 x86_64
% 0.12/0.32  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.32  % Memory   : 8042.1875MB
% 0.12/0.32  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.12/0.32  % CPULimit : 300
% 0.12/0.32  % WCLimit  : 300
% 0.12/0.32  % DateTime : Mon Jul 14 19:27:19 EDT 2025
% 0.12/0.33  % CPUTime  : 
% 25.61/25.24  % SZS status Satisfiable
% 25.61/25.24  The following TRS is a complete presentation of the axioms, but the goal is not joinable.
% 25.61/25.24  1: ir(X) -> true
% 25.61/25.24  2: eq(X, X) -> true0
% 25.61/25.24  3: iext(uri_rdf_type, uri_rdf_first, uri_rdf_Property) -> true
% 25.61/25.24  4: iext(uri_rdf_type, uri_rdf_nil, uri_rdf_List) -> true
% 25.61/25.24  5: iext(uri_rdf_type, uri_rdf_rest, uri_rdf_Property) -> true
% 25.61/25.24  6: iext(uri_rdf_type, uri_rdf__1, uri_rdf_Property) -> true
% 25.61/25.24  7: iext(uri_rdf_type, uri_rdf__2, uri_rdf_Property) -> true
% 25.61/25.24  8: iext(uri_rdf_type, uri_rdf__3, uri_rdf_Property) -> true
% 25.61/25.24  9: iext(uri_rdf_type, uri_rdf_object, uri_rdf_Property) -> true
% 25.61/25.24  10: iext(uri_rdf_type, uri_rdf_value, uri_rdf_Property) -> true
% 25.61/25.24  11: iext(uri_rdf_type, uri_rdf_subject, uri_rdf_Property) -> true
% 25.61/25.24  12: iext(uri_rdf_type, uri_rdf_type, uri_rdf_Property) -> true
% 25.61/25.24  13: iext(uri_rdfs_domain, uri_rdfs_comment, uri_rdfs_Resource) -> true
% 25.61/25.24  14: iext(uri_rdfs_range, uri_rdfs_comment, uri_rdfs_Literal) -> true
% 25.61/25.24  15: iext(uri_rdfs_domain, uri_rdfs_isDefinedBy, uri_rdfs_Resource) -> true
% 25.61/25.24  16: iext(uri_rdfs_range, uri_rdfs_isDefinedBy, uri_rdfs_Resource) -> true
% 25.61/25.24  17: iext(uri_rdfs_subPropertyOf, uri_rdfs_isDefinedBy, uri_rdfs_seeAlso) -> true
% 25.61/25.24  18: iext(uri_rdfs_domain, uri_rdfs_label, uri_rdfs_Resource) -> true
% 25.61/25.24  19: iext(uri_rdfs_range, uri_rdfs_label, uri_rdfs_Literal) -> true
% 25.61/25.24  20: iext(uri_rdfs_domain, uri_rdfs_seeAlso, uri_rdfs_Resource) -> true
% 25.61/25.24  21: iext(uri_rdfs_range, uri_rdfs_seeAlso, uri_rdfs_Resource) -> true
% 25.61/25.24  22: iext(uri_rdfs_domain, uri_rdf_first, uri_rdf_List) -> true
% 25.61/25.24  23: iext(uri_rdfs_range, uri_rdf_first, uri_rdfs_Resource) -> true
% 25.61/25.24  24: iext(uri_rdfs_domain, uri_rdf_rest, uri_rdf_List) -> true
% 25.61/25.24  25: iext(uri_rdfs_range, uri_rdf_rest, uri_rdf_List) -> true
% 25.61/25.24  26: iext(uri_rdfs_subClassOf, uri_rdf_Alt, uri_rdfs_Container) -> true
% 25.61/25.24  27: iext(uri_rdfs_subClassOf, uri_rdf_Bag, uri_rdfs_Container) -> true
% 25.61/25.24  28: iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, uri_rdf_Property) -> true
% 25.61/25.24  29: iext(uri_rdfs_domain, uri_rdfs_member, uri_rdfs_Resource) -> true
% 25.61/25.24  30: iext(uri_rdfs_range, uri_rdfs_member, uri_rdfs_Resource) -> true
% 25.61/25.24  31: iext(uri_rdfs_domain, uri_rdf__1, uri_rdfs_Resource) -> true
% 25.61/25.24  32: iext(uri_rdfs_domain, uri_rdf__2, uri_rdfs_Resource) -> true
% 25.61/25.24  33: iext(uri_rdfs_domain, uri_rdf__3, uri_rdfs_Resource) -> true
% 25.61/25.24  34: iext(uri_rdfs_range, uri_rdf__1, uri_rdfs_Resource) -> true
% 25.61/25.24  35: iext(uri_rdfs_range, uri_rdf__2, uri_rdfs_Resource) -> true
% 25.61/25.24  36: iext(uri_rdfs_range, uri_rdf__3, uri_rdfs_Resource) -> true
% 25.61/25.24  37: iext(uri_rdf_type, uri_rdf__1, uri_rdfs_ContainerMembershipProperty) -> true
% 25.61/25.24  38: iext(uri_rdf_type, uri_rdf__2, uri_rdfs_ContainerMembershipProperty) -> true
% 25.61/25.24  39: iext(uri_rdf_type, uri_rdf__3, uri_rdfs_ContainerMembershipProperty) -> true
% 25.61/25.24  40: iext(uri_rdfs_subClassOf, uri_rdfs_Seq, uri_rdfs_Container) -> true
% 25.61/25.24  41: iext(uri_rdfs_subClassOf, uri_rdf_XMLLiteral, uri_rdfs_Literal) -> true
% 25.61/25.24  42: iext(uri_rdf_type, uri_rdf_XMLLiteral, uri_rdfs_Datatype) -> true
% 25.61/25.24  43: iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, uri_rdfs_Class) -> true
% 25.61/25.24  44: iext(uri_rdfs_domain, uri_rdfs_domain, uri_rdf_Property) -> true
% 25.61/25.24  45: iext(uri_rdfs_range, uri_rdfs_domain, uri_rdfs_Class) -> true
% 25.61/25.24  46: iext(uri_rdf_type, uri_rdf_Property, uri_rdfs_Class) -> true
% 25.61/25.24  47: iext(uri_rdfs_domain, uri_rdfs_range, uri_rdf_Property) -> true
% 25.61/25.24  48: iext(uri_rdfs_range, uri_rdfs_range, uri_rdfs_Class) -> true
% 25.61/25.24  49: iext(uri_rdfs_domain, uri_rdf_object, uri_rdfs_Statement) -> true
% 25.61/25.24  50: iext(uri_rdfs_range, uri_rdf_predicate, uri_rdfs_Resource) -> true
% 25.61/25.24  51: iext(uri_rdfs_domain, uri_rdf_predicate, uri_rdfs_Statement) -> true
% 25.61/25.24  52: iext(uri_rdfs_domain, uri_rdf_subject, uri_rdfs_Statement) -> true
% 25.61/25.24  53: iext(uri_rdfs_range, uri_rdf_subject, uri_rdfs_Resource) -> true
% 25.61/25.24  54: iext(uri_rdfs_domain, uri_rdfs_subClassOf, uri_rdfs_Class) -> true
% 25.61/25.24  55: iext(uri_rdfs_range, uri_rdfs_subClassOf, uri_rdfs_Class) -> true
% 25.61/25.24  56: iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, uri_rdf_Property) -> true
% 25.61/25.24  57: iext(uri_rdfs_range, uri_rdfs_subPropertyOf, uri_rdf_Property) -> true
% 25.61/25.24  58: iext(uri_rdfs_domain, uri_rdf_type, uri_rdfs_Resource) -> true
% 25.61/25.24  59: iext(uri_rdfs_range, uri_rdf_type, uri_rdfs_Class) -> true
% 25.61/25.24  60: iext(uri_rdfs_domain, uri_rdf_value, uri_rdfs_Resource) -> true
% 25.61/25.24  61: iext(uri_rdfs_range, uri_rdf_value, uri_rdfs_Resource) -> true
% 25.61/25.24  62: iext(uri_owl_onProperty, sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z, uri_ex_hasAncestor) -> true
% 25.61/25.24  63: iext(uri_rdf_type, sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z, uri_owl_Restriction) -> true
% 25.61/25.24  64: iext(uri_rdf_type, uri_ex_bob, uri_ex_Person) -> true
% 25.61/25.24  65: iext(uri_rdf_type, uri_ex_alice, uri_ex_Person) -> true
% 25.61/25.24  66: iext(uri_rdf_type, uri_ex_hasAncestor, uri_owl_TransitiveProperty) -> true
% 25.61/25.24  67: iext(uri_ex_hasAncestor, uri_ex_alice, uri_ex_bob) -> true
% 25.61/25.24  68: iext(uri_rdfs_subClassOf, uri_ex_Person, sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z) -> true
% 25.61/25.24  69: ifeq(X, X, Y, Z) -> Y
% 25.61/25.24  70: iext(uri_owl_minCardinality, sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z, literal_typed(dat_str_1, uri_xsd_nonNegativeInteger)) -> true
% 25.61/25.24  72: ifeq(lv(X), true, true, true) -> true
% 25.61/25.24  74: ifeq(icext(uri_rdfs_Resource, X), true, true, true) -> true
% 25.61/25.24  75: ifeq(icext(uri_rdfs_Class, X), true, ic(X), true) -> true
% 25.61/25.24  77: icext(uri_rdfs_Resource, X) -> true
% 25.61/25.24  78: ifeq(icext(uri_rdfs_Literal, X), true, lv(X), true) -> true
% 25.61/25.24  79: ifeq(ic(X), true, icext(uri_rdfs_Class, X), true) -> true
% 25.61/25.24  80: ifeq(lv(X), true, icext(uri_rdfs_Literal, X), true) -> true
% 25.61/25.24  81: ifeq(iext(X, Y, Z), true, ip(X), true) -> true
% 25.61/25.24  82: ip(uri_ex_hasAncestor) -> true
% 25.61/25.24  83: true -> ip(uri_owl_minCardinality)
% 25.61/25.24  84: ip(uri_owl_onProperty) -> ip(uri_owl_minCardinality)
% 25.61/25.24  85: ip(uri_rdf_type) -> ip(uri_owl_minCardinality)
% 25.61/25.24  86: ip(uri_rdfs_domain) -> ip(uri_owl_minCardinality)
% 25.61/25.24  87: ip(uri_rdfs_range) -> ip(uri_owl_minCardinality)
% 25.61/25.24  88: ip(uri_rdfs_subClassOf) -> ip(uri_owl_minCardinality)
% 25.61/25.24  89: ip(uri_rdfs_subPropertyOf) -> ip(uri_owl_minCardinality)
% 25.61/25.24  91: ifeq(iext(uri_rdfs_subClassOf, X, Y), ip(uri_owl_minCardinality), ic(X), ip(uri_owl_minCardinality)) -> ip(uri_owl_minCardinality)
% 25.61/25.24  92: ic(uri_ex_Person) -> ip(uri_owl_minCardinality)
% 25.61/25.24  93: ic(uri_rdf_Alt) -> ip(uri_owl_minCardinality)
% 25.61/25.24  94: ic(uri_rdf_Bag) -> ip(uri_owl_minCardinality)
% 25.61/25.24  95: ic(uri_rdf_XMLLiteral) -> ip(uri_owl_minCardinality)
% 25.61/25.24  96: ic(uri_rdfs_ContainerMembershipProperty) -> ip(uri_owl_minCardinality)
% 25.61/25.24  97: ic(uri_rdfs_Datatype) -> ip(uri_owl_minCardinality)
% 25.61/25.24  98: ic(uri_rdfs_Seq) -> ip(uri_owl_minCardinality)
% 25.61/25.24  99: icext(uri_rdfs_Class, uri_rdfs_Seq) -> ip(uri_owl_minCardinality)
% 25.61/25.24  100: icext(uri_rdfs_Class, uri_rdfs_Datatype) -> ip(uri_owl_minCardinality)
% 25.61/25.24  101: icext(uri_rdfs_Class, uri_rdf_Alt) -> ip(uri_owl_minCardinality)
% 25.61/25.24  102: icext(uri_rdfs_Class, uri_rdfs_ContainerMembershipProperty) -> ip(uri_owl_minCardinality)
% 25.61/25.24  103: icext(uri_rdfs_Class, uri_rdf_Bag) -> ip(uri_owl_minCardinality)
% 25.61/25.24  104: icext(uri_rdfs_Class, uri_rdf_XMLLiteral) -> ip(uri_owl_minCardinality)
% 25.61/25.24  105: icext(uri_rdfs_Class, uri_ex_Person) -> ip(uri_owl_minCardinality)
% 25.61/25.24  107: ifeq(iext(uri_rdfs_subPropertyOf, X, Y), ip(uri_owl_minCardinality), ip(X), ip(uri_owl_minCardinality)) -> ip(uri_owl_minCardinality)
% 25.61/25.24  108: ip(uri_rdfs_isDefinedBy) -> ip(uri_owl_minCardinality)
% 25.61/25.24  110: ifeq(ip(X), ip(uri_owl_minCardinality), iext(uri_rdfs_subPropertyOf, X, X), ip(uri_owl_minCardinality)) -> ip(uri_owl_minCardinality)
% 25.61/25.24  111: iext(uri_rdfs_subPropertyOf, uri_owl_minCardinality, uri_owl_minCardinality) -> ip(uri_owl_minCardinality)
% 25.61/25.24  112: iext(uri_rdfs_subPropertyOf, uri_ex_hasAncestor, uri_ex_hasAncestor) -> ip(uri_owl_minCardinality)
% 25.61/25.24  113: iext(uri_rdfs_subPropertyOf, uri_owl_onProperty, uri_owl_onProperty) -> ip(uri_owl_minCardinality)
% 25.61/25.24  114: iext(uri_rdfs_subPropertyOf, uri_rdf_type, uri_rdf_type) -> ip(uri_owl_minCardinality)
% 25.61/25.24  115: iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, uri_rdfs_domain) -> ip(uri_owl_minCardinality)
% 25.61/25.24  116: iext(uri_rdfs_subPropertyOf, uri_rdfs_isDefinedBy, uri_rdfs_isDefinedBy) -> ip(uri_owl_minCardinality)
% 25.61/25.24  117: iext(uri_rdfs_subPropertyOf, uri_rdfs_range, uri_rdfs_range) -> ip(uri_owl_minCardinality)
% 25.61/25.24  118: iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, uri_rdfs_subClassOf) -> ip(uri_owl_minCardinality)
% 25.61/25.24  119: iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf) -> ip(uri_owl_minCardinality)
% 25.61/25.24  121: ifeq(iext(uri_rdfs_subClassOf, X, Y), ip(uri_owl_minCardinality), ic(Y), ip(uri_owl_minCardinality)) -> ip(uri_owl_minCardinality)
% 25.61/25.24  122: ip(uri_owl_minCardinality) -> ic(sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z)
% 25.61/25.24  123: ic(sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z) -> ic(uri_rdfs_Container)
% 25.61/25.24  124: ic(uri_rdfs_Literal) -> ic(uri_rdfs_Container)
% 25.61/25.24  125: ic(uri_rdf_Property) -> ic(uri_rdfs_Container)
% 25.61/25.24  126: ic(uri_rdfs_Class) -> ic(uri_rdfs_Container)
% 25.61/25.24  127: icext(uri_rdfs_Class, uri_rdfs_Class) -> ic(uri_rdfs_Container)
% 25.61/25.24  128: icext(uri_rdfs_Class, uri_rdfs_Literal) -> ic(uri_rdfs_Container)
% 25.61/25.24  129: icext(uri_rdfs_Class, uri_rdf_Property) -> ic(uri_rdfs_Container)
% 25.61/25.24  130: icext(uri_rdfs_Class, sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z) -> ic(uri_rdfs_Container)
% 25.61/25.24  132: ifeq(ic(X), ic(uri_rdfs_Container), iext(uri_rdfs_subClassOf, X, X), ic(uri_rdfs_Container)) -> ic(uri_rdfs_Container)
% 25.61/25.24  133: iext(uri_rdfs_subClassOf, uri_rdfs_Container, uri_rdfs_Container) -> ic(uri_rdfs_Container)
% 25.61/25.24  134: iext(uri_rdfs_subClassOf, sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z, sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z) -> ic(uri_rdfs_Container)
% 25.61/25.24  135: iext(uri_rdfs_subClassOf, uri_ex_Person, uri_ex_Person) -> ic(uri_rdfs_Container)
% 25.61/25.24  136: iext(uri_rdfs_subClassOf, uri_rdf_Alt, uri_rdf_Alt) -> ic(uri_rdfs_Container)
% 25.61/25.24  137: iext(uri_rdfs_subClassOf, uri_rdf_Bag, uri_rdf_Bag) -> ic(uri_rdfs_Container)
% 25.61/25.24  138: iext(uri_rdfs_subClassOf, uri_rdf_Property, uri_rdf_Property) -> ic(uri_rdfs_Container)
% 25.61/25.24  139: iext(uri_rdfs_subClassOf, uri_rdf_XMLLiteral, uri_rdf_XMLLiteral) -> ic(uri_rdfs_Container)
% 25.61/25.24  140: iext(uri_rdfs_subClassOf, uri_rdfs_Class, uri_rdfs_Class) -> ic(uri_rdfs_Container)
% 25.61/25.24  141: iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, uri_rdfs_ContainerMembershipProperty) -> ic(uri_rdfs_Container)
% 25.61/25.24  142: iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, uri_rdfs_Datatype) -> ic(uri_rdfs_Container)
% 25.61/25.24  143: iext(uri_rdfs_subClassOf, uri_rdfs_Literal, uri_rdfs_Literal) -> ic(uri_rdfs_Container)
% 25.61/25.24  144: iext(uri_rdfs_subClassOf, uri_rdfs_Seq, uri_rdfs_Seq) -> ic(uri_rdfs_Container)
% 25.61/25.24  146: ifeq(iext(uri_rdfs_subPropertyOf, X, Y), ic(uri_rdfs_Container), ip(Y), ic(uri_rdfs_Container)) -> ic(uri_rdfs_Container)
% 25.61/25.24  147: ip(uri_rdfs_seeAlso) -> ic(uri_rdfs_Container)
% 25.61/25.24  148: iext(uri_rdfs_subPropertyOf, uri_rdfs_seeAlso, uri_rdfs_seeAlso) -> ic(uri_rdfs_Container)
% 25.61/25.24  150: ifeq(ic(X), ic(uri_rdfs_Container), iext(uri_rdfs_subClassOf, X, uri_rdfs_Resource), ic(uri_rdfs_Container)) -> ic(uri_rdfs_Container)
% 25.61/25.24  151: iext(uri_rdfs_subClassOf, uri_rdfs_Container, uri_rdfs_Resource) -> ic(uri_rdfs_Container)
% 25.61/25.24  152: ic(uri_rdfs_Resource) -> ic(uri_rdfs_Container)
% 25.61/25.24  153: icext(uri_rdfs_Class, uri_rdfs_Resource) -> ic(uri_rdfs_Container)
% 25.61/25.24  154: iext(uri_rdfs_subClassOf, sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z, uri_rdfs_Resource) -> ic(uri_rdfs_Container)
% 25.61/25.24  155: iext(uri_rdfs_subClassOf, uri_ex_Person, uri_rdfs_Resource) -> ic(uri_rdfs_Container)
% 25.61/25.24  156: iext(uri_rdfs_subClassOf, uri_rdf_Alt, uri_rdfs_Resource) -> ic(uri_rdfs_Container)
% 25.61/25.24  157: iext(uri_rdfs_subClassOf, uri_rdf_Bag, uri_rdfs_Resource) -> ic(uri_rdfs_Container)
% 25.61/25.24  158: iext(uri_rdfs_subClassOf, uri_rdf_Property, uri_rdfs_Resource) -> ic(uri_rdfs_Container)
% 25.61/25.24  159: iext(uri_rdfs_subClassOf, uri_rdf_XMLLiteral, uri_rdfs_Resource) -> ic(uri_rdfs_Container)
% 25.61/25.24  160: iext(uri_rdfs_subClassOf, uri_rdfs_Class, uri_rdfs_Resource) -> ic(uri_rdfs_Container)
% 25.61/25.24  161: iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, uri_rdfs_Resource) -> ic(uri_rdfs_Container)
% 25.61/25.24  162: iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, uri_rdfs_Resource) -> ic(uri_rdfs_Container)
% 25.61/25.24  163: iext(uri_rdfs_subClassOf, uri_rdfs_Literal, uri_rdfs_Resource) -> ic(uri_rdfs_Container)
% 25.61/25.24  164: iext(uri_rdfs_subClassOf, uri_rdfs_Seq, uri_rdfs_Resource) -> ic(uri_rdfs_Container)
% 25.61/25.24  165: iext(uri_rdfs_subClassOf, uri_rdfs_Resource, uri_rdfs_Resource) -> ic(uri_rdfs_Container)
% 25.61/25.24  167: ifeq(ip(X), ic(uri_rdfs_Container), iext(uri_rdf_type, X, uri_rdf_Property), ic(uri_rdfs_Container)) -> ic(uri_rdfs_Container)
% 25.61/25.24  168: iext(uri_rdf_type, uri_ex_hasAncestor, uri_rdf_Property) -> ic(uri_rdfs_Container)
% 25.61/25.24  169: iext(uri_rdf_type, uri_owl_minCardinality, uri_rdf_Property) -> ic(uri_rdfs_Container)
% 25.61/25.24  170: iext(uri_rdf_type, uri_owl_onProperty, uri_rdf_Property) -> ic(uri_rdfs_Container)
% 25.61/25.24  171: iext(uri_rdf_type, uri_rdfs_domain, uri_rdf_Property) -> ic(uri_rdfs_Container)
% 25.61/25.24  172: iext(uri_rdf_type, uri_rdfs_isDefinedBy, uri_rdf_Property) -> ic(uri_rdfs_Container)
% 25.61/25.24  173: iext(uri_rdf_type, uri_rdfs_range, uri_rdf_Property) -> ic(uri_rdfs_Container)
% 25.61/25.24  174: iext(uri_rdf_type, uri_rdfs_seeAlso, uri_rdf_Property) -> ic(uri_rdfs_Container)
% 25.61/25.24  175: iext(uri_rdf_type, uri_rdfs_subClassOf, uri_rdf_Property) -> ic(uri_rdfs_Container)
% 25.61/25.24  176: iext(uri_rdf_type, uri_rdfs_subPropertyOf, uri_rdf_Property) -> ic(uri_rdfs_Container)
% 25.61/25.24  178: ifeq(iext(uri_rdf_type, X, uri_rdf_Property), ic(uri_rdfs_Container), ip(X), ic(uri_rdfs_Container)) -> ic(uri_rdfs_Container)
% 25.61/25.24  179: ip(uri_rdf__1) -> ic(uri_rdfs_Container)
% 25.61/25.24  180: ip(uri_rdf__2) -> ic(uri_rdfs_Container)
% 25.61/25.24  181: ip(uri_rdf__3) -> ic(uri_rdfs_Container)
% 25.61/25.24  182: ip(uri_rdf_first) -> ic(uri_rdfs_Container)
% 25.61/25.24  183: ip(uri_rdf_object) -> ic(uri_rdfs_Container)
% 25.61/25.24  184: ip(uri_rdf_rest) -> ic(uri_rdfs_Container)
% 25.61/25.24  185: ip(uri_rdf_subject) -> ic(uri_rdfs_Container)
% 25.61/25.24  186: ip(uri_rdf_value) -> ic(uri_rdfs_Container)
% 25.61/25.24  187: iext(uri_rdfs_subPropertyOf, uri_rdf_value, uri_rdf_value) -> ic(uri_rdfs_Container)
% 25.61/25.24  188: iext(uri_rdfs_subPropertyOf, uri_rdf_subject, uri_rdf_subject) -> ic(uri_rdfs_Container)
% 25.61/25.24  189: iext(uri_rdfs_subPropertyOf, uri_rdf_first, uri_rdf_first) -> ic(uri_rdfs_Container)
% 25.61/25.24  190: iext(uri_rdfs_subPropertyOf, uri_rdf_object, uri_rdf_object) -> ic(uri_rdfs_Container)
% 25.61/25.24  191: iext(uri_rdfs_subPropertyOf, uri_rdf__3, uri_rdf__3) -> ic(uri_rdfs_Container)
% 25.61/25.24  192: iext(uri_rdfs_subPropertyOf, uri_rdf_rest, uri_rdf_rest) -> ic(uri_rdfs_Container)
% 25.61/25.24  193: iext(uri_rdfs_subPropertyOf, uri_rdf__1, uri_rdf__1) -> ic(uri_rdfs_Container)
% 25.61/25.24  194: iext(uri_rdfs_subPropertyOf, uri_rdf__2, uri_rdf__2) -> ic(uri_rdfs_Container)
% 25.61/25.24  195: ifeq(iext(uri_ex_hasAncestor, X, Y), ic(uri_rdfs_Container), ic(uri_rdfs_Container), ic(uri_rdfs_Container)) -> ic(uri_rdfs_Container)
% 25.61/25.24  197: ifeq(icext(X, Y), ic(uri_rdfs_Container), iext(uri_rdf_type, Y, X), ic(uri_rdfs_Container)) -> ic(uri_rdfs_Container)
% 25.61/25.24  198: iext(uri_rdf_type, X, uri_rdfs_Resource) -> ic(uri_rdfs_Container)
% 25.61/25.24  199: iext(uri_rdf_type, sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z, uri_rdfs_Class) -> ic(uri_rdfs_Container)
% 25.61/25.24  200: iext(uri_rdf_type, uri_ex_Person, uri_rdfs_Class) -> ic(uri_rdfs_Container)
% 25.61/25.24  201: iext(uri_rdf_type, uri_rdf_Bag, uri_rdfs_Class) -> ic(uri_rdfs_Container)
% 25.61/25.24  202: iext(uri_rdf_type, uri_rdf_Alt, uri_rdfs_Class) -> ic(uri_rdfs_Container)
% 25.61/25.24  203: iext(uri_rdf_type, uri_rdf_XMLLiteral, uri_rdfs_Class) -> ic(uri_rdfs_Container)
% 25.61/25.24  204: iext(uri_rdf_type, uri_rdfs_Datatype, uri_rdfs_Class) -> ic(uri_rdfs_Container)
% 25.61/25.24  205: iext(uri_rdf_type, uri_rdfs_Class, uri_rdfs_Class) -> ic(uri_rdfs_Container)
% 25.61/25.24  206: iext(uri_rdf_type, uri_rdfs_ContainerMembershipProperty, uri_rdfs_Class) -> ic(uri_rdfs_Container)
% 25.61/25.24  207: iext(uri_rdf_type, uri_rdfs_Literal, uri_rdfs_Class) -> ic(uri_rdfs_Container)
% 25.61/25.24  208: iext(uri_rdf_type, uri_rdfs_Seq, uri_rdfs_Class) -> ic(uri_rdfs_Container)
% 25.61/25.24  209: iext(uri_rdf_type, uri_rdfs_Resource, uri_rdfs_Class) -> ic(uri_rdfs_Container)
% 25.61/25.24  211: ifeq(iext(uri_rdf_type, X, Y), ic(uri_rdfs_Container), icext(Y, X), ic(uri_rdfs_Container)) -> ic(uri_rdfs_Container)
% 25.61/25.24  212: icext(uri_owl_Restriction, sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z) -> ic(uri_rdfs_Container)
% 25.61/25.24  213: icext(uri_ex_Person, uri_ex_alice) -> ic(uri_rdfs_Container)
% 25.61/25.24  214: icext(uri_ex_Person, uri_ex_bob) -> ic(uri_rdfs_Container)
% 25.61/25.24  215: icext(uri_owl_TransitiveProperty, uri_ex_hasAncestor) -> ic(uri_rdfs_Container)
% 25.61/25.24  216: icext(uri_rdfs_Datatype, uri_rdf_XMLLiteral) -> ic(uri_rdfs_Container)
% 25.61/25.24  217: icext(uri_rdf_Property, uri_rdf__1) -> ic(uri_rdfs_Container)
% 25.61/25.24  218: icext(uri_rdfs_ContainerMembershipProperty, uri_rdf__1) -> ic(uri_rdfs_Container)
% 25.61/25.24  219: icext(uri_rdf_Property, uri_rdf__2) -> ic(uri_rdfs_Container)
% 25.61/25.24  220: icext(uri_rdfs_ContainerMembershipProperty, uri_rdf__2) -> ic(uri_rdfs_Container)
% 25.61/25.24  221: icext(uri_rdf_Property, uri_rdf__3) -> ic(uri_rdfs_Container)
% 25.61/25.24  222: icext(uri_rdfs_ContainerMembershipProperty, uri_rdf__3) -> ic(uri_rdfs_Container)
% 25.61/25.24  223: icext(uri_rdf_Property, uri_rdf_first) -> ic(uri_rdfs_Container)
% 25.61/25.24  224: icext(uri_rdf_List, uri_rdf_nil) -> ic(uri_rdfs_Container)
% 25.61/25.24  225: icext(uri_rdf_Property, uri_rdf_object) -> ic(uri_rdfs_Container)
% 25.61/25.24  226: icext(uri_rdf_Property, uri_rdf_rest) -> ic(uri_rdfs_Container)
% 25.61/25.24  227: icext(uri_rdf_Property, uri_rdf_subject) -> ic(uri_rdfs_Container)
% 25.61/25.24  228: icext(uri_rdf_Property, uri_rdf_type) -> ic(uri_rdfs_Container)
% 25.61/25.24  229: icext(uri_rdf_Property, uri_rdf_value) -> ic(uri_rdfs_Container)
% 25.61/25.24  230: icext(uri_rdf_Property, uri_owl_minCardinality) -> ic(uri_rdfs_Container)
% 25.61/25.24  231: icext(uri_rdf_Property, uri_rdfs_domain) -> ic(uri_rdfs_Container)
% 25.61/25.24  232: icext(uri_rdf_Property, uri_rdfs_isDefinedBy) -> ic(uri_rdfs_Container)
% 25.61/25.24  233: icext(uri_rdf_Property, uri_rdfs_range) -> ic(uri_rdfs_Container)
% 25.61/25.24  234: icext(uri_rdf_Property, uri_rdfs_seeAlso) -> ic(uri_rdfs_Container)
% 25.61/25.24  235: icext(uri_rdf_Property, uri_rdfs_subClassOf) -> ic(uri_rdfs_Container)
% 25.61/25.24  236: icext(uri_rdf_Property, uri_rdfs_subPropertyOf) -> ic(uri_rdfs_Container)
% 25.61/25.24  237: icext(uri_rdf_Property, uri_owl_onProperty) -> ic(uri_rdfs_Container)
% 25.61/25.24  238: icext(uri_rdf_Property, uri_ex_hasAncestor) -> ic(uri_rdfs_Container)
% 25.61/25.24  240: ifeq(icext(uri_rdfs_Datatype, X), ic(uri_rdfs_Container), iext(uri_rdfs_subClassOf, X, uri_rdfs_Literal), ic(uri_rdfs_Container)) -> ic(uri_rdfs_Container)
% 25.61/25.24  242: ifeq(icext(uri_rdfs_ContainerMembershipProperty, X), ic(uri_rdfs_Container), iext(uri_rdfs_subPropertyOf, X, uri_rdfs_member), ic(uri_rdfs_Container)) -> ic(uri_rdfs_Container)
% 25.61/25.24  243: iext(uri_rdfs_subPropertyOf, uri_rdf__1, uri_rdfs_member) -> ic(uri_rdfs_Container)
% 25.61/25.24  244: ip(uri_rdfs_member) -> ic(uri_rdfs_Container)
% 25.61/25.24  245: iext(uri_rdfs_subPropertyOf, uri_rdf__2, uri_rdfs_member) -> ic(uri_rdfs_Container)
% 25.61/25.24  246: iext(uri_rdfs_subPropertyOf, uri_rdf__3, uri_rdfs_member) -> ic(uri_rdfs_Container)
% 25.61/25.24  247: iext(uri_rdfs_subPropertyOf, uri_rdfs_member, uri_rdfs_member) -> ic(uri_rdfs_Container)
% 25.61/25.24  248: iext(uri_rdf_type, uri_rdfs_member, uri_rdf_Property) -> ic(uri_rdfs_Container)
% 25.61/25.24  249: icext(uri_rdf_Property, uri_rdfs_member) -> ic(uri_rdfs_Container)
% 25.61/25.24  250: ifeq(lv(X), ic(uri_rdfs_Container), ic(uri_rdfs_Container), ic(uri_rdfs_Container)) -> ic(uri_rdfs_Container)
% 25.61/25.24  251: ifeq(ic(X), ic(uri_rdfs_Container), icext(uri_rdfs_Class, X), ic(uri_rdfs_Container)) -> ic(uri_rdfs_Container)
% 25.61/25.24  252: icext(uri_rdfs_Class, uri_rdfs_Container) -> ic(uri_rdfs_Container)
% 25.61/25.24  253: iext(uri_rdf_type, uri_rdfs_Container, uri_rdfs_Class) -> ic(uri_rdfs_Container)
% 25.61/25.24  254: ifeq(lv(X), ic(uri_rdfs_Container), icext(uri_rdfs_Literal, X), ic(uri_rdfs_Container)) -> ic(uri_rdfs_Container)
% 25.61/25.24  255: ifeq(icext(uri_rdfs_Literal, X), ic(uri_rdfs_Container), lv(X), ic(uri_rdfs_Container)) -> ic(uri_rdfs_Container)
% 25.61/25.24  256: ifeq(icext(uri_rdfs_Class, X), ic(uri_rdfs_Container), ic(X), ic(uri_rdfs_Container)) -> ic(uri_rdfs_Container)
% 25.61/25.24  257: ifeq(iext(X, Y, Z), ic(uri_rdfs_Container), ip(X), ic(uri_rdfs_Container)) -> ic(uri_rdfs_Container)
% 25.61/25.24  258: ifeq(iext(uri_rdfs_subPropertyOf, X, Y), ic(uri_rdfs_Container), ip(X), ic(uri_rdfs_Container)) -> ic(uri_rdfs_Container)
% 25.61/25.24  259: ifeq(icext(uri_rdfs_Datatype, uri_rdfs_Literal), ic(uri_rdfs_Container), ic(uri_rdfs_Container), ic(uri_rdfs_Container)) -> ic(uri_rdfs_Container)
% 25.61/25.24  260: ifeq(iext(uri_rdfs_subClassOf, X, Y), ic(uri_rdfs_Container), ic(Y), ic(uri_rdfs_Container)) -> ic(uri_rdfs_Container)
% 25.61/25.24  261: ifeq(iext(uri_rdfs_subClassOf, X, Y), ic(uri_rdfs_Container), ic(X), ic(uri_rdfs_Container)) -> ic(uri_rdfs_Container)
% 25.61/25.24  262: ifeq(ip(X), ic(uri_rdfs_Container), iext(uri_rdfs_subPropertyOf, X, X), ic(uri_rdfs_Container)) -> ic(uri_rdfs_Container)
% 25.61/25.24  263: ifeq(iext(uri_rdf_subject, X, Y), ic(uri_rdfs_Container), ic(uri_rdfs_Container), ic(uri_rdfs_Container)) -> ic(uri_rdfs_Container)
% 25.61/25.24  264: ifeq(iext(uri_owl_minCardinality, X, Y), ic(uri_rdfs_Container), ic(uri_rdfs_Container), ic(uri_rdfs_Container)) -> ic(uri_rdfs_Container)
% 25.61/25.24  265: ifeq(iext(uri_rdfs_seeAlso, X, Y), ic(uri_rdfs_Container), ic(uri_rdfs_Container), ic(uri_rdfs_Container)) -> ic(uri_rdfs_Container)
% 25.61/25.24  266: ifeq(iext(uri_rdfs_subClassOf, X, Y), ic(uri_rdfs_Container), ic(uri_rdfs_Container), ic(uri_rdfs_Container)) -> ic(uri_rdfs_Container)
% 25.61/25.24  267: ifeq(iext(uri_rdfs_subPropertyOf, X, Y), ic(uri_rdfs_Container), ic(uri_rdfs_Container), ic(uri_rdfs_Container)) -> ic(uri_rdfs_Container)
% 25.61/25.24  268: ifeq(iext(uri_owl_onProperty, X, Y), ic(uri_rdfs_Container), ic(uri_rdfs_Container), ic(uri_rdfs_Container)) -> ic(uri_rdfs_Container)
% 25.61/25.24  269: ifeq(iext(uri_rdfs_isDefinedBy, X, Y), ic(uri_rdfs_Container), ic(uri_rdfs_Container), ic(uri_rdfs_Container)) -> ic(uri_rdfs_Container)
% 25.61/25.24  270: ifeq(iext(uri_rdfs_range, X, Y), ic(uri_rdfs_Container), ic(uri_rdfs_Container), ic(uri_rdfs_Container)) -> ic(uri_rdfs_Container)
% 25.61/25.24  271: ifeq(iext(uri_rdfs_domain, X, Y), ic(uri_rdfs_Container), ic(uri_rdfs_Container), ic(uri_rdfs_Container)) -> ic(uri_rdfs_Container)
% 25.61/25.24  272: ifeq(iext(uri_rdf_type, X, Y), ic(uri_rdfs_Container), ic(uri_rdfs_Container), ic(uri_rdfs_Container)) -> ic(uri_rdfs_Container)
% 25.61/25.24  273: ifeq(iext(uri_rdf_object, X, Y), ic(uri_rdfs_Container), ic(uri_rdfs_Container), ic(uri_rdfs_Container)) -> ic(uri_rdfs_Container)
% 25.61/25.24  274: ifeq(iext(uri_rdf_value, X, Y), ic(uri_rdfs_Container), ic(uri_rdfs_Container), ic(uri_rdfs_Container)) -> ic(uri_rdfs_Container)
% 25.61/25.24  275: ifeq(iext(uri_rdf__2, X, Y), ic(uri_rdfs_Container), ic(uri_rdfs_Container), ic(uri_rdfs_Container)) -> ic(uri_rdfs_Container)
% 25.61/25.24  276: ifeq(iext(uri_rdf_rest, X, Y), ic(uri_rdfs_Container), ic(uri_rdfs_Container), ic(uri_rdfs_Container)) -> ic(uri_rdfs_Container)
% 25.61/25.24  277: ifeq(iext(uri_rdf_first, X, Y), ic(uri_rdfs_Container), ic(uri_rdfs_Container), ic(uri_rdfs_Container)) -> ic(uri_rdfs_Container)
% 25.61/25.24  278: ifeq(iext(uri_rdf__3, X, Y), ic(uri_rdfs_Container), ic(uri_rdfs_Container), ic(uri_rdfs_Container)) -> ic(uri_rdfs_Container)
% 25.61/25.24  279: ifeq(iext(uri_rdf__1, X, Y), ic(uri_rdfs_Container), ic(uri_rdfs_Container), ic(uri_rdfs_Container)) -> ic(uri_rdfs_Container)
% 25.61/25.24  281: eq(tuple(iext(uri_ex_hasAncestor, uri_ex_alice, X), iext(uri_ex_hasAncestor, uri_ex_bob, X)), tuple(ic(uri_rdfs_Container), ic(uri_rdfs_Container))) -> false
% 25.61/25.24  282: ifeq(icext(uri_rdfs_ContainerMembershipProperty, uri_rdfs_member), ic(uri_rdfs_Container), ic(uri_rdfs_Container), ic(uri_rdfs_Container)) -> ic(uri_rdfs_Container)
% 25.61/25.24  283: ifeq(iext(uri_rdfs_member, X, Y), ic(uri_rdfs_Container), ic(uri_rdfs_Container), ic(uri_rdfs_Container)) -> ic(uri_rdfs_Container)
% 25.61/25.24  284: eq(tuple(ic(uri_rdfs_Container), iext(uri_ex_hasAncestor, uri_ex_bob, uri_ex_bob)), tuple(ic(uri_rdfs_Container), ic(uri_rdfs_Container))) -> false
% 25.61/25.24  286: ifeq(icext(X, Y), ic(uri_rdfs_Container), ifeq(iext(uri_rdfs_subClassOf, X, Z), ic(uri_rdfs_Container), icext(Z, Y), ic(uri_rdfs_Container)), ic(uri_rdfs_Container)) -> ic(uri_rdfs_Container)
% 25.61/25.24  287: ifeq(icext(X, Y), ic(uri_rdfs_Container), ic(uri_rdfs_Container), ic(uri_rdfs_Container)) -> ic(uri_rdfs_Container)
% 25.61/25.24  288: ifeq(icext(uri_rdf_XMLLiteral, X), ic(uri_rdfs_Container), icext(uri_rdfs_Literal, X), ic(uri_rdfs_Container)) -> ic(uri_rdfs_Container)
% 25.61/25.24  289: ifeq(icext(uri_rdfs_Seq, X), ic(uri_rdfs_Container), icext(uri_rdfs_Container, X), ic(uri_rdfs_Container)) -> ic(uri_rdfs_Container)
% 25.61/25.24  290: ifeq(icext(uri_ex_Person, X), ic(uri_rdfs_Container), icext(sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z, X), ic(uri_rdfs_Container)) -> ic(uri_rdfs_Container)
% 25.61/25.24  291: icext(sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z, uri_ex_alice) -> ic(uri_rdfs_Container)
% 25.61/25.24  292: icext(sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z, uri_ex_bob) -> ic(uri_rdfs_Container)
% 25.61/25.24  293: iext(uri_rdf_type, uri_ex_bob, sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z) -> ic(uri_rdfs_Container)
% 25.61/25.24  294: iext(uri_rdf_type, uri_ex_alice, sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z) -> ic(uri_rdfs_Container)
% 25.61/25.24  295: ifeq(icext(uri_rdf_Alt, X), ic(uri_rdfs_Container), icext(uri_rdfs_Container, X), ic(uri_rdfs_Container)) -> ic(uri_rdfs_Container)
% 25.61/25.24  296: ifeq(icext(uri_rdf_Bag, X), ic(uri_rdfs_Container), icext(uri_rdfs_Container, X), ic(uri_rdfs_Container)) -> ic(uri_rdfs_Container)
% 25.61/25.24  297: ifeq(icext(uri_rdfs_Datatype, X), ic(uri_rdfs_Container), icext(uri_rdfs_Class, X), ic(uri_rdfs_Container)) -> ic(uri_rdfs_Container)
% 25.61/25.24  298: ifeq(icext(uri_rdfs_ContainerMembershipProperty, X), ic(uri_rdfs_Container), icext(uri_rdf_Property, X), ic(uri_rdfs_Container)) -> ic(uri_rdfs_Container)
% 25.61/25.24  299: ifeq(icext(uri_rdfs_Container, X), ic(uri_rdfs_Container), icext(uri_rdfs_Container, X), ic(uri_rdfs_Container)) -> ic(uri_rdfs_Container)
% 25.61/25.24  300: ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Resource, X), ic(uri_rdfs_Container), icext(X, Y), ic(uri_rdfs_Container)) -> ic(uri_rdfs_Container)
% 25.61/25.24  301: ifeq(icext(sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z, X), ic(uri_rdfs_Container), icext(sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z, X), ic(uri_rdfs_Container)) -> ic(uri_rdfs_Container)
% 25.61/25.24  302: ifeq(icext(uri_ex_Person, X), ic(uri_rdfs_Container), icext(uri_ex_Person, X), ic(uri_rdfs_Container)) -> ic(uri_rdfs_Container)
% 25.61/25.24  303: ifeq(icext(uri_rdf_Alt, X), ic(uri_rdfs_Container), icext(uri_rdf_Alt, X), ic(uri_rdfs_Container)) -> ic(uri_rdfs_Container)
% 25.61/25.24  304: ifeq(icext(uri_rdf_XMLLiteral, X), ic(uri_rdfs_Container), icext(uri_rdf_XMLLiteral, X), ic(uri_rdfs_Container)) -> ic(uri_rdfs_Container)
% 25.61/25.24  305: ifeq(icext(uri_rdfs_Seq, X), ic(uri_rdfs_Container), icext(uri_rdfs_Seq, X), ic(uri_rdfs_Container)) -> ic(uri_rdfs_Container)
% 25.61/25.24  306: ifeq(icext(uri_rdfs_Class, X), ic(uri_rdfs_Container), icext(uri_rdfs_Class, X), ic(uri_rdfs_Container)) -> ic(uri_rdfs_Container)
% 25.61/25.24  307: ifeq(icext(uri_rdf_Property, X), ic(uri_rdfs_Container), icext(uri_rdf_Property, X), ic(uri_rdfs_Container)) -> ic(uri_rdfs_Container)
% 25.61/25.24  308: ifeq(icext(uri_rdf_Bag, X), ic(uri_rdfs_Container), icext(uri_rdf_Bag, X), ic(uri_rdfs_Container)) -> ic(uri_rdfs_Container)
% 25.61/25.24  309: ifeq(icext(uri_rdfs_Datatype, X), ic(uri_rdfs_Container), icext(uri_rdfs_Datatype, X), ic(uri_rdfs_Container)) -> ic(uri_rdfs_Container)
% 25.61/25.24  310: ifeq(icext(uri_rdfs_Literal, X), ic(uri_rdfs_Container), icext(uri_rdfs_Literal, X), ic(uri_rdfs_Container)) -> ic(uri_rdfs_Container)
% 25.61/25.24  311: ifeq(icext(uri_rdfs_ContainerMembershipProperty, X), ic(uri_rdfs_Container), icext(uri_rdfs_ContainerMembershipProperty, X), ic(uri_rdfs_Container)) -> ic(uri_rdfs_Container)
% 25.61/25.24  312: ifeq(iext(uri_rdfs_subClassOf, uri_ex_Person, X), ic(uri_rdfs_Container), icext(X, uri_ex_bob), ic(uri_rdfs_Container)) -> ic(uri_rdfs_Container)
% 25.61/25.24  313: ifeq(iext(uri_rdfs_subClassOf, uri_ex_Person, X), ic(uri_rdfs_Container), icext(X, uri_ex_alice), ic(uri_rdfs_Container)) -> ic(uri_rdfs_Container)
% 25.61/25.24  314: ifeq(iext(uri_rdfs_subClassOf, uri_owl_Restriction, X), ic(uri_rdfs_Container), icext(X, sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z), ic(uri_rdfs_Container)) -> ic(uri_rdfs_Container)
% 25.61/25.24  315: ifeq(iext(uri_rdfs_subClassOf, uri_rdf_List, X), ic(uri_rdfs_Container), icext(X, uri_rdf_nil), ic(uri_rdfs_Container)) -> ic(uri_rdfs_Container)
% 25.61/25.24  316: ifeq(iext(uri_rdfs_subClassOf, uri_owl_TransitiveProperty, X), ic(uri_rdfs_Container), icext(X, uri_ex_hasAncestor), ic(uri_rdfs_Container)) -> ic(uri_rdfs_Container)
% 25.61/25.24  317: ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, X), ic(uri_rdfs_Container), icext(X, uri_rdf__2), ic(uri_rdfs_Container)) -> ic(uri_rdfs_Container)
% 25.61/25.24  318: ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, X), ic(uri_rdfs_Container), icext(X, uri_rdf__1), ic(uri_rdfs_Container)) -> ic(uri_rdfs_Container)
% 25.61/25.24  319: ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, X), ic(uri_rdfs_Container), icext(X, uri_rdf__3), ic(uri_rdfs_Container)) -> ic(uri_rdfs_Container)
% 25.61/25.24  320: ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, X), ic(uri_rdfs_Container), icext(X, uri_rdf_object), ic(uri_rdfs_Container)) -> ic(uri_rdfs_Container)
% 25.61/25.24  321: ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, X), ic(uri_rdfs_Container), icext(X, uri_rdf_first), ic(uri_rdfs_Container)) -> ic(uri_rdfs_Container)
% 25.61/25.24  322: ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, X), ic(uri_rdfs_Container), icext(X, uri_rdf_rest), ic(uri_rdfs_Container)) -> ic(uri_rdfs_Container)
% 25.61/25.24  323: ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, X), ic(uri_rdfs_Container), icext(X, uri_rdf_value), ic(uri_rdfs_Container)) -> ic(uri_rdfs_Container)
% 25.61/25.24  324: ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, X), ic(uri_rdfs_Container), icext(X, uri_rdf_type), ic(uri_rdfs_Container)) -> ic(uri_rdfs_Container)
% 25.61/25.24  325: ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, X), ic(uri_rdfs_Container), icext(X, uri_rdf_subject), ic(uri_rdfs_Container)) -> ic(uri_rdfs_Container)
% 25.61/25.24  326: ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, X), ic(uri_rdfs_Container), icext(X, uri_rdf__2), ic(uri_rdfs_Container)) -> ic(uri_rdfs_Container)
% 25.61/25.24  327: ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, X), ic(uri_rdfs_Container), icext(X, uri_rdf__1), ic(uri_rdfs_Container)) -> ic(uri_rdfs_Container)
% 25.61/25.24  328: ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, X), ic(uri_rdfs_Container), icext(X, uri_rdf__3), ic(uri_rdfs_Container)) -> ic(uri_rdfs_Container)
% 25.61/25.24  329: ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, X), ic(uri_rdfs_Container), icext(X, uri_rdf_XMLLiteral), ic(uri_rdfs_Container)) -> ic(uri_rdfs_Container)
% 25.61/25.24  330: ifeq(iext(uri_rdfs_subClassOf, sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z, X), ic(uri_rdfs_Container), icext(X, uri_ex_alice), ic(uri_rdfs_Container)) -> ic(uri_rdfs_Container)
% 25.61/25.24  331: ifeq(iext(uri_rdfs_subClassOf, sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z, X), ic(uri_rdfs_Container), icext(X, uri_ex_bob), ic(uri_rdfs_Container)) -> ic(uri_rdfs_Container)
% 25.61/25.24  332: ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, X), ic(uri_rdfs_Container), icext(X, uri_ex_Person), ic(uri_rdfs_Container)) -> ic(uri_rdfs_Container)
% 25.61/25.24  333: ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, X), ic(uri_rdfs_Container), icext(X, uri_rdf_Alt), ic(uri_rdfs_Container)) -> ic(uri_rdfs_Container)
% 25.61/25.24  334: ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, X), ic(uri_rdfs_Container), icext(X, sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z), ic(uri_rdfs_Container)) -> ic(uri_rdfs_Container)
% 25.61/25.24  335: ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, X), ic(uri_rdfs_Container), icext(X, uri_rdf_Property), ic(uri_rdfs_Container)) -> ic(uri_rdfs_Container)
% 25.61/25.24  336: ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, X), ic(uri_rdfs_Container), icext(X, uri_rdf_Bag), ic(uri_rdfs_Container)) -> ic(uri_rdfs_Container)
% 25.61/25.24  337: ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, X), ic(uri_rdfs_Container), icext(X, uri_rdf_XMLLiteral), ic(uri_rdfs_Container)) -> ic(uri_rdfs_Container)
% 25.61/25.24  338: ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, X), ic(uri_rdfs_Container), icext(X, uri_rdfs_ContainerMembershipProperty), ic(uri_rdfs_Container)) -> ic(uri_rdfs_Container)
% 25.61/25.24  339: ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, X), ic(uri_rdfs_Container), icext(X, uri_rdfs_Class), ic(uri_rdfs_Container)) -> ic(uri_rdfs_Container)
% 25.61/25.24  340: ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, X), ic(uri_rdfs_Container), icext(X, uri_rdfs_Datatype), ic(uri_rdfs_Container)) -> ic(uri_rdfs_Container)
% 25.61/25.24  341: ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, X), ic(uri_rdfs_Container), icext(X, uri_rdfs_Seq), ic(uri_rdfs_Container)) -> ic(uri_rdfs_Container)
% 25.61/25.24  342: ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, X), ic(uri_rdfs_Container), icext(X, uri_rdfs_Literal), ic(uri_rdfs_Container)) -> ic(uri_rdfs_Container)
% 25.61/25.24  343: ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, X), ic(uri_rdfs_Container), icext(X, uri_rdfs_Resource), ic(uri_rdfs_Container)) -> ic(uri_rdfs_Container)
% 25.61/25.24  344: ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, X), ic(uri_rdfs_Container), icext(X, uri_rdfs_Container), ic(uri_rdfs_Container)) -> ic(uri_rdfs_Container)
% 25.61/25.24  345: ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, X), ic(uri_rdfs_Container), icext(X, uri_rdfs_subPropertyOf), ic(uri_rdfs_Container)) -> ic(uri_rdfs_Container)
% 25.61/25.24  346: ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, X), ic(uri_rdfs_Container), icext(X, uri_rdfs_subClassOf), ic(uri_rdfs_Container)) -> ic(uri_rdfs_Container)
% 25.61/25.24  347: ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, X), ic(uri_rdfs_Container), icext(X, uri_rdfs_domain), ic(uri_rdfs_Container)) -> ic(uri_rdfs_Container)
% 25.61/25.24  348: ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, X), ic(uri_rdfs_Container), icext(X, uri_ex_hasAncestor), ic(uri_rdfs_Container)) -> ic(uri_rdfs_Container)
% 25.61/25.24  349: ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, X), ic(uri_rdfs_Container), icext(X, uri_rdfs_seeAlso), ic(uri_rdfs_Container)) -> ic(uri_rdfs_Container)
% 25.61/25.24  350: ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, X), ic(uri_rdfs_Container), icext(X, uri_rdfs_range), ic(uri_rdfs_Container)) -> ic(uri_rdfs_Container)
% 25.61/25.24  351: ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, X), ic(uri_rdfs_Container), icext(X, uri_rdfs_isDefinedBy), ic(uri_rdfs_Container)) -> ic(uri_rdfs_Container)
% 25.61/25.24  352: ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, X), ic(uri_rdfs_Container), icext(X, uri_owl_onProperty), ic(uri_rdfs_Container)) -> ic(uri_rdfs_Container)
% 25.61/25.24  353: ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, X), ic(uri_rdfs_Container), icext(X, uri_owl_minCardinality), ic(uri_rdfs_Container)) -> ic(uri_rdfs_Container)
% 25.61/25.24  354: ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, X), ic(uri_rdfs_Container), icext(X, uri_rdfs_member), ic(uri_rdfs_Container)) -> ic(uri_rdfs_Container)
% 25.61/25.24  356: ifeq(iext(uri_rdfs_range, X, Y), ic(uri_rdfs_Container), ifeq(iext(X, Z, W), ic(uri_rdfs_Container), icext(Y, W), ic(uri_rdfs_Container)), ic(uri_rdfs_Container)) -> ic(uri_rdfs_Container)
% 25.61/25.24  357: ifeq(iext(uri_rdf_predicate, X, Y), ic(uri_rdfs_Container), ic(uri_rdfs_Container), ic(uri_rdfs_Container)) -> ic(uri_rdfs_Container)
% 25.61/25.24  358: ifeq(iext(uri_rdf_rest, X, Y), ic(uri_rdfs_Container), icext(uri_rdf_List, Y), ic(uri_rdfs_Container)) -> ic(uri_rdfs_Container)
% 25.61/25.24  359: ifeq(iext(uri_rdf_type, X, Y), ic(uri_rdfs_Container), icext(uri_rdfs_Class, Y), ic(uri_rdfs_Container)) -> ic(uri_rdfs_Container)
% 25.61/25.24  360: icext(uri_rdfs_Class, uri_owl_Restriction) -> ic(uri_rdfs_Container)
% 25.61/25.24  361: ic(uri_owl_Restriction) -> ic(uri_rdfs_Container)
% 25.61/25.24  362: icext(uri_rdfs_Class, uri_owl_TransitiveProperty) -> ic(uri_rdfs_Container)
% 25.61/25.24  363: ic(uri_owl_TransitiveProperty) -> ic(uri_rdfs_Container)
% 25.61/25.24  364: icext(uri_rdfs_Class, uri_rdf_List) -> ic(uri_rdfs_Container)
% 25.61/25.24  365: ic(uri_rdf_List) -> ic(uri_rdfs_Container)
% 25.61/25.24  366: iext(uri_rdf_type, uri_rdf_List, uri_rdfs_Class) -> ic(uri_rdfs_Container)
% 25.61/25.24  367: iext(uri_rdf_type, uri_owl_TransitiveProperty, uri_rdfs_Class) -> ic(uri_rdfs_Container)
% 25.61/25.24  368: iext(uri_rdf_type, uri_owl_Restriction, uri_rdfs_Class) -> ic(uri_rdfs_Container)
% 25.61/25.24  369: iext(uri_rdfs_subClassOf, uri_rdf_List, uri_rdfs_Resource) -> ic(uri_rdfs_Container)
% 25.61/25.25  370: iext(uri_rdfs_subClassOf, uri_rdf_List, uri_rdf_List) -> ic(uri_rdfs_Container)
% 25.61/25.25  371: iext(uri_rdfs_subClassOf, uri_owl_Restriction, uri_rdfs_Resource) -> ic(uri_rdfs_Container)
% 25.61/25.25  372: iext(uri_rdfs_subClassOf, uri_owl_Restriction, uri_owl_Restriction) -> ic(uri_rdfs_Container)
% 25.61/25.25  373: iext(uri_rdfs_subClassOf, uri_owl_TransitiveProperty, uri_rdfs_Resource) -> ic(uri_rdfs_Container)
% 25.61/25.25  374: iext(uri_rdfs_subClassOf, uri_owl_TransitiveProperty, uri_owl_TransitiveProperty) -> ic(uri_rdfs_Container)
% 25.61/25.25  375: ifeq(iext(uri_rdfs_comment, X, Y), ic(uri_rdfs_Container), icext(uri_rdfs_Literal, Y), ic(uri_rdfs_Container)) -> ic(uri_rdfs_Container)
% 25.61/25.25  376: ifeq(iext(uri_rdfs_domain, X, Y), ic(uri_rdfs_Container), icext(uri_rdfs_Class, Y), ic(uri_rdfs_Container)) -> ic(uri_rdfs_Container)
% 25.61/25.25  377: icext(uri_rdfs_Class, uri_rdfs_Statement) -> ic(uri_rdfs_Container)
% 25.61/25.25  378: ic(uri_rdfs_Container) -> ic(uri_rdfs_Statement)
% 25.61/25.25  379: iext(uri_rdf_type, uri_rdfs_Statement, uri_rdfs_Class) -> ic(uri_rdfs_Statement)
% 25.61/25.25  380: ifeq(lv(X), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  381: ifeq(icext(uri_rdfs_Class, X), ic(uri_rdfs_Statement), ic(X), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  382: ifeq(icext(uri_rdfs_Literal, X), ic(uri_rdfs_Statement), lv(X), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  383: ifeq(lv(X), ic(uri_rdfs_Statement), icext(uri_rdfs_Literal, X), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  384: ifeq(ic(X), ic(uri_rdfs_Statement), icext(uri_rdfs_Class, X), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  385: ifeq(icext(X, Y), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  386: ifeq(iext(uri_rdfs_label, X, Y), ic(uri_rdfs_Statement), icext(uri_rdfs_Literal, Y), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  387: ifeq(iext(uri_rdfs_range, X, Y), ic(uri_rdfs_Statement), icext(uri_rdfs_Class, Y), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  388: ifeq(iext(uri_rdfs_subClassOf, X, Y), ic(uri_rdfs_Statement), icext(uri_rdfs_Class, Y), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  389: ifeq(iext(uri_rdfs_subPropertyOf, X, Y), ic(uri_rdfs_Statement), icext(uri_rdf_Property, Y), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  390: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdf__1), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  391: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdf__2), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  392: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdf__3), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  393: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdf_first), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  394: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdf_object), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  395: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdf_rest), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  396: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdf_subject), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  397: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdf_type), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  398: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdf_value), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  399: ifeq(iext(uri_rdfs_range, uri_ex_hasAncestor, X), ic(uri_rdfs_Statement), icext(X, uri_ex_bob), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  400: ifeq(iext(uri_rdfs_range, uri_ex_hasAncestor, uri_ex_Person), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  401: ifeq(iext(uri_rdfs_range, uri_ex_hasAncestor, uri_rdfs_Resource), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  402: ifeq(iext(uri_rdfs_range, uri_owl_onProperty, X), ic(uri_rdfs_Statement), icext(X, uri_ex_hasAncestor), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  403: ifeq(iext(uri_rdfs_range, uri_owl_onProperty, uri_owl_TransitiveProperty), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  404: ifeq(iext(uri_rdfs_range, uri_owl_onProperty, uri_rdfs_Resource), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  405: ifeq(iext(uri_rdfs_range, uri_rdf_type, X), ic(uri_rdfs_Statement), icext(X, uri_owl_Restriction), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  406: ifeq(iext(uri_rdfs_range, uri_rdf_type, uri_rdfs_Resource), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  407: ifeq(iext(uri_rdfs_range, uri_rdf_type, X), ic(uri_rdfs_Statement), icext(X, uri_ex_Person), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  408: ifeq(iext(uri_rdfs_range, uri_rdf_type, X), ic(uri_rdfs_Statement), icext(X, uri_owl_TransitiveProperty), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  409: ifeq(iext(uri_rdfs_range, uri_rdf_type, X), ic(uri_rdfs_Statement), icext(X, uri_rdfs_Class), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  410: ifeq(iext(uri_rdfs_range, uri_rdf_type, X), ic(uri_rdfs_Statement), icext(X, uri_rdfs_Datatype), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  411: ifeq(iext(uri_rdfs_range, uri_rdf_type, X), ic(uri_rdfs_Statement), icext(X, uri_rdf_Property), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  412: ifeq(iext(uri_rdfs_range, uri_rdf_type, X), ic(uri_rdfs_Statement), icext(X, uri_rdfs_ContainerMembershipProperty), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  413: ifeq(iext(uri_rdfs_range, uri_rdf_type, X), ic(uri_rdfs_Statement), icext(X, uri_rdf_List), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  414: ifeq(iext(uri_rdfs_range, uri_rdfs_domain, X), ic(uri_rdfs_Statement), icext(X, uri_rdfs_Resource), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  415: ifeq(iext(uri_rdfs_range, uri_rdfs_domain, uri_rdfs_Resource), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  416: ifeq(iext(uri_rdfs_range, uri_rdfs_domain, X), ic(uri_rdfs_Statement), icext(X, uri_rdf_List), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  417: ifeq(iext(uri_rdfs_range, uri_rdfs_domain, X), ic(uri_rdfs_Statement), icext(X, uri_rdfs_Statement), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  418: ifeq(iext(uri_rdfs_range, uri_rdfs_domain, X), ic(uri_rdfs_Statement), icext(X, uri_rdf_Property), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  419: ifeq(iext(uri_rdfs_range, uri_rdfs_domain, X), ic(uri_rdfs_Statement), icext(X, uri_rdfs_Class), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  420: ifeq(iext(uri_rdfs_range, uri_rdfs_range, X), ic(uri_rdfs_Statement), icext(X, uri_rdfs_Resource), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  421: ifeq(iext(uri_rdfs_range, uri_rdfs_range, uri_rdfs_Resource), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  422: ifeq(iext(uri_rdfs_range, uri_rdfs_range, X), ic(uri_rdfs_Statement), icext(X, uri_rdf_List), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  423: ifeq(iext(uri_rdfs_range, uri_rdfs_range, X), ic(uri_rdfs_Statement), icext(X, uri_rdfs_Class), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  424: ifeq(iext(uri_rdfs_range, uri_rdfs_range, X), ic(uri_rdfs_Statement), icext(X, uri_rdfs_Literal), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  425: ifeq(iext(uri_rdfs_range, uri_rdfs_range, X), ic(uri_rdfs_Statement), icext(X, uri_rdf_Property), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  426: ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, X), ic(uri_rdfs_Statement), icext(X, sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  427: ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, uri_owl_Restriction), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  428: ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, uri_rdfs_Resource), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  429: ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, X), ic(uri_rdfs_Statement), icext(X, uri_rdfs_Container), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  430: ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, X), ic(uri_rdfs_Statement), icext(X, uri_rdfs_Literal), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  431: ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, X), ic(uri_rdfs_Statement), icext(X, uri_rdf_Property), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  432: ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, X), ic(uri_rdfs_Statement), icext(X, uri_rdfs_Class), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  433: ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, X), ic(uri_rdfs_Statement), icext(X, uri_rdfs_seeAlso), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  434: ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, uri_rdfs_Resource), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  435: ifeq(iext(uri_rdfs_range, X, sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  436: ifeq(iext(uri_rdfs_subClassOf, X, sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  437: ifeq(iext(uri_rdfs_subClassOf, X, uri_ex_Person), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  438: ifeq(iext(uri_rdfs_subClassOf, X, uri_owl_TransitiveProperty), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  439: ifeq(iext(uri_rdfs_subClassOf, X, uri_owl_Restriction), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  440: ifeq(iext(uri_rdfs_subClassOf, X, uri_rdf_Alt), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  441: ifeq(iext(uri_rdfs_range, X, uri_rdf_List), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  442: ifeq(iext(uri_rdfs_range, X, uri_rdf_Bag), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  443: ifeq(iext(uri_rdfs_range, X, uri_owl_TransitiveProperty), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  444: ifeq(iext(uri_rdfs_range, X, uri_rdf_Alt), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  445: ifeq(iext(uri_rdfs_range, X, uri_rdf_Property), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  446: ifeq(iext(uri_rdfs_range, X, uri_rdfs_Class), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  447: ifeq(iext(uri_rdfs_range, X, uri_rdf_XMLLiteral), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  448: ifeq(iext(uri_rdfs_range, X, uri_rdfs_Literal), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  449: ifeq(iext(uri_rdfs_range, X, uri_rdfs_Datatype), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  450: ifeq(iext(uri_rdfs_range, X, uri_rdfs_ContainerMembershipProperty), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  451: ifeq(iext(uri_rdfs_range, X, uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  452: ifeq(iext(uri_rdfs_range, X, uri_rdfs_Seq), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  453: ifeq(iext(uri_rdfs_subClassOf, X, uri_rdf_XMLLiteral), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  454: ifeq(iext(uri_rdfs_subClassOf, X, uri_rdf_List), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  455: ifeq(iext(uri_rdfs_subClassOf, X, uri_rdf_Property), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  456: ifeq(iext(uri_rdfs_subClassOf, X, uri_rdf_Bag), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  457: ifeq(iext(uri_rdfs_subClassOf, X, uri_rdfs_Class), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  458: ifeq(iext(uri_rdfs_subClassOf, X, uri_rdfs_ContainerMembershipProperty), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  459: ifeq(iext(uri_rdfs_subClassOf, X, uri_rdfs_Datatype), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  460: ifeq(iext(uri_rdfs_subClassOf, X, uri_rdfs_Seq), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  461: ifeq(iext(uri_rdfs_subClassOf, X, uri_rdfs_Literal), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  462: ifeq(iext(uri_rdfs_subClassOf, X, uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  463: ifeq(iext(uri_rdfs_range, X, uri_owl_Restriction), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  464: ifeq(iext(uri_rdfs_range, X, uri_ex_Person), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  465: ifeq(iext(X, Y, Z), ic(uri_rdfs_Statement), ip(X), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  466: ifeq(iext(uri_rdfs_range, uri_rdf_type, X), ic(uri_rdfs_Statement), icext(X, uri_rdfs_Resource), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  467: ifeq(iext(uri_rdfs_subPropertyOf, X, Y), ic(uri_rdfs_Statement), ip(X), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  468: ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, X), ic(uri_rdfs_Statement), icext(X, uri_rdfs_Resource), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  469: ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, X), ic(uri_rdfs_Statement), icext(X, uri_owl_minCardinality), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  470: ifeq(ip(X), ic(uri_rdfs_Statement), iext(uri_rdfs_subPropertyOf, X, X), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  471: ifeq(iext(uri_rdfs_subClassOf, X, Y), ic(uri_rdfs_Statement), ic(X), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  472: ifeq(iext(uri_rdfs_subClassOf, X, Y), ic(uri_rdfs_Statement), ic(Y), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  473: ifeq(iext(uri_rdfs_subPropertyOf, X, Y), ic(uri_rdfs_Statement), ip(Y), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  474: ifeq(ic(X), ic(uri_rdfs_Statement), iext(uri_rdfs_subClassOf, X, X), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  475: iext(uri_rdfs_subClassOf, uri_rdfs_Statement, uri_rdfs_Statement) -> ic(uri_rdfs_Statement)
% 25.61/25.25  476: ifeq(ip(X), ic(uri_rdfs_Statement), iext(uri_rdf_type, X, uri_rdf_Property), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  477: ifeq(ic(X), ic(uri_rdfs_Statement), iext(uri_rdfs_subClassOf, X, uri_rdfs_Resource), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  478: iext(uri_rdfs_subClassOf, uri_rdfs_Statement, uri_rdfs_Resource) -> ic(uri_rdfs_Statement)
% 25.61/25.25  479: ifeq(iext(uri_ex_hasAncestor, X, Y), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  480: ifeq(iext(uri_rdf_type, X, uri_rdf_Property), ic(uri_rdfs_Statement), ip(X), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  481: ifeq(icext(uri_ex_Person, X), ic(uri_rdfs_Statement), icext(sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z, X), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  482: ifeq(icext(uri_rdf_XMLLiteral, X), ic(uri_rdfs_Statement), icext(uri_rdfs_Literal, X), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  483: ifeq(icext(uri_rdfs_Seq, X), ic(uri_rdfs_Statement), icext(uri_rdfs_Container, X), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  484: ifeq(iext(uri_rdf_subject, X, Y), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  485: ifeq(iext(uri_rdfs_seeAlso, X, Y), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  486: ifeq(iext(uri_owl_minCardinality, X, Y), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  487: ifeq(iext(uri_rdf__1, X, Y), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  488: ifeq(iext(uri_rdf__3, X, Y), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  489: ifeq(iext(uri_rdf_first, X, Y), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  490: ifeq(iext(uri_rdf__2, X, Y), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  491: ifeq(iext(uri_rdf_rest, X, Y), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  492: ifeq(iext(uri_rdf_value, X, Y), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  493: ifeq(iext(uri_rdf_object, X, Y), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  494: ifeq(iext(uri_rdf_type, X, Y), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  495: ifeq(iext(uri_rdfs_domain, X, Y), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  496: ifeq(iext(uri_rdfs_range, X, Y), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  497: ifeq(iext(uri_rdfs_isDefinedBy, X, Y), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  498: ifeq(iext(uri_owl_onProperty, X, Y), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  499: ifeq(iext(uri_rdfs_subPropertyOf, X, Y), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  500: ifeq(iext(uri_rdfs_subClassOf, X, Y), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  501: ifeq(iext(uri_rdf_predicate, X, Y), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  502: ifeq(icext(uri_rdfs_ContainerMembershipProperty, X), ic(uri_rdfs_Statement), icext(uri_rdfs_ContainerMembershipProperty, X), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  503: ifeq(icext(uri_rdfs_Literal, X), ic(uri_rdfs_Statement), icext(uri_rdfs_Literal, X), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  504: ifeq(icext(uri_rdf_Bag, X), ic(uri_rdfs_Statement), icext(uri_rdf_Bag, X), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  505: ifeq(icext(uri_rdfs_Datatype, X), ic(uri_rdfs_Statement), icext(uri_rdfs_Datatype, X), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  506: ifeq(icext(uri_rdf_Property, X), ic(uri_rdfs_Statement), icext(uri_rdf_Property, X), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  507: ifeq(icext(uri_rdfs_Class, X), ic(uri_rdfs_Statement), icext(uri_rdfs_Class, X), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  508: ifeq(icext(uri_rdf_XMLLiteral, X), ic(uri_rdfs_Statement), icext(uri_rdf_XMLLiteral, X), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  509: ifeq(icext(uri_rdfs_Seq, X), ic(uri_rdfs_Statement), icext(uri_rdfs_Seq, X), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  510: ifeq(icext(uri_rdf_Alt, X), ic(uri_rdfs_Statement), icext(uri_rdf_Alt, X), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  511: ifeq(icext(uri_ex_Person, X), ic(uri_rdfs_Statement), icext(uri_ex_Person, X), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  512: ifeq(icext(sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z, X), ic(uri_rdfs_Statement), icext(sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z, X), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  513: ifeq(icext(uri_rdfs_Container, X), ic(uri_rdfs_Statement), icext(uri_rdfs_Container, X), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  514: ifeq(icext(uri_rdfs_ContainerMembershipProperty, X), ic(uri_rdfs_Statement), icext(uri_rdf_Property, X), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  515: ifeq(icext(uri_rdfs_Datatype, X), ic(uri_rdfs_Statement), icext(uri_rdfs_Class, X), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  516: ifeq(icext(uri_rdf_Bag, X), ic(uri_rdfs_Statement), icext(uri_rdfs_Container, X), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  517: ifeq(icext(uri_rdf_Alt, X), ic(uri_rdfs_Statement), icext(uri_rdfs_Container, X), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  518: ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, X), ic(uri_rdfs_Statement), icext(X, uri_rdfs_Datatype), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  519: ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, X), ic(uri_rdfs_Statement), icext(X, uri_owl_TransitiveProperty), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  520: ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, X), ic(uri_rdfs_Statement), icext(X, uri_rdf_List), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  521: ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, X), ic(uri_rdfs_Statement), icext(X, uri_owl_Restriction), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  522: ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, X), ic(uri_rdfs_Statement), icext(X, uri_rdfs_Statement), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  523: ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, X), ic(uri_rdfs_Statement), icext(X, uri_rdf_XMLLiteral), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  524: ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, X), ic(uri_rdfs_Statement), icext(X, uri_rdf_Bag), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  525: ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, X), ic(uri_rdfs_Statement), icext(X, uri_rdfs_member), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  526: ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, X), ic(uri_rdfs_Statement), icext(X, uri_rdf__2), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  527: ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, X), ic(uri_rdfs_Statement), icext(X, uri_rdf__1), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  528: ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, X), ic(uri_rdfs_Statement), icext(X, uri_rdf__3), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  529: ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, X), ic(uri_rdfs_Statement), icext(X, uri_rdf_first), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  530: ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, X), ic(uri_rdfs_Statement), icext(X, uri_rdf_object), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  531: ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, X), ic(uri_rdfs_Statement), icext(X, uri_rdf_type), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  532: ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, X), ic(uri_rdfs_Statement), icext(X, uri_rdf_subject), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  533: ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, X), ic(uri_rdfs_Statement), icext(X, uri_rdf_rest), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  534: ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, X), ic(uri_rdfs_Statement), icext(X, uri_rdf_value), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  535: ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, X), ic(uri_rdfs_Statement), icext(X, uri_rdfs_isDefinedBy), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  536: ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, X), ic(uri_rdfs_Statement), icext(X, uri_rdfs_domain), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  537: ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, X), ic(uri_rdfs_Statement), icext(X, uri_rdfs_range), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  538: ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, X), ic(uri_rdfs_Statement), icext(X, uri_rdfs_subClassOf), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  539: ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, X), ic(uri_rdfs_Statement), icext(X, uri_rdfs_subPropertyOf), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  540: ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, X), ic(uri_rdfs_Statement), icext(X, uri_ex_Person), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  541: ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, X), ic(uri_rdfs_Statement), icext(X, uri_rdf_Alt), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  542: ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, X), ic(uri_rdfs_Statement), icext(X, uri_rdfs_Seq), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  543: ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, X), ic(uri_rdfs_Statement), icext(X, uri_rdfs_ContainerMembershipProperty), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  544: ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, X), ic(uri_rdfs_Statement), icext(X, uri_ex_hasAncestor), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  545: ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, X), ic(uri_rdfs_Statement), icext(X, uri_owl_onProperty), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  546: ifeq(iext(uri_rdfs_member, X, Y), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  547: ifeq(icext(uri_owl_TransitiveProperty, X), ic(uri_rdfs_Statement), icext(uri_owl_TransitiveProperty, X), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  548: ifeq(icext(uri_rdf_List, X), ic(uri_rdfs_Statement), icext(uri_rdf_List, X), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  549: ifeq(icext(uri_owl_Restriction, X), ic(uri_rdfs_Statement), icext(uri_owl_Restriction, X), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  550: ifeq(iext(uri_rdf_type, X, Y), ic(uri_rdfs_Statement), icext(Y, X), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  551: ifeq(icext(X, Y), ic(uri_rdfs_Statement), iext(uri_rdf_type, Y, X), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  552: ifeq(iext(uri_rdf_rest, X, Y), ic(uri_rdfs_Statement), icext(uri_rdf_List, Y), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  553: ifeq(iext(uri_rdfs_comment, X, Y), ic(uri_rdfs_Statement), icext(uri_rdfs_Literal, Y), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  554: ifeq(iext(uri_rdfs_domain, X, Y), ic(uri_rdfs_Statement), icext(uri_rdfs_Class, Y), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  555: ifeq(iext(uri_rdf_type, X, Y), ic(uri_rdfs_Statement), icext(uri_rdfs_Class, Y), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  556: ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Resource, X), ic(uri_rdfs_Statement), icext(X, Y), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  557: ifeq(iext(uri_rdfs_range, uri_rdf_type, X), ic(uri_rdfs_Statement), icext(X, sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  558: ifeq(iext(uri_rdfs_subClassOf, uri_ex_Person, X), ic(uri_rdfs_Statement), icext(X, uri_ex_alice), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  559: ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, X), ic(uri_rdfs_Statement), icext(X, uri_rdf__2), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  560: ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, X), ic(uri_rdfs_Statement), icext(X, uri_rdf_subject), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  561: ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, X), ic(uri_rdfs_Statement), icext(X, uri_rdf__2), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  562: ifeq(iext(uri_rdfs_subClassOf, uri_ex_Person, X), ic(uri_rdfs_Statement), icext(X, uri_ex_bob), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  563: ifeq(iext(uri_rdfs_subClassOf, uri_owl_TransitiveProperty, X), ic(uri_rdfs_Statement), icext(X, uri_ex_hasAncestor), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  564: ifeq(iext(uri_rdfs_subClassOf, uri_rdf_List, X), ic(uri_rdfs_Statement), icext(X, uri_rdf_nil), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  565: ifeq(iext(uri_rdfs_subClassOf, uri_owl_Restriction, X), ic(uri_rdfs_Statement), icext(X, sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  566: ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, X), ic(uri_rdfs_Statement), icext(X, uri_rdf_value), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  567: ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, X), ic(uri_rdfs_Statement), icext(X, uri_rdf_type), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  568: ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, X), ic(uri_rdfs_Statement), icext(X, uri_rdf_rest), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  569: ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, X), ic(uri_rdfs_Statement), icext(X, uri_rdf_first), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  570: ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, X), ic(uri_rdfs_Statement), icext(X, uri_rdf_object), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  571: ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, X), ic(uri_rdfs_Statement), icext(X, uri_rdf__3), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  572: ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, X), ic(uri_rdfs_Statement), icext(X, uri_rdf__1), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  573: ifeq(icext(uri_rdfs_Datatype, X), ic(uri_rdfs_Statement), iext(uri_rdfs_subClassOf, X, uri_rdfs_Literal), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  574: ifeq(icext(uri_rdfs_ContainerMembershipProperty, X), ic(uri_rdfs_Statement), iext(uri_rdfs_subPropertyOf, X, uri_rdfs_member), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  575: ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, X), ic(uri_rdfs_Statement), icext(X, uri_rdfs_Literal), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  576: ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, X), ic(uri_rdfs_Statement), icext(X, uri_rdfs_Class), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  577: ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, X), ic(uri_rdfs_Statement), icext(X, uri_rdfs_Seq), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  578: ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, X), ic(uri_rdfs_Statement), icext(X, uri_rdfs_Datatype), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  579: ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, X), ic(uri_rdfs_Statement), icext(X, uri_rdfs_ContainerMembershipProperty), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  580: ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, X), ic(uri_rdfs_Statement), icext(X, uri_rdf_XMLLiteral), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  581: ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, X), ic(uri_rdfs_Statement), icext(X, uri_rdf_Bag), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  582: ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, X), ic(uri_rdfs_Statement), icext(X, uri_rdf_Property), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  583: ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, X), ic(uri_rdfs_Statement), icext(X, sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  584: ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, X), ic(uri_rdfs_Statement), icext(X, uri_ex_Person), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  585: ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, X), ic(uri_rdfs_Statement), icext(X, uri_rdf_Alt), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  586: ifeq(iext(uri_rdfs_subClassOf, sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z, X), ic(uri_rdfs_Statement), icext(X, uri_ex_bob), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  587: ifeq(iext(uri_rdfs_subClassOf, sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z, X), ic(uri_rdfs_Statement), icext(X, uri_ex_alice), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  588: ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, X), ic(uri_rdfs_Statement), icext(X, uri_rdf__3), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  589: ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, X), ic(uri_rdfs_Statement), icext(X, uri_rdf_XMLLiteral), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  590: ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, X), ic(uri_rdfs_Statement), icext(X, uri_rdf__1), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  591: ifeq(icext(uri_rdfs_Statement, X), ic(uri_rdfs_Statement), icext(uri_rdfs_Statement, X), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  592: ifeq(iext(uri_rdfs_range, uri_owl_minCardinality, X), ic(uri_rdfs_Statement), icext(X, literal_typed(dat_str_1, uri_xsd_nonNegativeInteger)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  593: ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, X), ic(uri_rdfs_Statement), icext(X, uri_rdfs_Container), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  594: ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, X), ic(uri_rdfs_Statement), icext(X, uri_rdfs_Resource), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  595: ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, X), ic(uri_rdfs_Statement), icext(X, uri_rdfs_domain), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  596: ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, X), ic(uri_rdfs_Statement), icext(X, uri_ex_hasAncestor), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  597: ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, X), ic(uri_rdfs_Statement), icext(X, uri_rdfs_subClassOf), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  598: ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, X), ic(uri_rdfs_Statement), icext(X, uri_rdfs_subPropertyOf), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  599: ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, X), ic(uri_rdfs_Statement), icext(X, uri_owl_Restriction), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  600: ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, X), ic(uri_rdfs_Statement), icext(X, uri_rdfs_seeAlso), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  601: ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, X), ic(uri_rdfs_Statement), icext(X, uri_rdf_List), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  602: ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, X), ic(uri_rdfs_Statement), icext(X, uri_owl_TransitiveProperty), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  603: ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, X), ic(uri_rdfs_Statement), icext(X, uri_owl_minCardinality), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  604: ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, X), ic(uri_rdfs_Statement), icext(X, uri_rdfs_isDefinedBy), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  605: ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, X), ic(uri_rdfs_Statement), icext(X, uri_owl_onProperty), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  606: ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, X), ic(uri_rdfs_Statement), icext(X, uri_rdfs_range), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  607: eq(tuple(ic(uri_rdfs_Statement), iext(uri_ex_hasAncestor, uri_ex_bob, uri_ex_bob)), tuple(ic(uri_rdfs_Statement), ic(uri_rdfs_Statement))) -> false
% 25.61/25.25  608: ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, X), ic(uri_rdfs_Statement), icext(X, uri_rdfs_Statement), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  609: ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, X), ic(uri_rdfs_Statement), icext(X, uri_rdfs_member), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  611: ifeq(iext(uri_rdfs_domain, X, Y), ic(uri_rdfs_Statement), ifeq(iext(X, Z, W), ic(uri_rdfs_Statement), icext(Y, Z), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  612: ifeq(iext(uri_rdfs_comment, X, Y), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  613: ifeq(iext(uri_rdfs_label, X, Y), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  614: ifeq(iext(uri_rdf_rest, X, Y), ic(uri_rdfs_Statement), icext(uri_rdf_List, X), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  615: ifeq(iext(uri_rdf_subject, X, Y), ic(uri_rdfs_Statement), icext(uri_rdfs_Statement, X), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  616: ifeq(iext(uri_rdf_object, X, Y), ic(uri_rdfs_Statement), icext(uri_rdfs_Statement, X), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  617: ifeq(iext(uri_rdf_first, X, Y), ic(uri_rdfs_Statement), icext(uri_rdf_List, X), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  618: ifeq(iext(uri_rdf_predicate, X, Y), ic(uri_rdfs_Statement), icext(uri_rdfs_Statement, X), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  619: ifeq(iext(uri_rdfs_domain, X, Y), ic(uri_rdfs_Statement), icext(uri_rdf_Property, X), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  620: icext(uri_rdf_Property, uri_rdf_predicate) -> ic(uri_rdfs_Statement)
% 25.61/25.25  621: icext(uri_rdf_Property, uri_rdfs_comment) -> ic(uri_rdfs_Statement)
% 25.61/25.25  622: icext(uri_rdf_Property, uri_rdfs_label) -> ic(uri_rdfs_Statement)
% 25.61/25.25  623: iext(uri_rdf_type, uri_rdfs_label, uri_rdf_Property) -> ic(uri_rdfs_Statement)
% 25.61/25.25  624: ip(uri_rdfs_label) -> ic(uri_rdfs_Statement)
% 25.61/25.25  625: iext(uri_rdf_type, uri_rdfs_comment, uri_rdf_Property) -> ic(uri_rdfs_Statement)
% 25.61/25.25  626: ip(uri_rdfs_comment) -> ic(uri_rdfs_Statement)
% 25.61/25.25  627: iext(uri_rdf_type, uri_rdf_predicate, uri_rdf_Property) -> ic(uri_rdfs_Statement)
% 25.61/25.25  628: ip(uri_rdf_predicate) -> ic(uri_rdfs_Statement)
% 25.61/25.25  629: iext(uri_rdfs_subPropertyOf, uri_rdf_predicate, uri_rdf_predicate) -> ic(uri_rdfs_Statement)
% 25.61/25.25  630: iext(uri_rdfs_subPropertyOf, uri_rdfs_comment, uri_rdfs_comment) -> ic(uri_rdfs_Statement)
% 25.61/25.25  631: iext(uri_rdfs_subPropertyOf, uri_rdfs_label, uri_rdfs_label) -> ic(uri_rdfs_Statement)
% 25.61/25.25  632: ifeq(iext(uri_rdfs_range, X, Y), ic(uri_rdfs_Statement), icext(uri_rdf_Property, X), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  633: ifeq(iext(uri_rdfs_subClassOf, X, Y), ic(uri_rdfs_Statement), icext(uri_rdfs_Class, X), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  634: ifeq(iext(uri_rdfs_subPropertyOf, X, Y), ic(uri_rdfs_Statement), icext(uri_rdf_Property, X), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  635: ifeq(iext(uri_rdfs_domain, uri_ex_hasAncestor, X), ic(uri_rdfs_Statement), icext(X, uri_ex_alice), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  636: ifeq(iext(uri_rdfs_domain, uri_owl_minCardinality, X), ic(uri_rdfs_Statement), icext(X, sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  637: ifeq(iext(uri_rdfs_domain, uri_owl_onProperty, X), ic(uri_rdfs_Statement), icext(X, sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  638: ifeq(iext(uri_rdfs_domain, uri_rdf_type, X), ic(uri_rdfs_Statement), icext(X, sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  639: ifeq(iext(uri_rdfs_domain, uri_rdf_type, X), ic(uri_rdfs_Statement), icext(X, uri_ex_alice), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  640: ifeq(iext(uri_rdfs_domain, uri_rdf_type, X), ic(uri_rdfs_Statement), icext(X, uri_ex_bob), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  641: ifeq(iext(uri_rdfs_domain, uri_rdf_type, X), ic(uri_rdfs_Statement), icext(X, uri_ex_hasAncestor), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  642: ifeq(iext(uri_rdfs_domain, uri_rdf_type, X), ic(uri_rdfs_Statement), icext(X, uri_rdf_Property), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  643: ifeq(iext(uri_rdfs_domain, uri_rdf_type, X), ic(uri_rdfs_Statement), icext(X, uri_rdf_XMLLiteral), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  644: ifeq(iext(uri_rdfs_domain, uri_rdf_type, X), ic(uri_rdfs_Statement), icext(X, uri_rdf__1), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  645: ifeq(iext(uri_rdfs_domain, uri_rdf_type, X), ic(uri_rdfs_Statement), icext(X, uri_rdf__2), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  646: ifeq(iext(uri_rdfs_domain, uri_rdf_type, X), ic(uri_rdfs_Statement), icext(X, uri_rdf__3), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  647: ifeq(iext(uri_rdfs_domain, uri_rdf_type, X), ic(uri_rdfs_Statement), icext(X, uri_rdf_first), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  648: ifeq(iext(uri_rdfs_domain, uri_rdf_type, X), ic(uri_rdfs_Statement), icext(X, uri_rdf_nil), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  649: ifeq(iext(uri_rdfs_domain, uri_rdf_type, X), ic(uri_rdfs_Statement), icext(X, uri_rdf_object), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  650: ifeq(iext(uri_rdfs_domain, uri_rdf_type, X), ic(uri_rdfs_Statement), icext(X, uri_rdf_rest), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  651: ifeq(iext(uri_rdfs_domain, uri_rdf_type, X), ic(uri_rdfs_Statement), icext(X, uri_rdf_subject), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  652: ifeq(iext(uri_rdfs_domain, uri_rdf_type, X), ic(uri_rdfs_Statement), icext(X, uri_rdf_type), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  653: ifeq(iext(uri_rdfs_domain, uri_rdf_type, X), ic(uri_rdfs_Statement), icext(X, uri_rdf_value), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  654: ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, X), ic(uri_rdfs_Statement), icext(X, uri_rdf__1), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  655: ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, X), ic(uri_rdfs_Statement), icext(X, uri_rdf__2), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  656: ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, X), ic(uri_rdfs_Statement), icext(X, uri_rdf__3), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  657: ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, X), ic(uri_rdfs_Statement), icext(X, uri_rdf_first), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  658: ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, X), ic(uri_rdfs_Statement), icext(X, uri_rdf_object), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  659: ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, X), ic(uri_rdfs_Statement), icext(X, uri_rdf_predicate), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  660: ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, X), ic(uri_rdfs_Statement), icext(X, uri_rdf_rest), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  661: ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, X), ic(uri_rdfs_Statement), icext(X, uri_rdf_subject), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  662: ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, X), ic(uri_rdfs_Statement), icext(X, uri_rdf_type), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  663: ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, X), ic(uri_rdfs_Statement), icext(X, uri_rdf_value), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  664: ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, X), ic(uri_rdfs_Statement), icext(X, uri_rdfs_comment), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  665: ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, X), ic(uri_rdfs_Statement), icext(X, uri_rdfs_domain), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  666: ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, X), ic(uri_rdfs_Statement), icext(X, uri_rdfs_isDefinedBy), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  667: ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, X), ic(uri_rdfs_Statement), icext(X, uri_rdfs_label), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  668: ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, X), ic(uri_rdfs_Statement), icext(X, uri_rdfs_member), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  669: ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, X), ic(uri_rdfs_Statement), icext(X, uri_rdfs_range), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  670: ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, X), ic(uri_rdfs_Statement), icext(X, uri_rdfs_seeAlso), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  671: ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, X), ic(uri_rdfs_Statement), icext(X, uri_rdfs_subClassOf), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  672: ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, X), ic(uri_rdfs_Statement), icext(X, uri_rdfs_subPropertyOf), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  673: ifeq(iext(uri_rdfs_domain, uri_rdfs_range, X), ic(uri_rdfs_Statement), icext(X, uri_rdf__1), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  674: ifeq(iext(uri_rdfs_domain, uri_rdfs_range, X), ic(uri_rdfs_Statement), icext(X, uri_rdf__2), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  675: ifeq(iext(uri_rdfs_domain, uri_rdfs_range, X), ic(uri_rdfs_Statement), icext(X, uri_rdf__3), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  676: ifeq(iext(uri_rdfs_domain, uri_rdfs_range, X), ic(uri_rdfs_Statement), icext(X, uri_rdf_first), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  677: ifeq(iext(uri_rdfs_domain, uri_rdfs_range, X), ic(uri_rdfs_Statement), icext(X, uri_rdf_predicate), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  678: ifeq(iext(uri_rdfs_domain, uri_rdfs_range, X), ic(uri_rdfs_Statement), icext(X, uri_rdf_rest), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  679: ifeq(iext(uri_rdfs_domain, uri_rdfs_range, X), ic(uri_rdfs_Statement), icext(X, uri_rdf_subject), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  680: ifeq(iext(uri_rdfs_domain, uri_rdfs_range, X), ic(uri_rdfs_Statement), icext(X, uri_rdf_type), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  681: ifeq(iext(uri_rdfs_domain, uri_rdfs_range, X), ic(uri_rdfs_Statement), icext(X, uri_rdf_value), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  682: ifeq(iext(uri_rdfs_domain, uri_rdfs_range, X), ic(uri_rdfs_Statement), icext(X, uri_rdfs_comment), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  683: ifeq(iext(uri_rdfs_domain, uri_rdfs_range, X), ic(uri_rdfs_Statement), icext(X, uri_rdfs_domain), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  684: ifeq(iext(uri_rdfs_domain, uri_rdfs_range, X), ic(uri_rdfs_Statement), icext(X, uri_rdfs_isDefinedBy), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  685: ifeq(iext(uri_rdfs_domain, uri_rdfs_range, X), ic(uri_rdfs_Statement), icext(X, uri_rdfs_label), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  686: ifeq(iext(uri_rdfs_domain, uri_rdfs_range, X), ic(uri_rdfs_Statement), icext(X, uri_rdfs_member), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  687: ifeq(iext(uri_rdfs_domain, uri_rdfs_range, X), ic(uri_rdfs_Statement), icext(X, uri_rdfs_range), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  688: ifeq(iext(uri_rdfs_domain, uri_rdfs_range, X), ic(uri_rdfs_Statement), icext(X, uri_rdfs_seeAlso), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  689: ifeq(iext(uri_rdfs_domain, uri_rdfs_range, X), ic(uri_rdfs_Statement), icext(X, uri_rdfs_subClassOf), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  690: ifeq(iext(uri_rdfs_domain, uri_rdfs_range, X), ic(uri_rdfs_Statement), icext(X, uri_rdfs_subPropertyOf), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  691: ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, X), ic(uri_rdfs_Statement), icext(X, uri_ex_Person), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  692: ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, X), ic(uri_rdfs_Statement), icext(X, uri_rdf_Alt), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  693: ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, X), ic(uri_rdfs_Statement), icext(X, uri_rdf_Bag), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  694: ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, X), ic(uri_rdfs_Statement), icext(X, uri_rdf_XMLLiteral), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  695: ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, X), ic(uri_rdfs_Statement), icext(X, uri_rdfs_ContainerMembershipProperty), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  696: ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, X), ic(uri_rdfs_Statement), icext(X, uri_rdfs_Datatype), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  697: ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, X), ic(uri_rdfs_Statement), icext(X, uri_rdfs_Seq), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  698: ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, X), ic(uri_rdfs_Statement), icext(X, uri_rdfs_isDefinedBy), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  699: ifeq(iext(uri_rdfs_domain, uri_rdf_type, X), ic(uri_rdfs_Statement), icext(X, Y), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  700: ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, X), ic(uri_rdfs_Statement), icext(X, uri_owl_minCardinality), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  701: ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, X), ic(uri_rdfs_Statement), icext(X, uri_rdfs_Container), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  702: ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, X), ic(uri_rdfs_Statement), icext(X, uri_rdfs_Class), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  703: ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, X), ic(uri_rdfs_Statement), icext(X, uri_ex_hasAncestor), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  704: ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, X), ic(uri_rdfs_Statement), icext(X, uri_rdf_Property), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  705: ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, X), ic(uri_rdfs_Statement), icext(X, uri_rdf__2), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  706: ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, X), ic(uri_rdfs_Statement), icext(X, uri_rdf__1), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  707: ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, X), ic(uri_rdfs_Statement), icext(X, uri_rdf__3), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  708: ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, X), ic(uri_rdfs_Statement), icext(X, uri_rdf_first), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  709: ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, X), ic(uri_rdfs_Statement), icext(X, uri_rdf_object), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  710: ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, X), ic(uri_rdfs_Statement), icext(X, uri_rdf_type), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  711: ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, X), ic(uri_rdfs_Statement), icext(X, uri_rdf_rest), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  712: ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, X), ic(uri_rdfs_Statement), icext(X, uri_rdf_subject), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  713: ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, X), ic(uri_rdfs_Statement), icext(X, uri_rdf_value), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  714: ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, X), ic(uri_rdfs_Statement), icext(X, uri_rdfs_domain), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  715: ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, X), ic(uri_rdfs_Statement), icext(X, uri_rdfs_range), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  716: ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, X), ic(uri_rdfs_Statement), icext(X, uri_rdfs_seeAlso), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  717: ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, X), ic(uri_rdfs_Statement), icext(X, uri_rdfs_subClassOf), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  718: ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, X), ic(uri_rdfs_Statement), icext(X, uri_rdfs_subPropertyOf), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  719: ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, X), ic(uri_rdfs_Statement), icext(X, uri_owl_onProperty), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  720: ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, X), ic(uri_rdfs_Statement), icext(X, uri_rdfs_Literal), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  721: ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, X), ic(uri_rdfs_Statement), icext(X, sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  722: ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, X), ic(uri_rdfs_Statement), icext(X, uri_rdfs_label), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  723: ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, X), ic(uri_rdfs_Statement), icext(X, uri_rdfs_comment), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  724: ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, X), ic(uri_rdfs_Statement), icext(X, uri_rdf_predicate), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  725: ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, X), ic(uri_rdfs_Statement), icext(X, uri_rdfs_Resource), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  726: ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, X), ic(uri_rdfs_Statement), icext(X, uri_owl_TransitiveProperty), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  727: ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, X), ic(uri_rdfs_Statement), icext(X, uri_owl_Restriction), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  728: ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, X), ic(uri_rdfs_Statement), icext(X, uri_rdfs_member), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  729: ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, X), ic(uri_rdfs_Statement), icext(X, uri_rdf_List), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  730: ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, X), ic(uri_rdfs_Statement), icext(X, uri_rdfs_Statement), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  731: ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, X), ic(uri_rdfs_Statement), icext(X, uri_rdfs_comment), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  732: ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, X), ic(uri_rdfs_Statement), icext(X, uri_rdf_predicate), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  733: ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, X), ic(uri_rdfs_Statement), icext(X, uri_rdf_predicate), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  734: ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, X), ic(uri_rdfs_Statement), icext(X, uri_rdfs_comment), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  735: ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, X), ic(uri_rdfs_Statement), icext(X, uri_rdfs_label), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  736: ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, X), ic(uri_rdfs_Statement), icext(X, uri_rdfs_label), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  738: ifeq(iext(uri_rdfs_subPropertyOf, X, Y), ic(uri_rdfs_Statement), ifeq(iext(X, Z, W), ic(uri_rdfs_Statement), iext(Y, Z, W), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  739: ifeq(iext(uri_rdfs_isDefinedBy, X, Y), ic(uri_rdfs_Statement), iext(uri_rdfs_seeAlso, X, Y), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  740: ifeq(iext(uri_rdfs_subPropertyOf, uri_ex_hasAncestor, X), ic(uri_rdfs_Statement), iext(X, uri_ex_alice, uri_ex_bob), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  741: ifeq(iext(uri_rdfs_subPropertyOf, uri_owl_onProperty, X), ic(uri_rdfs_Statement), iext(X, sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z, uri_ex_hasAncestor), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  742: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, X), ic(uri_rdfs_Statement), iext(X, sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z, uri_owl_Restriction), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  743: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, X), ic(uri_rdfs_Statement), iext(X, uri_ex_alice, uri_ex_Person), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  744: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, X), ic(uri_rdfs_Statement), iext(X, uri_ex_bob, uri_ex_Person), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  745: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, X), ic(uri_rdfs_Statement), iext(X, uri_ex_hasAncestor, uri_owl_TransitiveProperty), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  746: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, X), ic(uri_rdfs_Statement), iext(X, uri_rdf_Property, uri_rdfs_Class), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  747: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, X), ic(uri_rdfs_Statement), iext(X, uri_rdf_XMLLiteral, uri_rdfs_Datatype), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  748: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, X), ic(uri_rdfs_Statement), iext(X, uri_rdf__1, uri_rdf_Property), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  749: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, X), ic(uri_rdfs_Statement), iext(X, uri_rdf__1, uri_rdfs_ContainerMembershipProperty), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  750: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, X), ic(uri_rdfs_Statement), iext(X, uri_rdf__2, uri_rdf_Property), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  751: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, X), ic(uri_rdfs_Statement), iext(X, uri_rdf__2, uri_rdfs_ContainerMembershipProperty), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  752: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, X), ic(uri_rdfs_Statement), iext(X, uri_rdf__3, uri_rdf_Property), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  753: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, X), ic(uri_rdfs_Statement), iext(X, uri_rdf__3, uri_rdfs_ContainerMembershipProperty), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  754: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, X), ic(uri_rdfs_Statement), iext(X, uri_rdf_first, uri_rdf_Property), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  755: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, X), ic(uri_rdfs_Statement), iext(X, uri_rdf_nil, uri_rdf_List), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  756: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, X), ic(uri_rdfs_Statement), iext(X, uri_rdf_object, uri_rdf_Property), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  757: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, X), ic(uri_rdfs_Statement), iext(X, uri_rdf_rest, uri_rdf_Property), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  758: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, X), ic(uri_rdfs_Statement), iext(X, uri_rdf_subject, uri_rdf_Property), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  759: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, X), ic(uri_rdfs_Statement), iext(X, uri_rdf_type, uri_rdf_Property), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  760: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, X), ic(uri_rdfs_Statement), iext(X, uri_rdf_value, uri_rdf_Property), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  761: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, X), ic(uri_rdfs_Statement), iext(X, uri_rdf__1, uri_rdfs_Resource), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  762: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, X), ic(uri_rdfs_Statement), iext(X, uri_rdf__2, uri_rdfs_Resource), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  763: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, X), ic(uri_rdfs_Statement), iext(X, uri_rdf__3, uri_rdfs_Resource), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  764: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, X), ic(uri_rdfs_Statement), iext(X, uri_rdf_first, uri_rdf_List), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  765: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, X), ic(uri_rdfs_Statement), iext(X, uri_rdf_object, uri_rdfs_Statement), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  766: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, X), ic(uri_rdfs_Statement), iext(X, uri_rdf_predicate, uri_rdfs_Statement), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  767: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, X), ic(uri_rdfs_Statement), iext(X, uri_rdf_rest, uri_rdf_List), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  768: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, X), ic(uri_rdfs_Statement), iext(X, uri_rdf_subject, uri_rdfs_Statement), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  769: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, X), ic(uri_rdfs_Statement), iext(X, uri_rdf_type, uri_rdfs_Resource), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  770: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, X), ic(uri_rdfs_Statement), iext(X, uri_rdf_value, uri_rdfs_Resource), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  771: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, X), ic(uri_rdfs_Statement), iext(X, uri_rdfs_comment, uri_rdfs_Resource), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  772: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, X), ic(uri_rdfs_Statement), iext(X, uri_rdfs_domain, uri_rdf_Property), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  773: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, X), ic(uri_rdfs_Statement), iext(X, uri_rdfs_isDefinedBy, uri_rdfs_Resource), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  774: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, X), ic(uri_rdfs_Statement), iext(X, uri_rdfs_label, uri_rdfs_Resource), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  775: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, X), ic(uri_rdfs_Statement), iext(X, uri_rdfs_member, uri_rdfs_Resource), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  776: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, X), ic(uri_rdfs_Statement), iext(X, uri_rdfs_range, uri_rdf_Property), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  777: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, X), ic(uri_rdfs_Statement), iext(X, uri_rdfs_seeAlso, uri_rdfs_Resource), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  778: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, X), ic(uri_rdfs_Statement), iext(X, uri_rdfs_subClassOf, uri_rdfs_Class), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  779: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, X), ic(uri_rdfs_Statement), iext(X, uri_rdfs_subPropertyOf, uri_rdf_Property), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  780: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, X), ic(uri_rdfs_Statement), iext(X, uri_rdf__1, uri_rdfs_Resource), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  781: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, X), ic(uri_rdfs_Statement), iext(X, uri_rdf__2, uri_rdfs_Resource), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  782: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, X), ic(uri_rdfs_Statement), iext(X, uri_rdf__3, uri_rdfs_Resource), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  783: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, X), ic(uri_rdfs_Statement), iext(X, uri_rdf_first, uri_rdfs_Resource), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  784: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, X), ic(uri_rdfs_Statement), iext(X, uri_rdf_predicate, uri_rdfs_Resource), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  785: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, X), ic(uri_rdfs_Statement), iext(X, uri_rdf_rest, uri_rdf_List), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  786: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, X), ic(uri_rdfs_Statement), iext(X, uri_rdf_subject, uri_rdfs_Resource), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  787: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, X), ic(uri_rdfs_Statement), iext(X, uri_rdf_type, uri_rdfs_Class), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  788: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, X), ic(uri_rdfs_Statement), iext(X, uri_rdf_value, uri_rdfs_Resource), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  789: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, X), ic(uri_rdfs_Statement), iext(X, uri_rdfs_comment, uri_rdfs_Literal), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  790: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, X), ic(uri_rdfs_Statement), iext(X, uri_rdfs_domain, uri_rdfs_Class), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  791: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, X), ic(uri_rdfs_Statement), iext(X, uri_rdfs_isDefinedBy, uri_rdfs_Resource), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  792: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, X), ic(uri_rdfs_Statement), iext(X, uri_rdfs_label, uri_rdfs_Literal), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  793: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, X), ic(uri_rdfs_Statement), iext(X, uri_rdfs_member, uri_rdfs_Resource), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  794: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, X), ic(uri_rdfs_Statement), iext(X, uri_rdfs_range, uri_rdfs_Class), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  795: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, X), ic(uri_rdfs_Statement), iext(X, uri_rdfs_seeAlso, uri_rdfs_Resource), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  796: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, X), ic(uri_rdfs_Statement), iext(X, uri_rdfs_subClassOf, uri_rdfs_Class), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  797: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, X), ic(uri_rdfs_Statement), iext(X, uri_rdfs_subPropertyOf, uri_rdf_Property), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  798: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, X), ic(uri_rdfs_Statement), iext(X, uri_ex_Person, sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  799: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, X), ic(uri_rdfs_Statement), iext(X, uri_rdf_Alt, uri_rdfs_Container), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  800: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, X), ic(uri_rdfs_Statement), iext(X, uri_rdf_Bag, uri_rdfs_Container), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  801: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, X), ic(uri_rdfs_Statement), iext(X, uri_rdf_XMLLiteral, uri_rdfs_Literal), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  802: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, X), ic(uri_rdfs_Statement), iext(X, uri_rdfs_ContainerMembershipProperty, uri_rdf_Property), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  803: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, X), ic(uri_rdfs_Statement), iext(X, uri_rdfs_Datatype, uri_rdfs_Class), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  804: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, X), ic(uri_rdfs_Statement), iext(X, uri_rdfs_Seq, uri_rdfs_Container), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  805: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, X), ic(uri_rdfs_Statement), iext(X, uri_rdfs_isDefinedBy, uri_rdfs_seeAlso), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  806: ifeq(iext(uri_owl_minCardinality, X, Y), ic(uri_rdfs_Statement), iext(uri_owl_minCardinality, X, Y), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  807: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, X), ic(uri_rdfs_Statement), iext(X, Y, uri_rdfs_Resource), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  808: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, X), ic(uri_rdfs_Statement), iext(X, uri_rdfs_Container, uri_rdfs_Container), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  809: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, X), ic(uri_rdfs_Statement), iext(X, uri_rdfs_Container, uri_rdfs_Resource), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  810: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, X), ic(uri_rdfs_Statement), iext(X, uri_owl_minCardinality, uri_owl_minCardinality), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  811: ifeq(iext(uri_ex_hasAncestor, X, Y), ic(uri_rdfs_Statement), iext(uri_ex_hasAncestor, X, Y), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  812: ifeq(iext(uri_rdfs_range, X, Y), ic(uri_rdfs_Statement), iext(uri_rdfs_range, X, Y), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  813: ifeq(iext(uri_rdfs_seeAlso, X, Y), ic(uri_rdfs_Statement), iext(uri_rdfs_seeAlso, X, Y), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  814: ifeq(iext(uri_rdfs_subPropertyOf, X, Y), ic(uri_rdfs_Statement), iext(uri_rdfs_subPropertyOf, X, Y), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  815: ifeq(iext(uri_rdfs_subClassOf, X, Y), ic(uri_rdfs_Statement), iext(uri_rdfs_subClassOf, X, Y), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  816: ifeq(iext(uri_rdf__2, X, Y), ic(uri_rdfs_Statement), iext(uri_rdf__2, X, Y), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  817: ifeq(iext(uri_rdf_subject, X, Y), ic(uri_rdfs_Statement), iext(uri_rdf_subject, X, Y), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  818: ifeq(iext(uri_rdfs_domain, X, Y), ic(uri_rdfs_Statement), iext(uri_rdfs_domain, X, Y), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  819: ifeq(iext(uri_rdfs_isDefinedBy, X, Y), ic(uri_rdfs_Statement), iext(uri_rdfs_isDefinedBy, X, Y), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  820: ifeq(iext(uri_rdf_value, X, Y), ic(uri_rdfs_Statement), iext(uri_rdf_value, X, Y), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  821: ifeq(iext(uri_rdf_type, X, Y), ic(uri_rdfs_Statement), iext(uri_rdf_type, X, Y), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  822: ifeq(iext(uri_rdf__1, X, Y), ic(uri_rdfs_Statement), iext(uri_rdf__1, X, Y), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  823: ifeq(iext(uri_owl_onProperty, X, Y), ic(uri_rdfs_Statement), iext(uri_owl_onProperty, X, Y), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  824: ifeq(iext(uri_rdf__1, X, Y), ic(uri_rdfs_Statement), iext(uri_rdfs_member, X, Y), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  825: ifeq(iext(uri_rdf__3, X, Y), ic(uri_rdfs_Statement), iext(uri_rdfs_member, X, Y), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  826: ifeq(iext(uri_rdf__2, X, Y), ic(uri_rdfs_Statement), iext(uri_rdfs_member, X, Y), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  827: ifeq(iext(uri_rdf__3, X, Y), ic(uri_rdfs_Statement), iext(uri_rdf__3, X, Y), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  828: ifeq(iext(uri_rdf_first, X, Y), ic(uri_rdfs_Statement), iext(uri_rdf_first, X, Y), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  829: ifeq(iext(uri_rdf_rest, X, Y), ic(uri_rdfs_Statement), iext(uri_rdf_rest, X, Y), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  830: ifeq(iext(uri_rdf_object, X, Y), ic(uri_rdfs_Statement), iext(uri_rdf_object, X, Y), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  831: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, X), ic(uri_rdfs_Statement), iext(X, uri_rdfs_Literal, uri_rdfs_Resource), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  832: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, X), ic(uri_rdfs_Statement), iext(X, uri_rdfs_Datatype, uri_rdfs_Resource), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  833: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, X), ic(uri_rdfs_Statement), iext(X, uri_rdfs_Datatype, uri_rdfs_Datatype), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  834: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, X), ic(uri_rdfs_Statement), iext(X, uri_rdfs_Literal, uri_rdfs_Literal), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  835: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, X), ic(uri_rdfs_Statement), iext(X, uri_rdfs_Seq, uri_rdfs_Resource), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  836: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, X), ic(uri_rdfs_Statement), iext(X, uri_rdfs_Seq, uri_rdfs_Seq), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  837: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, X), ic(uri_rdfs_Statement), iext(X, uri_owl_onProperty, uri_rdf_Property), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  838: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, X), ic(uri_rdfs_Statement), iext(X, uri_owl_minCardinality, uri_rdf_Property), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  839: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, X), ic(uri_rdfs_Statement), iext(X, uri_ex_hasAncestor, uri_rdf_Property), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  840: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, X), ic(uri_rdfs_Statement), iext(X, uri_ex_hasAncestor, uri_ex_hasAncestor), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  841: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, X), ic(uri_rdfs_Statement), iext(X, uri_rdf__1, uri_rdf__1), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  842: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, X), ic(uri_rdfs_Statement), iext(X, uri_owl_onProperty, uri_owl_onProperty), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  843: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, X), ic(uri_rdfs_Statement), iext(X, uri_rdf__1, uri_rdfs_member), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  844: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, X), ic(uri_rdfs_Statement), iext(X, uri_rdfs_ContainerMembershipProperty, uri_rdfs_ContainerMembershipProperty), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  845: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, X), ic(uri_rdfs_Statement), iext(X, uri_rdfs_ContainerMembershipProperty, uri_rdfs_Resource), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  846: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, X), ic(uri_rdfs_Statement), iext(X, uri_rdfs_Class, uri_rdfs_Class), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  847: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, X), ic(uri_rdfs_Statement), iext(X, uri_rdf_XMLLiteral, uri_rdfs_Resource), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  848: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, X), ic(uri_rdfs_Statement), iext(X, uri_rdfs_Class, uri_rdfs_Resource), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  849: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, X), ic(uri_rdfs_Statement), iext(X, uri_rdf_Bag, uri_rdfs_Resource), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  850: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, X), ic(uri_rdfs_Statement), iext(X, uri_rdf_Property, uri_rdfs_Resource), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  851: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, X), ic(uri_rdfs_Statement), iext(X, uri_rdf_XMLLiteral, uri_rdf_XMLLiteral), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  852: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, X), ic(uri_rdfs_Statement), iext(X, uri_rdf_Property, uri_rdf_Property), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  853: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, X), ic(uri_rdfs_Statement), iext(X, uri_rdf_Alt, uri_rdfs_Resource), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  854: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, X), ic(uri_rdfs_Statement), iext(X, uri_rdf_Bag, uri_rdf_Bag), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  855: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, X), ic(uri_rdfs_Statement), iext(X, uri_rdf__3, uri_rdfs_member), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  856: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, X), ic(uri_rdfs_Statement), iext(X, uri_rdf__3, uri_rdf__3), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  857: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, X), ic(uri_rdfs_Statement), iext(X, uri_rdf__2, uri_rdf__2), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  858: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, X), ic(uri_rdfs_Statement), iext(X, uri_rdf__2, uri_rdfs_member), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  859: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, X), ic(uri_rdfs_Statement), iext(X, uri_rdf_first, uri_rdf_first), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  860: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, X), ic(uri_rdfs_Statement), iext(X, uri_rdf_rest, uri_rdf_rest), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  861: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, X), ic(uri_rdfs_Statement), iext(X, uri_rdf_object, uri_rdf_object), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  862: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, X), ic(uri_rdfs_Statement), iext(X, uri_rdf_value, uri_rdf_value), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  863: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, X), ic(uri_rdfs_Statement), iext(X, uri_rdf_type, uri_rdf_type), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  864: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, X), ic(uri_rdfs_Statement), iext(X, uri_rdf_subject, uri_rdf_subject), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  865: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, X), ic(uri_rdfs_Statement), iext(X, uri_rdfs_isDefinedBy, uri_rdfs_isDefinedBy), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  866: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, X), ic(uri_rdfs_Statement), iext(X, uri_rdfs_domain, uri_rdfs_domain), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  867: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, X), ic(uri_rdfs_Statement), iext(X, uri_rdfs_range, uri_rdfs_range), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  868: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, X), ic(uri_rdfs_Statement), iext(X, uri_rdfs_seeAlso, uri_rdfs_seeAlso), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  869: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, X), ic(uri_rdfs_Statement), iext(X, uri_rdfs_subClassOf, uri_rdfs_subClassOf), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  870: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, X), ic(uri_rdfs_Statement), iext(X, uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  871: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, X), ic(uri_rdfs_Statement), iext(X, uri_ex_Person, uri_rdfs_Resource), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  872: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, X), ic(uri_rdfs_Statement), iext(X, uri_rdf_Alt, uri_rdf_Alt), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  873: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, X), ic(uri_rdfs_Statement), iext(X, sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z, sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  874: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, X), ic(uri_rdfs_Statement), iext(X, uri_ex_Person, uri_ex_Person), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  875: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, X), ic(uri_rdfs_Statement), iext(X, sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z, uri_rdfs_Resource), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  876: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, X), ic(uri_rdfs_Statement), iext(X, uri_rdfs_subPropertyOf, uri_rdf_Property), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  877: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, X), ic(uri_rdfs_Statement), iext(X, uri_rdfs_range, uri_rdf_Property), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  878: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, X), ic(uri_rdfs_Statement), iext(X, uri_rdfs_seeAlso, uri_rdf_Property), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  879: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, X), ic(uri_rdfs_Statement), iext(X, uri_rdfs_subClassOf, uri_rdf_Property), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  880: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, X), ic(uri_rdfs_Statement), iext(X, uri_rdfs_domain, uri_rdf_Property), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  881: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, X), ic(uri_rdfs_Statement), iext(X, uri_rdfs_isDefinedBy, uri_rdf_Property), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  882: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, X), ic(uri_rdfs_Statement), iext(X, uri_rdfs_label, uri_rdf_Property), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  883: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, X), ic(uri_rdfs_Statement), iext(X, uri_rdfs_Seq, uri_rdfs_Class), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  884: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, X), ic(uri_rdfs_Statement), iext(X, uri_rdfs_Statement, uri_rdfs_Class), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  885: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, X), ic(uri_rdfs_Statement), iext(X, uri_rdfs_comment, uri_rdf_Property), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  886: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, X), ic(uri_rdfs_Statement), iext(X, uri_rdfs_Literal, uri_rdfs_Class), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  887: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, X), ic(uri_rdfs_Statement), iext(X, uri_rdfs_Datatype, uri_rdfs_Class), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  888: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, X), ic(uri_rdfs_Statement), iext(X, sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z, uri_rdfs_Class), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  889: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, X), ic(uri_rdfs_Statement), iext(X, uri_owl_TransitiveProperty, uri_rdfs_Class), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  890: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, X), ic(uri_rdfs_Statement), iext(X, uri_rdf_Bag, uri_rdfs_Class), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  891: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, X), ic(uri_rdfs_Statement), iext(X, uri_rdf_List, uri_rdfs_Class), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  892: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, X), ic(uri_rdfs_Statement), iext(X, uri_rdfs_Resource, uri_rdfs_Resource), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  893: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, X), ic(uri_rdfs_Statement), iext(X, uri_rdf_XMLLiteral, uri_rdfs_Class), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  894: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, X), ic(uri_rdfs_Statement), iext(X, uri_rdf_predicate, uri_rdf_Property), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  895: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, X), ic(uri_rdfs_Statement), iext(X, uri_rdfs_ContainerMembershipProperty, uri_rdfs_Class), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  896: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, X), ic(uri_rdfs_Statement), iext(X, uri_rdfs_Class, uri_rdfs_Class), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  897: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, X), ic(uri_rdfs_Statement), iext(X, uri_ex_bob, sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  898: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, X), ic(uri_rdfs_Statement), iext(X, uri_rdf_Alt, uri_rdfs_Class), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  899: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, X), ic(uri_rdfs_Statement), iext(X, uri_ex_Person, uri_rdfs_Class), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  900: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, X), ic(uri_rdfs_Statement), iext(X, uri_owl_Restriction, uri_rdfs_Class), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  901: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, X), ic(uri_rdfs_Statement), iext(X, uri_ex_alice, sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  902: ifeq(iext(uri_rdfs_member, X, Y), ic(uri_rdfs_Statement), iext(uri_rdfs_member, X, Y), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  903: ifeq(iext(uri_rdfs_subPropertyOf, uri_owl_minCardinality, X), ic(uri_rdfs_Statement), iext(X, sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z, literal_typed(dat_str_1, uri_xsd_nonNegativeInteger)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  904: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, X), ic(uri_rdfs_Statement), iext(X, uri_rdfs_Container, uri_rdfs_Class), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  905: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, X), ic(uri_rdfs_Statement), iext(X, uri_rdf_List, uri_rdf_List), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  906: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, X), ic(uri_rdfs_Statement), iext(X, uri_rdf_List, uri_rdfs_Resource), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  907: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, X), ic(uri_rdfs_Statement), iext(X, uri_rdfs_member, uri_rdf_Property), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  908: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, X), ic(uri_rdfs_Statement), iext(X, uri_rdfs_Resource, uri_rdfs_Class), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  909: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, X), ic(uri_rdfs_Statement), iext(X, uri_owl_TransitiveProperty, uri_rdfs_Resource), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  910: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, X), ic(uri_rdfs_Statement), iext(X, uri_owl_Restriction, uri_rdfs_Resource), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  911: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, X), ic(uri_rdfs_Statement), iext(X, uri_owl_Restriction, uri_owl_Restriction), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  912: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, X), ic(uri_rdfs_Statement), iext(X, uri_owl_TransitiveProperty, uri_owl_TransitiveProperty), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  913: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, X), ic(uri_rdfs_Statement), iext(X, uri_rdfs_member, uri_rdfs_member), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  914: ifeq(iext(uri_rdfs_comment, X, Y), ic(uri_rdfs_Statement), iext(uri_rdfs_comment, X, Y), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  915: ifeq(iext(uri_rdfs_label, X, Y), ic(uri_rdfs_Statement), iext(uri_rdfs_label, X, Y), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  916: ifeq(iext(uri_rdf_predicate, X, Y), ic(uri_rdfs_Statement), iext(uri_rdf_predicate, X, Y), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  917: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, X), ic(uri_rdfs_Statement), iext(X, uri_rdfs_label, uri_rdfs_label), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  918: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, X), ic(uri_rdfs_Statement), iext(X, uri_rdfs_comment, uri_rdfs_comment), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  919: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, X), ic(uri_rdfs_Statement), iext(X, uri_rdf_predicate, uri_rdf_predicate), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  920: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, X), ic(uri_rdfs_Statement), iext(X, uri_rdfs_Statement, uri_rdfs_Statement), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  921: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, X), ic(uri_rdfs_Statement), iext(X, uri_rdfs_Statement, uri_rdfs_Resource), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  922: eq(tuple(iext(uri_ex_hasAncestor, uri_ex_alice, X), iext(uri_ex_hasAncestor, uri_ex_bob, X)), tuple(ic(uri_rdfs_Statement), ic(uri_rdfs_Statement))) -> false
% 25.61/25.25  924: ifeq(iext(uri_rdfs_subPropertyOf, X, Y), ic(uri_rdfs_Statement), ifeq(iext(uri_rdfs_subPropertyOf, Z, X), ic(uri_rdfs_Statement), iext(uri_rdfs_subPropertyOf, Z, Y), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  925: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_isDefinedBy), ic(uri_rdfs_Statement), iext(uri_rdfs_subPropertyOf, X, uri_rdfs_seeAlso), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  926: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_seeAlso, X), ic(uri_rdfs_Statement), iext(uri_rdfs_subPropertyOf, uri_rdfs_isDefinedBy, X), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  927: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdf__2), ic(uri_rdfs_Statement), iext(uri_rdfs_subPropertyOf, X, uri_rdfs_member), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  928: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_member, X), ic(uri_rdfs_Statement), iext(uri_rdfs_subPropertyOf, uri_rdf__1, X), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  929: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdf__3), ic(uri_rdfs_Statement), iext(uri_rdfs_subPropertyOf, X, uri_rdfs_member), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  930: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdf__1), ic(uri_rdfs_Statement), iext(uri_rdfs_subPropertyOf, X, uri_rdfs_member), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  931: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_member, X), ic(uri_rdfs_Statement), iext(uri_rdfs_subPropertyOf, uri_rdf__3, X), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  932: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_member, X), ic(uri_rdfs_Statement), iext(uri_rdfs_subPropertyOf, uri_rdf__2, X), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  934: ifeq(iext(uri_rdfs_subClassOf, X, Y), ic(uri_rdfs_Statement), ifeq(iext(uri_rdfs_subClassOf, Z, X), ic(uri_rdfs_Statement), iext(uri_rdfs_subClassOf, Z, Y), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  935: ifeq(iext(uri_rdfs_subClassOf, X, uri_ex_Person), ic(uri_rdfs_Statement), iext(uri_rdfs_subClassOf, X, sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  936: ifeq(iext(uri_rdfs_subClassOf, X, uri_rdf_Alt), ic(uri_rdfs_Statement), iext(uri_rdfs_subClassOf, X, uri_rdfs_Container), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  937: ifeq(iext(uri_rdfs_subClassOf, X, uri_rdf_Bag), ic(uri_rdfs_Statement), iext(uri_rdfs_subClassOf, X, uri_rdfs_Container), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  938: ifeq(iext(uri_rdfs_subClassOf, X, uri_rdf_XMLLiteral), ic(uri_rdfs_Statement), iext(uri_rdfs_subClassOf, X, uri_rdfs_Literal), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  939: ifeq(iext(uri_rdfs_subClassOf, X, uri_rdfs_ContainerMembershipProperty), ic(uri_rdfs_Statement), iext(uri_rdfs_subClassOf, X, uri_rdf_Property), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  940: ifeq(iext(uri_rdfs_subClassOf, X, uri_rdfs_Datatype), ic(uri_rdfs_Statement), iext(uri_rdfs_subClassOf, X, uri_rdfs_Class), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  941: ifeq(iext(uri_rdfs_subClassOf, X, uri_rdfs_Seq), ic(uri_rdfs_Statement), iext(uri_rdfs_subClassOf, X, uri_rdfs_Container), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  942: ifeq(iext(uri_rdfs_subClassOf, sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z, X), ic(uri_rdfs_Statement), iext(uri_rdfs_subClassOf, uri_ex_Person, X), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  943: ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Container, X), ic(uri_rdfs_Statement), iext(uri_rdfs_subClassOf, uri_rdf_Alt, X), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  944: ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Container, X), ic(uri_rdfs_Statement), iext(uri_rdfs_subClassOf, uri_rdf_Bag, X), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  945: ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Literal, X), ic(uri_rdfs_Statement), iext(uri_rdfs_subClassOf, uri_rdf_XMLLiteral, X), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  946: ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, X), ic(uri_rdfs_Statement), iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, X), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  947: ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, X), ic(uri_rdfs_Statement), iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, X), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  948: ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Container, X), ic(uri_rdfs_Statement), iext(uri_rdfs_subClassOf, uri_rdfs_Seq, X), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  949: ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Resource, X), ic(uri_rdfs_Statement), iext(uri_rdfs_subClassOf, uri_rdfs_Container, X), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  950: ifeq(iext(uri_rdfs_subClassOf, X, uri_rdfs_Container), ic(uri_rdfs_Statement), iext(uri_rdfs_subClassOf, X, uri_rdfs_Resource), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  951: ifeq(iext(uri_rdfs_subClassOf, X, uri_rdfs_ContainerMembershipProperty), ic(uri_rdfs_Statement), iext(uri_rdfs_subClassOf, X, uri_rdfs_Resource), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  952: ifeq(iext(uri_rdfs_subClassOf, X, uri_rdfs_Class), ic(uri_rdfs_Statement), iext(uri_rdfs_subClassOf, X, uri_rdfs_Resource), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  953: ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Resource, X), ic(uri_rdfs_Statement), iext(uri_rdfs_subClassOf, sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z, X), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  954: ifeq(iext(uri_rdfs_subClassOf, X, uri_rdfs_Datatype), ic(uri_rdfs_Statement), iext(uri_rdfs_subClassOf, X, uri_rdfs_Resource), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  955: ifeq(iext(uri_rdfs_subClassOf, X, uri_rdfs_Literal), ic(uri_rdfs_Statement), iext(uri_rdfs_subClassOf, X, uri_rdfs_Resource), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  956: ifeq(iext(uri_rdfs_subClassOf, X, uri_rdfs_Seq), ic(uri_rdfs_Statement), iext(uri_rdfs_subClassOf, X, uri_rdfs_Resource), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  957: ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Resource, X), ic(uri_rdfs_Statement), iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, X), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  958: ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Resource, X), ic(uri_rdfs_Statement), iext(uri_rdfs_subClassOf, uri_rdfs_Class, X), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  959: ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Resource, X), ic(uri_rdfs_Statement), iext(uri_rdfs_subClassOf, uri_rdfs_Literal, X), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  960: ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Resource, X), ic(uri_rdfs_Statement), iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, X), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  961: ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Resource, X), ic(uri_rdfs_Statement), iext(uri_rdfs_subClassOf, uri_rdfs_Seq, X), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  962: ifeq(iext(uri_rdfs_subClassOf, X, uri_rdf_Alt), ic(uri_rdfs_Statement), iext(uri_rdfs_subClassOf, X, uri_rdfs_Resource), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  963: ifeq(iext(uri_rdfs_subClassOf, X, uri_rdf_Bag), ic(uri_rdfs_Statement), iext(uri_rdfs_subClassOf, X, uri_rdfs_Resource), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  964: ifeq(iext(uri_rdfs_subClassOf, X, uri_rdf_Property), ic(uri_rdfs_Statement), iext(uri_rdfs_subClassOf, X, uri_rdfs_Resource), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  965: ifeq(iext(uri_rdfs_subClassOf, X, uri_rdf_XMLLiteral), ic(uri_rdfs_Statement), iext(uri_rdfs_subClassOf, X, uri_rdfs_Resource), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  966: ifeq(iext(uri_rdfs_subClassOf, X, sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z), ic(uri_rdfs_Statement), iext(uri_rdfs_subClassOf, X, uri_rdfs_Resource), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  967: ifeq(iext(uri_rdfs_subClassOf, X, uri_ex_Person), ic(uri_rdfs_Statement), iext(uri_rdfs_subClassOf, X, uri_rdfs_Resource), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  968: ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Resource, X), ic(uri_rdfs_Statement), iext(uri_rdfs_subClassOf, uri_rdf_Alt, X), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  969: ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Resource, X), ic(uri_rdfs_Statement), iext(uri_rdfs_subClassOf, uri_rdf_Bag, X), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  970: ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Resource, X), ic(uri_rdfs_Statement), iext(uri_rdfs_subClassOf, uri_rdf_Property, X), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  971: ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Resource, X), ic(uri_rdfs_Statement), iext(uri_rdfs_subClassOf, uri_rdf_XMLLiteral, X), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  972: ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Resource, X), ic(uri_rdfs_Statement), iext(uri_rdfs_subClassOf, uri_ex_Person, X), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  973: ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Resource, X), ic(uri_rdfs_Statement), iext(uri_rdfs_subClassOf, uri_owl_Restriction, X), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  974: ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Resource, X), ic(uri_rdfs_Statement), iext(uri_rdfs_subClassOf, uri_owl_TransitiveProperty, X), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  975: ifeq(iext(uri_rdfs_subClassOf, X, uri_owl_Restriction), ic(uri_rdfs_Statement), iext(uri_rdfs_subClassOf, X, uri_rdfs_Resource), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  976: ifeq(iext(uri_rdfs_subClassOf, X, uri_owl_TransitiveProperty), ic(uri_rdfs_Statement), iext(uri_rdfs_subClassOf, X, uri_rdfs_Resource), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  977: ifeq(iext(uri_rdfs_subClassOf, X, uri_rdf_List), ic(uri_rdfs_Statement), iext(uri_rdfs_subClassOf, X, uri_rdfs_Resource), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  978: ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Resource, X), ic(uri_rdfs_Statement), iext(uri_rdfs_subClassOf, uri_rdf_List, X), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  979: ifeq(iext(uri_rdfs_subClassOf, X, uri_rdfs_Statement), ic(uri_rdfs_Statement), iext(uri_rdfs_subClassOf, X, uri_rdfs_Resource), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  980: ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Resource, X), ic(uri_rdfs_Statement), iext(uri_rdfs_subClassOf, uri_rdfs_Statement, X), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  981: ifeq(iext(uri_rdfs_range, X, uri_rdfs_Resource), ic(uri_rdfs_Statement), ifeq(iext(X, Y, Z), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  982: ifeq(iext(uri_rdfs_domain, X, uri_rdfs_Resource), ic(uri_rdfs_Statement), ifeq(iext(X, Y, Z), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  983: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_subPropertyOf), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdfs_isDefinedBy, uri_rdfs_seeAlso), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  984: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_owl_onProperty), ic(uri_rdfs_Statement), ifeq(iext(X, sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z, uri_ex_hasAncestor), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  985: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_ex_hasAncestor), ic(uri_rdfs_Statement), ifeq(iext(X, uri_ex_alice, uri_ex_bob), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  986: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdf_type), ic(uri_rdfs_Statement), ifeq(iext(X, sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z, uri_owl_Restriction), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  987: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_subClassOf), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdf_XMLLiteral, uri_rdfs_Literal), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  988: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_subClassOf), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdf_Bag, uri_rdfs_Container), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  989: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_subClassOf), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdfs_ContainerMembershipProperty, uri_rdf_Property), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  990: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_subClassOf), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdfs_Seq, uri_rdfs_Container), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  991: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_subClassOf), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdfs_Datatype, uri_rdfs_Class), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  992: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdf_type), ic(uri_rdfs_Statement), ifeq(iext(X, uri_ex_bob, uri_ex_Person), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  993: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdf_type), ic(uri_rdfs_Statement), ifeq(iext(X, uri_ex_hasAncestor, uri_owl_TransitiveProperty), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  994: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdf_type), ic(uri_rdfs_Statement), ifeq(iext(X, uri_ex_alice, uri_ex_Person), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  995: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdf_type), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdf_Property, uri_rdfs_Class), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  996: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdf_type), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdf__2, uri_rdf_Property), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  997: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdf_type), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdf_XMLLiteral, uri_rdfs_Datatype), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  998: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdf_type), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdf__1, uri_rdfs_ContainerMembershipProperty), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  999: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdf_type), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdf__1, uri_rdf_Property), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1000: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdf_type), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdf__2, uri_rdfs_ContainerMembershipProperty), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1001: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdf_type), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdf__3, uri_rdfs_ContainerMembershipProperty), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1002: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdf_type), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdf__3, uri_rdf_Property), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1003: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdf_type), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdf_first, uri_rdf_Property), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1004: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdf_type), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdf_rest, uri_rdf_Property), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1005: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdf_type), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdf_nil, uri_rdf_List), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1006: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdf_type), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdf_object, uri_rdf_Property), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1007: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdf_type), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdf_type, uri_rdf_Property), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1008: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdf_type), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdf_subject, uri_rdf_Property), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1009: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdf_type), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdf_value, uri_rdf_Property), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1010: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_domain), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdf__1, uri_rdfs_Resource), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1011: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_domain), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdf__2, uri_rdfs_Resource), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1012: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_domain), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdf_predicate, uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1013: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_domain), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdf_first, uri_rdf_List), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1014: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_domain), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdf_object, uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1015: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_domain), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdf__3, uri_rdfs_Resource), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1016: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_domain), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdf_rest, uri_rdf_List), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1017: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_domain), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdf_type, uri_rdfs_Resource), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1018: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_domain), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdf_subject, uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1019: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_domain), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdf_value, uri_rdfs_Resource), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1020: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_domain), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdfs_isDefinedBy, uri_rdfs_Resource), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1021: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_domain), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdfs_domain, uri_rdf_Property), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1022: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_domain), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdfs_comment, uri_rdfs_Resource), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1023: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_domain), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdfs_label, uri_rdfs_Resource), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1024: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_domain), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdfs_range, uri_rdf_Property), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1025: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_domain), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdfs_member, uri_rdfs_Resource), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1026: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_domain), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdfs_seeAlso, uri_rdfs_Resource), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1027: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_range), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdf__3, uri_rdfs_Resource), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1028: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_domain), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdfs_subPropertyOf, uri_rdf_Property), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1029: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_range), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdf__2, uri_rdfs_Resource), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1030: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_range), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdf__1, uri_rdfs_Resource), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1031: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_domain), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdfs_subClassOf, uri_rdfs_Class), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1032: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_range), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdf_first, uri_rdfs_Resource), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1033: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_range), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdf_rest, uri_rdf_List), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1034: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_range), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdf_predicate, uri_rdfs_Resource), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1035: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_range), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdf_subject, uri_rdfs_Resource), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1036: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_range), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdfs_comment, uri_rdfs_Literal), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1037: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_range), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdf_value, uri_rdfs_Resource), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1038: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_range), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdf_type, uri_rdfs_Class), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1039: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_range), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdfs_domain, uri_rdfs_Class), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1040: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_range), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdfs_label, uri_rdfs_Literal), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1041: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_range), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdfs_isDefinedBy, uri_rdfs_Resource), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1042: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_range), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdfs_member, uri_rdfs_Resource), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1043: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_range), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdfs_subPropertyOf, uri_rdf_Property), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1044: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_range), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdfs_seeAlso, uri_rdfs_Resource), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1045: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_range), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdfs_subClassOf, uri_rdfs_Class), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1046: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_range), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdfs_range, uri_rdfs_Class), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1047: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_subClassOf), ic(uri_rdfs_Statement), ifeq(iext(X, uri_ex_Person, sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1048: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_subClassOf), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdf_Alt, uri_rdfs_Container), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1049: ifeq(iext(uri_rdfs_range, X, uri_rdf_Property), ic(uri_rdfs_Statement), ifeq(iext(X, Y, uri_rdf_type), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1050: ifeq(iext(uri_rdfs_range, X, uri_rdfs_ContainerMembershipProperty), ic(uri_rdfs_Statement), ifeq(iext(X, Y, uri_rdf__3), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1051: ifeq(iext(uri_rdfs_range, X, uri_rdfs_Datatype), ic(uri_rdfs_Statement), ifeq(iext(X, Y, uri_rdf_XMLLiteral), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1052: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdf_type), ic(uri_rdfs_Statement), ifeq(iext(X, Y, uri_rdfs_Resource), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1053: ifeq(iext(uri_rdfs_domain, X, uri_owl_Restriction), ic(uri_rdfs_Statement), ifeq(iext(X, sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z, Y), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1054: ifeq(iext(uri_rdfs_domain, X, uri_ex_Person), ic(uri_rdfs_Statement), ifeq(iext(X, uri_ex_bob, Y), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1055: ifeq(iext(uri_rdfs_domain, X, uri_ex_Person), ic(uri_rdfs_Statement), ifeq(iext(X, uri_ex_alice, Y), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1056: ifeq(iext(uri_rdfs_domain, X, uri_owl_TransitiveProperty), ic(uri_rdfs_Statement), ifeq(iext(X, uri_ex_hasAncestor, Y), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1057: ifeq(iext(uri_rdfs_domain, X, uri_rdf_List), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdf_nil, Y), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1058: ifeq(iext(uri_rdfs_domain, X, uri_rdf_Property), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdf__2, Y), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1059: ifeq(iext(uri_rdfs_domain, X, uri_rdf_Property), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdf__3, Y), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1060: ifeq(iext(uri_rdfs_domain, X, uri_rdf_Property), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdf__1, Y), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1061: ifeq(iext(uri_rdfs_domain, X, uri_rdf_Property), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdf_object, Y), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1062: ifeq(iext(uri_rdfs_domain, X, uri_rdf_Property), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdf_first, Y), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1063: ifeq(iext(uri_rdfs_domain, X, uri_rdf_Property), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdf_rest, Y), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1064: ifeq(iext(uri_rdfs_domain, X, uri_rdf_Property), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdf_value, Y), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1065: ifeq(iext(uri_rdfs_domain, X, uri_rdf_Property), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdf_type, Y), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1066: ifeq(iext(uri_rdfs_domain, X, uri_rdf_Property), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdf_subject, Y), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1067: ifeq(iext(uri_rdfs_range, X, uri_rdfs_ContainerMembershipProperty), ic(uri_rdfs_Statement), ifeq(iext(X, Y, uri_rdf__1), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1068: ifeq(iext(uri_rdfs_range, X, uri_rdfs_ContainerMembershipProperty), ic(uri_rdfs_Statement), ifeq(iext(X, Y, uri_rdf__2), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1069: ifeq(iext(uri_rdfs_domain, X, uri_rdfs_ContainerMembershipProperty), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdf__1, Y), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1070: ifeq(iext(uri_rdfs_domain, X, uri_rdfs_ContainerMembershipProperty), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdf__3, Y), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1071: ifeq(iext(uri_rdfs_domain, X, uri_rdfs_ContainerMembershipProperty), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdf__2, Y), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1072: ifeq(iext(uri_rdfs_domain, X, uri_rdfs_Datatype), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdf_XMLLiteral, Y), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1073: ifeq(iext(uri_rdfs_range, X, uri_owl_TransitiveProperty), ic(uri_rdfs_Statement), ifeq(iext(X, Y, uri_ex_hasAncestor), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1074: ifeq(iext(uri_rdfs_range, X, uri_owl_Restriction), ic(uri_rdfs_Statement), ifeq(iext(X, Y, sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1075: ifeq(iext(uri_rdfs_range, X, uri_ex_Person), ic(uri_rdfs_Statement), ifeq(iext(X, Y, uri_ex_alice), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1076: ifeq(iext(uri_rdfs_range, X, uri_ex_Person), ic(uri_rdfs_Statement), ifeq(iext(X, Y, uri_ex_bob), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1077: ifeq(iext(uri_rdfs_range, X, uri_rdf_List), ic(uri_rdfs_Statement), ifeq(iext(X, Y, uri_rdf_nil), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1078: ifeq(iext(uri_rdfs_range, X, uri_rdf_Property), ic(uri_rdfs_Statement), ifeq(iext(X, Y, uri_rdf__3), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1079: ifeq(iext(uri_rdfs_range, X, uri_rdf_Property), ic(uri_rdfs_Statement), ifeq(iext(X, Y, uri_rdf__1), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1080: ifeq(iext(uri_rdfs_range, X, uri_rdf_Property), ic(uri_rdfs_Statement), ifeq(iext(X, Y, uri_rdf__2), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1081: ifeq(iext(uri_rdfs_range, X, uri_rdf_Property), ic(uri_rdfs_Statement), ifeq(iext(X, Y, uri_rdf_first), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1082: ifeq(iext(uri_rdfs_range, X, uri_rdf_Property), ic(uri_rdfs_Statement), ifeq(iext(X, Y, uri_rdf_rest), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1083: ifeq(iext(uri_rdfs_range, X, uri_rdf_Property), ic(uri_rdfs_Statement), ifeq(iext(X, Y, uri_rdf_object), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1084: ifeq(iext(uri_rdfs_range, X, uri_rdf_Property), ic(uri_rdfs_Statement), ifeq(iext(X, Y, uri_rdf_subject), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1085: ifeq(iext(uri_rdfs_range, X, uri_rdf_Property), ic(uri_rdfs_Statement), ifeq(iext(X, Y, uri_rdf_value), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1086: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_subPropertyOf), ic(uri_rdfs_Statement), ifeq(iext(X, uri_owl_minCardinality, uri_owl_minCardinality), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1087: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_subClassOf), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdfs_Container, uri_rdfs_Resource), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1088: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_subClassOf), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdfs_Container, uri_rdfs_Container), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1089: ifeq(iext(uri_rdfs_range, X, uri_rdf_Property), ic(uri_rdfs_Statement), ifeq(iext(X, Y, uri_rdfs_label), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1090: ifeq(iext(uri_rdfs_domain, X, uri_rdf_Property), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdfs_label, Y), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1091: ifeq(iext(uri_rdfs_domain, X, uri_rdfs_Class), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdf_Bag, Y), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1092: ifeq(iext(uri_rdfs_domain, X, sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z), ic(uri_rdfs_Statement), ifeq(iext(X, uri_ex_bob, Y), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1093: ifeq(iext(uri_rdfs_domain, X, sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z), ic(uri_rdfs_Statement), ifeq(iext(X, uri_ex_alice, Y), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1094: ifeq(iext(uri_rdfs_range, X, uri_rdfs_Class), ic(uri_rdfs_Statement), ifeq(iext(X, Y, uri_rdfs_Seq), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1095: ifeq(iext(uri_rdfs_range, X, uri_rdfs_Class), ic(uri_rdfs_Statement), ifeq(iext(X, Y, uri_rdfs_ContainerMembershipProperty), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1096: ifeq(iext(uri_rdfs_range, X, uri_rdfs_Class), ic(uri_rdfs_Statement), ifeq(iext(X, Y, uri_rdf_Alt), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1097: ifeq(iext(uri_rdfs_range, X, uri_rdfs_Class), ic(uri_rdfs_Statement), ifeq(iext(X, Y, uri_ex_Person), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1098: ifeq(iext(uri_rdfs_range, X, uri_rdfs_Class), ic(uri_rdfs_Statement), ifeq(iext(X, Y, sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1099: ifeq(iext(uri_rdfs_range, X, uri_rdfs_Class), ic(uri_rdfs_Statement), ifeq(iext(X, Y, uri_rdf_Bag), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1100: ifeq(iext(uri_rdfs_range, X, uri_rdfs_Class), ic(uri_rdfs_Statement), ifeq(iext(X, Y, uri_rdf_XMLLiteral), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1101: ifeq(iext(uri_rdfs_range, X, uri_rdfs_Class), ic(uri_rdfs_Statement), ifeq(iext(X, Y, uri_rdf_Property), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1102: ifeq(iext(uri_rdfs_range, X, uri_rdfs_Class), ic(uri_rdfs_Statement), ifeq(iext(X, Y, uri_rdfs_Class), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1103: ifeq(iext(uri_rdfs_range, X, uri_rdfs_Class), ic(uri_rdfs_Statement), ifeq(iext(X, Y, uri_owl_TransitiveProperty), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1104: ifeq(iext(uri_rdfs_range, X, sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z), ic(uri_rdfs_Statement), ifeq(iext(X, Y, uri_ex_bob), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1105: ifeq(iext(uri_rdfs_range, X, sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z), ic(uri_rdfs_Statement), ifeq(iext(X, Y, uri_ex_alice), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1106: ifeq(iext(uri_rdfs_range, X, uri_rdfs_Class), ic(uri_rdfs_Statement), ifeq(iext(X, Y, uri_owl_Restriction), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1107: ifeq(iext(uri_rdfs_range, X, uri_rdfs_Class), ic(uri_rdfs_Statement), ifeq(iext(X, Y, uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1108: ifeq(iext(uri_rdfs_domain, X, uri_rdfs_Class), ic(uri_rdfs_Statement), ifeq(iext(X, sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z, Y), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1109: ifeq(iext(uri_rdfs_domain, X, uri_rdfs_Class), ic(uri_rdfs_Statement), ifeq(iext(X, uri_ex_Person, Y), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1110: ifeq(iext(uri_rdfs_domain, X, uri_rdfs_Class), ic(uri_rdfs_Statement), ifeq(iext(X, uri_owl_TransitiveProperty, Y), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1111: ifeq(iext(uri_rdfs_domain, X, uri_rdfs_Class), ic(uri_rdfs_Statement), ifeq(iext(X, uri_owl_Restriction, Y), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1112: ifeq(iext(uri_rdfs_domain, X, uri_rdfs_Class), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdf_Alt, Y), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1113: ifeq(iext(uri_rdfs_range, X, uri_rdfs_Class), ic(uri_rdfs_Statement), ifeq(iext(X, Y, uri_rdfs_Literal), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1114: ifeq(iext(uri_rdfs_range, X, uri_rdfs_Class), ic(uri_rdfs_Statement), ifeq(iext(X, Y, uri_rdfs_Datatype), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1115: ifeq(iext(uri_rdfs_range, X, uri_rdfs_Class), ic(uri_rdfs_Statement), ifeq(iext(X, Y, uri_rdf_List), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1116: ifeq(iext(uri_rdfs_domain, X, uri_rdf_Property), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdf_predicate, Y), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1117: ifeq(iext(uri_rdfs_range, X, uri_rdf_Property), ic(uri_rdfs_Statement), ifeq(iext(X, Y, uri_rdf_predicate), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1118: ifeq(iext(uri_rdfs_domain, X, uri_rdf_Property), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdfs_comment, Y), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1119: ifeq(iext(uri_rdfs_range, X, uri_rdf_Property), ic(uri_rdfs_Statement), ifeq(iext(X, Y, uri_rdfs_comment), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1120: ifeq(iext(uri_rdfs_domain, X, uri_rdfs_Class), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdfs_Class, Y), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1121: ifeq(iext(uri_rdfs_domain, X, uri_rdfs_Class), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdf_Property, Y), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1122: ifeq(iext(uri_rdfs_domain, X, uri_rdfs_Class), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdf_XMLLiteral, Y), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1123: ifeq(iext(uri_rdfs_domain, X, uri_rdfs_Class), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdfs_Datatype, Y), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1124: ifeq(iext(uri_rdfs_domain, X, uri_rdfs_Class), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdfs_ContainerMembershipProperty, Y), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1125: ifeq(iext(uri_rdfs_domain, X, uri_rdfs_Class), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdfs_Literal, Y), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1126: ifeq(iext(uri_rdfs_domain, X, uri_rdfs_Class), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdf_List, Y), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1127: ifeq(iext(uri_rdfs_domain, X, uri_rdfs_Class), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdfs_Seq, Y), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1128: ifeq(iext(uri_rdfs_domain, X, uri_rdfs_Class), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdfs_Statement, Y), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1129: ifeq(icext(X, Y), ic(uri_rdfs_Statement), ifeq(iext(uri_rdfs_subClassOf, X, Z), ic(uri_rdfs_Statement), icext(Z, Y), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1130: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_subClassOf), ic(uri_rdfs_Statement), ifeq(iext(X, sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z, uri_rdfs_Resource), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1131: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_subClassOf), ic(uri_rdfs_Statement), ifeq(iext(X, uri_ex_Person, uri_ex_Person), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1132: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdf_type), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdfs_seeAlso, uri_rdf_Property), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1133: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdf_type), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdfs_range, uri_rdf_Property), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1134: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdf_type), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdfs_subClassOf, uri_rdf_Property), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1135: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_subClassOf), ic(uri_rdfs_Statement), ifeq(iext(X, sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z, sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1136: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdf_type), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdfs_isDefinedBy, uri_rdf_Property), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1137: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdf_type), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdfs_domain, uri_rdf_Property), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1138: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdf_type), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdfs_subPropertyOf, uri_rdf_Property), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1139: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdf_type), ic(uri_rdfs_Statement), ifeq(iext(X, uri_owl_minCardinality, uri_rdf_Property), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1140: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdf_type), ic(uri_rdfs_Statement), ifeq(iext(X, uri_owl_onProperty, uri_rdf_Property), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1141: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdf_type), ic(uri_rdfs_Statement), ifeq(iext(X, uri_ex_hasAncestor, uri_rdf_Property), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1142: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_subClassOf), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdf_Property, uri_rdf_Property), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1143: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_subPropertyOf), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdf__1, uri_rdf__1), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1144: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_subClassOf), ic(uri_rdfs_Statement), ifeq(iext(X, uri_ex_Person, uri_rdfs_Resource), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1145: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_subClassOf), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdf_Alt, uri_rdf_Alt), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1146: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_subClassOf), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdfs_Seq, uri_rdfs_Resource), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1147: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_subPropertyOf), ic(uri_rdfs_Statement), ifeq(iext(X, uri_ex_hasAncestor, uri_ex_hasAncestor), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1148: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_subPropertyOf), ic(uri_rdfs_Statement), ifeq(iext(X, uri_owl_onProperty, uri_owl_onProperty), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1149: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_subClassOf), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdfs_Seq, uri_rdfs_Seq), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1150: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_subClassOf), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdfs_Class, uri_rdfs_Class), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1151: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_subClassOf), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdfs_Class, uri_rdfs_Resource), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1152: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_subClassOf), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdf_XMLLiteral, uri_rdfs_Resource), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1153: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_subClassOf), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdfs_ContainerMembershipProperty, uri_rdfs_ContainerMembershipProperty), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1154: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_subPropertyOf), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdf__3, uri_rdf__3), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1155: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_subPropertyOf), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdf__2, uri_rdf__2), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1156: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_subPropertyOf), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdf__2, uri_rdfs_member), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1157: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_subPropertyOf), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdf__1, uri_rdfs_member), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1158: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_subPropertyOf), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdf__3, uri_rdfs_member), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1159: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_subPropertyOf), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdf_object, uri_rdf_object), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1160: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_subPropertyOf), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdf_first, uri_rdf_first), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1161: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_subPropertyOf), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdf_type, uri_rdf_type), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1162: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_subPropertyOf), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdf_rest, uri_rdf_rest), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1163: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_subPropertyOf), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdf_subject, uri_rdf_subject), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1164: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_subPropertyOf), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdf_value, uri_rdf_value), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1165: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_subPropertyOf), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdfs_domain, uri_rdfs_domain), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1166: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_subPropertyOf), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdfs_isDefinedBy, uri_rdfs_isDefinedBy), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1167: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_subPropertyOf), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1168: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_subClassOf), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdf_Alt, uri_rdfs_Resource), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1169: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_subPropertyOf), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdfs_range, uri_rdfs_range), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1170: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_subPropertyOf), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdfs_seeAlso, uri_rdfs_seeAlso), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1171: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_subClassOf), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdf_XMLLiteral, uri_rdf_XMLLiteral), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1172: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_subClassOf), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdfs_Literal, uri_rdfs_Resource), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1173: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_subClassOf), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdfs_ContainerMembershipProperty, uri_rdfs_Resource), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1174: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_subClassOf), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdfs_Datatype, uri_rdfs_Resource), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1175: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_subClassOf), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdfs_Datatype, uri_rdfs_Datatype), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1176: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_subClassOf), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdfs_Literal, uri_rdfs_Literal), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1177: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_subClassOf), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdf_Property, uri_rdfs_Resource), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1178: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_subClassOf), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdf_Bag, uri_rdfs_Resource), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1179: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_subClassOf), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdf_Bag, uri_rdf_Bag), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1180: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_subPropertyOf), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdfs_subClassOf, uri_rdfs_subClassOf), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1181: ifeq(iext(uri_rdfs_range, X, uri_rdfs_Class), ic(uri_rdfs_Statement), ifeq(iext(X, Y, uri_rdfs_Container), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1182: ifeq(iext(uri_rdfs_range, X, uri_rdf_Property), ic(uri_rdfs_Statement), ifeq(iext(X, Y, uri_owl_minCardinality), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1183: ifeq(iext(uri_rdfs_range, X, uri_rdf_Property), ic(uri_rdfs_Statement), ifeq(iext(X, Y, uri_ex_hasAncestor), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1184: ifeq(iext(uri_rdfs_range, X, uri_rdf_Property), ic(uri_rdfs_Statement), ifeq(iext(X, Y, uri_owl_onProperty), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1185: ifeq(iext(uri_rdfs_range, X, uri_rdf_Property), ic(uri_rdfs_Statement), ifeq(iext(X, Y, uri_rdfs_range), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1186: ifeq(iext(uri_rdfs_range, X, uri_rdf_Property), ic(uri_rdfs_Statement), ifeq(iext(X, Y, uri_rdfs_domain), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1187: ifeq(iext(uri_rdfs_range, X, uri_rdf_Property), ic(uri_rdfs_Statement), ifeq(iext(X, Y, uri_rdfs_isDefinedBy), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1188: ifeq(iext(uri_rdfs_range, X, uri_rdf_Property), ic(uri_rdfs_Statement), ifeq(iext(X, Y, uri_rdfs_subClassOf), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1189: ifeq(iext(uri_rdfs_range, X, uri_rdf_Property), ic(uri_rdfs_Statement), ifeq(iext(X, Y, uri_rdfs_seeAlso), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1190: ifeq(iext(uri_rdfs_range, X, uri_rdf_Property), ic(uri_rdfs_Statement), ifeq(iext(X, Y, uri_rdfs_subPropertyOf), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1191: ifeq(iext(uri_rdfs_domain, X, uri_rdf_Property), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdfs_isDefinedBy, Y), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1192: ifeq(iext(uri_rdfs_domain, X, uri_rdf_Property), ic(uri_rdfs_Statement), ifeq(iext(X, uri_owl_onProperty, Y), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1193: ifeq(iext(uri_rdfs_domain, X, uri_rdf_Property), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdfs_subPropertyOf, Y), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1194: ifeq(iext(uri_rdfs_domain, X, uri_rdf_Property), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdfs_subClassOf, Y), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1195: ifeq(iext(uri_rdfs_domain, X, uri_rdf_Property), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdfs_range, Y), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1196: ifeq(iext(uri_rdfs_domain, X, uri_rdf_Property), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdfs_seeAlso, Y), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1197: ifeq(iext(uri_rdfs_domain, X, uri_rdf_Property), ic(uri_rdfs_Statement), ifeq(iext(X, uri_ex_hasAncestor, Y), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1198: ifeq(iext(uri_rdfs_domain, X, uri_rdf_Property), ic(uri_rdfs_Statement), ifeq(iext(X, uri_owl_minCardinality, Y), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1199: ifeq(iext(uri_rdfs_domain, X, uri_rdf_Property), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdfs_domain, Y), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1200: ifeq(iext(uri_rdfs_range, X, uri_rdfs_Class), ic(uri_rdfs_Statement), ifeq(iext(X, Y, uri_rdfs_Resource), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1201: ifeq(iext(uri_rdfs_domain, X, uri_rdfs_Class), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdfs_Resource, Y), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1202: ifeq(iext(uri_rdfs_domain, X, uri_rdfs_Class), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdfs_Container, Y), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1203: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdf_type), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdf_predicate, uri_rdf_Property), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1204: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdf_type), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdfs_label, uri_rdf_Property), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1205: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdf_type), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdfs_Statement, uri_rdfs_Class), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1206: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdf_type), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdfs_Seq, uri_rdfs_Class), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1207: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdf_type), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdfs_comment, uri_rdf_Property), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1208: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdf_type), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdfs_Datatype, uri_rdfs_Class), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1209: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdf_type), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdfs_Literal, uri_rdfs_Class), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1210: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdf_type), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdfs_ContainerMembershipProperty, uri_rdfs_Class), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1211: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdf_type), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdf_XMLLiteral, uri_rdfs_Class), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1212: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_subClassOf), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdfs_Resource, uri_rdfs_Resource), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1213: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdf_type), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdfs_Class, uri_rdfs_Class), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1214: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdf_type), ic(uri_rdfs_Statement), ifeq(iext(X, uri_owl_Restriction, uri_rdfs_Class), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1215: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdf_type), ic(uri_rdfs_Statement), ifeq(iext(X, uri_ex_alice, sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1216: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdf_type), ic(uri_rdfs_Statement), ifeq(iext(X, uri_ex_bob, sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1217: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdf_type), ic(uri_rdfs_Statement), ifeq(iext(X, uri_ex_Person, uri_rdfs_Class), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1218: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdf_type), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdf_Bag, uri_rdfs_Class), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1219: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdf_type), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdf_List, uri_rdfs_Class), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1220: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdf_type), ic(uri_rdfs_Statement), ifeq(iext(X, sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z, uri_rdfs_Class), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1221: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdf_type), ic(uri_rdfs_Statement), ifeq(iext(X, uri_owl_TransitiveProperty, uri_rdfs_Class), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1222: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdf_type), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdf_Alt, uri_rdfs_Class), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1223: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_owl_minCardinality), ic(uri_rdfs_Statement), ifeq(iext(X, sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z, literal_typed(dat_str_1, uri_xsd_nonNegativeInteger)), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1224: ifeq(iext(uri_rdfs_range, X, Y), ic(uri_rdfs_Statement), ifeq(iext(X, Z, W), ic(uri_rdfs_Statement), icext(Y, W), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1225: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdf_type), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdfs_member, uri_rdf_Property), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1226: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdf_type), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdfs_Container, uri_rdfs_Class), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1227: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_subPropertyOf), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdfs_member, uri_rdfs_member), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1228: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdf_type), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdfs_Resource, uri_rdfs_Class), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1229: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_subClassOf), ic(uri_rdfs_Statement), ifeq(iext(X, uri_owl_TransitiveProperty, uri_rdfs_Resource), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1230: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_subClassOf), ic(uri_rdfs_Statement), ifeq(iext(X, uri_owl_Restriction, uri_rdfs_Resource), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1231: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_subClassOf), ic(uri_rdfs_Statement), ifeq(iext(X, uri_owl_Restriction, uri_owl_Restriction), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1232: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_subClassOf), ic(uri_rdfs_Statement), ifeq(iext(X, uri_owl_TransitiveProperty, uri_owl_TransitiveProperty), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1233: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_subClassOf), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdf_List, uri_rdfs_Resource), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1234: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_subClassOf), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdf_List, uri_rdf_List), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1235: ifeq(iext(uri_rdfs_range, X, uri_rdf_Property), ic(uri_rdfs_Statement), ifeq(iext(X, Y, uri_rdfs_member), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1236: ifeq(iext(uri_rdfs_domain, X, uri_rdf_Property), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdfs_member, Y), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1237: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_subClassOf), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdfs_Statement, uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1238: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_subPropertyOf), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdf_predicate, uri_rdf_predicate), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1239: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_subClassOf), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdfs_Statement, uri_rdfs_Resource), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1240: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_subPropertyOf), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdfs_label, uri_rdfs_label), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  1241: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_subPropertyOf), ic(uri_rdfs_Statement), ifeq(iext(X, uri_rdfs_comment, uri_rdfs_comment), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement), ic(uri_rdfs_Statement)), ic(uri_rdfs_Statement)) -> ic(uri_rdfs_Statement)
% 25.61/25.25  
%------------------------------------------------------------------------------