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