%------------------------------------------------------------------------------ % File : Toma---0.7 % Problem : SWB029-10 : TPTP v9.0.0. Released v7.5.0. % Transfm : none % Format : tptp:raw % Command : run_Leo-III %s %d THM % Computer : n013.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:44 AM UTC 2025 % Result : Satisfiable 60.68s 60.54s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.09/0.10 % Problem : SWB029-10 : TPTP v9.0.0. Released v7.5.0. % 0.09/0.10 % Command : run_Leo-III %s %d THM % 0.09/0.30 % Computer : n013.cluster.edu % 0.09/0.30 % Model : x86_64 x86_64 % 0.09/0.30 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.09/0.30 % Memory : 8042.1875MB % 0.09/0.30 % OS : Linux 3.10.0-693.el7.x86_64 % 0.09/0.30 % CPULimit : 300 % 0.09/0.30 % WCLimit : 300 % 0.09/0.30 % DateTime : Mon Jul 14 19:28:34 EDT 2025 % 0.09/0.30 % CPUTime : % 60.68/60.54 % SZS status Satisfiable % 60.68/60.54 The following TRS is a complete presentation of the axioms, but the goal is not joinable. % 60.68/60.54 1: ir(X) -> true % 60.68/60.54 2: iext(uri_rdf_type, uri_rdf_first, uri_rdf_Property) -> true % 60.68/60.54 3: iext(uri_rdf_type, uri_rdf_nil, uri_rdf_List) -> true % 60.68/60.54 4: iext(uri_rdf_type, uri_rdf_rest, uri_rdf_Property) -> true % 60.68/60.54 5: iext(uri_rdf_type, uri_rdf__1, uri_rdf_Property) -> true % 60.68/60.54 6: iext(uri_rdf_type, uri_rdf__2, uri_rdf_Property) -> true % 60.68/60.54 7: iext(uri_rdf_type, uri_rdf__3, uri_rdf_Property) -> true % 60.68/60.54 8: iext(uri_rdf_type, uri_rdf_object, uri_rdf_Property) -> true % 60.68/60.54 9: iext(uri_rdf_type, uri_rdf_value, uri_rdf_Property) -> true % 60.68/60.54 10: iext(uri_rdf_type, uri_rdf_subject, uri_rdf_Property) -> true % 60.68/60.54 11: iext(uri_rdf_type, uri_rdf_type, uri_rdf_Property) -> true % 60.68/60.54 12: iext(uri_rdfs_domain, uri_rdfs_comment, uri_rdfs_Resource) -> true % 60.68/60.54 13: iext(uri_rdfs_range, uri_rdfs_comment, uri_rdfs_Literal) -> true % 60.68/60.54 14: iext(uri_rdfs_domain, uri_rdfs_isDefinedBy, uri_rdfs_Resource) -> true % 60.68/60.54 15: iext(uri_rdfs_range, uri_rdfs_isDefinedBy, uri_rdfs_Resource) -> true % 60.68/60.54 16: iext(uri_rdfs_subPropertyOf, uri_rdfs_isDefinedBy, uri_rdfs_seeAlso) -> true % 60.68/60.54 17: iext(uri_rdfs_domain, uri_rdfs_label, uri_rdfs_Resource) -> true % 60.68/60.54 18: iext(uri_rdfs_range, uri_rdfs_label, uri_rdfs_Literal) -> true % 60.68/60.54 19: iext(uri_rdfs_domain, uri_rdfs_seeAlso, uri_rdfs_Resource) -> true % 60.68/60.54 20: iext(uri_rdfs_range, uri_rdfs_seeAlso, uri_rdfs_Resource) -> true % 60.68/60.54 21: iext(uri_rdfs_domain, uri_rdf_first, uri_rdf_List) -> true % 60.68/60.54 22: iext(uri_rdfs_range, uri_rdf_first, uri_rdfs_Resource) -> true % 60.68/60.54 23: iext(uri_rdfs_domain, uri_rdf_rest, uri_rdf_List) -> true % 60.68/60.54 24: iext(uri_rdfs_range, uri_rdf_rest, uri_rdf_List) -> true % 60.68/60.54 25: iext(uri_rdfs_subClassOf, uri_rdf_Alt, uri_rdfs_Container) -> true % 60.68/60.54 26: iext(uri_rdfs_subClassOf, uri_rdf_Bag, uri_rdfs_Container) -> true % 60.68/60.54 27: iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, uri_rdf_Property) -> true % 60.68/60.54 28: iext(uri_rdfs_domain, uri_rdfs_member, uri_rdfs_Resource) -> true % 60.68/60.54 29: iext(uri_rdfs_range, uri_rdfs_member, uri_rdfs_Resource) -> true % 60.68/60.54 30: iext(uri_rdfs_domain, uri_rdf__1, uri_rdfs_Resource) -> true % 60.68/60.54 31: iext(uri_rdfs_domain, uri_rdf__2, uri_rdfs_Resource) -> true % 60.68/60.54 32: iext(uri_rdfs_domain, uri_rdf__3, uri_rdfs_Resource) -> true % 60.68/60.54 33: iext(uri_rdfs_range, uri_rdf__1, uri_rdfs_Resource) -> true % 60.68/60.54 34: iext(uri_rdfs_range, uri_rdf__2, uri_rdfs_Resource) -> true % 60.68/60.54 35: iext(uri_rdfs_range, uri_rdf__3, uri_rdfs_Resource) -> true % 60.68/60.54 36: iext(uri_rdf_type, uri_rdf__1, uri_rdfs_ContainerMembershipProperty) -> true % 60.68/60.54 37: iext(uri_rdf_type, uri_rdf__2, uri_rdfs_ContainerMembershipProperty) -> true % 60.68/60.54 38: iext(uri_rdf_type, uri_rdf__3, uri_rdfs_ContainerMembershipProperty) -> true % 60.68/60.54 39: iext(uri_rdfs_subClassOf, uri_rdfs_Seq, uri_rdfs_Container) -> true % 60.68/60.54 40: iext(uri_rdfs_subClassOf, uri_rdf_XMLLiteral, uri_rdfs_Literal) -> true % 60.68/60.54 41: iext(uri_rdf_type, uri_rdf_XMLLiteral, uri_rdfs_Datatype) -> true % 60.68/60.54 42: iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, uri_rdfs_Class) -> true % 60.68/60.54 43: iext(uri_rdfs_domain, uri_rdfs_domain, uri_rdf_Property) -> true % 60.68/60.54 44: iext(uri_rdfs_range, uri_rdfs_domain, uri_rdfs_Class) -> true % 60.68/60.54 45: iext(uri_rdf_type, uri_rdf_Property, uri_rdfs_Class) -> true % 60.68/60.54 46: iext(uri_rdfs_domain, uri_rdfs_range, uri_rdf_Property) -> true % 60.68/60.54 47: iext(uri_rdfs_range, uri_rdfs_range, uri_rdfs_Class) -> true % 60.68/60.54 48: iext(uri_rdfs_domain, uri_rdf_object, uri_rdfs_Statement) -> true % 60.68/60.54 49: iext(uri_rdfs_range, uri_rdf_predicate, uri_rdfs_Resource) -> true % 60.68/60.54 50: iext(uri_rdfs_domain, uri_rdf_predicate, uri_rdfs_Statement) -> true % 60.68/60.54 51: iext(uri_rdfs_domain, uri_rdf_subject, uri_rdfs_Statement) -> true % 60.68/60.54 52: iext(uri_rdfs_range, uri_rdf_subject, uri_rdfs_Resource) -> true % 60.68/60.54 53: iext(uri_rdfs_domain, uri_rdfs_subClassOf, uri_rdfs_Class) -> true % 60.68/60.54 54: iext(uri_rdfs_range, uri_rdfs_subClassOf, uri_rdfs_Class) -> true % 60.68/60.54 55: iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, uri_rdf_Property) -> true % 60.68/60.54 56: iext(uri_rdfs_range, uri_rdfs_subPropertyOf, uri_rdf_Property) -> true % 60.68/60.54 57: iext(uri_rdfs_domain, uri_rdf_type, uri_rdfs_Resource) -> true % 60.68/60.54 58: iext(uri_rdfs_range, uri_rdf_type, uri_rdfs_Class) -> true % 60.68/60.54 59: iext(uri_rdfs_domain, uri_rdf_value, uri_rdfs_Resource) -> true % 60.68/60.54 60: iext(uri_rdfs_range, uri_rdf_value, uri_rdfs_Resource) -> true % 60.68/60.54 61: iext(uri_owl_complementOf, sK1_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_y, uri_ex_A) -> true % 60.68/60.54 62: iext(uri_owl_intersectionOf, sK3_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_x, sK4_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l1) -> true % 60.68/60.54 63: iext(uri_rdf_rest, sK2_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l2, uri_rdf_nil) -> true % 60.68/60.54 64: iext(uri_rdf_rest, sK4_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l1, sK2_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l2) -> true % 60.68/60.54 65: iext(uri_rdf_first, sK2_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l2, sK1_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_y) -> true % 60.68/60.54 66: iext(uri_rdf_first, sK4_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l1, uri_ex_A) -> true % 60.68/60.54 67: iext(uri_rdf_type, uri_ex_A, uri_owl_Class) -> true % 60.68/60.54 68: iext(uri_rdf_type, uri_ex_B, uri_owl_Class) -> true % 60.68/60.54 69: iext(uri_rdf_type, uri_ex_w, sK3_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_x) -> true % 60.68/60.54 70: ifeq(X, X, Y, Z) -> Y % 60.68/60.54 72: ifeq(lv(X), true, true, true) -> true % 60.68/60.54 73: ifeq(lv(X), true, icext(uri_rdfs_Literal, X), true) -> true % 60.68/60.54 74: ifeq(icext(uri_rdfs_Literal, X), true, lv(X), true) -> true % 60.68/60.54 75: ifeq(ic(X), true, icext(uri_rdfs_Class, X), true) -> true % 60.68/60.54 77: ifeq(icext(uri_rdfs_Resource, X), true, true, true) -> true % 60.68/60.54 78: ifeq(icext(uri_rdfs_Class, X), true, ic(X), true) -> true % 60.68/60.54 80: icext(uri_rdfs_Resource, X) -> true % 60.68/60.54 81: ifeq(iext(X, Y, Z), true, ip(X), true) -> true % 60.68/60.54 82: ip(uri_owl_complementOf) -> true % 60.68/60.54 83: ip(uri_owl_intersectionOf) -> true % 60.68/60.54 84: ip(uri_rdf_first) -> true % 60.68/60.54 85: ip(uri_rdf_rest) -> true % 60.68/60.54 86: ip(uri_rdf_type) -> true % 60.68/60.54 87: ip(uri_rdfs_domain) -> true % 60.68/60.54 88: ip(uri_rdfs_range) -> true % 60.68/60.54 89: ip(uri_rdfs_subClassOf) -> true % 60.68/60.54 90: ip(uri_rdfs_subPropertyOf) -> true % 60.68/60.54 91: ifeq(ip(X), true, iext(uri_rdfs_subPropertyOf, X, X), true) -> true % 60.68/60.54 92: iext(uri_rdfs_subPropertyOf, uri_owl_complementOf, uri_owl_complementOf) -> true % 60.68/60.54 93: iext(uri_rdfs_subPropertyOf, uri_owl_intersectionOf, uri_owl_intersectionOf) -> true % 60.68/60.54 94: iext(uri_rdfs_subPropertyOf, uri_rdf_first, uri_rdf_first) -> true % 60.68/60.54 95: iext(uri_rdfs_subPropertyOf, uri_rdf_rest, uri_rdf_rest) -> true % 60.68/60.54 96: iext(uri_rdfs_subPropertyOf, uri_rdf_type, uri_rdf_type) -> true % 60.68/60.54 97: iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, uri_rdfs_domain) -> true % 60.68/60.54 98: iext(uri_rdfs_subPropertyOf, uri_rdfs_range, uri_rdfs_range) -> true % 60.68/60.54 99: iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, uri_rdfs_subClassOf) -> true % 60.68/60.54 100: iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf) -> true % 60.68/60.54 101: ifeq(iext(uri_rdfs_subPropertyOf, X, Y), true, ip(X), true) -> true % 60.68/60.54 102: ip(uri_rdfs_isDefinedBy) -> true % 60.68/60.54 103: iext(uri_rdfs_subPropertyOf, uri_rdfs_isDefinedBy, uri_rdfs_isDefinedBy) -> true % 60.68/60.54 104: ifeq(ic(X), true, iext(uri_rdfs_subClassOf, X, X), true) -> true % 60.68/60.54 105: ifeq(iext(uri_rdfs_subPropertyOf, X, Y), true, ip(Y), true) -> true % 60.68/60.54 106: ip(uri_rdfs_seeAlso) -> true % 60.68/60.54 107: iext(uri_rdfs_subPropertyOf, uri_rdfs_seeAlso, uri_rdfs_seeAlso) -> true % 60.68/60.54 108: ifeq(iext(uri_rdfs_subClassOf, X, Y), true, ic(Y), true) -> true % 60.68/60.54 109: ic(uri_rdfs_Container) -> true % 60.68/60.54 110: ic(uri_rdfs_Literal) -> true % 60.68/60.54 111: ic(uri_rdf_Property) -> true % 60.68/60.54 112: ic(uri_rdfs_Class) -> true % 60.68/60.54 113: icext(uri_rdfs_Class, uri_rdfs_Class) -> true % 60.68/60.54 114: icext(uri_rdfs_Class, uri_rdf_Property) -> true % 60.68/60.54 115: icext(uri_rdfs_Class, uri_rdfs_Literal) -> true % 60.68/60.54 116: icext(uri_rdfs_Class, uri_rdfs_Container) -> true % 60.68/60.54 117: iext(uri_rdfs_subClassOf, uri_rdfs_Literal, uri_rdfs_Literal) -> true % 60.68/60.54 118: iext(uri_rdfs_subClassOf, uri_rdfs_Container, uri_rdfs_Container) -> true % 60.68/60.54 119: iext(uri_rdfs_subClassOf, uri_rdf_Property, uri_rdf_Property) -> true % 60.68/60.54 120: iext(uri_rdfs_subClassOf, uri_rdfs_Class, uri_rdfs_Class) -> true % 60.68/60.54 121: ifeq(iext(uri_rdfs_subClassOf, X, Y), true, ic(X), true) -> true % 60.68/60.54 122: ic(uri_rdf_Alt) -> true % 60.68/60.54 123: ic(uri_rdf_Bag) -> true % 60.68/60.54 124: ic(uri_rdf_XMLLiteral) -> true % 60.68/60.54 125: ic(uri_rdfs_ContainerMembershipProperty) -> true % 60.68/60.54 126: ic(uri_rdfs_Datatype) -> true % 60.68/60.54 127: ic(uri_rdfs_Seq) -> true % 60.68/60.54 128: icext(uri_rdfs_Class, uri_rdfs_Seq) -> true % 60.68/60.54 129: icext(uri_rdfs_Class, uri_rdf_Alt) -> true % 60.68/60.54 130: icext(uri_rdfs_Class, uri_rdfs_Datatype) -> true % 60.68/60.54 131: icext(uri_rdfs_Class, uri_rdfs_ContainerMembershipProperty) -> true % 60.68/60.54 132: icext(uri_rdfs_Class, uri_rdf_XMLLiteral) -> true % 60.68/60.54 133: icext(uri_rdfs_Class, uri_rdf_Bag) -> true % 60.68/60.54 134: iext(uri_rdfs_subClassOf, uri_rdf_Bag, uri_rdf_Bag) -> true % 60.68/60.54 135: iext(uri_rdfs_subClassOf, uri_rdf_Alt, uri_rdf_Alt) -> true % 60.68/60.54 136: iext(uri_rdfs_subClassOf, uri_rdf_XMLLiteral, uri_rdf_XMLLiteral) -> true % 60.68/60.54 137: iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, uri_rdfs_ContainerMembershipProperty) -> true % 60.68/60.54 138: iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, uri_rdfs_Datatype) -> true % 60.68/60.54 139: iext(uri_rdfs_subClassOf, uri_rdfs_Seq, uri_rdfs_Seq) -> true % 60.68/60.54 140: ifeq(ip(X), true, iext(uri_rdf_type, X, uri_rdf_Property), true) -> true % 60.68/60.54 141: iext(uri_rdf_type, uri_owl_complementOf, uri_rdf_Property) -> true % 60.68/60.54 142: iext(uri_rdf_type, uri_owl_intersectionOf, uri_rdf_Property) -> true % 60.68/60.54 143: iext(uri_rdf_type, uri_rdfs_domain, uri_rdf_Property) -> true % 60.68/60.54 144: iext(uri_rdf_type, uri_rdfs_isDefinedBy, uri_rdf_Property) -> true % 60.68/60.54 145: iext(uri_rdf_type, uri_rdfs_range, uri_rdf_Property) -> true % 60.68/60.54 146: iext(uri_rdf_type, uri_rdfs_seeAlso, uri_rdf_Property) -> true % 60.68/60.54 147: iext(uri_rdf_type, uri_rdfs_subClassOf, uri_rdf_Property) -> true % 60.68/60.54 148: iext(uri_rdf_type, uri_rdfs_subPropertyOf, uri_rdf_Property) -> true % 60.68/60.54 149: ifeq(ip(uri_rdf__1), true, true, true) -> true % 60.68/60.54 150: ifeq(ip(uri_rdf__2), true, true, true) -> true % 60.68/60.54 151: ifeq(ip(uri_rdf__3), true, true, true) -> true % 60.68/60.54 152: ifeq(ip(uri_rdf_object), true, true, true) -> true % 60.68/60.54 153: ifeq(ip(uri_rdf_subject), true, true, true) -> true % 60.68/60.54 154: ifeq(ip(uri_rdf_value), true, true, true) -> true % 60.68/60.54 155: ifeq(ic(X), true, iext(uri_rdfs_subClassOf, X, uri_rdfs_Resource), true) -> true % 60.68/60.54 156: iext(uri_rdfs_subClassOf, uri_rdf_Alt, uri_rdfs_Resource) -> true % 60.68/60.54 157: ic(uri_rdfs_Resource) -> true % 60.68/60.54 158: iext(uri_rdfs_subClassOf, uri_rdf_Bag, uri_rdfs_Resource) -> true % 60.68/60.54 159: iext(uri_rdfs_subClassOf, uri_rdf_Property, uri_rdfs_Resource) -> true % 60.68/60.54 160: iext(uri_rdfs_subClassOf, uri_rdf_XMLLiteral, uri_rdfs_Resource) -> true % 60.68/60.54 161: iext(uri_rdfs_subClassOf, uri_rdfs_Class, uri_rdfs_Resource) -> true % 60.68/60.54 162: iext(uri_rdfs_subClassOf, uri_rdfs_Container, uri_rdfs_Resource) -> true % 60.68/60.54 163: iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, uri_rdfs_Resource) -> true % 60.68/60.54 164: iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, uri_rdfs_Resource) -> true % 60.68/60.54 165: iext(uri_rdfs_subClassOf, uri_rdfs_Literal, uri_rdfs_Resource) -> true % 60.68/60.54 166: iext(uri_rdfs_subClassOf, uri_rdfs_Seq, uri_rdfs_Resource) -> true % 60.68/60.54 167: icext(uri_rdfs_Class, uri_rdfs_Resource) -> true % 60.68/60.54 168: iext(uri_rdfs_subClassOf, uri_rdfs_Resource, uri_rdfs_Resource) -> true % 60.68/60.54 169: ifeq(iext(uri_rdf_type, X, uri_rdf_Property), true, ip(X), true) -> true % 60.68/60.54 170: ip(uri_rdf__1) -> true % 60.68/60.54 171: ip(uri_rdf__2) -> true % 60.68/60.54 172: ip(uri_rdf__3) -> true % 60.68/60.54 173: ip(uri_rdf_object) -> true % 60.68/60.54 174: ip(uri_rdf_subject) -> true % 60.68/60.54 175: ip(uri_rdf_value) -> true % 60.68/60.54 176: iext(uri_rdfs_subPropertyOf, uri_rdf_value, uri_rdf_value) -> true % 60.68/60.54 177: iext(uri_rdfs_subPropertyOf, uri_rdf_subject, uri_rdf_subject) -> true % 60.68/60.54 178: iext(uri_rdfs_subPropertyOf, uri_rdf__3, uri_rdf__3) -> true % 60.68/60.54 179: iext(uri_rdfs_subPropertyOf, uri_rdf_object, uri_rdf_object) -> true % 60.68/60.54 180: iext(uri_rdfs_subPropertyOf, uri_rdf__1, uri_rdf__1) -> true % 60.68/60.54 181: iext(uri_rdfs_subPropertyOf, uri_rdf__2, uri_rdf__2) -> true % 60.68/60.54 182: ifeq(iext(uri_rdf__2, X, Y), true, true, true) -> true % 60.68/60.54 183: ifeq(iext(uri_rdf_object, X, Y), true, true, true) -> true % 60.68/60.54 184: ifeq(iext(uri_rdf__3, X, Y), true, true, true) -> true % 60.68/60.54 185: ifeq(iext(uri_rdf__1, X, Y), true, true, true) -> true % 60.68/60.54 186: ifeq(iext(uri_rdf_value, X, Y), true, true, true) -> true % 60.68/60.54 187: ifeq(iext(uri_rdfs_subClassOf, X, Y), true, true, true) -> true % 60.68/60.54 188: ifeq(iext(uri_rdf_subject, X, Y), true, true, true) -> true % 60.68/60.54 189: ifeq(iext(uri_rdfs_domain, X, Y), true, true, true) -> true % 60.68/60.54 190: ifeq(iext(uri_rdfs_range, X, Y), true, true, true) -> true % 60.68/60.54 191: ifeq(iext(uri_owl_intersectionOf, X, Y), true, true, true) -> true % 60.68/60.54 192: ifeq(iext(uri_rdf_first, X, Y), true, true, true) -> true % 60.68/60.54 193: ifeq(iext(uri_owl_complementOf, X, Y), true, true, true) -> true % 60.68/60.54 194: ifeq(iext(uri_rdf_type, X, Y), true, true, true) -> true % 60.68/60.54 195: ifeq(iext(uri_rdf_rest, X, Y), true, true, true) -> true % 60.68/60.54 196: ifeq(iext(uri_rdfs_subPropertyOf, X, Y), true, true, true) -> true % 60.68/60.54 197: ifeq(iext(uri_rdfs_seeAlso, X, Y), true, true, true) -> true % 60.68/60.54 198: ifeq(iext(uri_rdfs_isDefinedBy, X, Y), true, true, true) -> true % 60.68/60.54 199: ifeq(iext(uri_rdf_type, X, Y), true, icext(Y, X), true) -> true % 60.68/60.54 200: icext(uri_owl_Class, uri_ex_A) -> true % 60.68/60.54 201: icext(uri_owl_Class, uri_ex_B) -> true % 60.68/60.54 202: icext(sK3_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_x, uri_ex_w) -> true % 60.68/60.54 203: icext(uri_rdfs_Datatype, uri_rdf_XMLLiteral) -> true % 60.68/60.54 204: icext(uri_rdf_Property, uri_rdf__1) -> true % 60.68/60.54 205: icext(uri_rdfs_ContainerMembershipProperty, uri_rdf__1) -> true % 60.68/60.54 206: icext(uri_rdf_Property, uri_rdf__2) -> true % 60.68/60.54 207: icext(uri_rdfs_ContainerMembershipProperty, uri_rdf__2) -> true % 60.68/60.54 208: icext(uri_rdf_Property, uri_rdf__3) -> true % 60.68/60.54 209: icext(uri_rdfs_ContainerMembershipProperty, uri_rdf__3) -> true % 60.68/60.54 210: icext(uri_rdf_Property, uri_rdf_first) -> true % 60.68/60.54 211: icext(uri_rdf_List, uri_rdf_nil) -> true % 60.68/60.54 212: icext(uri_rdf_Property, uri_rdf_object) -> true % 60.68/60.54 213: icext(uri_rdf_Property, uri_rdf_rest) -> true % 60.68/60.54 214: icext(uri_rdf_Property, uri_rdf_subject) -> true % 60.68/60.54 215: icext(uri_rdf_Property, uri_rdf_type) -> true % 60.68/60.54 216: icext(uri_rdf_Property, uri_rdf_value) -> true % 60.68/60.54 217: icext(uri_rdf_Property, uri_owl_complementOf) -> true % 60.68/60.54 218: icext(uri_rdf_Property, uri_rdfs_domain) -> true % 60.68/60.54 219: icext(uri_rdf_Property, uri_owl_intersectionOf) -> true % 60.68/60.54 220: icext(uri_rdf_Property, uri_rdfs_isDefinedBy) -> true % 60.68/60.54 221: icext(uri_rdf_Property, uri_rdfs_range) -> true % 60.68/60.54 222: icext(uri_rdf_Property, uri_rdfs_seeAlso) -> true % 60.68/60.54 223: icext(uri_rdf_Property, uri_rdfs_subClassOf) -> true % 60.68/60.54 224: icext(uri_rdf_Property, uri_rdfs_subPropertyOf) -> true % 60.68/60.54 225: ifeq(icext(X, Y), true, iext(uri_rdf_type, Y, X), true) -> true % 60.68/60.54 226: iext(uri_rdf_type, X, uri_rdfs_Resource) -> true % 60.68/60.54 227: iext(uri_rdf_type, uri_rdf_Alt, uri_rdfs_Class) -> true % 60.68/60.54 228: iext(uri_rdf_type, uri_rdf_XMLLiteral, uri_rdfs_Class) -> true % 60.68/60.54 229: iext(uri_rdf_type, uri_rdf_Bag, uri_rdfs_Class) -> true % 60.68/60.54 230: iext(uri_rdf_type, uri_rdfs_Class, uri_rdfs_Class) -> true % 60.68/60.54 231: iext(uri_rdf_type, uri_rdfs_Datatype, uri_rdfs_Class) -> true % 60.68/60.54 232: iext(uri_rdf_type, uri_rdfs_Container, uri_rdfs_Class) -> true % 60.68/60.54 233: iext(uri_rdf_type, uri_rdfs_ContainerMembershipProperty, uri_rdfs_Class) -> true % 60.68/60.54 234: iext(uri_rdf_type, uri_rdfs_Literal, uri_rdfs_Class) -> true % 60.68/60.54 235: iext(uri_rdf_type, uri_rdfs_Seq, uri_rdfs_Class) -> true % 60.68/60.54 236: iext(uri_rdf_type, uri_rdfs_Resource, uri_rdfs_Class) -> true % 60.68/60.54 237: ifeq(icext(uri_rdfs_ContainerMembershipProperty, X), true, iext(uri_rdfs_subPropertyOf, X, uri_rdfs_member), true) -> true % 60.68/60.54 238: iext(uri_rdfs_subPropertyOf, uri_rdf__1, uri_rdfs_member) -> true % 60.68/60.54 239: ip(uri_rdfs_member) -> true % 60.68/60.54 240: iext(uri_rdfs_subPropertyOf, uri_rdf__2, uri_rdfs_member) -> true % 60.68/60.54 241: iext(uri_rdfs_subPropertyOf, uri_rdf__3, uri_rdfs_member) -> true % 60.68/60.54 242: iext(uri_rdfs_subPropertyOf, uri_rdfs_member, uri_rdfs_member) -> true % 60.68/60.54 243: iext(uri_rdf_type, uri_rdfs_member, uri_rdf_Property) -> true % 60.68/60.54 244: icext(uri_rdf_Property, uri_rdfs_member) -> true % 60.68/60.54 245: ifeq(icext(uri_rdfs_Datatype, X), true, iext(uri_rdfs_subClassOf, X, uri_rdfs_Literal), true) -> true % 60.68/60.54 246: ifeq(icext(uri_rdfs_Datatype, uri_rdfs_Literal), true, true, true) -> true % 60.68/60.54 247: ifeq(icext(uri_rdfs_ContainerMembershipProperty, uri_rdfs_member), true, true, true) -> true % 60.68/60.54 248: ifeq(iext(uri_rdfs_member, X, Y), true, true, true) -> true % 60.68/60.54 249: ifeq(icext(X, Y), true, ifeq(iext(uri_rdfs_subClassOf, X, Z), true, icext(Z, Y), true), true) -> true % 60.68/60.54 250: ifeq(icext(X, Y), true, true, true) -> true % 60.68/60.54 251: ifeq(icext(uri_rdfs_Datatype, X), true, icext(uri_rdfs_Class, X), true) -> true % 60.68/60.54 252: ifeq(icext(uri_rdf_Alt, X), true, icext(uri_rdfs_Container, X), true) -> true % 60.68/60.54 253: ifeq(icext(uri_rdfs_ContainerMembershipProperty, X), true, icext(uri_rdf_Property, X), true) -> true % 60.68/60.54 254: ifeq(icext(uri_rdfs_Seq, X), true, icext(uri_rdfs_Container, X), true) -> true % 60.68/60.54 255: ifeq(icext(uri_rdf_XMLLiteral, X), true, icext(uri_rdfs_Literal, X), true) -> true % 60.68/60.54 256: ifeq(icext(uri_rdf_Bag, X), true, icext(uri_rdfs_Container, X), true) -> true % 60.68/60.54 257: ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Resource, X), true, icext(X, Y), true) -> true % 60.68/60.54 258: ifeq(icext(uri_rdf_Bag, X), true, icext(uri_rdf_Bag, X), true) -> true % 60.68/60.54 259: ifeq(icext(uri_rdf_Property, X), true, icext(uri_rdf_Property, X), true) -> true % 60.68/60.54 260: ifeq(icext(uri_rdf_XMLLiteral, X), true, icext(uri_rdf_XMLLiteral, X), true) -> true % 60.68/60.54 261: ifeq(icext(uri_rdfs_Seq, X), true, icext(uri_rdfs_Seq, X), true) -> true % 60.68/60.54 262: ifeq(icext(uri_rdfs_ContainerMembershipProperty, X), true, icext(uri_rdfs_ContainerMembershipProperty, X), true) -> true % 60.68/60.54 263: ifeq(icext(uri_rdfs_Datatype, X), true, icext(uri_rdfs_Datatype, X), true) -> true % 60.68/60.54 264: ifeq(icext(uri_rdfs_Literal, X), true, icext(uri_rdfs_Literal, X), true) -> true % 60.68/60.54 265: ifeq(icext(uri_rdfs_Class, X), true, icext(uri_rdfs_Class, X), true) -> true % 60.68/60.54 266: ifeq(icext(uri_rdfs_Container, X), true, icext(uri_rdfs_Container, X), true) -> true % 60.68/60.54 267: ifeq(icext(uri_rdf_Alt, X), true, icext(uri_rdf_Alt, X), true) -> true % 60.68/60.54 268: ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, X), true, icext(X, uri_rdf_XMLLiteral), true) -> true % 60.68/60.54 269: ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, X), true, icext(X, uri_rdf__3), true) -> true % 60.68/60.54 270: ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, X), true, icext(X, uri_rdf__2), true) -> true % 60.68/60.54 271: ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, X), true, icext(X, uri_rdf__1), true) -> true % 60.68/60.54 272: ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, X), true, icext(X, uri_rdf__3), true) -> true % 60.68/60.54 273: ifeq(iext(uri_rdfs_subClassOf, sK3_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_x, X), true, icext(X, uri_ex_w), true) -> true % 60.68/60.54 274: ifeq(iext(uri_rdfs_subClassOf, uri_rdf_List, X), true, icext(X, uri_rdf_nil), true) -> true % 60.68/60.54 275: ifeq(iext(uri_rdfs_subClassOf, uri_owl_Class, X), true, icext(X, uri_ex_B), true) -> true % 60.68/60.54 276: ifeq(iext(uri_rdfs_subClassOf, uri_owl_Class, X), true, icext(X, uri_ex_A), true) -> true % 60.68/60.54 277: ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, X), true, icext(X, uri_rdf__1), true) -> true % 60.68/60.54 278: ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, X), true, icext(X, uri_rdf__2), true) -> true % 60.68/60.54 279: ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, X), true, icext(X, uri_rdf_subject), true) -> true % 60.68/60.54 280: ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, X), true, icext(X, uri_rdf_object), true) -> true % 60.68/60.54 281: ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, X), true, icext(X, uri_rdf_rest), true) -> true % 60.68/60.54 282: ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, X), true, icext(X, uri_rdf_first), true) -> true % 60.68/60.54 283: ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, X), true, icext(X, uri_rdf_type), true) -> true % 60.68/60.54 284: ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, X), true, icext(X, uri_rdf_value), true) -> true % 60.68/60.54 285: ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, X), true, icext(X, uri_rdf_Alt), true) -> true % 60.68/60.54 286: ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, X), true, icext(X, uri_rdf_Bag), true) -> true % 60.68/60.54 287: ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, X), true, icext(X, uri_rdf_Property), true) -> true % 60.68/60.54 288: ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, X), true, icext(X, uri_rdfs_Seq), true) -> true % 60.68/60.54 289: ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, X), true, icext(X, uri_rdfs_Container), true) -> true % 60.68/60.54 290: ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, X), true, icext(X, uri_rdfs_Class), true) -> true % 60.68/60.54 291: ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, X), true, icext(X, uri_rdf_XMLLiteral), true) -> true % 60.68/60.54 292: ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, X), true, icext(X, uri_rdfs_ContainerMembershipProperty), true) -> true % 60.68/60.54 293: ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, X), true, icext(X, uri_rdfs_Literal), true) -> true % 60.68/60.54 294: ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, X), true, icext(X, uri_rdfs_Datatype), true) -> true % 60.68/60.54 295: ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, X), true, icext(X, uri_rdfs_domain), true) -> true % 60.68/60.54 296: ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, X), true, icext(X, uri_rdfs_seeAlso), true) -> true % 60.68/60.54 297: ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, X), true, icext(X, uri_rdfs_range), true) -> true % 60.68/60.54 298: ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, X), true, icext(X, uri_rdfs_subClassOf), true) -> true % 60.68/60.54 299: ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, X), true, icext(X, uri_rdfs_isDefinedBy), true) -> true % 60.68/60.54 300: ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, X), true, icext(X, uri_owl_intersectionOf), true) -> true % 60.68/60.54 301: ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, X), true, icext(X, uri_owl_complementOf), true) -> true % 60.68/60.54 302: ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, X), true, icext(X, uri_rdfs_subPropertyOf), true) -> true % 60.68/60.54 303: ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, X), true, icext(X, uri_rdfs_Resource), true) -> true % 60.68/60.54 304: ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, X), true, icext(X, uri_rdfs_member), true) -> true % 60.68/60.54 305: ifeq(iext(uri_rdfs_range, X, Y), true, ifeq(iext(X, Z, W), true, icext(Y, W), true), true) -> true % 60.68/60.54 306: ifeq(iext(uri_rdf_predicate, X, Y), true, true, true) -> true % 60.68/60.54 307: ifeq(iext(uri_rdf_rest, X, Y), true, icext(uri_rdf_List, Y), true) -> true % 60.68/60.54 308: icext(uri_rdf_List, sK2_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l2) -> true % 60.68/60.54 309: iext(uri_rdf_type, sK2_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l2, uri_rdf_List) -> true % 60.68/60.54 310: ifeq(iext(uri_rdf_type, X, Y), true, icext(uri_rdfs_Class, Y), true) -> true % 60.68/60.54 311: icext(uri_rdfs_Class, uri_owl_Class) -> true % 60.68/60.54 312: ic(uri_owl_Class) -> true % 60.68/60.54 313: icext(uri_rdfs_Class, sK3_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_x) -> true % 60.68/60.54 314: ic(sK3_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_x) -> true % 60.68/60.54 315: icext(uri_rdfs_Class, uri_rdf_List) -> true % 60.68/60.54 316: ic(uri_rdf_List) -> true % 60.68/60.54 317: iext(uri_rdf_type, uri_rdf_List, uri_rdfs_Class) -> true % 60.68/60.54 318: iext(uri_rdf_type, sK3_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_x, uri_rdfs_Class) -> true % 60.68/60.54 319: iext(uri_rdf_type, uri_owl_Class, uri_rdfs_Class) -> true % 60.68/60.54 320: iext(uri_rdfs_subClassOf, uri_owl_Class, uri_rdfs_Resource) -> true % 60.68/60.54 321: iext(uri_rdfs_subClassOf, uri_owl_Class, uri_owl_Class) -> true % 60.68/60.54 322: iext(uri_rdfs_subClassOf, sK3_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_x, uri_rdfs_Resource) -> true % 60.68/60.54 323: iext(uri_rdfs_subClassOf, sK3_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_x, sK3_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_x) -> true % 60.68/60.54 324: iext(uri_rdfs_subClassOf, uri_rdf_List, uri_rdf_List) -> true % 60.68/60.54 325: iext(uri_rdfs_subClassOf, uri_rdf_List, uri_rdfs_Resource) -> true % 60.68/60.54 326: ifeq(iext(uri_rdfs_comment, X, Y), true, icext(uri_rdfs_Literal, Y), true) -> true % 60.68/60.54 327: ifeq(iext(uri_rdfs_domain, X, Y), true, icext(uri_rdfs_Class, Y), true) -> true % 60.68/60.54 328: icext(uri_rdfs_Class, uri_rdfs_Statement) -> true % 60.68/60.54 329: ic(uri_rdfs_Statement) -> true % 60.68/60.54 330: iext(uri_rdf_type, uri_rdfs_Statement, uri_rdfs_Class) -> true % 60.68/60.54 331: iext(uri_rdfs_subClassOf, uri_rdfs_Statement, uri_rdfs_Resource) -> true % 60.68/60.54 332: iext(uri_rdfs_subClassOf, uri_rdfs_Statement, uri_rdfs_Statement) -> true % 60.68/60.54 333: ifeq(iext(uri_rdfs_label, X, Y), true, icext(uri_rdfs_Literal, Y), true) -> true % 60.68/60.54 334: ifeq(iext(uri_rdfs_range, X, Y), true, icext(uri_rdfs_Class, Y), true) -> true % 60.68/60.54 335: ifeq(iext(uri_rdfs_subClassOf, X, Y), true, icext(uri_rdfs_Class, Y), true) -> true % 60.68/60.54 336: ifeq(iext(uri_rdfs_subPropertyOf, X, Y), true, icext(uri_rdf_Property, Y), true) -> true % 60.68/60.54 337: ifeq(iext(uri_rdfs_range, uri_owl_complementOf, X), true, icext(X, uri_ex_A), true) -> true % 60.68/60.54 338: ifeq(iext(uri_rdfs_range, uri_owl_intersectionOf, X), true, icext(X, sK4_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l1), true) -> true % 60.68/60.54 339: ifeq(iext(uri_rdfs_range, uri_rdf_first, X), true, icext(X, sK1_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_y), true) -> true % 60.68/60.54 340: ifeq(iext(uri_rdfs_range, uri_rdf_first, X), true, icext(X, uri_ex_A), true) -> true % 60.68/60.54 341: ifeq(iext(uri_rdfs_range, uri_rdf_rest, X), true, icext(X, uri_rdf_nil), true) -> true % 60.68/60.54 342: ifeq(iext(uri_rdfs_range, uri_rdf_rest, X), true, icext(X, sK2_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l2), true) -> true % 60.68/60.54 343: ifeq(iext(uri_rdfs_range, uri_rdf_type, X), true, icext(X, uri_owl_Class), true) -> true % 60.68/60.54 344: ifeq(iext(uri_rdfs_range, uri_rdf_type, X), true, icext(X, sK3_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_x), true) -> true % 60.68/60.54 345: ifeq(iext(uri_rdfs_range, uri_rdf_type, X), true, icext(X, uri_rdfs_Class), true) -> true % 60.68/60.54 346: ifeq(iext(uri_rdfs_range, uri_rdf_type, X), true, icext(X, uri_rdfs_Datatype), true) -> true % 60.68/60.54 347: ifeq(iext(uri_rdfs_range, uri_rdf_type, X), true, icext(X, uri_rdf_Property), true) -> true % 60.68/60.54 348: ifeq(iext(uri_rdfs_range, uri_rdf_type, X), true, icext(X, uri_rdfs_ContainerMembershipProperty), true) -> true % 60.68/60.54 349: ifeq(iext(uri_rdfs_range, uri_rdf_type, X), true, icext(X, uri_rdf_List), true) -> true % 60.68/60.54 350: ifeq(iext(uri_rdfs_range, uri_rdfs_domain, X), true, icext(X, uri_rdfs_Resource), true) -> true % 60.68/60.54 351: ifeq(iext(uri_rdfs_range, uri_rdfs_domain, X), true, icext(X, uri_rdf_List), true) -> true % 60.68/60.54 352: ifeq(iext(uri_rdfs_range, uri_rdfs_domain, X), true, icext(X, uri_rdfs_Statement), true) -> true % 60.68/60.54 353: ifeq(iext(uri_rdfs_range, uri_rdfs_domain, X), true, icext(X, uri_rdf_Property), true) -> true % 60.68/60.54 354: ifeq(iext(uri_rdfs_range, uri_rdfs_domain, X), true, icext(X, uri_rdfs_Class), true) -> true % 60.68/60.54 355: ifeq(iext(uri_rdfs_range, uri_rdfs_range, X), true, icext(X, uri_rdfs_Resource), true) -> true % 60.68/60.54 356: ifeq(iext(uri_rdfs_range, uri_rdfs_range, X), true, icext(X, uri_rdf_List), true) -> true % 60.68/60.54 357: ifeq(iext(uri_rdfs_range, uri_rdfs_range, X), true, icext(X, uri_rdfs_Class), true) -> true % 60.68/60.54 358: ifeq(iext(uri_rdfs_range, uri_rdfs_range, X), true, icext(X, uri_rdfs_Literal), true) -> true % 60.68/60.54 359: ifeq(iext(uri_rdfs_range, uri_rdfs_range, X), true, icext(X, uri_rdf_Property), true) -> true % 60.68/60.54 360: ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, X), true, icext(X, uri_rdfs_Container), true) -> true % 60.68/60.54 361: ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, X), true, icext(X, uri_rdfs_Literal), true) -> true % 60.68/60.54 362: ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, X), true, icext(X, uri_rdf_Property), true) -> true % 60.68/60.54 363: ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, X), true, icext(X, uri_rdfs_Class), true) -> true % 60.68/60.54 364: ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, X), true, icext(X, uri_rdfs_seeAlso), true) -> true % 60.68/60.54 365: ifeq(iext(uri_rdfs_range, uri_rdf_type, X), true, icext(X, uri_rdfs_Resource), true) -> true % 60.68/60.54 366: ifeq(iext(uri_rdfs_subClassOf, uri_rdf_List, X), true, icext(X, sK2_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l2), true) -> true % 60.68/60.54 367: ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, X), true, icext(X, uri_rdfs_Resource), true) -> true % 60.68/60.54 368: ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, X), true, icext(X, uri_rdfs_Statement), true) -> true % 60.68/60.54 369: ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, X), true, icext(X, uri_owl_Class), true) -> true % 60.68/60.54 370: ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, X), true, icext(X, sK3_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_x), true) -> true % 60.68/60.54 371: ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, X), true, icext(X, uri_rdf_List), true) -> true % 60.68/60.54 372: ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, X), true, icext(X, uri_owl_complementOf), true) -> true % 60.68/60.54 373: ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, X), true, icext(X, uri_rdfs_Seq), true) -> true % 60.68/60.54 374: ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, X), true, icext(X, uri_owl_intersectionOf), true) -> true % 60.68/60.54 375: ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, X), true, icext(X, uri_rdfs_Datatype), true) -> true % 60.68/60.54 376: ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, X), true, icext(X, uri_rdfs_ContainerMembershipProperty), true) -> true % 60.68/60.54 377: ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, X), true, icext(X, uri_rdfs_member), true) -> true % 60.68/60.54 378: ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, X), true, icext(X, uri_rdf__2), true) -> true % 60.68/60.54 379: ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, X), true, icext(X, uri_rdf__1), true) -> true % 60.68/60.54 380: ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, X), true, icext(X, uri_rdf__3), true) -> true % 60.68/60.54 381: ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, X), true, icext(X, uri_rdf_first), true) -> true % 60.68/60.54 382: ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, X), true, icext(X, uri_rdf_object), true) -> true % 60.68/60.54 383: ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, X), true, icext(X, uri_rdf_type), true) -> true % 60.68/60.54 384: ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, X), true, icext(X, uri_rdf_subject), true) -> true % 60.68/60.54 385: ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, X), true, icext(X, uri_rdf_rest), true) -> true % 60.68/60.54 386: ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, X), true, icext(X, uri_rdf_value), true) -> true % 60.68/60.54 387: ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, X), true, icext(X, uri_rdfs_isDefinedBy), true) -> true % 60.68/60.54 388: ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, X), true, icext(X, uri_rdfs_domain), true) -> true % 60.68/60.54 389: ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, X), true, icext(X, uri_rdfs_range), true) -> true % 60.68/60.54 390: ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, X), true, icext(X, uri_rdfs_subClassOf), true) -> true % 60.68/60.54 391: ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, X), true, icext(X, uri_rdfs_subPropertyOf), true) -> true % 60.68/60.54 392: ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, X), true, icext(X, uri_rdf_XMLLiteral), true) -> true % 60.68/60.54 393: ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, X), true, icext(X, uri_rdf_Bag), true) -> true % 60.68/60.54 394: ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, X), true, icext(X, uri_rdf_Alt), true) -> true % 60.68/60.54 395: ifeq(icext(uri_owl_Class, X), true, icext(uri_owl_Class, X), true) -> true % 60.68/60.54 396: ifeq(icext(sK3_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_x, X), true, icext(sK3_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_x, X), true) -> true % 60.68/60.54 397: ifeq(icext(uri_rdf_List, X), true, icext(uri_rdf_List, X), true) -> true % 60.68/60.54 398: ifeq(icext(uri_rdfs_Statement, X), true, icext(uri_rdfs_Statement, X), true) -> true % 60.68/60.54 399: ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, X), true, icext(X, uri_owl_Class), true) -> true % 60.68/60.54 400: ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, X), true, icext(X, uri_rdf_List), true) -> true % 60.68/60.54 401: ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, X), true, icext(X, sK3_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_x), true) -> true % 60.68/60.54 402: ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, X), true, icext(X, uri_rdfs_Statement), true) -> true % 60.68/60.54 403: ifeq(iext(uri_rdfs_range, X, uri_rdfs_Resource), true, ifeq(iext(X, Y, Z), true, true, true), true) -> true % 60.68/60.54 404: ifeq(iext(uri_rdfs_range, X, uri_owl_Class), true, ifeq(iext(X, Y, uri_ex_B), true, true, true), true) -> true % 60.68/60.54 405: ifeq(iext(uri_rdfs_range, X, uri_owl_Class), true, ifeq(iext(X, Y, uri_ex_A), true, true, true), true) -> true % 60.68/60.54 406: ifeq(iext(uri_rdfs_range, X, sK3_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_x), true, ifeq(iext(X, Y, uri_ex_w), true, true, true), true) -> true % 60.68/60.54 407: ifeq(iext(uri_rdfs_range, X, uri_rdf_List), true, ifeq(iext(X, Y, uri_rdf_nil), true, true, true), true) -> true % 60.68/60.54 408: ifeq(iext(uri_rdfs_range, X, uri_rdf_Property), true, ifeq(iext(X, Y, uri_rdf__1), true, true, true), true) -> true % 60.68/60.54 409: ifeq(iext(uri_rdfs_range, X, uri_rdf_Property), true, ifeq(iext(X, Y, uri_rdf_rest), true, true, true), true) -> true % 60.68/60.54 410: ifeq(iext(uri_rdfs_range, X, uri_rdf_Property), true, ifeq(iext(X, Y, uri_rdf__3), true, true, true), true) -> true % 60.68/60.54 411: ifeq(iext(uri_rdfs_range, X, uri_rdf_Property), true, ifeq(iext(X, Y, uri_rdf_object), true, true, true), true) -> true % 60.68/60.54 412: ifeq(iext(uri_rdfs_range, X, uri_rdf_Property), true, ifeq(iext(X, Y, uri_rdf_first), true, true, true), true) -> true % 60.68/60.54 413: ifeq(iext(uri_rdfs_range, X, uri_rdf_Property), true, ifeq(iext(X, Y, uri_rdf__2), true, true, true), true) -> true % 60.68/60.54 414: ifeq(iext(uri_rdfs_range, X, uri_rdf_Property), true, ifeq(iext(X, Y, uri_rdf_subject), true, true, true), true) -> true % 60.68/60.54 415: ifeq(iext(uri_rdfs_range, X, uri_rdf_Property), true, ifeq(iext(X, Y, uri_rdf_value), true, true, true), true) -> true % 60.68/60.54 416: ifeq(iext(uri_rdfs_range, X, uri_rdf_Property), true, ifeq(iext(X, Y, uri_rdf_type), true, true, true), true) -> true % 60.68/60.54 417: ifeq(iext(uri_rdfs_range, X, uri_rdfs_ContainerMembershipProperty), true, ifeq(iext(X, Y, uri_rdf__1), true, true, true), true) -> true % 60.68/60.54 418: ifeq(iext(uri_rdfs_range, X, uri_rdfs_ContainerMembershipProperty), true, ifeq(iext(X, Y, uri_rdf__2), true, true, true), true) -> true % 60.68/60.54 419: ifeq(iext(uri_rdfs_range, X, uri_rdfs_Datatype), true, ifeq(iext(X, Y, uri_rdf_XMLLiteral), true, true, true), true) -> true % 60.68/60.54 420: ifeq(iext(uri_rdfs_range, X, uri_rdfs_ContainerMembershipProperty), true, ifeq(iext(X, Y, uri_rdf__3), true, true, true), true) -> true % 60.68/60.54 421: ifeq(iext(uri_rdfs_domain, X, Y), true, ifeq(iext(X, Z, W), true, icext(Y, Z), true), true) -> true % 60.68/60.54 422: ifeq(iext(uri_rdfs_comment, X, Y), true, true, true) -> true % 60.68/60.54 423: ifeq(iext(uri_rdfs_label, X, Y), true, true, true) -> true % 60.68/60.54 424: ifeq(iext(uri_rdf_rest, X, Y), true, icext(uri_rdf_List, X), true) -> true % 60.68/60.54 425: icext(uri_rdf_List, sK4_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l1) -> true % 60.68/60.54 426: iext(uri_rdf_type, sK4_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l1, uri_rdf_List) -> true % 60.68/60.54 427: ifeq(iext(uri_rdf_subject, X, Y), true, icext(uri_rdfs_Statement, X), true) -> true % 60.68/60.54 428: ifeq(iext(uri_rdf_object, X, Y), true, icext(uri_rdfs_Statement, X), true) -> true % 60.68/60.54 429: ifeq(iext(uri_rdf_first, X, Y), true, icext(uri_rdf_List, X), true) -> true % 60.68/60.54 430: ifeq(iext(uri_rdf_predicate, X, Y), true, icext(uri_rdfs_Statement, X), true) -> true % 60.68/60.54 431: ifeq(iext(uri_rdfs_domain, X, Y), true, icext(uri_rdf_Property, X), true) -> true % 60.68/60.54 432: icext(uri_rdf_Property, uri_rdf_predicate) -> true % 60.68/60.54 433: icext(uri_rdf_Property, uri_rdfs_comment) -> true % 60.68/60.54 434: icext(uri_rdf_Property, uri_rdfs_label) -> true % 60.68/60.54 435: iext(uri_rdf_type, uri_rdfs_label, uri_rdf_Property) -> true % 60.68/60.54 436: ip(uri_rdfs_label) -> true % 60.68/60.54 437: iext(uri_rdf_type, uri_rdfs_comment, uri_rdf_Property) -> true % 60.68/60.54 438: ip(uri_rdfs_comment) -> true % 60.68/60.54 439: iext(uri_rdf_type, uri_rdf_predicate, uri_rdf_Property) -> true % 60.68/60.54 440: ip(uri_rdf_predicate) -> true % 60.68/60.54 441: iext(uri_rdfs_subPropertyOf, uri_rdf_predicate, uri_rdf_predicate) -> true % 60.68/60.54 442: iext(uri_rdfs_subPropertyOf, uri_rdfs_comment, uri_rdfs_comment) -> true % 60.68/60.54 443: iext(uri_rdfs_subPropertyOf, uri_rdfs_label, uri_rdfs_label) -> true % 60.68/60.54 444: ifeq(iext(uri_rdfs_range, X, Y), true, icext(uri_rdf_Property, X), true) -> true % 60.68/60.54 445: ifeq(iext(uri_rdfs_subClassOf, X, Y), true, icext(uri_rdfs_Class, X), true) -> true % 60.68/60.54 446: ifeq(iext(uri_rdfs_subPropertyOf, X, Y), true, icext(uri_rdf_Property, X), true) -> true % 60.68/60.54 447: ifeq(iext(uri_rdfs_domain, uri_owl_complementOf, X), true, icext(X, sK1_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_y), true) -> true % 60.68/60.54 448: ifeq(iext(uri_rdfs_domain, uri_owl_intersectionOf, X), true, icext(X, sK3_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_x), true) -> true % 60.68/60.54 449: ifeq(iext(uri_rdfs_domain, uri_rdf_first, X), true, icext(X, sK2_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l2), true) -> true % 60.68/60.54 450: ifeq(iext(uri_rdfs_domain, uri_rdf_first, X), true, icext(X, sK4_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l1), true) -> true % 60.68/60.54 451: ifeq(iext(uri_rdfs_domain, uri_rdf_rest, X), true, icext(X, sK2_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l2), true) -> true % 60.68/60.54 452: ifeq(iext(uri_rdfs_domain, uri_rdf_rest, X), true, icext(X, sK4_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l1), true) -> true % 60.68/60.54 453: ifeq(iext(uri_rdfs_domain, uri_rdf_type, X), true, icext(X, uri_ex_A), true) -> true % 60.68/60.54 454: ifeq(iext(uri_rdfs_domain, uri_rdf_type, X), true, icext(X, uri_ex_B), true) -> true % 60.68/60.54 455: ifeq(iext(uri_rdfs_domain, uri_rdf_type, X), true, icext(X, uri_ex_w), true) -> true % 60.68/60.54 456: ifeq(iext(uri_rdfs_domain, uri_rdf_type, X), true, icext(X, uri_rdf_Property), true) -> true % 60.68/60.54 457: ifeq(iext(uri_rdfs_domain, uri_rdf_type, X), true, icext(X, uri_rdf_XMLLiteral), true) -> true % 60.68/60.54 458: ifeq(iext(uri_rdfs_domain, uri_rdf_type, X), true, icext(X, uri_rdf__1), true) -> true % 60.68/60.54 459: ifeq(iext(uri_rdfs_domain, uri_rdf_type, X), true, icext(X, uri_rdf__2), true) -> true % 60.68/60.54 460: ifeq(iext(uri_rdfs_domain, uri_rdf_type, X), true, icext(X, uri_rdf__3), true) -> true % 60.68/60.54 461: ifeq(iext(uri_rdfs_domain, uri_rdf_type, X), true, icext(X, uri_rdf_first), true) -> true % 60.68/60.54 462: ifeq(iext(uri_rdfs_domain, uri_rdf_type, X), true, icext(X, uri_rdf_nil), true) -> true % 60.68/60.54 463: ifeq(iext(uri_rdfs_domain, uri_rdf_type, X), true, icext(X, uri_rdf_object), true) -> true % 60.68/60.54 464: ifeq(iext(uri_rdfs_domain, uri_rdf_type, X), true, icext(X, uri_rdf_rest), true) -> true % 60.68/60.54 465: ifeq(iext(uri_rdfs_domain, uri_rdf_type, X), true, icext(X, uri_rdf_subject), true) -> true % 60.68/60.54 466: ifeq(iext(uri_rdfs_domain, uri_rdf_type, X), true, icext(X, uri_rdf_type), true) -> true % 60.68/60.54 467: ifeq(iext(uri_rdfs_domain, uri_rdf_type, X), true, icext(X, uri_rdf_value), true) -> true % 60.68/60.54 468: ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, X), true, icext(X, uri_rdf__1), true) -> true % 60.68/60.54 469: ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, X), true, icext(X, uri_rdf__2), true) -> true % 60.68/60.54 470: ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, X), true, icext(X, uri_rdf__3), true) -> true % 60.68/60.54 471: ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, X), true, icext(X, uri_rdf_first), true) -> true % 60.68/60.54 472: ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, X), true, icext(X, uri_rdf_object), true) -> true % 60.68/60.54 473: ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, X), true, icext(X, uri_rdf_predicate), true) -> true % 60.68/60.54 474: ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, X), true, icext(X, uri_rdf_rest), true) -> true % 60.68/60.54 475: ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, X), true, icext(X, uri_rdf_subject), true) -> true % 60.68/60.54 476: ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, X), true, icext(X, uri_rdf_type), true) -> true % 60.68/60.54 477: ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, X), true, icext(X, uri_rdf_value), true) -> true % 60.68/60.54 478: ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, X), true, icext(X, uri_rdfs_comment), true) -> true % 60.68/60.54 479: ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, X), true, icext(X, uri_rdfs_domain), true) -> true % 60.68/60.54 480: ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, X), true, icext(X, uri_rdfs_isDefinedBy), true) -> true % 60.68/60.54 481: ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, X), true, icext(X, uri_rdfs_label), true) -> true % 60.68/60.54 482: ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, X), true, icext(X, uri_rdfs_member), true) -> true % 60.68/60.54 483: ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, X), true, icext(X, uri_rdfs_range), true) -> true % 60.68/60.54 484: ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, X), true, icext(X, uri_rdfs_seeAlso), true) -> true % 60.68/60.54 485: ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, X), true, icext(X, uri_rdfs_subClassOf), true) -> true % 60.68/60.54 486: ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, X), true, icext(X, uri_rdfs_subPropertyOf), true) -> true % 60.68/60.54 487: ifeq(iext(uri_rdfs_domain, uri_rdfs_range, X), true, icext(X, uri_rdf__1), true) -> true % 60.68/60.54 488: ifeq(iext(uri_rdfs_domain, uri_rdfs_range, X), true, icext(X, uri_rdf__2), true) -> true % 60.68/60.54 489: ifeq(iext(uri_rdfs_domain, uri_rdfs_range, X), true, icext(X, uri_rdf__3), true) -> true % 60.68/60.54 490: ifeq(iext(uri_rdfs_domain, uri_rdfs_range, X), true, icext(X, uri_rdf_first), true) -> true % 60.68/60.54 491: ifeq(iext(uri_rdfs_domain, uri_rdfs_range, X), true, icext(X, uri_rdf_predicate), true) -> true % 60.68/60.54 492: ifeq(iext(uri_rdfs_domain, uri_rdfs_range, X), true, icext(X, uri_rdf_rest), true) -> true % 60.68/60.54 493: ifeq(iext(uri_rdfs_domain, uri_rdfs_range, X), true, icext(X, uri_rdf_subject), true) -> true % 60.68/60.54 494: ifeq(iext(uri_rdfs_domain, uri_rdfs_range, X), true, icext(X, uri_rdf_type), true) -> true % 60.68/60.54 495: ifeq(iext(uri_rdfs_domain, uri_rdfs_range, X), true, icext(X, uri_rdf_value), true) -> true % 60.68/60.54 496: ifeq(iext(uri_rdfs_domain, uri_rdfs_range, X), true, icext(X, uri_rdfs_comment), true) -> true % 60.68/60.54 497: ifeq(iext(uri_rdfs_domain, uri_rdfs_range, X), true, icext(X, uri_rdfs_domain), true) -> true % 60.68/60.54 498: ifeq(iext(uri_rdfs_domain, uri_rdfs_range, X), true, icext(X, uri_rdfs_isDefinedBy), true) -> true % 60.68/60.54 499: ifeq(iext(uri_rdfs_domain, uri_rdfs_range, X), true, icext(X, uri_rdfs_label), true) -> true % 60.68/60.54 500: ifeq(iext(uri_rdfs_domain, uri_rdfs_range, X), true, icext(X, uri_rdfs_member), true) -> true % 60.68/60.54 501: ifeq(iext(uri_rdfs_domain, uri_rdfs_range, X), true, icext(X, uri_rdfs_range), true) -> true % 60.68/60.54 502: ifeq(iext(uri_rdfs_domain, uri_rdfs_range, X), true, icext(X, uri_rdfs_seeAlso), true) -> true % 60.68/60.54 503: ifeq(iext(uri_rdfs_domain, uri_rdfs_range, X), true, icext(X, uri_rdfs_subClassOf), true) -> true % 60.68/60.54 504: ifeq(iext(uri_rdfs_domain, uri_rdfs_range, X), true, icext(X, uri_rdfs_subPropertyOf), true) -> true % 60.68/60.54 505: ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, X), true, icext(X, uri_rdf_Alt), true) -> true % 60.68/60.54 506: ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, X), true, icext(X, uri_rdf_Bag), true) -> true % 60.68/60.54 507: ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, X), true, icext(X, uri_rdf_XMLLiteral), true) -> true % 60.68/60.54 508: ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, X), true, icext(X, uri_rdfs_ContainerMembershipProperty), true) -> true % 60.68/60.54 509: ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, X), true, icext(X, uri_rdfs_Datatype), true) -> true % 60.68/60.54 510: ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, X), true, icext(X, uri_rdfs_Seq), true) -> true % 60.68/60.54 511: ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, X), true, icext(X, uri_rdfs_isDefinedBy), true) -> true % 60.68/60.54 512: ifeq(iext(uri_rdfs_domain, uri_rdf_type, X), true, icext(X, Y), true) -> true % 60.68/60.54 513: ifeq(iext(uri_rdfs_subClassOf, uri_rdf_List, X), true, icext(X, sK4_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l1), true) -> true % 60.68/60.54 514: ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, X), true, icext(X, uri_rdfs_Literal), true) -> true % 60.68/60.54 515: ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, X), true, icext(X, uri_owl_complementOf), true) -> true % 60.68/60.54 516: ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, X), true, icext(X, uri_owl_intersectionOf), true) -> true % 60.68/60.54 517: ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, X), true, icext(X, uri_rdfs_label), true) -> true % 60.68/60.54 518: ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, X), true, icext(X, uri_rdfs_comment), true) -> true % 60.68/60.54 519: ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, X), true, icext(X, uri_rdf_predicate), true) -> true % 60.68/60.54 520: ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, X), true, icext(X, uri_rdfs_Class), true) -> true % 60.68/60.54 521: ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, X), true, icext(X, uri_rdf_Property), true) -> true % 60.68/60.54 522: ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, X), true, icext(X, uri_rdfs_Container), true) -> true % 60.68/60.54 523: ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, X), true, icext(X, uri_rdf__2), true) -> true % 60.68/60.54 524: ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, X), true, icext(X, uri_rdf__1), true) -> true % 60.68/60.54 525: ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, X), true, icext(X, uri_rdf__3), true) -> true % 60.68/60.54 526: ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, X), true, icext(X, uri_rdf_first), true) -> true % 60.68/60.54 527: ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, X), true, icext(X, uri_rdf_object), true) -> true % 60.68/60.54 528: ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, X), true, icext(X, uri_rdf_type), true) -> true % 60.68/60.54 529: ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, X), true, icext(X, uri_rdf_subject), true) -> true % 60.68/60.54 530: ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, X), true, icext(X, uri_rdf_rest), true) -> true % 60.68/60.54 531: ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, X), true, icext(X, uri_rdf_value), true) -> true % 60.68/60.54 532: ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, X), true, icext(X, uri_rdfs_domain), true) -> true % 60.68/60.54 533: ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, X), true, icext(X, uri_rdfs_range), true) -> true % 60.68/60.54 534: ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, X), true, icext(X, uri_rdfs_seeAlso), true) -> true % 60.68/60.54 535: ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, X), true, icext(X, uri_rdfs_subClassOf), true) -> true % 60.68/60.54 536: ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, X), true, icext(X, uri_rdfs_subPropertyOf), true) -> true % 60.68/60.54 537: ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, X), true, icext(X, uri_rdfs_Resource), true) -> true % 60.68/60.54 538: ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, X), true, icext(X, uri_rdfs_Statement), true) -> true % 60.68/60.54 539: ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, X), true, icext(X, uri_rdf_List), true) -> true % 60.68/60.54 540: ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, X), true, icext(X, uri_rdfs_member), true) -> true % 60.68/60.54 541: ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, X), true, icext(X, sK3_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_x), true) -> true % 60.68/60.54 542: ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, X), true, icext(X, uri_owl_Class), true) -> true % 60.68/60.54 543: ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, X), true, icext(X, uri_rdf_predicate), true) -> true % 60.68/60.54 544: ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, X), true, icext(X, uri_rdf_predicate), true) -> true % 60.68/60.54 545: ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, X), true, icext(X, uri_rdfs_comment), true) -> true % 60.68/60.54 546: ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, X), true, icext(X, uri_rdfs_label), true) -> true % 60.68/60.54 547: ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, X), true, icext(X, uri_rdfs_label), true) -> true % 60.68/60.54 548: ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, X), true, icext(X, uri_rdfs_comment), true) -> true % 60.68/60.54 549: ifeq(iext(uri_rdfs_domain, X, uri_rdfs_Resource), true, ifeq(iext(X, Y, Z), true, true, true), true) -> true % 60.68/60.54 550: ifeq(iext(uri_rdfs_domain, X, uri_owl_Class), true, ifeq(iext(X, uri_ex_A, Y), true, true, true), true) -> true % 60.68/60.54 551: ifeq(iext(uri_rdfs_domain, X, uri_rdf_List), true, ifeq(iext(X, uri_rdf_nil, Y), true, true, true), true) -> true % 60.68/60.54 552: ifeq(iext(uri_rdfs_domain, X, uri_owl_Class), true, ifeq(iext(X, uri_ex_B, Y), true, true, true), true) -> true % 60.68/60.54 553: ifeq(iext(uri_rdfs_domain, X, uri_rdf_Property), true, ifeq(iext(X, uri_rdf__1, Y), true, true, true), true) -> true % 60.68/60.54 554: ifeq(iext(uri_rdfs_domain, X, uri_rdf_Property), true, ifeq(iext(X, uri_rdf__2, Y), true, true, true), true) -> true % 60.68/60.54 555: ifeq(iext(uri_rdfs_domain, X, uri_rdf_Property), true, ifeq(iext(X, uri_rdf_first, Y), true, true, true), true) -> true % 60.68/60.54 556: ifeq(iext(uri_rdfs_domain, X, uri_rdf_Property), true, ifeq(iext(X, uri_rdf__3, Y), true, true, true), true) -> true % 60.68/60.54 557: ifeq(iext(uri_rdfs_domain, X, uri_rdf_Property), true, ifeq(iext(X, uri_rdf_object, Y), true, true, true), true) -> true % 60.68/60.54 558: ifeq(iext(uri_rdfs_domain, X, sK3_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_x), true, ifeq(iext(X, uri_ex_w, Y), true, true, true), true) -> true % 60.68/60.54 559: ifeq(iext(uri_rdfs_domain, X, uri_rdf_Property), true, ifeq(iext(X, uri_rdf_value, Y), true, true, true), true) -> true % 60.68/60.54 560: ifeq(iext(uri_rdfs_domain, X, uri_rdf_Property), true, ifeq(iext(X, uri_rdf_subject, Y), true, true, true), true) -> true % 60.68/60.54 561: ifeq(iext(uri_rdfs_domain, X, uri_rdf_Property), true, ifeq(iext(X, uri_rdf_rest, Y), true, true, true), true) -> true % 60.68/60.54 562: ifeq(iext(uri_rdfs_domain, X, uri_rdf_Property), true, ifeq(iext(X, uri_rdf_type, Y), true, true, true), true) -> true % 60.68/60.54 563: ifeq(iext(uri_rdfs_domain, X, uri_rdfs_ContainerMembershipProperty), true, ifeq(iext(X, uri_rdf__1, Y), true, true, true), true) -> true % 60.68/60.54 564: ifeq(iext(uri_rdfs_domain, X, uri_rdfs_ContainerMembershipProperty), true, ifeq(iext(X, uri_rdf__2, Y), true, true, true), true) -> true % 60.68/60.54 565: ifeq(iext(uri_rdfs_domain, X, uri_rdfs_Datatype), true, ifeq(iext(X, uri_rdf_XMLLiteral, Y), true, true, true), true) -> true % 60.68/60.54 566: ifeq(iext(uri_rdfs_domain, X, uri_rdfs_ContainerMembershipProperty), true, ifeq(iext(X, uri_rdf__3, Y), true, true, true), true) -> true % 60.68/60.54 567: ifeq(iext(uri_rdfs_range, X, uri_rdfs_Class), true, ifeq(iext(X, Y, uri_rdfs_Seq), true, true, true), true) -> true % 60.68/60.54 568: ifeq(iext(uri_rdfs_range, X, uri_rdfs_Class), true, ifeq(iext(X, Y, uri_rdf_Bag), true, true, true), true) -> true % 60.68/60.54 569: ifeq(iext(uri_rdfs_range, X, uri_rdf_List), true, ifeq(iext(X, Y, sK4_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l1), true, true, true), true) -> true % 60.68/60.54 570: ifeq(iext(uri_rdfs_domain, X, uri_rdfs_Class), true, ifeq(iext(X, uri_rdfs_Seq, Y), true, true, true), true) -> true % 60.68/60.54 571: ifeq(iext(uri_rdfs_domain, X, uri_rdfs_Class), true, ifeq(iext(X, uri_rdfs_Statement, Y), true, true, true), true) -> true % 60.68/60.54 572: ifeq(iext(uri_rdfs_domain, X, uri_rdfs_Class), true, ifeq(iext(X, uri_rdf_Property, Y), true, true, true), true) -> true % 60.68/60.54 573: ifeq(iext(uri_rdfs_domain, X, uri_rdfs_Class), true, ifeq(iext(X, uri_rdfs_Container, Y), true, true, true), true) -> true % 60.68/60.54 574: ifeq(iext(uri_rdfs_domain, X, uri_rdfs_Class), true, ifeq(iext(X, uri_rdf_XMLLiteral, Y), true, true, true), true) -> true % 60.68/60.54 575: ifeq(iext(uri_rdfs_domain, X, uri_rdfs_Class), true, ifeq(iext(X, uri_rdfs_Class, Y), true, true, true), true) -> true % 60.68/60.54 576: ifeq(iext(uri_rdfs_domain, X, uri_rdfs_Class), true, ifeq(iext(X, uri_rdfs_ContainerMembershipProperty, Y), true, true, true), true) -> true % 60.68/60.54 577: ifeq(iext(uri_rdfs_domain, X, uri_rdfs_Class), true, ifeq(iext(X, uri_rdfs_Literal, Y), true, true, true), true) -> true % 60.68/60.54 578: ifeq(iext(uri_rdfs_domain, X, uri_rdfs_Class), true, ifeq(iext(X, uri_rdfs_Datatype, Y), true, true, true), true) -> true % 60.68/60.54 579: ifeq(iext(uri_rdfs_domain, X, uri_rdf_Property), true, ifeq(iext(X, uri_rdf_predicate, Y), true, true, true), true) -> true % 60.68/60.54 580: ifeq(iext(uri_rdfs_range, X, uri_rdf_Property), true, ifeq(iext(X, Y, uri_rdf_predicate), true, true, true), true) -> true % 60.68/60.54 581: ifeq(iext(uri_rdfs_domain, X, uri_rdf_List), true, ifeq(iext(X, sK4_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l1, Y), true, true, true), true) -> true % 60.68/60.54 582: ifeq(iext(uri_rdfs_range, X, uri_rdf_Property), true, ifeq(iext(X, Y, uri_rdfs_label), true, true, true), true) -> true % 60.68/60.54 583: ifeq(iext(uri_rdfs_domain, X, uri_rdf_List), true, ifeq(iext(X, sK2_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l2, Y), true, true, true), true) -> true % 60.68/60.54 584: ifeq(iext(uri_rdfs_domain, X, uri_rdf_Property), true, ifeq(iext(X, uri_rdfs_label, Y), true, true, true), true) -> true % 60.68/60.54 585: ifeq(iext(uri_rdfs_domain, X, uri_rdf_Property), true, ifeq(iext(X, uri_rdfs_comment, Y), true, true, true), true) -> true % 60.68/60.54 586: ifeq(iext(uri_rdfs_range, X, uri_rdf_Property), true, ifeq(iext(X, Y, uri_rdfs_comment), true, true, true), true) -> true % 60.68/60.54 587: ifeq(iext(uri_rdfs_domain, X, uri_rdfs_Class), true, ifeq(iext(X, sK3_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_x, Y), true, true, true), true) -> true % 60.68/60.54 588: ifeq(iext(uri_rdfs_domain, X, uri_rdfs_Class), true, ifeq(iext(X, uri_owl_Class, Y), true, true, true), true) -> true % 60.68/60.54 589: ifeq(iext(uri_rdfs_domain, X, uri_rdfs_Class), true, ifeq(iext(X, uri_rdf_Bag, Y), true, true, true), true) -> true % 60.68/60.54 590: ifeq(iext(uri_rdfs_domain, X, uri_rdfs_Class), true, ifeq(iext(X, uri_rdf_Alt, Y), true, true, true), true) -> true % 60.68/60.54 591: ifeq(iext(uri_rdfs_domain, X, uri_rdfs_Class), true, ifeq(iext(X, uri_rdf_List, Y), true, true, true), true) -> true % 60.68/60.54 592: ifeq(iext(uri_rdfs_range, X, uri_rdfs_Class), true, ifeq(iext(X, Y, uri_rdfs_Class), true, true, true), true) -> true % 60.68/60.54 593: ifeq(iext(uri_rdfs_range, X, uri_rdfs_Class), true, ifeq(iext(X, Y, uri_rdf_XMLLiteral), true, true, true), true) -> true % 60.68/60.54 594: ifeq(iext(uri_rdfs_range, X, uri_rdfs_Class), true, ifeq(iext(X, Y, uri_rdf_Property), true, true, true), true) -> true % 60.68/60.54 595: ifeq(iext(uri_rdfs_range, X, uri_rdfs_Class), true, ifeq(iext(X, Y, uri_rdfs_Container), true, true, true), true) -> true % 60.68/60.54 596: ifeq(iext(uri_rdfs_range, X, uri_rdfs_Class), true, ifeq(iext(X, Y, uri_rdfs_Datatype), true, true, true), true) -> true % 60.68/60.54 597: ifeq(iext(uri_rdfs_range, X, uri_rdfs_Class), true, ifeq(iext(X, Y, uri_rdfs_ContainerMembershipProperty), true, true, true), true) -> true % 60.68/60.54 598: ifeq(iext(uri_rdfs_range, X, uri_rdfs_Class), true, ifeq(iext(X, Y, uri_rdfs_Literal), true, true, true), true) -> true % 60.68/60.54 599: ifeq(iext(uri_rdfs_range, X, uri_rdf_List), true, ifeq(iext(X, Y, sK2_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l2), true, true, true), true) -> true % 60.68/60.54 600: ifeq(iext(uri_rdfs_range, X, uri_rdfs_Class), true, ifeq(iext(X, Y, uri_rdf_Alt), true, true, true), true) -> true % 60.68/60.54 601: ifeq(iext(uri_rdfs_range, X, uri_rdfs_Class), true, ifeq(iext(X, Y, uri_owl_Class), true, true, true), true) -> true % 60.68/60.54 602: ifeq(iext(uri_rdfs_range, X, uri_rdfs_Class), true, ifeq(iext(X, Y, uri_rdf_List), true, true, true), true) -> true % 60.68/60.54 603: ifeq(iext(uri_rdfs_range, X, uri_rdfs_Class), true, ifeq(iext(X, Y, sK3_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_x), true, true, true), true) -> true % 60.68/60.54 604: ifeq(iext(uri_rdfs_range, X, uri_rdfs_Class), true, ifeq(iext(X, Y, uri_rdfs_Statement), true, true, true), true) -> true % 60.68/60.54 605: ifeq(iext(uri_rdfs_range, X, uri_rdf_Property), true, ifeq(iext(X, Y, uri_rdfs_isDefinedBy), true, true, true), true) -> true % 60.68/60.54 606: ifeq(iext(uri_rdfs_range, X, uri_rdf_Property), true, ifeq(iext(X, Y, uri_rdfs_subClassOf), true, true, true), true) -> true % 60.68/60.54 607: ifeq(iext(uri_rdfs_range, X, uri_rdf_Property), true, ifeq(iext(X, Y, uri_rdfs_subPropertyOf), true, true, true), true) -> true % 60.68/60.54 608: ifeq(iext(uri_rdfs_range, X, uri_rdf_Property), true, ifeq(iext(X, Y, uri_rdfs_range), true, true, true), true) -> true % 60.68/60.54 609: ifeq(iext(uri_rdfs_range, X, uri_rdf_Property), true, ifeq(iext(X, Y, uri_rdfs_seeAlso), true, true, true), true) -> true % 60.68/60.54 610: ifeq(iext(uri_rdfs_domain, X, uri_rdf_Property), true, ifeq(iext(X, uri_owl_intersectionOf, Y), true, true, true), true) -> true % 60.68/60.54 611: ifeq(iext(uri_rdfs_domain, X, uri_rdf_Property), true, ifeq(iext(X, uri_owl_complementOf, Y), true, true, true), true) -> true % 60.68/60.54 612: ifeq(iext(uri_rdfs_domain, X, uri_rdf_Property), true, ifeq(iext(X, uri_rdfs_isDefinedBy, Y), true, true, true), true) -> true % 60.68/60.54 613: ifeq(iext(uri_rdfs_subPropertyOf, X, Y), true, ifeq(iext(X, Z, W), true, iext(Y, Z, W), true), true) -> true % 60.68/60.54 614: ifeq(iext(uri_rdfs_isDefinedBy, X, Y), true, iext(uri_rdfs_seeAlso, X, Y), true) -> true % 60.68/60.54 615: ifeq(iext(uri_rdfs_subPropertyOf, uri_owl_complementOf, X), true, iext(X, sK1_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_y, uri_ex_A), true) -> true % 60.68/60.54 616: ifeq(iext(uri_rdfs_subPropertyOf, uri_owl_intersectionOf, X), true, iext(X, sK3_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_x, sK4_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l1), true) -> true % 60.68/60.54 617: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_first, X), true, iext(X, sK2_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l2, sK1_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_y), true) -> true % 60.68/60.54 618: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_first, X), true, iext(X, sK4_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l1, uri_ex_A), true) -> true % 60.68/60.54 619: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_rest, X), true, iext(X, sK2_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l2, uri_rdf_nil), true) -> true % 60.68/60.54 620: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_rest, X), true, iext(X, sK4_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l1, sK2_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l2), true) -> true % 60.68/60.54 621: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, X), true, iext(X, uri_ex_A, uri_owl_Class), true) -> true % 60.68/60.54 622: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, X), true, iext(X, uri_ex_B, uri_owl_Class), true) -> true % 60.68/60.54 623: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, X), true, iext(X, uri_ex_w, sK3_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_x), true) -> true % 60.68/60.54 624: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, X), true, iext(X, uri_rdf_Property, uri_rdfs_Class), true) -> true % 60.68/60.54 625: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, X), true, iext(X, uri_rdf_XMLLiteral, uri_rdfs_Datatype), true) -> true % 60.68/60.54 626: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, X), true, iext(X, uri_rdf__1, uri_rdf_Property), true) -> true % 60.68/60.54 627: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, X), true, iext(X, uri_rdf__1, uri_rdfs_ContainerMembershipProperty), true) -> true % 60.68/60.54 628: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, X), true, iext(X, uri_rdf__2, uri_rdf_Property), true) -> true % 60.68/60.54 629: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, X), true, iext(X, uri_rdf__2, uri_rdfs_ContainerMembershipProperty), true) -> true % 60.68/60.54 630: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, X), true, iext(X, uri_rdf__3, uri_rdf_Property), true) -> true % 60.68/60.54 631: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, X), true, iext(X, uri_rdf__3, uri_rdfs_ContainerMembershipProperty), true) -> true % 60.68/60.54 632: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, X), true, iext(X, uri_rdf_first, uri_rdf_Property), true) -> true % 60.68/60.54 633: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, X), true, iext(X, uri_rdf_nil, uri_rdf_List), true) -> true % 60.68/60.54 634: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, X), true, iext(X, uri_rdf_object, uri_rdf_Property), true) -> true % 60.68/60.54 635: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, X), true, iext(X, uri_rdf_rest, uri_rdf_Property), true) -> true % 60.68/60.54 636: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, X), true, iext(X, uri_rdf_subject, uri_rdf_Property), true) -> true % 60.68/60.54 637: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, X), true, iext(X, uri_rdf_type, uri_rdf_Property), true) -> true % 60.68/60.54 638: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, X), true, iext(X, uri_rdf_value, uri_rdf_Property), true) -> true % 60.68/60.54 639: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, X), true, iext(X, uri_rdf__1, uri_rdfs_Resource), true) -> true % 60.68/60.54 640: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, X), true, iext(X, uri_rdf__2, uri_rdfs_Resource), true) -> true % 60.68/60.54 641: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, X), true, iext(X, uri_rdf__3, uri_rdfs_Resource), true) -> true % 60.68/60.54 642: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, X), true, iext(X, uri_rdf_first, uri_rdf_List), true) -> true % 60.68/60.54 643: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, X), true, iext(X, uri_rdf_object, uri_rdfs_Statement), true) -> true % 60.68/60.54 644: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, X), true, iext(X, uri_rdf_predicate, uri_rdfs_Statement), true) -> true % 60.68/60.54 645: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, X), true, iext(X, uri_rdf_rest, uri_rdf_List), true) -> true % 60.68/60.54 646: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, X), true, iext(X, uri_rdf_subject, uri_rdfs_Statement), true) -> true % 60.68/60.54 647: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, X), true, iext(X, uri_rdf_type, uri_rdfs_Resource), true) -> true % 60.68/60.54 648: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, X), true, iext(X, uri_rdf_value, uri_rdfs_Resource), true) -> true % 60.68/60.54 649: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, X), true, iext(X, uri_rdfs_comment, uri_rdfs_Resource), true) -> true % 60.68/60.54 650: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, X), true, iext(X, uri_rdfs_domain, uri_rdf_Property), true) -> true % 60.68/60.54 651: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, X), true, iext(X, uri_rdfs_isDefinedBy, uri_rdfs_Resource), true) -> true % 60.68/60.54 652: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, X), true, iext(X, uri_rdfs_label, uri_rdfs_Resource), true) -> true % 60.68/60.54 653: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, X), true, iext(X, uri_rdfs_member, uri_rdfs_Resource), true) -> true % 60.68/60.54 654: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, X), true, iext(X, uri_rdfs_range, uri_rdf_Property), true) -> true % 60.68/60.54 655: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, X), true, iext(X, uri_rdfs_seeAlso, uri_rdfs_Resource), true) -> true % 60.68/60.54 656: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, X), true, iext(X, uri_rdfs_subClassOf, uri_rdfs_Class), true) -> true % 60.68/60.54 657: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, X), true, iext(X, uri_rdfs_subPropertyOf, uri_rdf_Property), true) -> true % 60.68/60.54 658: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, X), true, iext(X, uri_rdf__1, uri_rdfs_Resource), true) -> true % 60.68/60.54 659: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, X), true, iext(X, uri_rdf__2, uri_rdfs_Resource), true) -> true % 60.68/60.54 660: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, X), true, iext(X, uri_rdf__3, uri_rdfs_Resource), true) -> true % 60.68/60.54 661: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, X), true, iext(X, uri_rdf_first, uri_rdfs_Resource), true) -> true % 60.68/60.54 662: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, X), true, iext(X, uri_rdf_predicate, uri_rdfs_Resource), true) -> true % 60.68/60.54 663: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, X), true, iext(X, uri_rdf_rest, uri_rdf_List), true) -> true % 60.68/60.54 664: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, X), true, iext(X, uri_rdf_subject, uri_rdfs_Resource), true) -> true % 60.68/60.54 665: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, X), true, iext(X, uri_rdf_type, uri_rdfs_Class), true) -> true % 60.68/60.54 666: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, X), true, iext(X, uri_rdf_value, uri_rdfs_Resource), true) -> true % 60.68/60.54 667: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, X), true, iext(X, uri_rdfs_comment, uri_rdfs_Literal), true) -> true % 60.68/60.54 668: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, X), true, iext(X, uri_rdfs_domain, uri_rdfs_Class), true) -> true % 60.68/60.54 669: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, X), true, iext(X, uri_rdfs_isDefinedBy, uri_rdfs_Resource), true) -> true % 60.68/60.54 670: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, X), true, iext(X, uri_rdfs_label, uri_rdfs_Literal), true) -> true % 60.68/60.54 671: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, X), true, iext(X, uri_rdfs_member, uri_rdfs_Resource), true) -> true % 60.68/60.54 672: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, X), true, iext(X, uri_rdfs_range, uri_rdfs_Class), true) -> true % 60.68/60.54 673: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, X), true, iext(X, uri_rdfs_seeAlso, uri_rdfs_Resource), true) -> true % 60.68/60.54 674: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, X), true, iext(X, uri_rdfs_subClassOf, uri_rdfs_Class), true) -> true % 60.68/60.54 675: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, X), true, iext(X, uri_rdfs_subPropertyOf, uri_rdf_Property), true) -> true % 60.68/60.54 676: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, X), true, iext(X, uri_rdf_Alt, uri_rdfs_Container), true) -> true % 60.68/60.54 677: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, X), true, iext(X, uri_rdf_Bag, uri_rdfs_Container), true) -> true % 60.68/60.54 678: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, X), true, iext(X, uri_rdf_XMLLiteral, uri_rdfs_Literal), true) -> true % 60.68/60.54 679: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, X), true, iext(X, uri_rdfs_ContainerMembershipProperty, uri_rdf_Property), true) -> true % 60.68/60.54 680: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, X), true, iext(X, uri_rdfs_Datatype, uri_rdfs_Class), true) -> true % 60.68/60.54 681: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, X), true, iext(X, uri_rdfs_Seq, uri_rdfs_Container), true) -> true % 60.68/60.54 682: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, X), true, iext(X, uri_rdfs_isDefinedBy, uri_rdfs_seeAlso), true) -> true % 60.68/60.54 683: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, X), true, iext(X, Y, uri_rdfs_Resource), true) -> true % 60.68/60.54 684: ifeq(iext(uri_rdfs_subPropertyOf, X, Y), true, iext(uri_rdfs_subPropertyOf, X, Y), true) -> true % 60.68/60.54 685: ifeq(iext(uri_rdfs_range, X, Y), true, iext(uri_rdfs_range, X, Y), true) -> true % 60.68/60.54 686: ifeq(iext(uri_rdfs_seeAlso, X, Y), true, iext(uri_rdfs_seeAlso, X, Y), true) -> true % 60.68/60.54 687: ifeq(iext(uri_rdfs_subClassOf, X, Y), true, iext(uri_rdfs_subClassOf, X, Y), true) -> true % 60.68/60.54 688: ifeq(iext(uri_rdf_subject, X, Y), true, iext(uri_rdf_subject, X, Y), true) -> true % 60.68/60.54 689: ifeq(iext(uri_rdfs_domain, X, Y), true, iext(uri_rdfs_domain, X, Y), true) -> true % 60.68/60.54 690: ifeq(iext(uri_rdf__2, X, Y), true, iext(uri_rdf__2, X, Y), true) -> true % 60.68/60.54 691: ifeq(iext(uri_rdfs_isDefinedBy, X, Y), true, iext(uri_rdfs_isDefinedBy, X, Y), true) -> true % 60.68/60.54 692: ifeq(iext(uri_owl_complementOf, X, Y), true, iext(uri_owl_complementOf, X, Y), true) -> true % 60.68/60.54 693: ifeq(iext(uri_rdf_value, X, Y), true, iext(uri_rdf_value, X, Y), true) -> true % 60.68/60.54 694: ifeq(iext(uri_rdf_type, X, Y), true, iext(uri_rdf_type, X, Y), true) -> true % 60.68/60.54 695: ifeq(iext(uri_rdf__1, X, Y), true, iext(uri_rdf__1, X, Y), true) -> true % 60.68/60.54 696: ifeq(iext(uri_owl_intersectionOf, X, Y), true, iext(uri_owl_intersectionOf, X, Y), true) -> true % 60.68/60.54 697: ifeq(iext(uri_rdf__1, X, Y), true, iext(uri_rdfs_member, X, Y), true) -> true % 60.68/60.54 698: ifeq(iext(uri_rdf__3, X, Y), true, iext(uri_rdfs_member, X, Y), true) -> true % 60.68/60.54 699: ifeq(iext(uri_rdf__2, X, Y), true, iext(uri_rdfs_member, X, Y), true) -> true % 60.68/60.54 700: ifeq(iext(uri_rdf__3, X, Y), true, iext(uri_rdf__3, X, Y), true) -> true % 60.68/60.54 701: ifeq(iext(uri_rdf_first, X, Y), true, iext(uri_rdf_first, X, Y), true) -> true % 60.68/60.54 702: ifeq(iext(uri_rdf_rest, X, Y), true, iext(uri_rdf_rest, X, Y), true) -> true % 60.68/60.54 703: ifeq(iext(uri_rdf_object, X, Y), true, iext(uri_rdf_object, X, Y), true) -> true % 60.68/60.54 704: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, X), true, iext(X, uri_owl_intersectionOf, uri_rdf_Property), true) -> true % 60.68/60.54 705: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, X), true, iext(X, uri_owl_complementOf, uri_rdf_Property), true) -> true % 60.68/60.54 706: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, X), true, iext(X, uri_rdfs_Literal, uri_rdfs_Resource), true) -> true % 60.68/60.54 707: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, X), true, iext(X, uri_rdfs_domain, uri_rdf_Property), true) -> true % 60.68/60.54 708: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, X), true, iext(X, uri_rdfs_isDefinedBy, uri_rdf_Property), true) -> true % 60.68/60.54 709: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, X), true, iext(X, uri_rdfs_Seq, uri_rdfs_Resource), true) -> true % 60.68/60.54 710: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, X), true, iext(X, uri_rdfs_Datatype, uri_rdfs_Resource), true) -> true % 60.68/60.54 711: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, X), true, iext(X, uri_rdfs_Datatype, uri_rdfs_Datatype), true) -> true % 60.68/60.54 712: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, X), true, iext(X, uri_rdfs_Literal, uri_rdfs_Literal), true) -> true % 60.68/60.54 713: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, X), true, iext(X, uri_owl_complementOf, uri_owl_complementOf), true) -> true % 60.68/60.54 714: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, X), true, iext(X, uri_rdfs_Seq, uri_rdfs_Seq), true) -> true % 60.68/60.54 715: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, X), true, iext(X, uri_rdf__1, uri_rdf__1), true) -> true % 60.68/60.54 716: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, X), true, iext(X, uri_owl_intersectionOf, uri_owl_intersectionOf), true) -> true % 60.68/60.54 717: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, X), true, iext(X, uri_rdf__1, uri_rdfs_member), true) -> true % 60.68/60.54 718: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, X), true, iext(X, uri_rdfs_Class, uri_rdfs_Class), true) -> true % 60.68/60.54 719: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, X), true, iext(X, uri_rdf_XMLLiteral, uri_rdfs_Resource), true) -> true % 60.68/60.54 720: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, X), true, iext(X, uri_rdfs_Class, uri_rdfs_Resource), true) -> true % 60.68/60.54 721: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, X), true, iext(X, uri_rdf_Property, uri_rdfs_Resource), true) -> true % 60.68/60.54 722: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, X), true, iext(X, uri_rdf_Bag, uri_rdfs_Resource), true) -> true % 60.68/60.54 723: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, X), true, iext(X, uri_rdfs_ContainerMembershipProperty, uri_rdfs_ContainerMembershipProperty), true) -> true % 60.68/60.54 724: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, X), true, iext(X, uri_rdfs_ContainerMembershipProperty, uri_rdfs_Resource), true) -> true % 60.68/60.54 725: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, X), true, iext(X, uri_rdfs_Container, uri_rdfs_Container), true) -> true % 60.68/60.54 726: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, X), true, iext(X, uri_rdfs_Container, uri_rdfs_Resource), true) -> true % 60.68/60.54 727: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, X), true, iext(X, uri_rdf__3, uri_rdfs_member), true) -> true % 60.68/60.54 728: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, X), true, iext(X, uri_rdf__2, uri_rdf__2), true) -> true % 60.68/60.54 729: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, X), true, iext(X, uri_rdf__3, uri_rdf__3), true) -> true % 60.68/60.54 730: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, X), true, iext(X, uri_rdf__2, uri_rdfs_member), true) -> true % 60.68/60.54 731: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, X), true, iext(X, uri_rdf_first, uri_rdf_first), true) -> true % 60.68/60.54 732: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, X), true, iext(X, uri_rdf_rest, uri_rdf_rest), true) -> true % 60.68/60.54 733: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, X), true, iext(X, uri_rdf_object, uri_rdf_object), true) -> true % 60.68/60.54 734: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, X), true, iext(X, uri_rdf_value, uri_rdf_value), true) -> true % 60.68/60.54 735: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, X), true, iext(X, uri_rdf_type, uri_rdf_type), true) -> true % 60.68/60.54 736: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, X), true, iext(X, uri_rdf_subject, uri_rdf_subject), true) -> true % 60.68/60.54 737: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, X), true, iext(X, uri_rdfs_isDefinedBy, uri_rdfs_isDefinedBy), true) -> true % 60.68/60.54 738: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, X), true, iext(X, uri_rdfs_domain, uri_rdfs_domain), true) -> true % 60.68/60.54 739: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, X), true, iext(X, uri_rdfs_range, uri_rdfs_range), true) -> true % 60.68/60.54 740: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, X), true, iext(X, uri_rdfs_seeAlso, uri_rdfs_seeAlso), true) -> true % 60.68/60.54 741: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, X), true, iext(X, uri_rdfs_subClassOf, uri_rdfs_subClassOf), true) -> true % 60.68/60.54 742: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, X), true, iext(X, uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf), true) -> true % 60.68/60.54 743: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, X), true, iext(X, uri_rdf_XMLLiteral, uri_rdf_XMLLiteral), true) -> true % 60.68/60.54 744: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, X), true, iext(X, uri_rdf_Alt, uri_rdfs_Resource), true) -> true % 60.68/60.54 745: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, X), true, iext(X, uri_rdf_Property, uri_rdf_Property), true) -> true % 60.68/60.54 746: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, X), true, iext(X, uri_rdf_Bag, uri_rdf_Bag), true) -> true % 60.68/60.54 747: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, X), true, iext(X, uri_rdf_Alt, uri_rdf_Alt), true) -> true % 60.68/60.54 748: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, X), true, iext(X, uri_rdfs_subPropertyOf, uri_rdf_Property), true) -> true % 60.68/60.54 749: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, X), true, iext(X, uri_rdfs_subClassOf, uri_rdf_Property), true) -> true % 60.68/60.54 750: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, X), true, iext(X, uri_rdfs_range, uri_rdf_Property), true) -> true % 60.68/60.54 751: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, X), true, iext(X, uri_rdfs_seeAlso, uri_rdf_Property), true) -> true % 60.68/60.54 752: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, X), true, iext(X, uri_rdfs_Container, uri_rdfs_Class), true) -> true % 60.68/60.54 753: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, X), true, iext(X, uri_rdfs_Class, uri_rdfs_Class), true) -> true % 60.68/60.54 754: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, X), true, iext(X, uri_rdfs_ContainerMembershipProperty, uri_rdfs_Class), true) -> true % 60.68/60.54 755: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, X), true, iext(X, uri_rdfs_label, uri_rdf_Property), true) -> true % 60.68/60.54 756: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, X), true, iext(X, uri_rdfs_Datatype, uri_rdfs_Class), true) -> true % 60.68/60.54 757: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, X), true, iext(X, sK2_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l2, uri_rdf_List), true) -> true % 60.68/60.54 758: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, X), true, iext(X, sK4_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l1, uri_rdf_List), true) -> true % 60.68/60.54 759: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, X), true, iext(X, uri_rdf_Alt, uri_rdfs_Class), true) -> true % 60.68/60.54 760: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, X), true, iext(X, uri_rdf_List, uri_rdfs_Class), true) -> true % 60.68/60.54 761: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, X), true, iext(X, sK3_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_x, uri_rdfs_Class), true) -> true % 60.68/60.54 762: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, X), true, iext(X, uri_rdfs_Seq, uri_rdfs_Class), true) -> true % 60.68/60.54 763: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, X), true, iext(X, uri_rdfs_Statement, uri_rdfs_Class), true) -> true % 60.68/60.54 764: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, X), true, iext(X, uri_rdfs_comment, uri_rdf_Property), true) -> true % 60.68/60.54 765: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, X), true, iext(X, uri_rdfs_Literal, uri_rdfs_Class), true) -> true % 60.68/60.54 766: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, X), true, iext(X, uri_rdf_XMLLiteral, uri_rdfs_Class), true) -> true % 60.68/60.54 767: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, X), true, iext(X, uri_rdf_predicate, uri_rdf_Property), true) -> true % 60.68/60.54 768: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, X), true, iext(X, uri_rdf_Bag, uri_rdfs_Class), true) -> true % 60.68/60.54 769: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, X), true, iext(X, uri_owl_Class, uri_rdfs_Class), true) -> true % 60.68/60.54 770: ifeq(iext(uri_rdfs_member, X, Y), true, iext(uri_rdfs_member, X, Y), true) -> true % 60.68/60.54 771: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, X), true, iext(X, uri_rdfs_Resource, uri_rdfs_Resource), true) -> true % 60.68/60.54 772: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, X), true, iext(X, uri_rdfs_member, uri_rdf_Property), true) -> true % 60.68/60.54 773: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, X), true, iext(X, uri_rdfs_Statement, uri_rdfs_Resource), true) -> true % 60.68/60.54 774: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, X), true, iext(X, uri_rdfs_Statement, uri_rdfs_Statement), true) -> true % 60.68/60.54 775: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, X), true, iext(X, sK3_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_x, uri_rdfs_Resource), true) -> true % 60.68/60.54 776: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, X), true, iext(X, sK3_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_x, sK3_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_x), true) -> true % 60.68/60.54 777: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, X), true, iext(X, uri_owl_Class, uri_owl_Class), true) -> true % 60.68/60.54 778: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, X), true, iext(X, uri_rdfs_member, uri_rdfs_member), true) -> true % 60.68/60.54 779: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, X), true, iext(X, uri_rdf_List, uri_rdfs_Resource), true) -> true % 60.68/60.54 780: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, X), true, iext(X, uri_owl_Class, uri_rdfs_Resource), true) -> true % 60.68/60.54 781: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, X), true, iext(X, uri_rdf_List, uri_rdf_List), true) -> true % 60.68/60.54 782: ifeq(iext(uri_rdfs_comment, X, Y), true, iext(uri_rdfs_comment, X, Y), true) -> true % 60.68/60.54 783: ifeq(iext(uri_rdfs_label, X, Y), true, iext(uri_rdfs_label, X, Y), true) -> true % 60.68/60.54 784: ifeq(iext(uri_rdf_predicate, X, Y), true, iext(uri_rdf_predicate, X, Y), true) -> true % 60.68/60.54 785: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, X), true, iext(X, uri_rdfs_Resource, uri_rdfs_Class), true) -> true % 60.68/60.54 786: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, X), true, iext(X, uri_rdfs_comment, uri_rdfs_comment), true) -> true % 60.68/60.54 787: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, X), true, iext(X, uri_rdf_predicate, uri_rdf_predicate), true) -> true % 60.68/60.54 788: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, X), true, iext(X, uri_rdfs_label, uri_rdfs_label), true) -> true % 60.68/60.54 789: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_owl_complementOf), true, ifeq(iext(X, sK1_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_y, uri_ex_A), true, true, true), true) -> true % 60.68/60.54 790: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_owl_intersectionOf), true, ifeq(iext(X, sK3_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_x, sK4_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l1), true, true, true), true) -> true % 60.68/60.54 791: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdf_first), true, ifeq(iext(X, sK2_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l2, sK1_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_y), true, true, true), true) -> true % 60.68/60.54 792: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdf_first), true, ifeq(iext(X, sK4_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l1, uri_ex_A), true, true, true), true) -> true % 60.68/60.54 793: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdf_rest), true, ifeq(iext(X, sK2_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l2, uri_rdf_nil), true, true, true), true) -> true % 60.68/60.54 794: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdf_rest), true, ifeq(iext(X, sK4_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l1, sK2_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l2), true, true, true), true) -> true % 60.68/60.54 795: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdf_type), true, ifeq(iext(X, uri_ex_A, uri_owl_Class), true, true, true), true) -> true % 60.68/60.54 796: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdf_type), true, ifeq(iext(X, uri_ex_B, uri_owl_Class), true, true, true), true) -> true % 60.68/60.54 797: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdf_type), true, ifeq(iext(X, uri_ex_w, sK3_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_x), true, true, true), true) -> true % 60.68/60.54 798: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdf_type), true, ifeq(iext(X, uri_rdf_Property, uri_rdfs_Class), true, true, true), true) -> true % 60.68/60.54 799: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdf_type), true, ifeq(iext(X, uri_rdf_XMLLiteral, uri_rdfs_Datatype), true, true, true), true) -> true % 60.68/60.54 800: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdf_type), true, ifeq(iext(X, uri_rdf__1, uri_rdf_Property), true, true, true), true) -> true % 60.68/60.54 801: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdf_type), true, ifeq(iext(X, uri_rdf__1, uri_rdfs_ContainerMembershipProperty), true, true, true), true) -> true % 60.68/60.54 802: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdf_type), true, ifeq(iext(X, uri_rdf__2, uri_rdf_Property), true, true, true), true) -> true % 60.68/60.54 803: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdf_type), true, ifeq(iext(X, uri_rdf__2, uri_rdfs_ContainerMembershipProperty), true, true, true), true) -> true % 60.68/60.54 804: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdf_type), true, ifeq(iext(X, uri_rdf__3, uri_rdf_Property), true, true, true), true) -> true % 60.68/60.54 805: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdf_type), true, ifeq(iext(X, uri_rdf__3, uri_rdfs_ContainerMembershipProperty), true, true, true), true) -> true % 60.68/60.54 806: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdf_type), true, ifeq(iext(X, uri_rdf_first, uri_rdf_Property), true, true, true), true) -> true % 60.68/60.54 807: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdf_type), true, ifeq(iext(X, uri_rdf_nil, uri_rdf_List), true, true, true), true) -> true % 60.68/60.54 808: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdf_type), true, ifeq(iext(X, uri_rdf_object, uri_rdf_Property), true, true, true), true) -> true % 60.68/60.54 809: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdf_type), true, ifeq(iext(X, uri_rdf_rest, uri_rdf_Property), true, true, true), true) -> true % 60.68/60.54 810: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdf_type), true, ifeq(iext(X, uri_rdf_subject, uri_rdf_Property), true, true, true), true) -> true % 60.68/60.54 811: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdf_type), true, ifeq(iext(X, uri_rdf_type, uri_rdf_Property), true, true, true), true) -> true % 60.68/60.54 812: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdf_type), true, ifeq(iext(X, uri_rdf_value, uri_rdf_Property), true, true, true), true) -> true % 60.68/60.54 813: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_domain), true, ifeq(iext(X, uri_rdf__1, uri_rdfs_Resource), true, true, true), true) -> true % 60.68/60.54 814: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_domain), true, ifeq(iext(X, uri_rdf__2, uri_rdfs_Resource), true, true, true), true) -> true % 60.68/60.54 815: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_domain), true, ifeq(iext(X, uri_rdf__3, uri_rdfs_Resource), true, true, true), true) -> true % 60.68/60.54 816: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_domain), true, ifeq(iext(X, uri_rdf_first, uri_rdf_List), true, true, true), true) -> true % 60.68/60.54 817: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_domain), true, ifeq(iext(X, uri_rdf_object, uri_rdfs_Statement), true, true, true), true) -> true % 60.68/60.54 818: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_domain), true, ifeq(iext(X, uri_rdf_predicate, uri_rdfs_Statement), true, true, true), true) -> true % 60.68/60.54 819: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_domain), true, ifeq(iext(X, uri_rdf_rest, uri_rdf_List), true, true, true), true) -> true % 60.68/60.54 820: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_domain), true, ifeq(iext(X, uri_rdf_subject, uri_rdfs_Statement), true, true, true), true) -> true % 60.68/60.54 821: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_domain), true, ifeq(iext(X, uri_rdf_type, uri_rdfs_Resource), true, true, true), true) -> true % 60.68/60.54 822: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_domain), true, ifeq(iext(X, uri_rdf_value, uri_rdfs_Resource), true, true, true), true) -> true % 60.68/60.54 823: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_domain), true, ifeq(iext(X, uri_rdfs_comment, uri_rdfs_Resource), true, true, true), true) -> true % 60.68/60.54 824: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_domain), true, ifeq(iext(X, uri_rdfs_domain, uri_rdf_Property), true, true, true), true) -> true % 60.68/60.54 825: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_domain), true, ifeq(iext(X, uri_rdfs_isDefinedBy, uri_rdfs_Resource), true, true, true), true) -> true % 60.68/60.54 826: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_domain), true, ifeq(iext(X, uri_rdfs_label, uri_rdfs_Resource), true, true, true), true) -> true % 60.68/60.54 827: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_domain), true, ifeq(iext(X, uri_rdfs_member, uri_rdfs_Resource), true, true, true), true) -> true % 60.68/60.54 828: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_domain), true, ifeq(iext(X, uri_rdfs_range, uri_rdf_Property), true, true, true), true) -> true % 60.68/60.54 829: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_domain), true, ifeq(iext(X, uri_rdfs_seeAlso, uri_rdfs_Resource), true, true, true), true) -> true % 60.68/60.54 830: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_domain), true, ifeq(iext(X, uri_rdfs_subClassOf, uri_rdfs_Class), true, true, true), true) -> true % 60.68/60.54 831: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_domain), true, ifeq(iext(X, uri_rdfs_subPropertyOf, uri_rdf_Property), true, true, true), true) -> true % 60.68/60.54 832: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_range), true, ifeq(iext(X, uri_rdf__1, uri_rdfs_Resource), true, true, true), true) -> true % 60.68/60.54 833: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_range), true, ifeq(iext(X, uri_rdf__2, uri_rdfs_Resource), true, true, true), true) -> true % 60.68/60.54 834: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_range), true, ifeq(iext(X, uri_rdf__3, uri_rdfs_Resource), true, true, true), true) -> true % 60.68/60.54 835: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_range), true, ifeq(iext(X, uri_rdf_first, uri_rdfs_Resource), true, true, true), true) -> true % 60.68/60.54 836: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_range), true, ifeq(iext(X, uri_rdf_predicate, uri_rdfs_Resource), true, true, true), true) -> true % 60.68/60.54 837: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_range), true, ifeq(iext(X, uri_rdf_rest, uri_rdf_List), true, true, true), true) -> true % 60.68/60.54 838: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_range), true, ifeq(iext(X, uri_rdf_subject, uri_rdfs_Resource), true, true, true), true) -> true % 60.68/60.54 839: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_range), true, ifeq(iext(X, uri_rdf_type, uri_rdfs_Class), true, true, true), true) -> true % 60.68/60.54 840: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_range), true, ifeq(iext(X, uri_rdf_value, uri_rdfs_Resource), true, true, true), true) -> true % 60.68/60.54 841: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_range), true, ifeq(iext(X, uri_rdfs_comment, uri_rdfs_Literal), true, true, true), true) -> true % 60.68/60.54 842: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_range), true, ifeq(iext(X, uri_rdfs_domain, uri_rdfs_Class), true, true, true), true) -> true % 60.68/60.54 843: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_range), true, ifeq(iext(X, uri_rdfs_isDefinedBy, uri_rdfs_Resource), true, true, true), true) -> true % 60.68/60.54 844: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_range), true, ifeq(iext(X, uri_rdfs_label, uri_rdfs_Literal), true, true, true), true) -> true % 60.68/60.54 845: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_range), true, ifeq(iext(X, uri_rdfs_member, uri_rdfs_Resource), true, true, true), true) -> true % 60.68/60.54 846: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_range), true, ifeq(iext(X, uri_rdfs_range, uri_rdfs_Class), true, true, true), true) -> true % 60.68/60.54 847: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_range), true, ifeq(iext(X, uri_rdfs_seeAlso, uri_rdfs_Resource), true, true, true), true) -> true % 60.68/60.54 848: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_range), true, ifeq(iext(X, uri_rdfs_subClassOf, uri_rdfs_Class), true, true, true), true) -> true % 60.68/60.54 849: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_range), true, ifeq(iext(X, uri_rdfs_subPropertyOf, uri_rdf_Property), true, true, true), true) -> true % 60.68/60.54 850: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_subClassOf), true, ifeq(iext(X, uri_rdf_Alt, uri_rdfs_Container), true, true, true), true) -> true % 60.68/60.54 851: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_subClassOf), true, ifeq(iext(X, uri_rdf_Bag, uri_rdfs_Container), true, true, true), true) -> true % 60.68/60.54 852: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_subClassOf), true, ifeq(iext(X, uri_rdf_XMLLiteral, uri_rdfs_Literal), true, true, true), true) -> true % 60.68/60.54 853: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_subClassOf), true, ifeq(iext(X, uri_rdfs_ContainerMembershipProperty, uri_rdf_Property), true, true, true), true) -> true % 60.68/60.54 854: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_subClassOf), true, ifeq(iext(X, uri_rdfs_Datatype, uri_rdfs_Class), true, true, true), true) -> true % 60.68/60.54 855: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_subClassOf), true, ifeq(iext(X, uri_rdfs_Seq, uri_rdfs_Container), true, true, true), true) -> true % 60.68/60.54 856: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_subPropertyOf), true, ifeq(iext(X, uri_rdfs_isDefinedBy, uri_rdfs_seeAlso), true, true, true), true) -> true % 60.68/60.54 857: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdf_type), true, ifeq(iext(X, Y, uri_rdfs_Resource), true, true, true), true) -> true % 60.68/60.54 858: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_subClassOf), true, ifeq(iext(X, uri_rdfs_Literal, uri_rdfs_Resource), true, true, true), true) -> true % 60.68/60.54 859: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_subClassOf), true, ifeq(iext(X, uri_rdfs_Seq, uri_rdfs_Resource), true, true, true), true) -> true % 60.68/60.54 860: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdf_type), true, ifeq(iext(X, uri_owl_intersectionOf, uri_rdf_Property), true, true, true), true) -> true % 60.68/60.54 861: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdf_type), true, ifeq(iext(X, uri_owl_complementOf, uri_rdf_Property), true, true, true), true) -> true % 60.68/60.54 862: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_subPropertyOf), true, ifeq(iext(X, uri_owl_complementOf, uri_owl_complementOf), true, true, true), true) -> true % 60.68/60.54 863: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_subClassOf), true, ifeq(iext(X, uri_rdfs_Seq, uri_rdfs_Seq), true, true, true), true) -> true % 60.68/60.54 864: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_subPropertyOf), true, ifeq(iext(X, uri_rdf__1, uri_rdf__1), true, true, true), true) -> true % 60.68/60.54 865: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_subPropertyOf), true, ifeq(iext(X, uri_owl_intersectionOf, uri_owl_intersectionOf), true, true, true), true) -> true % 60.68/60.54 866: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_subPropertyOf), true, ifeq(iext(X, uri_rdf__1, uri_rdfs_member), true, true, true), true) -> true % 60.68/60.54 867: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdf_type), true, ifeq(iext(X, uri_rdfs_domain, uri_rdf_Property), true, true, true), true) -> true % 60.68/60.54 868: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdf_type), true, ifeq(iext(X, uri_rdfs_isDefinedBy, uri_rdf_Property), true, true, true), true) -> true % 60.68/60.54 869: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_subClassOf), true, ifeq(iext(X, uri_rdf_Property, uri_rdf_Property), true, true, true), true) -> true % 60.68/60.54 870: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_subClassOf), true, ifeq(iext(X, uri_rdf_Bag, uri_rdf_Bag), true, true, true), true) -> true % 60.68/60.54 871: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_subClassOf), true, ifeq(iext(X, uri_rdf_Property, uri_rdfs_Resource), true, true, true), true) -> true % 60.68/60.54 872: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_subClassOf), true, ifeq(iext(X, uri_rdf_Bag, uri_rdfs_Resource), true, true, true), true) -> true % 60.68/60.54 873: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_subClassOf), true, ifeq(iext(X, uri_rdf_XMLLiteral, uri_rdf_XMLLiteral), true, true, true), true) -> true % 60.68/60.54 874: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_subClassOf), true, ifeq(iext(X, uri_rdf_Alt, uri_rdfs_Resource), true, true, true), true) -> true % 60.68/60.54 875: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_subClassOf), true, ifeq(iext(X, uri_rdf_Alt, uri_rdf_Alt), true, true, true), true) -> true % 60.68/60.54 876: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdf_type), true, ifeq(iext(X, uri_rdfs_subPropertyOf, uri_rdf_Property), true, true, true), true) -> true % 60.68/60.54 877: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdf_type), true, ifeq(iext(X, uri_rdfs_range, uri_rdf_Property), true, true, true), true) -> true % 60.68/60.54 878: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdf_type), true, ifeq(iext(X, uri_rdfs_seeAlso, uri_rdf_Property), true, true, true), true) -> true % 60.68/60.54 879: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdf_type), true, ifeq(iext(X, uri_rdfs_subClassOf, uri_rdf_Property), true, true, true), true) -> true % 60.68/60.54 880: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_subClassOf), true, ifeq(iext(X, uri_rdfs_Datatype, uri_rdfs_Resource), true, true, true), true) -> true % 60.68/60.54 881: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_subClassOf), true, ifeq(iext(X, uri_rdfs_Datatype, uri_rdfs_Datatype), true, true, true), true) -> true % 60.68/60.54 882: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_subClassOf), true, ifeq(iext(X, uri_rdfs_Literal, uri_rdfs_Literal), true, true, true), true) -> true % 60.68/60.54 883: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_subClassOf), true, ifeq(iext(X, uri_rdfs_ContainerMembershipProperty, uri_rdfs_ContainerMembershipProperty), true, true, true), true) -> true % 60.68/60.54 884: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_subClassOf), true, ifeq(iext(X, uri_rdfs_ContainerMembershipProperty, uri_rdfs_Resource), true, true, true), true) -> true % 60.68/60.54 885: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_subClassOf), true, ifeq(iext(X, uri_rdfs_Class, uri_rdfs_Class), true, true, true), true) -> true % 60.68/60.54 886: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_subClassOf), true, ifeq(iext(X, uri_rdf_XMLLiteral, uri_rdfs_Resource), true, true, true), true) -> true % 60.68/60.54 887: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_subClassOf), true, ifeq(iext(X, uri_rdfs_Class, uri_rdfs_Resource), true, true, true), true) -> true % 60.68/60.54 888: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_subClassOf), true, ifeq(iext(X, uri_rdfs_Container, uri_rdfs_Container), true, true, true), true) -> true % 60.68/60.54 889: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_subClassOf), true, ifeq(iext(X, uri_rdfs_Container, uri_rdfs_Resource), true, true, true), true) -> true % 60.68/60.54 890: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_subPropertyOf), true, ifeq(iext(X, uri_rdf__3, uri_rdfs_member), true, true, true), true) -> true % 60.68/60.54 891: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_subPropertyOf), true, ifeq(iext(X, uri_rdf__2, uri_rdfs_member), true, true, true), true) -> true % 60.68/60.54 892: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_subPropertyOf), true, ifeq(iext(X, uri_rdf__3, uri_rdf__3), true, true, true), true) -> true % 60.68/60.54 893: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_subPropertyOf), true, ifeq(iext(X, uri_rdf__2, uri_rdf__2), true, true, true), true) -> true % 60.68/60.54 894: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_subPropertyOf), true, ifeq(iext(X, uri_rdf_first, uri_rdf_first), true, true, true), true) -> true % 60.68/60.54 895: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_subPropertyOf), true, ifeq(iext(X, uri_rdf_rest, uri_rdf_rest), true, true, true), true) -> true % 60.68/60.54 896: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_subPropertyOf), true, ifeq(iext(X, uri_rdf_object, uri_rdf_object), true, true, true), true) -> true % 60.68/60.54 897: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_subPropertyOf), true, ifeq(iext(X, uri_rdf_value, uri_rdf_value), true, true, true), true) -> true % 60.68/60.54 898: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_subPropertyOf), true, ifeq(iext(X, uri_rdf_subject, uri_rdf_subject), true, true, true), true) -> true % 60.68/60.54 899: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_subPropertyOf), true, ifeq(iext(X, uri_rdf_type, uri_rdf_type), true, true, true), true) -> true % 60.68/60.54 900: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_subPropertyOf), true, ifeq(iext(X, uri_rdfs_isDefinedBy, uri_rdfs_isDefinedBy), true, true, true), true) -> true % 60.68/60.54 901: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_subPropertyOf), true, ifeq(iext(X, uri_rdfs_domain, uri_rdfs_domain), true, true, true), true) -> true % 60.68/60.54 902: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_subPropertyOf), true, ifeq(iext(X, uri_rdfs_range, uri_rdfs_range), true, true, true), true) -> true % 60.68/60.54 903: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_subPropertyOf), true, ifeq(iext(X, uri_rdfs_seeAlso, uri_rdfs_seeAlso), true, true, true), true) -> true % 60.68/60.54 904: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_subPropertyOf), true, ifeq(iext(X, uri_rdfs_subClassOf, uri_rdfs_subClassOf), true, true, true), true) -> true % 60.68/60.54 905: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_subPropertyOf), true, ifeq(iext(X, uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf), true, true, true), true) -> true % 60.68/60.54 906: ifeq(iext(uri_rdfs_domain, X, uri_rdf_Property), true, ifeq(iext(X, uri_rdfs_domain, Y), true, true, true), true) -> true % 60.68/60.54 907: ifeq(iext(uri_rdfs_range, X, uri_rdf_Property), true, ifeq(iext(X, Y, uri_owl_intersectionOf), true, true, true), true) -> true % 60.68/60.54 908: ifeq(iext(uri_rdfs_range, X, uri_rdf_Property), true, ifeq(iext(X, Y, uri_rdfs_domain), true, true, true), true) -> true % 60.68/60.54 909: ifeq(iext(uri_rdfs_range, X, uri_rdf_Property), true, ifeq(iext(X, Y, uri_owl_complementOf), true, true, true), true) -> true % 60.68/60.54 910: ifeq(iext(uri_rdfs_domain, X, uri_rdf_Property), true, ifeq(iext(X, uri_rdfs_range, Y), true, true, true), true) -> true % 60.68/60.54 911: ifeq(iext(uri_rdfs_domain, X, uri_rdf_Property), true, ifeq(iext(X, uri_rdfs_seeAlso, Y), true, true, true), true) -> true % 60.68/60.54 912: ifeq(iext(uri_rdfs_domain, X, uri_rdf_Property), true, ifeq(iext(X, uri_rdfs_subPropertyOf, Y), true, true, true), true) -> true % 60.68/60.54 913: ifeq(iext(uri_rdfs_domain, X, uri_rdf_Property), true, ifeq(iext(X, uri_rdfs_subClassOf, Y), true, true, true), true) -> true % 60.68/60.54 914: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdf_type), true, ifeq(iext(X, uri_rdfs_Datatype, uri_rdfs_Class), true, true, true), true) -> true % 60.68/60.54 915: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdf_type), true, ifeq(iext(X, uri_rdfs_label, uri_rdf_Property), true, true, true), true) -> true % 60.68/60.54 916: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdf_type), true, ifeq(iext(X, uri_rdfs_Seq, uri_rdfs_Class), true, true, true), true) -> true % 60.68/60.54 917: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdf_type), true, ifeq(iext(X, uri_rdfs_Statement, uri_rdfs_Class), true, true, true), true) -> true % 60.68/60.54 918: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdf_type), true, ifeq(iext(X, uri_rdfs_comment, uri_rdf_Property), true, true, true), true) -> true % 60.68/60.54 919: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdf_type), true, ifeq(iext(X, uri_rdfs_Literal, uri_rdfs_Class), true, true, true), true) -> true % 60.68/60.54 920: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdf_type), true, ifeq(iext(X, uri_rdf_XMLLiteral, uri_rdfs_Class), true, true, true), true) -> true % 60.68/60.54 921: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdf_type), true, ifeq(iext(X, uri_rdf_predicate, uri_rdf_Property), true, true, true), true) -> true % 60.68/60.54 922: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdf_type), true, ifeq(iext(X, uri_rdfs_Container, uri_rdfs_Class), true, true, true), true) -> true % 60.68/60.54 923: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdf_type), true, ifeq(iext(X, uri_rdfs_Class, uri_rdfs_Class), true, true, true), true) -> true % 60.68/60.54 924: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdf_type), true, ifeq(iext(X, uri_rdfs_ContainerMembershipProperty, uri_rdfs_Class), true, true, true), true) -> true % 60.68/60.54 925: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdf_type), true, ifeq(iext(X, uri_owl_Class, uri_rdfs_Class), true, true, true), true) -> true % 60.68/60.54 926: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdf_type), true, ifeq(iext(X, uri_rdf_Bag, uri_rdfs_Class), true, true, true), true) -> true % 60.68/60.54 927: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdf_type), true, ifeq(iext(X, uri_rdf_List, uri_rdfs_Class), true, true, true), true) -> true % 60.68/60.54 928: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdf_type), true, ifeq(iext(X, uri_rdf_Alt, uri_rdfs_Class), true, true, true), true) -> true % 60.68/60.54 929: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdf_type), true, ifeq(iext(X, sK2_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l2, uri_rdf_List), true, true, true), true) -> true % 60.68/60.54 930: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdf_type), true, ifeq(iext(X, sK3_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_x, uri_rdfs_Class), true, true, true), true) -> true % 60.68/60.54 931: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdf_type), true, ifeq(iext(X, sK4_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l1, uri_rdf_List), true, true, true), true) -> true % 60.68/60.54 932: ifeq(iext(uri_rdfs_subPropertyOf, X, Y), true, ifeq(iext(uri_rdfs_subPropertyOf, Z, X), true, iext(uri_rdfs_subPropertyOf, Z, Y), true), true) -> true % 60.68/60.54 933: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_isDefinedBy), true, iext(uri_rdfs_subPropertyOf, X, uri_rdfs_seeAlso), true) -> true % 60.68/60.54 934: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_seeAlso, X), true, iext(uri_rdfs_subPropertyOf, uri_rdfs_isDefinedBy, X), true) -> true % 60.68/60.54 935: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdf__2), true, iext(uri_rdfs_subPropertyOf, X, uri_rdfs_member), true) -> true % 60.68/60.54 936: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_member, X), true, iext(uri_rdfs_subPropertyOf, uri_rdf__1, X), true) -> true % 60.68/60.54 937: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdf__3), true, iext(uri_rdfs_subPropertyOf, X, uri_rdfs_member), true) -> true % 60.68/60.54 938: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdf__1), true, iext(uri_rdfs_subPropertyOf, X, uri_rdfs_member), true) -> true % 60.68/60.54 939: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_member, X), true, iext(uri_rdfs_subPropertyOf, uri_rdf__3, X), true) -> true % 60.68/60.54 940: ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_member, X), true, iext(uri_rdfs_subPropertyOf, uri_rdf__2, X), true) -> true % 60.68/60.54 941: ifeq(iext(uri_rdfs_subClassOf, X, Y), true, ifeq(iext(uri_rdfs_subClassOf, Z, X), true, iext(uri_rdfs_subClassOf, Z, Y), true), true) -> true % 60.68/60.54 942: ifeq(iext(uri_rdfs_subClassOf, X, uri_rdf_Alt), true, iext(uri_rdfs_subClassOf, X, uri_rdfs_Container), true) -> true % 60.68/60.54 943: ifeq(iext(uri_rdfs_subClassOf, X, uri_rdf_Bag), true, iext(uri_rdfs_subClassOf, X, uri_rdfs_Container), true) -> true % 60.68/60.54 944: ifeq(iext(uri_rdfs_subClassOf, X, uri_rdf_XMLLiteral), true, iext(uri_rdfs_subClassOf, X, uri_rdfs_Literal), true) -> true % 60.68/60.54 945: ifeq(iext(uri_rdfs_subClassOf, X, uri_rdfs_ContainerMembershipProperty), true, iext(uri_rdfs_subClassOf, X, uri_rdf_Property), true) -> true % 60.68/60.54 946: ifeq(iext(uri_rdfs_subClassOf, X, uri_rdfs_Datatype), true, iext(uri_rdfs_subClassOf, X, uri_rdfs_Class), true) -> true % 60.68/60.54 947: ifeq(iext(uri_rdfs_subClassOf, X, uri_rdfs_Seq), true, iext(uri_rdfs_subClassOf, X, uri_rdfs_Container), true) -> true % 60.68/60.54 948: ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Container, X), true, iext(uri_rdfs_subClassOf, uri_rdf_Alt, X), true) -> true % 60.68/60.54 949: ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Container, X), true, iext(uri_rdfs_subClassOf, uri_rdf_Bag, X), true) -> true % 60.68/60.54 950: ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Literal, X), true, iext(uri_rdfs_subClassOf, uri_rdf_XMLLiteral, X), true) -> true % 60.68/60.54 951: ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, X), true, iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, X), true) -> true % 60.68/60.54 952: ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, X), true, iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, X), true) -> true % 60.68/60.54 953: ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Container, X), true, iext(uri_rdfs_subClassOf, uri_rdfs_Seq, X), true) -> true % 60.68/60.54 954: ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Resource, X), true, iext(uri_rdfs_subClassOf, uri_rdfs_Literal, X), true) -> true % 60.68/60.54 955: ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Resource, X), true, iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, X), true) -> true % 60.68/60.54 956: ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Resource, X), true, iext(uri_rdfs_subClassOf, uri_rdfs_Seq, X), true) -> true % 60.68/60.54 957: ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Resource, X), true, iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, X), true) -> true % 60.68/60.54 958: ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Resource, X), true, iext(uri_rdfs_subClassOf, uri_rdfs_Class, X), true) -> true % 60.68/60.54 959: ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Resource, X), true, iext(uri_rdfs_subClassOf, uri_rdfs_Container, X), true) -> true % 60.68/60.54 960: ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Resource, X), true, iext(uri_rdfs_subClassOf, uri_rdf_Alt, X), true) -> true % 60.68/60.54 961: ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Resource, X), true, iext(uri_rdfs_subClassOf, uri_rdf_Bag, X), true) -> true % 60.68/60.54 962: ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Resource, X), true, iext(uri_rdfs_subClassOf, uri_rdf_Property, X), true) -> true % 60.68/60.54 963: ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Resource, X), true, iext(uri_rdfs_subClassOf, uri_rdf_XMLLiteral, X), true) -> true % 60.68/60.54 964: ifeq(iext(uri_rdfs_subClassOf, X, uri_rdfs_Seq), true, iext(uri_rdfs_subClassOf, X, uri_rdfs_Resource), true) -> true % 60.68/60.54 965: ifeq(iext(uri_rdfs_subClassOf, X, uri_rdfs_Datatype), true, iext(uri_rdfs_subClassOf, X, uri_rdfs_Resource), true) -> true % 60.68/60.54 966: ifeq(iext(uri_rdfs_subClassOf, X, uri_rdfs_Literal), true, iext(uri_rdfs_subClassOf, X, uri_rdfs_Resource), true) -> true % 60.68/60.54 967: ifeq(iext(uri_rdfs_subClassOf, X, uri_rdfs_ContainerMembershipProperty), true, iext(uri_rdfs_subClassOf, X, uri_rdfs_Resource), true) -> true % 60.68/60.54 968: ifeq(iext(uri_rdfs_subClassOf, X, uri_rdfs_Class), true, iext(uri_rdfs_subClassOf, X, uri_rdfs_Resource), true) -> true % 60.68/60.54 969: ifeq(iext(uri_rdfs_subClassOf, X, uri_rdfs_Container), true, iext(uri_rdfs_subClassOf, X, uri_rdfs_Resource), true) -> true % 60.68/60.54 970: ifeq(iext(uri_rdfs_subClassOf, X, uri_rdf_Property), true, iext(uri_rdfs_subClassOf, X, uri_rdfs_Resource), true) -> true % 60.68/60.54 971: ifeq(iext(uri_rdfs_subClassOf, X, uri_rdf_XMLLiteral), true, iext(uri_rdfs_subClassOf, X, uri_rdfs_Resource), true) -> true % 60.68/60.54 972: ifeq(iext(uri_rdfs_subClassOf, X, uri_rdf_Alt), true, iext(uri_rdfs_subClassOf, X, uri_rdfs_Resource), true) -> true % 60.68/60.54 973: ifeq(iext(uri_rdfs_subClassOf, X, uri_rdf_Bag), true, iext(uri_rdfs_subClassOf, X, uri_rdfs_Resource), true) -> true % 60.68/60.54 974: ifeq(iext(uri_rdfs_subClassOf, X, sK3_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_x), true, iext(uri_rdfs_subClassOf, X, uri_rdfs_Resource), true) -> true % 60.68/60.54 975: ifeq(iext(uri_rdfs_subClassOf, X, uri_owl_Class), true, iext(uri_rdfs_subClassOf, X, uri_rdfs_Resource), true) -> true % 60.68/60.54 976: ifeq(iext(uri_rdfs_subClassOf, X, uri_rdf_List), true, iext(uri_rdfs_subClassOf, X, uri_rdfs_Resource), true) -> true % 60.68/60.54 977: ifeq(iext(uri_rdfs_subClassOf, X, uri_rdfs_Statement), true, iext(uri_rdfs_subClassOf, X, uri_rdfs_Resource), true) -> true % 60.68/60.54 978: ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Resource, X), true, iext(uri_rdfs_subClassOf, sK3_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_x, X), true) -> true % 60.68/60.54 979: ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Resource, X), true, iext(uri_rdfs_subClassOf, uri_owl_Class, X), true) -> true % 60.68/60.54 980: ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Resource, X), true, iext(uri_rdfs_subClassOf, uri_rdf_List, X), true) -> true % 60.68/60.54 981: ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Resource, X), true, iext(uri_rdfs_subClassOf, uri_rdfs_Statement, X), true) -> true % 60.68/60.54 982: ifeq(iext(uri_rdfs_range, X, uri_rdfs_Class), true, ifeq(iext(X, Y, uri_rdfs_Resource), true, true, true), true) -> true % 60.68/60.54 983: ifeq(iext(uri_rdfs_domain, X, uri_rdfs_Class), true, ifeq(iext(X, uri_rdfs_Resource, Y), true, true, true), true) -> true % 60.68/60.54 984: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_subClassOf), true, ifeq(iext(X, sK3_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_x, uri_rdfs_Resource), true, true, true), true) -> true % 60.68/60.54 985: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_subClassOf), true, ifeq(iext(X, sK3_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_x, sK3_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_x), true, true, true), true) -> true % 60.68/60.54 986: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_subClassOf), true, ifeq(iext(X, uri_owl_Class, uri_owl_Class), true, true, true), true) -> true % 60.68/60.54 987: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_subClassOf), true, ifeq(iext(X, uri_owl_Class, uri_rdfs_Resource), true, true, true), true) -> true % 60.68/60.54 988: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_subClassOf), true, ifeq(iext(X, uri_rdf_List, uri_rdf_List), true, true, true), true) -> true % 60.68/60.54 989: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_subClassOf), true, ifeq(iext(X, uri_rdf_List, uri_rdfs_Resource), true, true, true), true) -> true % 60.68/60.54 990: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_subClassOf), true, ifeq(iext(X, uri_rdfs_Statement, uri_rdfs_Resource), true, true, true), true) -> true % 60.68/60.54 991: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_subPropertyOf), true, ifeq(iext(X, uri_rdfs_member, uri_rdfs_member), true, true, true), true) -> true % 60.68/60.54 992: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdf_type), true, ifeq(iext(X, uri_rdfs_member, uri_rdf_Property), true, true, true), true) -> true % 60.68/60.54 993: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_subClassOf), true, ifeq(iext(X, uri_rdfs_Resource, uri_rdfs_Resource), true, true, true), true) -> true % 60.68/60.54 994: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_subClassOf), true, ifeq(iext(X, uri_rdfs_Statement, uri_rdfs_Statement), true, true, true), true) -> true % 60.68/60.54 995: ifeq(iext(uri_rdfs_domain, X, uri_rdf_Property), true, ifeq(iext(X, uri_rdfs_member, Y), true, true, true), true) -> true % 60.68/60.54 996: ifeq(iext(uri_rdfs_range, X, uri_rdf_Property), true, ifeq(iext(X, Y, uri_rdfs_member), true, true, true), true) -> true % 60.68/60.54 997: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_subPropertyOf), true, ifeq(iext(X, uri_rdfs_label, uri_rdfs_label), true, true, true), true) -> true % 60.68/60.54 998: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_subPropertyOf), true, ifeq(iext(X, uri_rdfs_comment, uri_rdfs_comment), true, true, true), true) -> true % 60.68/60.54 999: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdfs_subPropertyOf), true, ifeq(iext(X, uri_rdf_predicate, uri_rdf_predicate), true, true, true), true) -> true % 60.68/60.54 1000: ifeq(iext(uri_rdfs_subPropertyOf, X, uri_rdf_type), true, ifeq(iext(X, uri_rdfs_Resource, uri_rdfs_Class), true, true, true), true) -> true % 60.68/60.54 %------------------------------------------------------------------------------