%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : SWB009-10 : TPTP v9.0.0. Released v7.5.0. % Transfm : none % Format : tptp:raw % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % Computer : n007.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 : Wed Apr 9 09:15:47 PM UTC 2025 % Result : Satisfiable 32.54s 21.84s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.06/0.12 % Problem : SWB009-10 : TPTP v9.0.0. Released v7.5.0. % 0.06/0.13 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % 0.13/0.33 % Computer : n007.cluster.edu % 0.13/0.33 % Model : x86_64 x86_64 % 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.33 % Memory : 8042.1875MB % 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.33 % CPULimit : 300 % 0.13/0.33 % WCLimit : 300 % 0.13/0.33 % DateTime : Wed Apr 9 00:55:09 EDT 2025 % 0.13/0.33 % CPUTime : % 32.54/21.84 % 32.54/21.84 % SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 32.54/21.84 % 32.54/21.84 % SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 32.65/21.86 %$ ifeq > iext > tuple > icext > #nlpp > lv > ir > ip > ic > uri_rdfs_subPropertyOf > uri_rdfs_subClassOf > uri_rdfs_seeAlso > uri_rdfs_range > uri_rdfs_member > uri_rdfs_label > uri_rdfs_isDefinedBy > uri_rdfs_domain > uri_rdfs_comment > uri_rdfs_Statement > uri_rdfs_Seq > uri_rdfs_Resource > uri_rdfs_Literal > uri_rdfs_Datatype > uri_rdfs_ContainerMembershipProperty > uri_rdfs_Container > uri_rdfs_Class > uri_rdf_value > uri_rdf_type > uri_rdf_subject > uri_rdf_rest > uri_rdf_predicate > uri_rdf_object > uri_rdf_nil > uri_rdf_first > uri_rdf__3 > uri_rdf__2 > uri_rdf__1 > uri_rdf_XMLLiteral > uri_rdf_Property > uri_rdf_List > uri_rdf_Bag > uri_rdf_Alt > uri_owl_someValuesFrom > uri_owl_onProperty > uri_owl_Restriction > uri_owl_ObjectProperty > uri_owl_Class > uri_ex_s > uri_ex_p > uri_ex_c > true > sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z % 32.65/21.86 % 32.65/21.86 %Foreground sorts: % 32.65/21.86 % 32.65/21.86 % 32.65/21.86 %Background operators: % 32.65/21.86 % 32.65/21.86 % 32.65/21.86 %Foreground operators: % 32.65/21.86 tff(uri_rdfs_Datatype, type, uri_rdfs_Datatype: $i). % 32.65/21.86 tff(uri_rdfs_ContainerMembershipProperty, type, uri_rdfs_ContainerMembershipProperty: $i). % 32.65/21.86 tff(uri_rdfs_Resource, type, uri_rdfs_Resource: $i). % 32.65/21.86 tff(uri_rdf_Property, type, uri_rdf_Property: $i). % 32.65/21.86 tff(uri_rdf_subject, type, uri_rdf_subject: $i). % 32.65/21.86 tff(uri_rdf_type, type, uri_rdf_type: $i). % 32.65/21.86 tff(uri_owl_onProperty, type, uri_owl_onProperty: $i). % 32.65/21.86 tff(uri_rdfs_subPropertyOf, type, uri_rdfs_subPropertyOf: $i). % 32.65/21.86 tff(uri_rdfs_seeAlso, type, uri_rdfs_seeAlso: $i). % 32.65/21.86 tff(icext, type, icext: ($i * $i) > $i). % 32.65/21.86 tff(uri_rdfs_range, type, uri_rdfs_range: $i). % 32.65/21.86 tff(uri_rdf_XMLLiteral, type, uri_rdf_XMLLiteral: $i). % 32.65/21.86 tff(uri_rdf_List, type, uri_rdf_List: $i). % 32.65/21.86 tff(uri_ex_s, type, uri_ex_s: $i). % 32.65/21.86 tff(uri_rdf_first, type, uri_rdf_first: $i). % 32.65/21.86 tff(uri_rdf_predicate, type, uri_rdf_predicate: $i). % 32.65/21.86 tff(tuple, type, tuple: ($i * $i) > $i). % 32.65/21.86 tff(ir, type, ir: $i > $i). % 32.65/21.86 tff(lv, type, lv: $i > $i). % 32.65/21.86 tff(uri_ex_c, type, uri_ex_c: $i). % 32.65/21.86 tff(uri_rdf__3, type, uri_rdf__3: $i). % 32.65/21.86 tff(uri_rdf_value, type, uri_rdf_value: $i). % 32.65/21.86 tff(sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z, type, sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z: $i). % 32.65/21.86 tff(ic, type, ic: $i > $i). % 32.65/21.86 tff(uri_rdfs_Statement, type, uri_rdfs_Statement: $i). % 32.65/21.86 tff(uri_ex_p, type, uri_ex_p: $i). % 32.65/21.86 tff(uri_rdf__1, type, uri_rdf__1: $i). % 32.65/21.86 tff(iext, type, iext: ($i * $i * $i) > $i). % 32.65/21.86 tff(uri_owl_Restriction, type, uri_owl_Restriction: $i). % 32.65/21.86 tff(uri_rdf_rest, type, uri_rdf_rest: $i). % 32.65/21.86 tff(uri_rdfs_label, type, uri_rdfs_label: $i). % 32.65/21.86 tff(uri_rdfs_Container, type, uri_rdfs_Container: $i). % 32.65/21.86 tff(uri_owl_ObjectProperty, type, uri_owl_ObjectProperty: $i). % 32.65/21.86 tff(uri_rdfs_subClassOf, type, uri_rdfs_subClassOf: $i). % 32.65/21.86 tff(uri_rdf_object, type, uri_rdf_object: $i). % 32.65/21.86 tff(ip, type, ip: $i > $i). % 32.65/21.86 tff(uri_rdfs_Class, type, uri_rdfs_Class: $i). % 32.65/21.86 tff(uri_rdfs_Seq, type, uri_rdfs_Seq: $i). % 32.65/21.86 tff(uri_owl_Class, type, uri_owl_Class: $i). % 32.65/21.86 tff(uri_rdfs_member, type, uri_rdfs_member: $i). % 32.65/21.86 tff(uri_rdf_Bag, type, uri_rdf_Bag: $i). % 32.65/21.86 tff(uri_rdf__2, type, uri_rdf__2: $i). % 32.65/21.86 tff(uri_rdfs_comment, type, uri_rdfs_comment: $i). % 32.65/21.86 tff(uri_rdfs_Literal, type, uri_rdfs_Literal: $i). % 32.65/21.86 tff(true, type, true: $i). % 32.65/21.86 tff(uri_owl_someValuesFrom, type, uri_owl_someValuesFrom: $i). % 32.65/21.86 tff(uri_rdf_Alt, type, uri_rdf_Alt: $i). % 32.65/21.86 tff(uri_rdf_nil, type, uri_rdf_nil: $i). % 32.65/21.86 tff(uri_rdfs_isDefinedBy, type, uri_rdfs_isDefinedBy: $i). % 32.65/21.86 tff(uri_rdfs_domain, type, uri_rdfs_domain: $i). % 32.65/21.86 tff(ifeq, type, ifeq: ($i * $i * $i * $i) > $i). % 32.65/21.86 % 32.65/21.86 %Saturated clause set: % 32.65/21.86 tff(c_15672, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdf_Property), true, ifeq(iext(P_18, uri_rdfs_member, Y_21), true, true, true), true)=true))). % 32.65/21.87 tff(c_15669, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdf_Property), true, ifeq(iext(P_28, X_30, uri_rdfs_member), true, true, true), true)=true))). % 32.65/21.87 tff(c_16164, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, uri_rdfs_Resource, uri_rdfs_Class), true, true, true), true)=true))). % 32.65/21.87 tff(c_75087, plain, (![X_1289, Y_1290]: (ifeq(iext(uri_rdfs_label, X_1289, Y_1290), true, iext(uri_rdfs_label, X_1289, Y_1290), true)=true))). % 32.65/21.87 tff(c_75059, plain, (![X_1285, Y_1286]: (ifeq(iext(uri_rdfs_comment, X_1285, Y_1286), true, iext(uri_rdfs_comment, X_1285, Y_1286), true)=true))). % 32.65/21.87 tff(c_16012, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subPropertyOf), true, ifeq(iext(P_47, uri_rdfs_label, uri_rdfs_label), true, true, true), true)=true))). % 32.65/21.87 tff(c_16102, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subPropertyOf), true, ifeq(iext(P_47, uri_rdf_predicate, uri_rdf_predicate), true, true, true), true)=true))). % 32.65/21.87 tff(c_18646, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subPropertyOf), true, ifeq(iext(P_47, uri_rdfs_comment, uri_rdfs_comment), true, true, true), true)=true))). % 32.65/21.87 tff(c_74670, plain, (![X_1278, Y_1279]: (ifeq(iext(uri_rdf_predicate, X_1278, Y_1279), true, iext(uri_rdf_predicate, X_1278, Y_1279), true)=true))). % 32.65/21.87 tff(c_5242, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdfs_Class), true, ifeq(iext(P_18, uri_rdfs_Resource, Y_21), true, true, true), true)=true))). % 32.65/21.87 tff(c_15843, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subClassOf), true, ifeq(iext(P_47, uri_rdfs_Resource, uri_rdfs_Resource), true, true, true), true)=true))). % 32.65/21.87 tff(c_15942, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subPropertyOf), true, ifeq(iext(P_47, uri_rdfs_member, uri_rdfs_member), true, true, true), true)=true))). % 32.65/21.87 tff(c_5239, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdfs_Class), true, ifeq(iext(P_28, X_30, uri_rdfs_Resource), true, true, true), true)=true))). % 32.65/21.87 tff(c_15614, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, uri_rdfs_member, uri_rdf_Property), true, true, true), true)=true))). % 32.65/21.87 tff(c_73867, plain, (![X_1267, Y_1268]: (ifeq(iext(uri_rdfs_member, X_1267, Y_1268), true, iext(uri_rdfs_member, X_1267, Y_1268), true)=true))). % 32.65/21.87 tff(c_20092, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subClassOf), true, ifeq(iext(P_47, sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z, uri_rdfs_Resource), true, true, true), true)=true))). % 32.65/21.87 tff(c_15159, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subClassOf), true, ifeq(iext(P_47, uri_owl_Restriction, uri_rdfs_Resource), true, true, true), true)=true))). % 32.65/21.87 tff(c_14818, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subClassOf), true, ifeq(iext(P_47, uri_owl_Class, uri_rdfs_Resource), true, true, true), true)=true))). % 32.65/21.87 tff(c_14998, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subClassOf), true, ifeq(iext(P_47, uri_rdfs_Statement, uri_rdfs_Statement), true, true, true), true)=true))). % 32.65/21.87 tff(c_15548, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subClassOf), true, ifeq(iext(P_47, uri_owl_ObjectProperty, uri_owl_ObjectProperty), true, true, true), true)=true))). % 32.65/21.87 tff(c_15368, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subClassOf), true, ifeq(iext(P_47, uri_owl_ObjectProperty, uri_rdfs_Resource), true, true, true), true)=true))). % 32.65/21.87 tff(c_72954, plain, (![C_1259]: (ifeq(iext(uri_rdfs_subClassOf, C_1259, uri_owl_Class), true, iext(uri_rdfs_subClassOf, C_1259, uri_rdfs_Resource), true)=true))). % 32.65/21.87 tff(c_19997, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subClassOf), true, ifeq(iext(P_47, sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z, sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z), true, true, true), true)=true))). % 32.65/21.87 tff(c_15093, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subClassOf), true, ifeq(iext(P_47, uri_owl_Restriction, uri_owl_Restriction), true, true, true), true)=true))). % 32.65/21.87 tff(c_14550, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subClassOf), true, ifeq(iext(P_47, uri_owl_Class, uri_owl_Class), true, true, true), true)=true))). % 32.65/21.87 tff(c_14641, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subClassOf), true, ifeq(iext(P_47, uri_rdfs_Statement, uri_rdfs_Resource), true, true, true), true)=true))). % 32.65/21.87 tff(c_72298, plain, (![C_1253]: (ifeq(iext(uri_rdfs_subClassOf, C_1253, sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z), true, iext(uri_rdfs_subClassOf, C_1253, uri_rdfs_Resource), true)=true))). % 32.65/21.87 tff(c_72126, plain, (![C_1251]: (ifeq(iext(uri_rdfs_subClassOf, C_1251, uri_rdfs_Statement), true, iext(uri_rdfs_subClassOf, C_1251, uri_rdfs_Resource), true)=true))). % 32.65/21.87 tff(c_71956, plain, (![C_1249]: (ifeq(iext(uri_rdfs_subClassOf, C_1249, uri_owl_Restriction), true, iext(uri_rdfs_subClassOf, C_1249, uri_rdfs_Resource), true)=true))). % 32.65/21.87 tff(c_71784, plain, (![C_1247]: (ifeq(iext(uri_rdfs_subClassOf, C_1247, uri_owl_ObjectProperty), true, iext(uri_rdfs_subClassOf, C_1247, uri_rdfs_Resource), true)=true))). % 32.65/21.87 tff(c_7988, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdf_Property), true, ifeq(iext(P_28, X_30, uri_rdfs_subClassOf), true, true, true), true)=true))). % 32.65/21.87 tff(c_13756, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, uri_rdfs_Literal, uri_rdfs_Class), true, true, true), true)=true))). % 32.65/21.87 tff(c_13926, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, uri_rdfs_Datatype, uri_rdfs_Class), true, true, true), true)=true))). % 32.65/21.87 tff(c_14045, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, uri_rdfs_Container, uri_rdfs_Class), true, true, true), true)=true))). % 32.65/21.87 tff(c_5595, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdf_Property), true, ifeq(iext(P_28, X_30, uri_rdfs_seeAlso), true, true, true), true)=true))). % 32.65/21.87 tff(c_14503, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, uri_rdf_XMLLiteral, uri_rdfs_Class), true, true, true), true)=true))). % 32.65/21.87 tff(c_8425, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdf_Property), true, ifeq(iext(P_18, uri_owl_onProperty, Y_21), true, true, true), true)=true))). % 32.65/21.87 tff(c_14171, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, uri_rdfs_Seq, uri_rdfs_Class), true, true, true), true)=true))). % 32.65/21.87 tff(c_16815, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subClassOf), true, ifeq(iext(P_47, uri_rdf_List, uri_rdfs_Resource), true, true, true), true)=true))). % 32.65/21.87 tff(c_9117, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdf_Property), true, ifeq(iext(P_18, uri_rdfs_range, Y_21), true, true, true), true)=true))). % 32.65/21.87 tff(c_13832, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, uri_rdfs_ContainerMembershipProperty, uri_rdfs_Class), true, true, true), true)=true))). % 32.65/21.87 tff(c_8422, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdf_Property), true, ifeq(iext(P_28, X_30, uri_owl_onProperty), true, true, true), true)=true))). % 32.65/21.87 tff(c_13879, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, uri_rdfs_Class, uri_rdfs_Class), true, true, true), true)=true))). % 32.65/21.87 tff(c_11262, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdf_Property), true, ifeq(iext(P_28, X_30, uri_rdfs_subPropertyOf), true, true, true), true)=true))). % 32.65/21.87 tff(c_13998, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, uri_rdf_Bag, uri_rdfs_Class), true, true, true), true)=true))). % 32.65/21.87 tff(c_5598, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdf_Property), true, ifeq(iext(P_18, uri_rdfs_seeAlso, Y_21), true, true, true), true)=true))). % 32.65/21.87 tff(c_16724, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subClassOf), true, ifeq(iext(P_47, uri_rdf_List, uri_rdf_List), true, true, true), true)=true))). % 32.65/21.87 tff(c_14092, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, uri_rdf_Alt, uri_rdfs_Class), true, true, true), true)=true))). % 32.65/21.87 tff(c_9114, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdf_Property), true, ifeq(iext(P_28, X_30, uri_rdfs_range), true, true, true), true)=true))). % 32.65/21.87 tff(c_69247, plain, (![C_1218]: (ifeq(iext(uri_rdfs_subClassOf, C_1218, uri_rdf_List), true, iext(uri_rdfs_subClassOf, C_1218, uri_rdfs_Resource), true)=true))). % 32.65/21.88 tff(c_11265, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdf_Property), true, ifeq(iext(P_18, uri_rdfs_subPropertyOf, Y_21), true, true, true), true)=true))). % 32.65/21.88 tff(c_7991, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdf_Property), true, ifeq(iext(P_18, uri_rdfs_subClassOf, Y_21), true, true, true), true)=true))). % 32.65/21.88 tff(c_9680, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdf_Property), true, ifeq(iext(P_18, uri_owl_someValuesFrom, Y_21), true, true, true), true)=true))). % 32.65/21.88 tff(c_9677, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdf_Property), true, ifeq(iext(P_28, X_30, uri_owl_someValuesFrom), true, true, true), true)=true))). % 32.65/21.88 tff(c_14456, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, uri_owl_ObjectProperty, uri_rdfs_Class), true, true, true), true)=true))). % 32.65/21.88 tff(c_13411, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, uri_rdf_predicate, uri_rdf_Property), true, true, true), true)=true))). % 32.65/21.88 tff(c_19950, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z, uri_rdfs_Class), true, true, true), true)=true))). % 32.65/21.88 tff(c_13364, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, uri_owl_Restriction, uri_rdfs_Class), true, true, true), true)=true))). % 32.65/21.88 tff(c_13535, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, uri_rdfs_Statement, uri_rdfs_Class), true, true, true), true)=true))). % 32.65/21.88 tff(c_13703, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, uri_owl_Class, uri_rdfs_Class), true, true, true), true)=true))). % 32.65/21.88 tff(c_13604, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, uri_rdfs_label, uri_rdf_Property), true, true, true), true)=true))). % 32.65/21.88 tff(c_18543, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, uri_rdfs_comment, uri_rdf_Property), true, true, true), true)=true))). % 32.65/21.88 tff(c_4529, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdfs_Class), true, ifeq(iext(P_28, X_30, uri_rdfs_Seq), true, true, true), true)=true))). % 32.65/21.88 tff(c_12764, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subPropertyOf), true, ifeq(iext(P_47, uri_rdfs_subClassOf, uri_rdfs_subClassOf), true, true, true), true)=true))). % 32.65/21.88 tff(c_9060, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, uri_rdfs_range, uri_rdf_Property), true, true, true), true)=true))). % 32.65/21.88 tff(c_67215, plain, (![X_1193, Y_1194]: (ifeq(iext(uri_rdfs_isDefinedBy, X_1193, Y_1194), true, iext(uri_rdfs_isDefinedBy, X_1193, Y_1194), true)=true))). % 32.65/21.88 tff(c_8998, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subPropertyOf), true, ifeq(iext(P_47, uri_owl_onProperty, uri_owl_onProperty), true, true, true), true)=true))). % 32.65/21.88 tff(c_9232, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subPropertyOf), true, ifeq(iext(P_47, uri_rdfs_seeAlso, uri_rdfs_seeAlso), true, true, true), true)=true))). % 32.65/21.88 tff(c_8750, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subPropertyOf), true, ifeq(iext(P_47, uri_rdf_type, uri_rdf_type), true, true, true), true)=true))). % 32.65/21.88 tff(c_66948, plain, (![X_1187, Y_1188]: (ifeq(iext(uri_rdf_subject, X_1187, Y_1188), true, iext(uri_rdf_subject, X_1187, Y_1188), true)=true))). % 32.65/21.88 tff(c_66777, plain, (![C_1185]: (ifeq(iext(uri_rdfs_subClassOf, C_1185, uri_rdfs_ContainerMembershipProperty), true, iext(uri_rdfs_subClassOf, C_1185, uri_rdfs_Resource), true)=true))). % 32.65/21.88 tff(c_4624, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdfs_Class), true, ifeq(iext(P_28, X_30, uri_rdfs_Container), true, true, true), true)=true))). % 32.65/21.88 tff(c_7460, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subClassOf), true, ifeq(iext(P_47, uri_rdf_Property, uri_rdfs_Resource), true, true, true), true)=true))). % 32.65/21.88 tff(c_66480, plain, (![X_1178, Y_1179]: (ifeq(iext(uri_rdf__2, X_1178, Y_1179), true, iext(uri_rdfs_member, X_1178, Y_1179), true)=true))). % 32.65/21.88 tff(c_13301, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subPropertyOf), true, ifeq(iext(P_47, uri_rdf_first, uri_rdf_first), true, true, true), true)=true))). % 32.65/21.88 tff(c_66056, plain, (![C_1173]: (ifeq(iext(uri_rdfs_subClassOf, C_1173, uri_rdfs_Datatype), true, iext(uri_rdfs_subClassOf, C_1173, uri_rdfs_Resource), true)=true))). % 32.65/21.88 tff(c_4283, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdfs_Class), true, ifeq(iext(P_28, X_30, uri_rdf_Bag), true, true, true), true)=true))). % 32.65/21.88 tff(c_9958, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subClassOf), true, ifeq(iext(P_47, uri_rdfs_Seq, uri_rdfs_Resource), true, true, true), true)=true))). % 32.65/21.88 tff(c_4286, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdfs_Class), true, ifeq(iext(P_18, uri_rdf_Bag, Y_21), true, true, true), true)=true))). % 32.65/21.88 tff(c_6091, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subPropertyOf), true, ifeq(iext(P_47, uri_rdf_rest, uri_rdf_rest), true, true, true), true)=true))). % 32.65/21.88 tff(c_10901, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subClassOf), true, ifeq(iext(P_47, uri_rdfs_Datatype, uri_rdfs_Datatype), true, true, true), true)=true))). % 32.65/21.88 tff(c_65522, plain, (![X_1164, Y_1165]: (ifeq(iext(uri_rdf__3, X_1164, Y_1165), true, iext(uri_rdfs_member, X_1164, Y_1165), true)=true))). % 32.65/21.88 tff(c_5075, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subClassOf), true, ifeq(iext(P_47, uri_rdfs_Datatype, uri_rdfs_Resource), true, true, true), true)=true))). % 32.65/21.88 tff(c_10840, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subPropertyOf), true, ifeq(iext(P_47, uri_rdf__3, uri_rdfs_member), true, true, true), true)=true))). % 32.65/21.88 tff(c_65248, plain, (![X_1158, Y_1159]: (ifeq(iext(uri_rdf__3, X_1158, Y_1159), true, iext(uri_rdf__3, X_1158, Y_1159), true)=true))). % 32.65/21.88 tff(c_65204, plain, (![X_1154, Y_1155]: (ifeq(iext(uri_owl_onProperty, X_1154, Y_1155), true, iext(uri_owl_onProperty, X_1154, Y_1155), true)=true))). % 32.65/21.88 tff(c_4329, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdfs_Class), true, ifeq(iext(P_18, uri_rdfs_Literal, Y_21), true, true, true), true)=true))). % 32.65/21.88 tff(c_6487, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subPropertyOf), true, ifeq(iext(P_47, uri_rdf__2, uri_rdf__2), true, true, true), true)=true))). % 32.65/21.88 tff(c_4233, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdfs_Class), true, ifeq(iext(P_28, X_30, uri_rdfs_ContainerMembershipProperty), true, true, true), true)=true))). % 32.76/21.88 tff(c_10382, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, uri_rdfs_isDefinedBy, uri_rdf_Property), true, true, true), true)=true))). % 32.76/21.88 tff(c_64512, plain, (![C_1146]: (ifeq(iext(uri_rdfs_subClassOf, C_1146, uri_rdf_XMLLiteral), true, iext(uri_rdfs_subClassOf, C_1146, uri_rdfs_Resource), true)=true))). % 32.76/21.88 tff(c_64485, plain, (![X_1142, Y_1143]: (ifeq(iext(uri_rdf_rest, X_1142, Y_1143), true, iext(uri_rdf_rest, X_1142, Y_1143), true)=true))). % 32.76/21.88 tff(c_9623, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, uri_owl_someValuesFrom, uri_rdf_Property), true, true, true), true)=true))). % 32.76/21.88 tff(c_7934, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, uri_rdfs_subClassOf, uri_rdf_Property), true, true, true), true)=true))). % 32.76/21.88 tff(c_64202, plain, (![X_1136, Y_1137]: (ifeq(iext(uri_owl_someValuesFrom, X_1136, Y_1137), true, iext(uri_owl_someValuesFrom, X_1136, Y_1137), true)=true))). % 32.76/21.88 tff(c_63870, plain, (![X_1132, Y_1133]: (ifeq(iext(uri_rdfs_domain, X_1132, Y_1133), true, iext(uri_rdfs_domain, X_1132, Y_1133), true)=true))). % 32.76/21.88 tff(c_6847, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subClassOf), true, ifeq(iext(P_47, uri_rdfs_ContainerMembershipProperty, uri_rdfs_Resource), true, true, true), true)=true))). % 32.76/21.88 tff(c_8619, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subClassOf), true, ifeq(iext(P_47, uri_rdf_Bag, uri_rdfs_Resource), true, true, true), true)=true))). % 32.76/21.88 tff(c_13008, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, uri_rdfs_domain, uri_rdf_Property), true, true, true), true)=true))). % 32.76/21.88 tff(c_63322, plain, (![C_1127]: (ifeq(iext(uri_rdfs_subClassOf, C_1127, uri_rdf_Alt), true, iext(uri_rdfs_subClassOf, C_1127, uri_rdfs_Resource), true)=true))). % 32.76/21.88 tff(c_5538, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, uri_rdfs_seeAlso, uri_rdf_Property), true, true, true), true)=true))). % 32.76/21.88 tff(c_10442, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subPropertyOf), true, ifeq(iext(P_47, uri_rdf__1, uri_rdf__1), true, true, true), true)=true))). % 32.76/21.88 tff(c_62902, plain, (![C_1123]: (ifeq(iext(uri_rdfs_subClassOf, C_1123, uri_rdfs_Literal), true, iext(uri_rdfs_subClassOf, C_1123, uri_rdfs_Resource), true)=true))). % 32.76/21.88 tff(c_13232, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subPropertyOf), true, ifeq(iext(P_47, uri_rdf__1, uri_rdfs_member), true, true, true), true)=true))). % 32.76/21.88 tff(c_62755, plain, (![X_1118, Y_1119]: (ifeq(iext(uri_rdf_first, X_1118, Y_1119), true, iext(uri_rdf_first, X_1118, Y_1119), true)=true))). % 32.76/21.88 tff(c_12377, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subClassOf), true, ifeq(iext(P_47, uri_rdf_Property, uri_rdf_Property), true, true, true), true)=true))). % 32.76/21.88 tff(c_62568, plain, (![P_1115]: (ifeq(iext(uri_rdfs_subPropertyOf, P_1115, uri_rdf__1), true, iext(uri_rdfs_subPropertyOf, P_1115, uri_rdfs_member), true)=true))). % 32.76/21.88 tff(c_4377, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdfs_Class), true, ifeq(iext(P_18, uri_rdf_XMLLiteral, Y_21), true, true, true), true)=true))). % 32.76/21.88 tff(c_8812, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subClassOf), true, ifeq(iext(P_47, uri_rdfs_Class, uri_rdfs_Class), true, true, true), true)=true))). % 32.76/21.88 tff(c_4627, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdfs_Class), true, ifeq(iext(P_18, uri_rdfs_Container, Y_21), true, true, true), true)=true))). % 32.76/21.88 tff(c_6180, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subClassOf), true, ifeq(iext(P_47, uri_rdfs_Literal, uri_rdfs_Resource), true, true, true), true)=true))). % 32.76/21.89 tff(c_4475, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdfs_Class), true, ifeq(iext(P_28, X_30, uri_rdfs_Class), true, true, true), true)=true))). % 32.76/21.89 tff(c_10294, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subPropertyOf), true, ifeq(iext(P_47, uri_rdfs_range, uri_rdfs_range), true, true, true), true)=true))). % 32.76/21.89 tff(c_6992, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subPropertyOf), true, ifeq(iext(P_47, uri_rdf__2, uri_rdfs_member), true, true, true), true)=true))). % 32.76/21.89 tff(c_60828, plain, (![X_1101, Y_1102]: (ifeq(iext(uri_rdfs_subClassOf, X_1101, Y_1102), true, iext(uri_rdfs_subClassOf, X_1101, Y_1102), true)=true))). % 32.76/21.89 tff(c_11611, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subPropertyOf), true, ifeq(iext(P_47, uri_rdf_object, uri_rdf_object), true, true, true), true)=true))). % 32.76/21.89 tff(c_4991, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subClassOf), true, ifeq(iext(P_47, uri_rdf_Alt, uri_rdf_Alt), true, true, true), true)=true))). % 32.76/21.89 tff(c_4577, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdfs_Class), true, ifeq(iext(P_18, uri_rdf_Alt, Y_21), true, true, true), true)=true))). % 32.76/21.89 tff(c_5647, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subClassOf), true, ifeq(iext(P_47, uri_rdf_XMLLiteral, uri_rdfs_Resource), true, true, true), true)=true))). % 32.76/21.89 tff(c_12692, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subClassOf), true, ifeq(iext(P_47, uri_rdf_Bag, uri_rdf_Bag), true, true, true), true)=true))). % 32.76/21.89 tff(c_16677, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, uri_rdf_List, uri_rdfs_Class), true, true, true), true)=true))). % 32.76/21.89 tff(c_5306, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subClassOf), true, ifeq(iext(P_47, uri_rdfs_Seq, uri_rdfs_Seq), true, true, true), true)=true))). % 32.76/21.89 tff(c_59524, plain, (![C_1089]: (ifeq(iext(uri_rdfs_subClassOf, C_1089, uri_rdf_Bag), true, iext(uri_rdfs_subClassOf, C_1089, uri_rdfs_Resource), true)=true))). % 32.76/21.89 tff(c_7675, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subPropertyOf), true, ifeq(iext(P_47, uri_owl_someValuesFrom, uri_owl_someValuesFrom), true, true, true), true)=true))). % 32.76/21.89 tff(c_59086, plain, (![P_1084]: (ifeq(iext(uri_rdfs_subPropertyOf, P_1084, uri_rdf__2), true, iext(uri_rdfs_subPropertyOf, P_1084, uri_rdfs_member), true)=true))). % 32.76/21.89 tff(c_5739, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subClassOf), true, ifeq(iext(P_47, uri_rdfs_Class, uri_rdfs_Resource), true, true, true), true)=true))). % 32.76/21.89 tff(c_8935, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subPropertyOf), true, ifeq(iext(P_47, uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf), true, true, true), true)=true))). % 32.76/21.89 tff(c_11116, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subClassOf), true, ifeq(iext(P_47, uri_rdf_XMLLiteral, uri_rdf_XMLLiteral), true, true, true), true)=true))). % 32.76/21.89 tff(c_58694, plain, (![X_1077, Y_1078]: (ifeq(iext(uri_rdfs_seeAlso, X_1077, Y_1078), true, iext(uri_rdfs_seeAlso, X_1077, Y_1078), true)=true))). % 32.76/21.89 tff(c_4478, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdfs_Class), true, ifeq(iext(P_18, uri_rdfs_Class, Y_21), true, true, true), true)=true))). % 32.76/21.89 tff(c_11208, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, uri_rdfs_subPropertyOf, uri_rdf_Property), true, true, true), true)=true))). % 32.76/21.89 tff(c_4236, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdfs_Class), true, ifeq(iext(P_18, uri_rdfs_ContainerMembershipProperty, Y_21), true, true, true), true)=true))). % 32.76/21.89 tff(c_57717, plain, (![X_1064, Y_1065]: (ifeq(iext(uri_rdf_object, X_1064, Y_1065), true, iext(uri_rdf_object, X_1064, Y_1065), true)=true))). % 32.76/21.89 tff(c_57690, plain, (![X_1060, Y_1061]: (ifeq(iext(uri_rdf__1, X_1060, Y_1061), true, iext(uri_rdfs_member, X_1060, Y_1061), true)=true))). % 32.76/21.89 tff(c_4532, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdfs_Class), true, ifeq(iext(P_18, uri_rdfs_Seq, Y_21), true, true, true), true)=true))). % 32.76/21.89 tff(c_11674, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subClassOf), true, ifeq(iext(P_47, uri_rdf_Alt, uri_rdfs_Resource), true, true, true), true)=true))). % 32.76/21.89 tff(c_6280, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subPropertyOf), true, ifeq(iext(P_47, uri_rdf_value, uri_rdf_value), true, true, true), true)=true))). % 32.76/21.89 tff(c_8368, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, uri_owl_onProperty, uri_rdf_Property), true, true, true), true)=true))). % 32.76/21.89 tff(c_56658, plain, (![X_1047, Y_1048]: (ifeq(iext(uri_rdf__1, X_1047, Y_1048), true, iext(uri_rdf__1, X_1047, Y_1048), true)=true))). % 32.76/21.89 tff(c_56631, plain, (![X_1043, Y_1044]: (ifeq(iext(uri_rdf_value, X_1043, Y_1044), true, iext(uri_rdf_value, X_1043, Y_1044), true)=true))). % 32.76/21.89 tff(c_56460, plain, (![C_1041]: (ifeq(iext(uri_rdfs_subClassOf, C_1041, uri_rdfs_Seq), true, iext(uri_rdfs_subClassOf, C_1041, uri_rdfs_Resource), true)=true))). % 32.76/21.89 tff(c_56281, plain, (![C_1039]: (ifeq(iext(uri_rdfs_subClassOf, C_1039, uri_rdfs_Class), true, iext(uri_rdfs_subClassOf, C_1039, uri_rdfs_Resource), true)=true))). % 32.76/21.89 tff(c_5385, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subClassOf), true, ifeq(iext(P_47, uri_rdfs_ContainerMembershipProperty, uri_rdfs_ContainerMembershipProperty), true, true, true), true)=true))). % 32.76/21.89 tff(c_4374, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdfs_Class), true, ifeq(iext(P_28, X_30, uri_rdf_XMLLiteral), true, true, true), true)=true))). % 32.76/21.89 tff(c_12828, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subClassOf), true, ifeq(iext(P_47, uri_rdfs_Container, uri_rdfs_Resource), true, true, true), true)=true))). % 32.76/21.89 tff(c_55109, plain, (![X_1031, Y_1032]: (ifeq(iext(uri_rdf_type, X_1031, Y_1032), true, iext(uri_rdf_type, X_1031, Y_1032), true)=true))). % 32.76/21.89 tff(c_4892, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subClassOf), true, ifeq(iext(P_47, uri_rdfs_Container, uri_rdfs_Container), true, true, true), true)=true))). % 32.76/21.89 tff(c_6591, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subPropertyOf), true, ifeq(iext(P_47, uri_rdf__3, uri_rdf__3), true, true, true), true)=true))). % 32.76/21.89 tff(c_12231, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subPropertyOf), true, ifeq(iext(P_47, uri_rdfs_isDefinedBy, uri_rdfs_isDefinedBy), true, true, true), true)=true))). % 32.76/21.89 tff(c_5922, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subClassOf), true, ifeq(iext(P_47, uri_rdfs_Literal, uri_rdfs_Literal), true, true, true), true)=true))). % 32.76/21.89 tff(c_8115, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subPropertyOf), true, ifeq(iext(P_47, uri_rdfs_domain, uri_rdfs_domain), true, true, true), true)=true))). % 32.76/21.89 tff(c_54439, plain, (![P_1024]: (ifeq(iext(uri_rdfs_subPropertyOf, P_1024, uri_rdf__3), true, iext(uri_rdfs_subPropertyOf, P_1024, uri_rdfs_member), true)=true))). % 32.76/21.89 tff(c_54124, plain, (![X_1020, Y_1021]: (ifeq(iext(uri_rdfs_range, X_1020, Y_1021), true, iext(uri_rdfs_range, X_1020, Y_1021), true)=true))). % 32.76/21.89 tff(c_54096, plain, (![X_1016, Y_1017]: (ifeq(iext(uri_rdf__2, X_1016, Y_1017), true, iext(uri_rdf__2, X_1016, Y_1017), true)=true))). % 32.76/21.89 tff(c_53917, plain, (![C_1014]: (ifeq(iext(uri_rdfs_subClassOf, C_1014, uri_rdf_Property), true, iext(uri_rdfs_subClassOf, C_1014, uri_rdfs_Resource), true)=true))). % 32.76/21.89 tff(c_4326, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdfs_Class), true, ifeq(iext(P_28, X_30, uri_rdfs_Literal), true, true, true), true)=true))). % 32.76/21.89 tff(c_6018, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subPropertyOf), true, ifeq(iext(P_47, uri_rdf_subject, uri_rdf_subject), true, true, true), true)=true))). % 32.76/21.89 tff(c_4427, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdfs_Class), true, ifeq(iext(P_18, uri_rdfs_Datatype, Y_21), true, true, true), true)=true))). % 32.76/21.89 tff(c_4574, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdfs_Class), true, ifeq(iext(P_28, X_30, uri_rdf_Alt), true, true, true), true)=true))). % 32.76/21.89 tff(c_52854, plain, (![X_1003, Y_1004]: (ifeq(iext(uri_rdfs_subPropertyOf, X_1003, Y_1004), true, iext(uri_rdfs_subPropertyOf, X_1003, Y_1004), true)=true))). % 32.76/21.89 tff(c_4424, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdfs_Class), true, ifeq(iext(P_28, X_30, uri_rdfs_Datatype), true, true, true), true)=true))). % 32.76/21.89 tff(c_52523, plain, (![C_999]: (ifeq(iext(uri_rdfs_subClassOf, C_999, uri_rdfs_Container), true, iext(uri_rdfs_subClassOf, C_999, uri_rdfs_Resource), true)=true))). % 32.76/21.89 tff(c_18337, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdf_Property), true, ifeq(iext(P_28, X_30, uri_rdfs_comment), true, true, true), true)=true))). % 32.76/21.89 tff(c_9318, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdf_Property), true, ifeq(iext(P_18, uri_rdfs_isDefinedBy, Y_21), true, true, true), true)=true))). % 32.76/21.89 tff(c_19689, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdfs_Class), true, ifeq(iext(P_18, sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z, Y_21), true, true, true), true)=true))). % 32.76/21.89 tff(c_8178, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdfs_Class), true, ifeq(iext(P_28, X_30, uri_owl_Class), true, true, true), true)=true))). % 32.76/21.89 tff(c_4832, plain, (![P_47, X_141]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, X_141, uri_rdfs_Resource), true, true, true), true)=true))). % 32.76/21.89 tff(c_19686, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdfs_Class), true, ifeq(iext(P_28, X_30, sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z), true, true, true), true)=true))). % 32.76/21.89 tff(c_18340, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdf_Property), true, ifeq(iext(P_18, uri_rdfs_comment, Y_21), true, true, true), true)=true))). % 32.76/21.89 tff(c_9315, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdf_Property), true, ifeq(iext(P_28, X_30, uri_rdfs_isDefinedBy), true, true, true), true)=true))). % 32.76/21.89 tff(c_7107, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdf_Property), true, ifeq(iext(P_28, X_30, uri_rdfs_label), true, true, true), true)=true))). % 32.76/21.89 tff(c_6342, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdf_Property), true, ifeq(iext(P_28, X_30, uri_rdfs_domain), true, true, true), true)=true))). % 32.76/21.89 tff(c_10992, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdf_Property), true, ifeq(iext(P_18, uri_rdf_predicate, Y_21), true, true, true), true)=true))). % 32.76/21.89 tff(c_14244, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdfs_Class), true, ifeq(iext(P_18, uri_owl_ObjectProperty, Y_21), true, true, true), true)=true))). % 32.76/21.89 tff(c_14241, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdfs_Class), true, ifeq(iext(P_28, X_30, uri_owl_ObjectProperty), true, true, true), true)=true))). % 32.76/21.89 tff(c_7234, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdfs_Class), true, ifeq(iext(P_18, uri_owl_Restriction, Y_21), true, true, true), true)=true))). % 32.76/21.89 tff(c_8181, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdfs_Class), true, ifeq(iext(P_18, uri_owl_Class, Y_21), true, true, true), true)=true))). % 32.76/21.89 tff(c_6677, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdfs_Class), true, ifeq(iext(P_18, uri_rdfs_Statement, Y_21), true, true, true), true)=true))). % 32.76/21.89 tff(c_6345, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdf_Property), true, ifeq(iext(P_18, uri_rdfs_domain, Y_21), true, true, true), true)=true))). % 32.76/21.89 tff(c_10989, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdf_Property), true, ifeq(iext(P_28, X_30, uri_rdf_predicate), true, true, true), true)=true))). % 32.76/21.89 tff(c_6674, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdfs_Class), true, ifeq(iext(P_28, X_30, uri_rdfs_Statement), true, true, true), true)=true))). % 32.76/21.89 tff(c_7110, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdf_Property), true, ifeq(iext(P_18, uri_rdfs_label, Y_21), true, true, true), true)=true))). % 32.76/21.89 tff(c_7231, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdfs_Class), true, ifeq(iext(P_28, X_30, uri_owl_Restriction), true, true, true), true)=true))). % 32.76/21.89 tff(c_3521, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdf_Property), true, ifeq(iext(P_28, X_30, uri_rdf_value), true, true, true), true)=true))). % 32.76/21.89 tff(c_3860, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdf_Property), true, ifeq(iext(P_18, uri_rdf_subject, Y_21), true, true, true), true)=true))). % 32.76/21.89 tff(c_3909, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdf_Property), true, ifeq(iext(P_28, X_30, uri_rdf_rest), true, true, true), true)=true))). % 32.76/21.89 tff(c_3524, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdf_Property), true, ifeq(iext(P_18, uri_rdf_value, Y_21), true, true, true), true)=true))). % 32.76/21.89 tff(c_4195, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdf_Property), true, ifeq(iext(P_28, X_30, uri_rdf_type), true, true, true), true)=true))). % 32.76/21.89 tff(c_4029, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdfs_ContainerMembershipProperty), true, ifeq(iext(P_18, uri_rdf__2, Y_21), true, true, true), true)=true))). % 32.76/21.89 tff(c_3987, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdf_Property), true, ifeq(iext(P_28, X_30, uri_rdf__2), true, true, true), true)=true))). % 32.76/21.89 tff(c_4198, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdf_Property), true, ifeq(iext(P_18, uri_rdf_type, Y_21), true, true, true), true)=true))). % 32.76/21.89 tff(c_4026, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdfs_ContainerMembershipProperty), true, ifeq(iext(P_28, X_30, uri_rdf__2), true, true, true), true)=true))). % 32.76/21.90 tff(c_3635, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_owl_ObjectProperty), true, ifeq(iext(P_18, uri_ex_p, Y_21), true, true, true), true)=true))). % 32.76/21.90 tff(c_4108, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdf_Property), true, ifeq(iext(P_28, X_30, uri_rdf_first), true, true, true), true)=true))). % 32.76/21.90 tff(c_3952, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdf_Property), true, ifeq(iext(P_18, uri_rdf_object, Y_21), true, true, true), true)=true))). % 32.76/21.90 tff(c_3454, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_owl_Class), true, ifeq(iext(P_28, X_30, uri_ex_c), true, true, true), true)=true))). % 32.76/21.90 tff(c_3598, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdf_List), true, ifeq(iext(P_18, uri_rdf_nil, Y_21), true, true, true), true)=true))). % 32.76/21.90 tff(c_3484, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdfs_ContainerMembershipProperty), true, ifeq(iext(P_18, uri_rdf__1, Y_21), true, true, true), true)=true))). % 32.76/21.90 tff(c_4111, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdf_Property), true, ifeq(iext(P_18, uri_rdf_first, Y_21), true, true, true), true)=true))). % 32.76/21.90 tff(c_3857, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdf_Property), true, ifeq(iext(P_28, X_30, uri_rdf_subject), true, true, true), true)=true))). % 32.76/21.90 tff(c_3672, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdfs_ContainerMembershipProperty), true, ifeq(iext(P_18, uri_rdf__3, Y_21), true, true, true), true)=true))). % 32.76/21.90 tff(c_3561, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdf_Property), true, ifeq(iext(P_18, uri_rdf__1, Y_21), true, true, true), true)=true))). % 32.76/21.90 tff(c_16429, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdfs_Class), true, ifeq(iext(P_18, uri_rdf_List, Y_21), true, true, true), true)=true))). % 32.76/21.90 tff(c_4071, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z), true, ifeq(iext(P_18, uri_ex_s, Y_21), true, true, true), true)=true))). % 32.76/21.90 tff(c_3595, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdf_List), true, ifeq(iext(P_28, X_30, uri_rdf_nil), true, true, true), true)=true))). % 32.76/21.90 tff(c_3813, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdfs_Class), true, ifeq(iext(P_18, uri_rdf_Property, Y_21), true, true, true), true)=true))). % 32.76/21.90 tff(c_4154, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdfs_Datatype), true, ifeq(iext(P_18, uri_rdf_XMLLiteral, Y_21), true, true, true), true)=true))). % 32.76/21.90 tff(c_3457, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_owl_Class), true, ifeq(iext(P_18, uri_ex_c, Y_21), true, true, true), true)=true))). % 32.76/21.90 tff(c_3912, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdf_Property), true, ifeq(iext(P_18, uri_rdf_rest, Y_21), true, true, true), true)=true))). % 32.76/21.90 tff(c_3764, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdf_Property), true, ifeq(iext(P_18, uri_rdf__3, Y_21), true, true, true), true)=true))). % 32.76/21.90 tff(c_3669, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdfs_ContainerMembershipProperty), true, ifeq(iext(P_28, X_30, uri_rdf__3), true, true, true), true)=true))). % 32.76/21.90 tff(c_3949, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdf_Property), true, ifeq(iext(P_28, X_30, uri_rdf_object), true, true, true), true)=true))). % 32.76/21.90 tff(c_3761, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdf_Property), true, ifeq(iext(P_28, X_30, uri_rdf__3), true, true, true), true)=true))). % 32.76/21.90 tff(c_16426, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdfs_Class), true, ifeq(iext(P_28, X_30, uri_rdf_List), true, true, true), true)=true))). % 32.76/21.90 tff(c_3632, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_owl_ObjectProperty), true, ifeq(iext(P_28, X_30, uri_ex_p), true, true, true), true)=true))). % 32.76/21.90 tff(c_4068, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z), true, ifeq(iext(P_28, X_30, uri_ex_s), true, true, true), true)=true))). % 32.76/21.90 tff(c_3810, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdfs_Class), true, ifeq(iext(P_28, X_30, uri_rdf_Property), true, true, true), true)=true))). % 32.76/21.90 tff(c_3713, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_owl_Restriction), true, ifeq(iext(P_28, X_30, sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z), true, true, true), true)=true))). % 32.76/21.90 tff(c_3990, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdf_Property), true, ifeq(iext(P_18, uri_rdf__2, Y_21), true, true, true), true)=true))). % 32.76/21.90 tff(c_3716, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_owl_Restriction), true, ifeq(iext(P_18, sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z, Y_21), true, true, true), true)=true))). % 32.76/21.90 tff(c_4151, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdfs_Datatype), true, ifeq(iext(P_28, X_30, uri_rdf_XMLLiteral), true, true, true), true)=true))). % 32.76/21.90 tff(c_3481, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdfs_ContainerMembershipProperty), true, ifeq(iext(P_28, X_30, uri_rdf__1), true, true, true), true)=true))). % 32.76/21.90 tff(c_3558, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdf_Property), true, ifeq(iext(P_28, X_30, uri_rdf__1), true, true, true), true)=true))). % 32.76/21.90 tff(c_1719, plain, (![P_94, X_63, Y_97]: (ifeq(iext(uri_rdfs_domain, P_94, uri_rdfs_Resource), true, ifeq(iext(P_94, X_63, Y_97), true, true, true), true)=true))). % 32.76/21.90 tff(c_2063, plain, (![P_98, X_100, X_63]: (ifeq(iext(uri_rdfs_range, P_98, uri_rdfs_Resource), true, ifeq(iext(P_98, X_100, X_63), true, true, true), true)=true))). % 32.76/21.90 tff(c_2727, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_owl_someValuesFrom), true, ifeq(iext(P_108, sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z, uri_ex_c), true, true, true), true)=true))). % 32.76/21.90 tff(c_2592, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdf_type), true, ifeq(iext(P_108, uri_rdf__3, uri_rdfs_ContainerMembershipProperty), true, true, true), true)=true))). % 32.76/21.90 tff(c_2937, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdfs_domain), true, ifeq(iext(P_108, uri_rdf_rest, uri_rdf_List), true, true, true), true)=true))). % 32.76/21.90 tff(c_2871, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdfs_subClassOf), true, ifeq(iext(P_108, uri_rdfs_ContainerMembershipProperty, uri_rdf_Property), true, true, true), true)=true))). % 32.76/21.90 tff(c_2925, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdfs_range), true, ifeq(iext(P_108, uri_rdfs_subClassOf, uri_rdfs_Class), true, true, true), true)=true))). % 32.76/21.90 tff(c_2604, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdf_type), true, ifeq(iext(P_108, uri_rdf_nil, uri_rdf_List), true, true, true), true)=true))). % 32.76/21.90 tff(c_2733, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdfs_domain), true, ifeq(iext(P_108, uri_rdfs_comment, uri_rdfs_Resource), true, true, true), true)=true))). % 32.76/21.90 tff(c_2757, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdf_type), true, ifeq(iext(P_108, uri_rdf__2, uri_rdfs_ContainerMembershipProperty), true, true, true), true)=true))). % 32.76/21.90 tff(c_2931, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdfs_domain), true, ifeq(iext(P_108, uri_rdf_object, uri_rdfs_Statement), true, true, true), true)=true))). % 32.76/21.90 tff(c_2751, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdf_type), true, ifeq(iext(P_108, uri_rdf_value, uri_rdf_Property), true, true, true), true)=true))). % 32.76/21.90 tff(c_2895, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdfs_domain), true, ifeq(iext(P_108, uri_rdf_subject, uri_rdfs_Statement), true, true, true), true)=true))). % 32.76/21.90 tff(c_2610, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdf_type), true, ifeq(iext(P_108, uri_rdf_XMLLiteral, uri_rdfs_Datatype), true, true, true), true)=true))). % 32.76/21.90 tff(c_41277, plain, (![C_857]: (ifeq(iext(uri_rdfs_subClassOf, C_857, uri_rdf_Alt), true, iext(uri_rdfs_subClassOf, C_857, uri_rdfs_Container), true)=true))). % 32.76/21.90 tff(c_2694, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdf_type), true, ifeq(iext(P_108, uri_rdf__1, uri_rdf_Property), true, true, true), true)=true))). % 32.76/21.90 tff(c_2913, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdf_type), true, ifeq(iext(P_108, uri_rdf_first, uri_rdf_Property), true, true, true), true)=true))). % 32.76/21.90 tff(c_2799, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdfs_range), true, ifeq(iext(P_108, uri_rdf__1, uri_rdfs_Resource), true, true, true), true)=true))). % 32.76/21.90 tff(c_40840, plain, (![C_852]: (ifeq(iext(uri_rdfs_subClassOf, C_852, uri_rdf_Bag), true, iext(uri_rdfs_subClassOf, C_852, uri_rdfs_Container), true)=true))). % 32.76/21.90 tff(c_2739, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdfs_domain), true, ifeq(iext(P_108, uri_rdfs_seeAlso, uri_rdfs_Resource), true, true, true), true)=true))). % 32.76/21.90 tff(c_40650, plain, (![X_846, Y_847]: (ifeq(iext(uri_rdfs_isDefinedBy, X_846, Y_847), true, iext(uri_rdfs_seeAlso, X_846, Y_847), true)=true))). % 32.76/21.90 tff(c_40617, plain, (![C_845]: (ifeq(iext(uri_rdfs_subClassOf, C_845, uri_rdfs_Seq), true, iext(uri_rdfs_subClassOf, C_845, uri_rdfs_Container), true)=true))). % 32.76/21.90 tff(c_2646, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdf_type), true, ifeq(iext(P_108, uri_rdf_Property, uri_rdfs_Class), true, true, true), true)=true))). % 32.76/21.90 tff(c_2811, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdfs_subClassOf), true, ifeq(iext(P_108, uri_rdf_Alt, uri_rdfs_Container), true, true, true), true)=true))). % 32.76/21.90 tff(c_2670, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdf_type), true, ifeq(iext(P_108, uri_rdf__1, uri_rdfs_ContainerMembershipProperty), true, true, true), true)=true))). % 32.76/21.90 tff(c_2889, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdfs_domain), true, ifeq(iext(P_108, uri_rdf_predicate, uri_rdfs_Statement), true, true, true), true)=true))). % 32.76/21.90 tff(c_2793, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdfs_range), true, ifeq(iext(P_108, uri_rdfs_subPropertyOf, uri_rdf_Property), true, true, true), true)=true))). % 32.76/21.90 tff(c_2865, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdfs_domain), true, ifeq(iext(P_108, uri_rdf_type, uri_rdfs_Resource), true, true, true), true)=true))). % 32.76/21.90 tff(c_2835, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdfs_domain), true, ifeq(iext(P_108, uri_rdfs_isDefinedBy, uri_rdfs_Resource), true, true, true), true)=true))). % 32.76/21.90 tff(c_2805, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdfs_domain), true, ifeq(iext(P_108, uri_rdfs_member, uri_rdfs_Resource), true, true, true), true)=true))). % 32.76/21.90 tff(c_2688, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdf_type), true, ifeq(iext(P_108, uri_rdf_object, uri_rdf_Property), true, true, true), true)=true))). % 32.76/21.90 tff(c_2907, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdfs_range), true, ifeq(iext(P_108, uri_rdfs_range, uri_rdfs_Class), true, true, true), true)=true))). % 32.76/21.90 tff(c_2883, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdf_type), true, ifeq(iext(P_108, uri_rdf__2, uri_rdf_Property), true, true, true), true)=true))). % 32.76/21.90 tff(c_2961, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdf_type), true, ifeq(iext(P_108, uri_ex_p, uri_owl_ObjectProperty), true, true, true), true)=true))). % 32.76/21.90 tff(c_2616, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdfs_domain), true, ifeq(iext(P_108, uri_rdfs_subClassOf, uri_rdfs_Class), true, true, true), true)=true))). % 32.76/21.90 tff(c_2586, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_owl_onProperty), true, ifeq(iext(P_108, sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z, uri_ex_p), true, true, true), true)=true))). % 32.76/21.90 tff(c_2949, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdfs_domain), true, ifeq(iext(P_108, uri_rdfs_range, uri_rdf_Property), true, true, true), true)=true))). % 32.76/21.90 tff(c_2919, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdf_type), true, ifeq(iext(P_108, uri_rdf_subject, uri_rdf_Property), true, true, true), true)=true))). % 32.76/21.90 tff(c_2853, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdfs_domain), true, ifeq(iext(P_108, uri_rdf_value, uri_rdfs_Resource), true, true, true), true)=true))). % 32.76/21.90 tff(c_2781, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdfs_range), true, ifeq(iext(P_108, uri_rdf_subject, uri_rdfs_Resource), true, true, true), true)=true))). % 32.76/21.90 tff(c_2598, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdfs_range), true, ifeq(iext(P_108, uri_rdf_first, uri_rdfs_Resource), true, true, true), true)=true))). % 32.76/21.90 tff(c_2682, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdfs_range), true, ifeq(iext(P_108, uri_rdf_predicate, uri_rdfs_Resource), true, true, true), true)=true))). % 32.76/21.90 tff(c_2658, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdf_type), true, ifeq(iext(P_108, uri_rdf__3, uri_rdf_Property), true, true, true), true)=true))). % 32.76/21.90 tff(c_37965, plain, (![D_822]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_822), true, icext(D_822, uri_rdfs_member), true)=true))). % 32.76/21.90 tff(c_2823, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdfs_range), true, ifeq(iext(P_108, uri_rdfs_member, uri_rdfs_Resource), true, true, true), true)=true))). % 32.76/21.90 tff(c_37769, plain, (![D_819]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_819), true, icext(D_819, uri_rdfs_Resource), true)=true))). % 32.76/21.90 tff(c_37703, plain, (![D_817]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_817), true, icext(D_817, uri_owl_someValuesFrom), true)=true))). % 32.76/21.90 tff(c_37637, plain, (![D_815]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_815), true, icext(D_815, uri_rdfs_subClassOf), true)=true))). % 32.76/21.90 tff(c_2763, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdf_type), true, ifeq(iext(P_108, uri_ex_c, uri_owl_Class), true, true, true), true)=true))). % 32.76/21.90 tff(c_37451, plain, (![D_812]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_812), true, icext(D_812, uri_owl_onProperty), true)=true))). % 32.76/21.90 tff(c_37385, plain, (![D_810]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_810), true, icext(D_810, uri_rdfs_subPropertyOf), true)=true))). % 32.76/21.90 tff(c_37198, plain, (![D_807]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_807), true, icext(D_807, uri_rdfs_seeAlso), true)=true))). % 32.76/21.90 tff(c_2901, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdfs_domain), true, ifeq(iext(P_108, uri_rdf_first, uri_rdf_List), true, true, true), true)=true))). % 32.76/21.90 tff(c_37132, plain, (![D_805]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_805), true, icext(D_805, uri_rdfs_range), true)=true))). % 32.76/21.90 tff(c_37066, plain, (![D_803]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_803), true, icext(D_803, uri_rdf_Alt), true)=true))). % 32.76/21.90 tff(c_37015, plain, (![C_801]: (ifeq(iext(uri_rdfs_subClassOf, C_801, uri_rdf_XMLLiteral), true, iext(uri_rdfs_subClassOf, C_801, uri_rdfs_Literal), true)=true))). % 32.76/21.90 tff(c_36948, plain, (![D_799]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_799), true, icext(D_799, uri_rdfs_Datatype), true)=true))). % 32.76/21.90 tff(c_36881, plain, (![D_797]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_797), true, icext(D_797, uri_rdf_Bag), true)=true))). % 32.76/21.90 tff(c_2877, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdfs_range), true, ifeq(iext(P_108, uri_rdfs_isDefinedBy, uri_rdfs_Resource), true, true, true), true)=true))). % 32.76/21.90 tff(c_36685, plain, (![D_794]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_794), true, icext(D_794, uri_rdfs_Seq), true)=true))). % 32.76/21.90 tff(c_36619, plain, (![D_792]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_792), true, icext(D_792, uri_rdfs_Container), true)=true))). % 32.76/21.90 tff(c_36567, plain, (![C_790]: (ifeq(iext(uri_rdfs_subClassOf, C_790, uri_rdfs_Datatype), true, iext(uri_rdfs_subClassOf, C_790, uri_rdfs_Class), true)=true))). % 32.76/21.90 tff(c_36502, plain, (![D_788]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_788), true, icext(D_788, uri_rdfs_Literal), true)=true))). % 32.76/21.90 tff(c_36436, plain, (![D_786]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_786), true, icext(D_786, uri_rdfs_ContainerMembershipProperty), true)=true))). % 32.76/21.90 tff(c_36342, plain, (![D_784]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_784), true, icext(D_784, uri_rdfs_Class), true)=true))). % 32.76/21.90 tff(c_2859, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdfs_range), true, ifeq(iext(P_108, uri_rdfs_domain, uri_rdfs_Class), true, true, true), true)=true))). % 32.76/21.90 tff(c_36143, plain, (![D_781]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_781), true, icext(D_781, uri_rdf_XMLLiteral), true)=true))). % 32.76/21.90 tff(c_2847, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdfs_subClassOf), true, ifeq(iext(P_108, uri_rdf_Bag, uri_rdfs_Container), true, true, true), true)=true))). % 32.76/21.91 tff(c_35956, plain, (![D_778]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_778), true, icext(D_778, uri_rdfs_comment), true)=true))). % 32.76/21.91 tff(c_35882, plain, (![D_776]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_776), true, icext(D_776, sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z), true)=true))). % 32.76/21.91 tff(c_35795, plain, (![C_773]: (ifeq(iext(uri_rdfs_subClassOf, C_773, uri_rdfs_ContainerMembershipProperty), true, iext(uri_rdfs_subClassOf, C_773, uri_rdf_Property), true)=true))). % 32.76/21.91 tff(c_35765, plain, (![D_772]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_772), true, icext(D_772, uri_owl_Restriction), true)=true))). % 32.76/21.91 tff(c_35699, plain, (![D_770]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_770), true, icext(D_770, uri_owl_ObjectProperty), true)=true))). % 32.76/21.91 tff(c_35633, plain, (![D_768]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_768), true, icext(D_768, uri_rdfs_domain), true)=true))). % 32.76/21.91 tff(c_35438, plain, (![D_765]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_765), true, icext(D_765, uri_rdfs_label), true)=true))). % 32.76/21.91 tff(c_2775, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdfs_domain), true, ifeq(iext(P_108, uri_rdf__3, uri_rdfs_Resource), true, true, true), true)=true))). % 32.76/21.91 tff(c_35372, plain, (![D_763]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_763), true, icext(D_763, uri_rdfs_Statement), true)=true))). % 32.76/21.91 tff(c_35306, plain, (![D_761]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_761), true, icext(D_761, uri_owl_Class), true)=true))). % 32.76/21.91 tff(c_35120, plain, (![D_758]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_758), true, icext(D_758, uri_rdfs_isDefinedBy), true)=true))). % 32.76/21.91 tff(c_2841, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdfs_range), true, ifeq(iext(P_108, uri_rdf_type, uri_rdfs_Class), true, true, true), true)=true))). % 32.76/21.91 tff(c_35054, plain, (![D_756]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_756), true, icext(D_756, uri_rdf_predicate), true)=true))). % 32.76/21.91 tff(c_34972, plain, (![D_754]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, D_754), true, icext(D_754, uri_rdf__1), true)=true))). % 32.76/21.91 tff(c_34778, plain, (![D_751]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_751), true, icext(D_751, uri_rdf__3), true)=true))). % 32.76/21.91 tff(c_2769, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdfs_range), true, ifeq(iext(P_108, uri_rdfs_label, uri_rdfs_Literal), true, true, true), true)=true))). % 32.76/21.91 tff(c_16183, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, uri_rdfs_Resource, uri_rdfs_Class), true)=true))). % 32.76/21.91 tff(c_16043, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_48), true, iext(Q_48, uri_rdfs_label, uri_rdfs_label), true)=true))). % 32.76/21.91 tff(c_16133, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_48), true, iext(Q_48, uri_rdf_predicate, uri_rdf_predicate), true)=true))). % 32.76/21.91 tff(c_2955, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdfs_range), true, ifeq(iext(P_108, uri_rdf_value, uri_rdfs_Resource), true, true, true), true)=true))). % 32.76/21.91 tff(c_18677, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_48), true, iext(Q_48, uri_rdfs_comment, uri_rdfs_comment), true)=true))). % 32.76/21.91 tff(c_15880, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_48), true, iext(Q_48, uri_rdfs_Resource, uri_rdfs_Resource), true)=true))). % 32.76/21.91 tff(c_34415, plain, (![D_740]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, D_740), true, icext(D_740, uri_rdf_XMLLiteral), true)=true))). % 32.76/21.91 tff(c_15976, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_48), true, iext(Q_48, uri_rdfs_member, uri_rdfs_member), true)=true))). % 32.76/21.91 tff(c_15639, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, uri_rdfs_member, uri_rdf_Property), true)=true))). % 32.76/21.91 tff(c_2574, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdfs_range), true, ifeq(iext(P_108, uri_rdf__3, uri_rdfs_Resource), true, true, true), true)=true))). % 32.76/21.91 tff(c_15402, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_48), true, iext(Q_48, uri_owl_ObjectProperty, uri_rdfs_Resource), true)=true))). % 32.76/21.91 tff(c_15032, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_48), true, iext(Q_48, uri_rdfs_Statement, uri_rdfs_Statement), true)=true))). % 32.76/21.91 tff(c_20031, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_48), true, iext(Q_48, sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z, sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z), true)=true))). % 32.76/21.91 tff(c_15403, plain, (![E_41]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Resource, E_41), true, iext(uri_rdfs_subClassOf, uri_owl_ObjectProperty, E_41), true)=true))). % 32.76/21.91 tff(c_15582, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_48), true, iext(Q_48, uri_owl_ObjectProperty, uri_owl_ObjectProperty), true)=true))). % 32.76/21.91 tff(c_14675, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_48), true, iext(Q_48, uri_rdfs_Statement, uri_rdfs_Resource), true)=true))). % 32.76/21.91 tff(c_2634, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdf_type), true, ifeq(iext(P_108, uri_rdf_rest, uri_rdf_Property), true, true, true), true)=true))). % 32.76/21.91 tff(c_15194, plain, (![E_41]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Resource, E_41), true, iext(uri_rdfs_subClassOf, uri_owl_Restriction, E_41), true)=true))). % 32.76/21.91 tff(c_20126, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_48), true, iext(Q_48, sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z, uri_rdfs_Resource), true)=true))). % 32.76/21.91 tff(c_33810, plain, (![D_722]: (ifeq(iext(uri_rdfs_subClassOf, uri_owl_Restriction, D_722), true, icext(D_722, sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z), true)=true))). % 32.76/21.91 tff(c_15127, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_48), true, iext(Q_48, uri_owl_Restriction, uri_owl_Restriction), true)=true))). % 32.76/21.91 tff(c_2721, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdfs_subPropertyOf), true, ifeq(iext(P_108, uri_rdfs_isDefinedBy, uri_rdfs_seeAlso), true, true, true), true)=true))). % 32.76/21.91 tff(c_14852, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_48), true, iext(Q_48, uri_owl_Class, uri_rdfs_Resource), true)=true))). % 32.76/21.91 tff(c_14853, plain, (![E_41]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Resource, E_41), true, iext(uri_rdfs_subClassOf, uri_owl_Class, E_41), true)=true))). % 32.76/21.91 tff(c_33477, plain, (![D_713]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_713), true, icext(D_713, uri_rdf_List), true)=true))). % 32.76/21.91 tff(c_14676, plain, (![E_41]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Resource, E_41), true, iext(uri_rdfs_subClassOf, uri_rdfs_Statement, E_41), true)=true))). % 32.76/21.91 tff(c_14584, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_48), true, iext(Q_48, uri_owl_Class, uri_owl_Class), true)=true))). % 32.76/21.91 tff(c_15193, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_48), true, iext(Q_48, uri_owl_Restriction, uri_rdfs_Resource), true)=true))). % 32.76/21.91 tff(c_2745, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdfs_domain), true, ifeq(iext(P_108, uri_rdf__1, uri_rdfs_Resource), true, true, true), true)=true))). % 32.76/21.91 tff(c_20127, plain, (![E_41]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Resource, E_41), true, iext(uri_rdfs_subClassOf, sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z, E_41), true)=true))). % 32.76/21.91 tff(c_14522, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, uri_rdf_XMLLiteral, uri_rdfs_Class), true)=true))). % 32.76/21.91 tff(c_14190, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, uri_rdfs_Seq, uri_rdfs_Class), true)=true))). % 32.76/21.91 tff(c_33179, plain, (![D_704]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_704), true, icext(D_704, uri_rdf_subject), true)=true))). % 32.76/21.91 tff(c_14111, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, uri_rdf_Alt, uri_rdfs_Class), true)=true))). % 32.76/21.91 tff(c_16758, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_48), true, iext(Q_48, uri_rdf_List, uri_rdf_List), true)=true))). % 32.76/21.91 tff(c_13898, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, uri_rdfs_Class, uri_rdfs_Class), true)=true))). % 32.76/21.91 tff(c_2943, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdfs_range), true, ifeq(iext(P_108, uri_rdf_rest, uri_rdf_List), true, true, true), true)=true))). % 32.76/21.91 tff(c_13851, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, uri_rdfs_ContainerMembershipProperty, uri_rdfs_Class), true)=true))). % 32.76/21.91 tff(c_14017, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, uri_rdf_Bag, uri_rdfs_Class), true)=true))). % 32.76/21.91 tff(c_16850, plain, (![E_41]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Resource, E_41), true, iext(uri_rdfs_subClassOf, uri_rdf_List, E_41), true)=true))). % 32.76/21.91 tff(c_32891, plain, (![D_695]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_695), true, icext(D_695, uri_rdf_Property), true)=true))). % 32.76/21.91 tff(c_13775, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, uri_rdfs_Literal, uri_rdfs_Class), true)=true))). % 32.76/21.91 tff(c_16849, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_48), true, iext(Q_48, uri_rdf_List, uri_rdfs_Resource), true)=true))). % 32.76/21.91 tff(c_14064, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, uri_rdfs_Container, uri_rdfs_Class), true)=true))). % 32.76/21.91 tff(c_2817, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdf_type), true, ifeq(iext(P_108, sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z, uri_owl_Restriction), true, true, true), true)=true))). % 32.76/21.91 tff(c_13945, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, uri_rdfs_Datatype, uri_rdfs_Class), true)=true))). % 32.76/21.91 tff(c_18568, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, uri_rdfs_comment, uri_rdf_Property), true)=true))). % 32.76/21.91 tff(c_19969, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z, uri_rdfs_Class), true)=true))). % 32.76/21.91 tff(c_13383, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, uri_owl_Restriction, uri_rdfs_Class), true)=true))). % 32.76/21.91 tff(c_13722, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, uri_owl_Class, uri_rdfs_Class), true)=true))). % 32.76/21.91 tff(c_13554, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, uri_rdfs_Statement, uri_rdfs_Class), true)=true))). % 32.76/21.91 tff(c_14475, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, uri_owl_ObjectProperty, uri_rdfs_Class), true)=true))). % 32.76/21.91 tff(c_2712, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdfs_range), true, ifeq(iext(P_108, uri_rdfs_seeAlso, uri_rdfs_Resource), true, true, true), true)=true))). % 32.76/21.91 tff(c_13436, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, uri_rdf_predicate, uri_rdf_Property), true)=true))). % 32.76/21.91 tff(c_13629, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, uri_rdfs_label, uri_rdf_Property), true)=true))). % 32.76/21.91 tff(c_11233, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, uri_rdfs_subPropertyOf, uri_rdf_Property), true)=true))). % 32.76/21.91 tff(c_5773, plain, (![E_41]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Resource, E_41), true, iext(uri_rdfs_subClassOf, uri_rdfs_Class, E_41), true)=true))). % 32.76/21.91 tff(c_9263, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_48), true, iext(Q_48, uri_rdfs_seeAlso, uri_rdfs_seeAlso), true)=true))). % 32.76/21.91 tff(c_2700, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdfs_range), true, ifeq(iext(P_108, uri_rdf__2, uri_rdfs_Resource), true, true, true), true)=true))). % 32.76/21.91 tff(c_7705, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_48), true, iext(Q_48, uri_owl_someValuesFrom, uri_owl_someValuesFrom), true)=true))). % 32.76/21.91 tff(c_5419, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_48), true, iext(Q_48, uri_rdfs_ContainerMembershipProperty, uri_rdfs_ContainerMembershipProperty), true)=true))). % 32.76/21.91 tff(c_8780, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_48), true, iext(Q_48, uri_rdf_type, uri_rdf_type), true)=true))). % 32.76/21.91 tff(c_11708, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_48), true, iext(Q_48, uri_rdf_Alt, uri_rdfs_Resource), true)=true))). % 32.76/21.91 tff(c_12726, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_48), true, iext(Q_48, uri_rdf_Bag, uri_rdf_Bag), true)=true))). % 32.76/21.91 tff(c_10870, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_48), true, iext(Q_48, uri_rdf__3, uri_rdfs_member), true)=true))). % 32.76/21.91 tff(c_9648, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, uri_owl_someValuesFrom, uri_rdf_Property), true)=true))). % 32.76/21.91 tff(c_2640, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdfs_subClassOf), true, ifeq(iext(P_108, uri_rdfs_Datatype, uri_rdfs_Class), true, true, true), true)=true))). % 32.76/21.91 tff(c_7023, plain, (![R_53]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_member, R_53), true, iext(uri_rdfs_subPropertyOf, uri_rdf__2, R_53), true)=true))). % 32.76/21.91 tff(c_9085, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, uri_rdfs_range, uri_rdf_Property), true)=true))). % 32.76/21.91 tff(c_6881, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_48), true, iext(Q_48, uri_rdfs_ContainerMembershipProperty, uri_rdfs_Resource), true)=true))). % 32.76/21.91 tff(c_5772, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_48), true, iext(Q_48, uri_rdfs_Class, uri_rdfs_Resource), true)=true))). % 32.76/21.91 tff(c_6517, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_48), true, iext(Q_48, uri_rdf__2, uri_rdf__2), true)=true))). % 32.76/21.91 tff(c_7022, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_48), true, iext(Q_48, uri_rdf__2, uri_rdfs_member), true)=true))). % 32.76/21.91 tff(c_2628, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdfs_domain), true, ifeq(iext(P_108, uri_rdfs_subPropertyOf, uri_rdf_Property), true, true, true), true)=true))). % 32.76/21.91 tff(c_6214, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_48), true, iext(Q_48, uri_rdfs_Literal, uri_rdfs_Resource), true)=true))). % 32.76/21.91 tff(c_10871, plain, (![R_53]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_member, R_53), true, iext(uri_rdfs_subPropertyOf, uri_rdf__3, R_53), true)=true))). % 32.76/21.91 tff(c_31440, plain, (![D_650]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_650), true, icext(D_650, uri_rdf_rest), true)=true))). % 32.76/21.91 tff(c_8846, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_48), true, iext(Q_48, uri_rdfs_Class, uri_rdfs_Class), true)=true))). % 32.76/21.91 tff(c_16696, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, uri_rdf_List, uri_rdfs_Class), true)=true))). % 32.76/21.91 tff(c_2664, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdf_type), true, ifeq(iext(P_108, uri_rdf_type, uri_rdf_Property), true, true, true), true)=true))). % 32.76/21.91 tff(c_8965, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_48), true, iext(Q_48, uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf), true)=true))). % 32.76/21.91 tff(c_9993, plain, (![E_41]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Resource, E_41), true, iext(uri_rdfs_subClassOf, uri_rdfs_Seq, E_41), true)=true))). % 32.76/21.91 tff(c_5959, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_48), true, iext(Q_48, uri_rdfs_Literal, uri_rdfs_Literal), true)=true))). % 32.76/21.91 tff(c_2676, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdfs_subClassOf), true, ifeq(iext(P_108, uri_rdfs_Seq, uri_rdfs_Container), true, true, true), true)=true))). % 32.76/21.91 tff(c_11150, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_48), true, iext(Q_48, uri_rdf_XMLLiteral, uri_rdf_XMLLiteral), true)=true))). % 32.76/21.91 tff(c_8145, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_48), true, iext(Q_48, uri_rdfs_domain, uri_rdfs_domain), true)=true))). % 32.76/21.91 tff(c_10935, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_48), true, iext(Q_48, uri_rdfs_Datatype, uri_rdfs_Datatype), true)=true))). % 32.76/21.91 tff(c_6311, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_48), true, iext(Q_48, uri_rdf_value, uri_rdf_value), true)=true))). % 32.76/21.91 tff(c_5681, plain, (![E_41]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Resource, E_41), true, iext(uri_rdfs_subClassOf, uri_rdf_XMLLiteral, E_41), true)=true))). % 32.76/21.91 tff(c_7494, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_48), true, iext(Q_48, uri_rdf_Property, uri_rdfs_Resource), true)=true))). % 32.76/21.91 tff(c_12796, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_48), true, iext(Q_48, uri_rdfs_subClassOf, uri_rdfs_subClassOf), true)=true))). % 32.76/21.91 tff(c_2787, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdfs_domain), true, ifeq(iext(P_108, uri_rdfs_domain, uri_rdf_Property), true, true, true), true)=true))). % 32.76/21.91 tff(c_5108, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_48), true, iext(Q_48, uri_rdfs_Datatype, uri_rdfs_Resource), true)=true))). % 32.76/21.91 tff(c_8654, plain, (![E_41]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Resource, E_41), true, iext(uri_rdfs_subClassOf, uri_rdf_Bag, E_41), true)=true))). % 32.76/21.91 tff(c_10326, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_48), true, iext(Q_48, uri_rdfs_range, uri_rdfs_range), true)=true))). % 32.76/21.91 tff(c_30510, plain, (![D_623]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_623), true, icext(D_623, uri_rdf__1), true)=true))). % 32.76/21.91 tff(c_13332, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_48), true, iext(Q_48, uri_rdf_first, uri_rdf_first), true)=true))). % 32.76/21.91 tff(c_12863, plain, (![E_41]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Resource, E_41), true, iext(uri_rdfs_subClassOf, uri_rdfs_Container, E_41), true)=true))). % 32.76/21.91 tff(c_2652, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdf_type), true, ifeq(iext(P_108, uri_ex_s, sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z), true, true, true), true)=true))). % 32.76/21.91 tff(c_10474, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_48), true, iext(Q_48, uri_rdf__1, uri_rdf__1), true)=true))). % 32.76/21.92 tff(c_13263, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_48), true, iext(Q_48, uri_rdf__1, uri_rdfs_member), true)=true))). % 32.76/21.92 tff(c_11643, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_48), true, iext(Q_48, uri_rdf_object, uri_rdf_object), true)=true))). % 32.76/21.92 tff(c_2622, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdfs_subClassOf), true, ifeq(iext(P_108, uri_rdf_XMLLiteral, uri_rdfs_Literal), true, true, true), true)=true))). % 32.76/21.92 tff(c_6215, plain, (![E_41]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Resource, E_41), true, iext(uri_rdfs_subClassOf, uri_rdfs_Literal, E_41), true)=true))). % 32.76/21.92 tff(c_11709, plain, (![E_41]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Resource, E_41), true, iext(uri_rdfs_subClassOf, uri_rdf_Alt, E_41), true)=true))). % 32.76/21.92 tff(c_29889, plain, (![D_605]: (ifeq(iext(uri_rdfs_subClassOf, sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z, D_605), true, icext(D_605, uri_ex_s), true)=true))). % 32.76/21.92 tff(c_5339, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_48), true, iext(Q_48, uri_rdfs_Seq, uri_rdfs_Seq), true)=true))). % 32.76/21.92 tff(c_5563, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, uri_rdfs_seeAlso, uri_rdf_Property), true)=true))). % 32.76/21.92 tff(c_5680, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_48), true, iext(Q_48, uri_rdf_XMLLiteral, uri_rdfs_Resource), true)=true))). % 32.76/21.92 tff(c_2580, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdfs_domain), true, ifeq(iext(P_108, uri_rdfs_label, uri_rdfs_Resource), true, true, true), true)=true))). % 32.76/21.92 tff(c_7959, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, uri_rdfs_subClassOf, uri_rdf_Property), true)=true))). % 32.76/21.92 tff(c_6622, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_48), true, iext(Q_48, uri_rdf__3, uri_rdf__3), true)=true))). % 32.76/21.92 tff(c_9992, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_48), true, iext(Q_48, uri_rdfs_Seq, uri_rdfs_Resource), true)=true))). % 32.76/21.92 tff(c_13264, plain, (![R_53]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_member, R_53), true, iext(uri_rdfs_subPropertyOf, uri_rdf__1, R_53), true)=true))). % 32.76/21.92 tff(c_9029, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_48), true, iext(Q_48, uri_owl_onProperty, uri_owl_onProperty), true)=true))). % 32.76/21.92 tff(c_12411, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_48), true, iext(Q_48, uri_rdf_Property, uri_rdf_Property), true)=true))). % 32.76/21.92 tff(c_29563, plain, (![P_593]: (ifeq(iext(uri_rdfs_subPropertyOf, P_593, uri_rdfs_isDefinedBy), true, iext(uri_rdfs_subPropertyOf, P_593, uri_rdfs_seeAlso), true)=true))). % 32.76/21.92 tff(c_13033, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, uri_rdfs_domain, uri_rdf_Property), true)=true))). % 32.76/21.92 tff(c_8393, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, uri_owl_onProperty, uri_rdf_Property), true)=true))). % 32.76/21.92 tff(c_4925, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_48), true, iext(Q_48, uri_rdfs_Container, uri_rdfs_Container), true)=true))). % 32.76/21.92 tff(c_29432, plain, (![D_588]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, D_588), true, icext(D_588, uri_rdf__2), true)=true))). % 32.76/21.92 tff(c_5024, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_48), true, iext(Q_48, uri_rdf_Alt, uri_rdf_Alt), true)=true))). % 32.76/21.92 tff(c_6121, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_48), true, iext(Q_48, uri_rdf_rest, uri_rdf_rest), true)=true))). % 32.76/21.92 tff(c_7495, plain, (![E_41]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Resource, E_41), true, iext(uri_rdfs_subClassOf, uri_rdf_Property, E_41), true)=true))). % 32.76/21.92 tff(c_6049, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_48), true, iext(Q_48, uri_rdf_subject, uri_rdf_subject), true)=true))). % 32.76/21.92 tff(c_8653, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_48), true, iext(Q_48, uri_rdf_Bag, uri_rdfs_Resource), true)=true))). % 32.76/21.92 tff(c_12862, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_48), true, iext(Q_48, uri_rdfs_Container, uri_rdfs_Resource), true)=true))). % 32.76/21.92 tff(c_12262, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_48), true, iext(Q_48, uri_rdfs_isDefinedBy, uri_rdfs_isDefinedBy), true)=true))). % 32.76/21.92 tff(c_2706, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdfs_domain), true, ifeq(iext(P_108, uri_rdf__2, uri_rdfs_Resource), true, true, true), true)=true))). % 32.76/21.92 tff(c_5109, plain, (![E_41]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Resource, E_41), true, iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, E_41), true)=true))). % 32.76/21.92 tff(c_28931, plain, (![D_571]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_571), true, icext(D_571, uri_rdf_type), true)=true))). % 32.76/21.92 tff(c_6882, plain, (![E_41]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Resource, E_41), true, iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, E_41), true)=true))). % 32.76/21.92 tff(c_10407, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, uri_rdfs_isDefinedBy, uri_rdf_Property), true)=true))). % 32.76/21.92 tff(c_4852, plain, (![Q_48, X_141]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, X_141, uri_rdfs_Resource), true)=true))). % 32.76/21.92 tff(c_2829, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdfs_range), true, ifeq(iext(P_108, uri_rdfs_comment, uri_rdfs_Literal), true, true, true), true)=true))). % 32.76/21.92 tff(c_3007, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_109), true, iext(Q_109, uri_rdfs_member, uri_rdfs_Resource), true)=true))). % 32.76/21.92 tff(c_3004, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_109), true, iext(Q_109, uri_rdfs_member, uri_rdfs_Resource), true)=true))). % 32.76/21.92 tff(c_3021, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_109), true, iext(Q_109, uri_rdfs_range, uri_rdfs_Class), true)=true))). % 32.76/21.92 tff(c_2970, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_109), true, iext(Q_109, uri_rdf_first, uri_rdfs_Resource), true)=true))). % 32.76/21.92 tff(c_2980, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_109), true, iext(Q_109, uri_rdf__3, uri_rdf_Property), true)=true))). % 32.76/21.92 tff(c_3022, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_109), true, iext(Q_109, uri_rdf_first, uri_rdf_Property), true)=true))). % 32.76/21.92 tff(c_2993, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_109), true, iext(Q_109, uri_rdfs_seeAlso, uri_rdfs_Resource), true)=true))). % 32.76/21.92 tff(c_2513, plain, (![E_106]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Container, E_106), true, iext(uri_rdfs_subClassOf, uri_rdfs_Seq, E_106), true)=true))). % 32.76/21.92 tff(c_2979, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_109), true, iext(Q_109, uri_ex_s, sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z), true)=true))). % 32.76/21.92 tff(c_2974, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_109), true, iext(Q_109, uri_rdf_XMLLiteral, uri_rdfs_Literal), true)=true))). % 32.76/21.92 tff(c_3018, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_109), true, iext(Q_109, uri_rdf_predicate, uri_rdfs_Statement), true)=true))). % 32.76/21.92 tff(c_3023, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_109), true, iext(Q_109, uri_rdf_subject, uri_rdf_Property), true)=true))). % 32.76/21.92 tff(c_28283, plain, (![D_552]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, D_552), true, icext(D_552, uri_rdf__3), true)=true))). % 32.76/21.92 tff(c_3016, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_109), true, iext(Q_109, uri_rdfs_isDefinedBy, uri_rdfs_Resource), true)=true))). % 32.76/21.92 tff(c_3009, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_109), true, iext(Q_109, uri_rdfs_isDefinedBy, uri_rdfs_Resource), true)=true))). % 32.76/21.92 tff(c_2515, plain, (![E_106]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Container, E_106), true, iext(uri_rdfs_subClassOf, uri_rdf_Bag, E_106), true)=true))). % 32.76/21.92 tff(c_3008, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_109), true, iext(Q_109, uri_rdfs_comment, uri_rdfs_Literal), true)=true))). % 32.76/21.92 tff(c_2977, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_109), true, iext(Q_109, uri_rdfs_Datatype, uri_rdfs_Class), true)=true))). % 32.76/21.92 tff(c_2975, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_109), true, iext(Q_109, uri_rdfs_subPropertyOf, uri_rdf_Property), true)=true))). % 32.76/21.92 tff(c_3014, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_109), true, iext(Q_109, uri_rdf_type, uri_rdfs_Resource), true)=true))). % 32.76/21.92 tff(c_28065, plain, (![D_543]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_543), true, icext(D_543, uri_rdf_first), true)=true))). % 32.76/21.92 tff(c_3015, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_109), true, iext(Q_109, uri_rdfs_ContainerMembershipProperty, uri_rdf_Property), true)=true))). % 32.76/21.92 tff(c_2516, plain, (![E_106]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, E_106), true, iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, E_106), true)=true))). % 32.76/21.92 tff(c_3020, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_109), true, iext(Q_109, uri_rdf_first, uri_rdf_List), true)=true))). % 32.76/21.92 tff(c_3002, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_109), true, iext(Q_109, uri_rdfs_subPropertyOf, uri_rdf_Property), true)=true))). % 32.76/21.92 tff(c_2997, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_109), true, iext(Q_109, uri_ex_c, uri_owl_Class), true)=true))). % 32.76/21.92 tff(c_3024, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_109), true, iext(Q_109, uri_rdfs_subClassOf, uri_rdfs_Class), true)=true))). % 32.76/21.92 tff(c_2982, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_109), true, iext(Q_109, uri_rdf__1, uri_rdfs_ContainerMembershipProperty), true)=true))). % 32.76/21.92 tff(c_27870, plain, (![D_534]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_534), true, icext(D_534, uri_rdf_object), true)=true))). % 32.76/21.92 tff(c_3029, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_109), true, iext(Q_109, uri_rdf_value, uri_rdfs_Resource), true)=true))). % 32.76/21.92 tff(c_2990, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_109), true, iext(Q_109, uri_rdfs_isDefinedBy, uri_rdfs_seeAlso), true)=true))). % 32.76/21.92 tff(c_2972, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_109), true, iext(Q_109, uri_rdf_XMLLiteral, uri_rdfs_Datatype), true)=true))). % 32.76/21.92 tff(c_3000, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_109), true, iext(Q_109, uri_rdf_subject, uri_rdfs_Resource), true)=true))). % 32.76/21.92 tff(c_2514, plain, (![E_106]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Container, E_106), true, iext(uri_rdfs_subClassOf, uri_rdf_Alt, E_106), true)=true))). % 32.76/21.92 tff(c_3006, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_109), true, iext(Q_109, sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z, uri_owl_Restriction), true)=true))). % 32.76/21.92 tff(c_2512, plain, (![E_106]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, E_106), true, iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, E_106), true)=true))). % 32.76/21.92 tff(c_3005, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_109), true, iext(Q_109, uri_rdf_Alt, uri_rdfs_Container), true)=true))). % 32.76/21.92 tff(c_2414, plain, (![R_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_seeAlso, R_103), true, iext(uri_rdfs_subPropertyOf, uri_rdfs_isDefinedBy, R_103), true)=true))). % 32.76/21.92 tff(c_3013, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_109), true, iext(Q_109, uri_rdfs_domain, uri_rdfs_Class), true)=true))). % 32.76/21.92 tff(c_2967, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_109), true, iext(Q_109, uri_rdfs_label, uri_rdfs_Resource), true)=true))). % 32.76/21.92 tff(c_2991, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_owl_someValuesFrom, Q_109), true, iext(Q_109, sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z, uri_ex_c), true)=true))). % 32.76/21.92 tff(c_3019, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_109), true, iext(Q_109, uri_rdf_subject, uri_rdfs_Statement), true)=true))). % 32.76/21.92 tff(c_3028, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_109), true, iext(Q_109, uri_rdfs_range, uri_rdf_Property), true)=true))). % 32.76/21.92 tff(c_2978, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_109), true, iext(Q_109, uri_rdf_Property, uri_rdfs_Class), true)=true))). % 32.76/21.92 tff(c_3017, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_109), true, iext(Q_109, uri_rdf__2, uri_rdf_Property), true)=true))). % 32.76/21.92 tff(c_27504, plain, (![D_516]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_516), true, icext(D_516, uri_rdf__2), true)=true))). % 32.96/21.92 tff(c_3030, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_109), true, iext(Q_109, uri_ex_p, uri_owl_ObjectProperty), true)=true))). % 32.96/21.92 tff(c_2511, plain, (![E_106]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Literal, E_106), true, iext(uri_rdfs_subClassOf, uri_rdf_XMLLiteral, E_106), true)=true))). % 32.96/21.92 tff(c_3025, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_109), true, iext(Q_109, uri_rdf_object, uri_rdfs_Statement), true)=true))). % 32.96/21.92 tff(c_2988, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_109), true, iext(Q_109, uri_rdf__2, uri_rdfs_Resource), true)=true))). % 32.96/21.92 tff(c_2973, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_109), true, iext(Q_109, uri_rdfs_subClassOf, uri_rdfs_Class), true)=true))). % 32.96/21.92 tff(c_3001, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_109), true, iext(Q_109, uri_rdfs_domain, uri_rdf_Property), true)=true))). % 32.96/21.92 tff(c_2989, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_109), true, iext(Q_109, uri_rdfs_seeAlso, uri_rdfs_Resource), true)=true))). % 32.96/21.92 tff(c_16136, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_predicate), true)=true))). % 32.96/21.92 tff(c_16046, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_label), true)=true))). % 32.96/21.92 tff(c_16047, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_label), true)=true))). % 32.96/21.92 tff(c_16137, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_predicate), true)=true))). % 32.96/21.92 tff(c_2992, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_109), true, iext(Q_109, uri_rdfs_comment, uri_rdfs_Resource), true)=true))). % 32.96/21.92 tff(c_18680, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_comment), true)=true))). % 32.96/21.92 tff(c_18681, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_comment), true)=true))). % 32.96/21.92 tff(c_27112, plain, (![D_500]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_500), true, icext(D_500, uri_rdf_value), true)=true))). % 32.96/21.92 tff(c_15980, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_member), true)=true))). % 32.96/21.92 tff(c_15884, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdfs_Resource), true)=true))). % 32.96/21.92 tff(c_3027, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_109), true, iext(Q_109, uri_rdf_rest, uri_rdf_List), true)=true))). % 32.96/21.92 tff(c_26973, plain, (![D_495]: (ifeq(iext(uri_rdfs_subClassOf, uri_owl_ObjectProperty, D_495), true, icext(D_495, uri_ex_p), true)=true))). % 32.96/21.92 tff(c_2999, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_109), true, iext(Q_109, uri_rdf__3, uri_rdfs_Resource), true)=true))). % 32.96/21.92 tff(c_15035, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdfs_Statement), true)=true))). % 32.96/21.92 tff(c_14856, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_owl_Class), true)=true))). % 32.96/21.92 tff(c_26829, plain, (![D_490]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_List, D_490), true, icext(D_490, uri_rdf_nil), true)=true))). % 32.96/21.92 tff(c_20130, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z), true)=true))). % 32.96/21.92 tff(c_15585, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_owl_ObjectProperty), true)=true))). % 32.96/21.92 tff(c_3012, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_109), true, iext(Q_109, uri_rdf_value, uri_rdfs_Resource), true)=true))). % 32.96/21.92 tff(c_14679, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdfs_Statement), true)=true))). % 32.96/21.92 tff(c_15131, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_owl_Restriction), true)=true))). % 32.96/21.92 tff(c_15130, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_owl_Restriction), true)=true))). % 32.96/21.92 tff(c_14587, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_owl_Class), true)=true))). % 32.96/21.92 tff(c_15586, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_owl_ObjectProperty), true)=true))). % 32.96/21.92 tff(c_3026, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_109), true, iext(Q_109, uri_rdf_rest, uri_rdf_List), true)=true))). % 32.96/21.92 tff(c_20034, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z), true)=true))). % 32.96/21.92 tff(c_26505, plain, (![D_478]: (ifeq(iext(uri_rdfs_subClassOf, uri_owl_Class, D_478), true, icext(D_478, uri_ex_c), true)=true))). % 32.96/21.92 tff(c_2996, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_109), true, iext(Q_109, uri_rdf__2, uri_rdfs_ContainerMembershipProperty), true)=true))). % 32.96/21.92 tff(c_16761, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdf_List), true)=true))). % 32.96/21.92 tff(c_16853, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdf_List), true)=true))). % 32.96/21.92 tff(c_2994, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_109), true, iext(Q_109, uri_rdf__1, uri_rdfs_Resource), true)=true))). % 32.96/21.92 tff(c_3011, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_109), true, iext(Q_109, uri_rdf_Bag, uri_rdfs_Container), true)=true))). % 32.96/21.92 tff(c_25926, plain, (![D_469, X_470]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Resource, D_469), true, icext(D_469, X_470), true)=true))). % 32.96/21.93 tff(c_2981, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_109), true, iext(Q_109, uri_rdf_type, uri_rdf_Property), true)=true))). % 32.96/21.93 tff(c_6053, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_subject), true)=true))). % 32.96/21.93 tff(c_8968, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_subPropertyOf), true)=true))). % 32.96/21.93 tff(c_25641, plain, (![C_91, X_63]: (ifeq(icext(C_91, X_63), true, true, true)=true))). % 32.96/21.93 tff(c_10477, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf__1), true)=true))). % 32.96/21.93 tff(c_10329, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_range), true)=true))). % 32.96/21.93 tff(c_3010, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_109), true, iext(Q_109, uri_rdf_type, uri_rdfs_Class), true)=true))). % 32.96/21.93 tff(c_8850, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdfs_Class), true)=true))). % 32.96/21.93 tff(c_25185, plain, (![X_456, Y_457]: (ifeq(iext(uri_rdfs_range, X_456, Y_457), true, icext(uri_rdf_Property, X_456), true)=true))). % 32.96/21.93 tff(c_10330, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_range), true)=true))). % 32.96/21.93 tff(c_2968, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_owl_onProperty, Q_109), true, iext(Q_109, sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z, uri_ex_p), true)=true))). % 32.96/21.93 tff(c_24752, plain, (![X_450, Y_451]: (ifeq(iext(uri_rdfs_domain, X_450, Y_451), true, icext(uri_rdf_Property, X_450), true)=true))). % 32.96/21.93 tff(c_2986, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_109), true, iext(Q_109, uri_rdf__1, uri_rdf_Property), true)=true))). % 32.96/21.93 tff(c_13336, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_first), true)=true))). % 32.96/21.93 tff(c_24675, plain, (![X_444, Y_445]: (ifeq(iext(uri_rdfs_comment, X_444, Y_445), true, icext(uri_rdfs_Literal, Y_445), true)=true))). % 32.96/21.93 tff(c_7707, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_owl_someValuesFrom), true)=true))). % 32.96/21.93 tff(c_9031, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_owl_onProperty), true)=true))). % 32.96/21.93 tff(c_2971, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_109), true, iext(Q_109, uri_rdf_nil, uri_rdf_List), true)=true))). % 32.96/21.93 tff(c_6313, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_value), true)=true))). % 32.96/21.93 tff(c_24018, plain, (![X_436, Y_437]: (ifeq(iext(uri_rdf_type, X_436, Y_437), true, icext(uri_rdfs_Class, Y_437), true)=true))). % 32.96/21.93 tff(c_6124, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_rest), true)=true))). % 32.96/21.93 tff(c_8782, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_type), true)=true))). % 32.96/21.93 tff(c_2998, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_109), true, iext(Q_109, uri_rdfs_label, uri_rdfs_Literal), true)=true))). % 32.96/21.93 tff(c_9032, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_owl_onProperty), true)=true))). % 32.96/21.93 tff(c_23873, plain, (![X_428, Y_429]: (ifeq(iext(uri_rdf_rest, X_428, Y_429), true, icext(uri_rdf_List, X_428), true)=true))). % 32.96/21.93 tff(c_10938, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdfs_Datatype), true)=true))). % 32.96/21.93 tff(c_12799, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_subClassOf), true)=true))). % 32.96/21.93 tff(c_2985, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_109), true, iext(Q_109, uri_rdf_object, uri_rdf_Property), true)=true))). % 32.96/21.93 tff(c_23023, plain, (![X_420, Y_421]: (ifeq(iext(uri_rdfs_subClassOf, X_420, Y_421), true, icext(uri_rdfs_Class, X_420), true)=true))). % 32.96/21.93 tff(c_2969, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_109), true, iext(Q_109, uri_rdf__3, uri_rdfs_ContainerMembershipProperty), true)=true))). % 32.96/21.93 tff(c_6218, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdfs_Literal), true)=true))). % 32.96/21.93 tff(c_7708, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_owl_someValuesFrom), true)=true))). % 32.96/21.93 tff(c_22542, plain, (![X_413, Y_414]: (ifeq(iext(uri_rdfs_subPropertyOf, X_413, Y_414), true, icext(uri_rdf_Property, Y_414), true)=true))). % 32.96/21.93 tff(c_5026, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdf_Alt), true)=true))). % 32.96/21.93 tff(c_12415, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdf_Property), true)=true))). % 32.96/21.93 tff(c_2995, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_109), true, iext(Q_109, uri_rdf_value, uri_rdf_Property), true)=true))). % 32.96/21.93 tff(c_6520, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf__2), true)=true))). % 32.96/21.93 tff(c_12800, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_subClassOf), true)=true))). % 32.96/21.93 tff(c_21796, plain, (![X_403, Y_404]: (ifeq(iext(uri_rdfs_subClassOf, X_403, Y_404), true, icext(uri_rdfs_Class, Y_404), true)=true))). % 32.96/21.93 tff(c_13267, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf__1), true)=true))). % 32.96/21.93 tff(c_11647, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_object), true)=true))). % 32.96/21.93 tff(c_2984, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_109), true, iext(Q_109, uri_rdf_predicate, uri_rdfs_Resource), true)=true))). % 32.96/21.93 tff(c_11153, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdf_XMLLiteral), true)=true))). % 32.96/21.93 tff(c_12866, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdfs_Container), true)=true))). % 32.96/21.93 tff(c_21634, plain, (![X_394, Y_395]: (ifeq(iext(uri_rdf_subject, X_394, Y_395), true, icext(uri_rdfs_Statement, X_394), true)=true))). % 32.96/21.93 tff(c_9266, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_seeAlso), true)=true))). % 32.96/21.93 tff(c_8967, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_subPropertyOf), true)=true))). % 32.96/21.93 tff(c_2966, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_109), true, iext(Q_109, uri_rdf__3, uri_rdfs_Resource), true)=true))). % 32.96/21.93 tff(c_12265, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_isDefinedBy), true)=true))). % 32.96/21.93 tff(c_8147, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_domain), true)=true))). % 32.96/21.93 tff(c_13335, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_first), true)=true))). % 32.96/21.93 tff(c_21120, plain, (![X_384, Y_385]: (ifeq(iext(uri_rdfs_range, X_384, Y_385), true, icext(uri_rdfs_Class, Y_385), true)=true))). % 32.96/21.93 tff(c_6052, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_subject), true)=true))). % 32.96/21.93 tff(c_8148, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_domain), true)=true))). % 32.96/21.93 tff(c_3003, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_109), true, iext(Q_109, uri_rdf__1, uri_rdfs_Resource), true)=true))). % 32.96/21.93 tff(c_6625, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf__3), true)=true))). % 32.96/21.93 tff(c_6519, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf__2), true)=true))). % 32.96/21.93 tff(c_20954, plain, (![X_375, Y_376]: (ifeq(iext(uri_rdf_predicate, X_375, Y_376), true, icext(uri_rdfs_Statement, X_375), true)=true))). % 32.96/21.93 tff(c_5774, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdfs_Resource), true)=true))). % 32.96/21.93 tff(c_6123, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_rest), true)=true))). % 32.96/21.93 tff(c_6314, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_value), true)=true))). % 32.96/21.93 tff(c_2987, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_109), true, iext(Q_109, uri_rdf__2, uri_rdfs_Resource), true)=true))). % 32.96/21.93 tff(c_6624, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf__3), true)=true))). % 32.96/21.93 tff(c_20784, plain, (![X_366, Y_367]: (ifeq(iext(uri_rdf_first, X_366, Y_367), true, icext(uri_rdf_List, X_366), true)=true))). % 32.96/21.93 tff(c_11646, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_object), true)=true))). % 32.96/21.93 tff(c_5341, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdfs_Seq), true)=true))). % 32.96/21.93 tff(c_2983, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_109), true, iext(Q_109, uri_rdfs_Seq, uri_rdfs_Container), true)=true))). % 32.96/21.93 tff(c_7024, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_member), true)=true))). % 32.96/21.93 tff(c_12729, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdf_Bag), true)=true))). % 32.96/21.93 tff(c_20635, plain, (![X_357, Y_358]: (ifeq(iext(uri_rdf_object, X_357, Y_358), true, icext(uri_rdfs_Statement, X_357), true)=true))). % 32.96/21.93 tff(c_8783, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_type), true)=true))). % 32.96/21.93 tff(c_5421, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdfs_ContainerMembershipProperty), true)=true))). % 32.96/21.93 tff(c_2976, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_109), true, iext(Q_109, uri_rdf_rest, uri_rdf_Property), true)=true))). % 32.96/21.93 tff(c_4853, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_29), true, icext(C_29, uri_rdfs_Resource), true)=true))). % 32.96/21.93 tff(c_4854, plain, (![C_19, X_141]: (ifeq(iext(uri_rdfs_domain, uri_rdf_type, C_19), true, icext(C_19, X_141), true)=true))). % 32.96/21.93 tff(c_20036, plain, (![X_33]: (ifeq(icext(sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z, X_33), true, icext(sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z, X_33), true)=true))). % 32.96/21.93 tff(c_20046, plain, (iext(uri_rdfs_subClassOf, sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z, uri_rdfs_Resource)=true)). % 32.96/21.93 tff(c_1974, plain, (![C_95]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_95), true, icext(C_95, uri_rdf__3), true)=true))). % 32.96/21.93 tff(c_19980, plain, (iext(uri_rdfs_subClassOf, sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z, sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z)=true)). % 32.96/21.93 tff(c_19933, plain, (iext(uri_rdf_type, sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z, uri_rdfs_Class)=true)). % 32.96/21.93 tff(c_2328, plain, (![C_99]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_99), true, icext(C_99, uri_rdfs_Class), true)=true))). % 32.96/21.93 tff(c_19730, plain, (ic(sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z)=true)). % 32.96/21.93 tff(c_19648, plain, (icext(uri_rdfs_Class, sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z)=true)). % 32.96/21.93 tff(c_2330, plain, (![C_99]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_99), true, icext(C_99, sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z), true)=true))). % 32.96/21.93 tff(c_2026, plain, (![C_95]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_95), true, icext(C_95, uri_rdf_type), true)=true))). % 32.96/21.93 tff(c_2000, plain, (![C_95]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_95), true, icext(C_95, uri_rdfs_isDefinedBy), true)=true))). % 32.96/21.93 tff(c_2039, plain, (![C_95]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_95), true, icext(C_95, uri_rdfs_range), true)=true))). % 32.96/21.93 tff(c_1983, plain, (![C_95]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_95), true, icext(C_95, uri_rdf_XMLLiteral), true)=true))). % 32.96/21.93 tff(c_2005, plain, (![C_95]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_95), true, icext(C_95, uri_rdfs_seeAlso), true)=true))). % 32.96/21.93 tff(c_19122, plain, (![X_332, Y_333]: (ifeq(iext(uri_rdfs_subPropertyOf, X_332, Y_333), true, icext(uri_rdf_Property, X_332), true)=true))). % 32.96/21.93 tff(c_1982, plain, (![C_95]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_95), true, icext(C_95, uri_rdfs_subClassOf), true)=true))). % 32.96/21.93 tff(c_2027, plain, (![C_95]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_95), true, icext(C_95, uri_rdf_Bag), true)=true))). % 32.96/21.93 tff(c_2046, plain, (![C_95]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_95), true, icext(C_95, uri_rdfs_range), true)=true))). % 32.96/21.93 tff(c_2016, plain, (![C_95]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_95), true, icext(C_95, uri_rdfs_subPropertyOf), true)=true))). % 32.96/21.93 tff(c_1996, plain, (![C_95]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_95), true, icext(C_95, uri_rdf__2), true)=true))). % 32.96/21.93 tff(c_2325, plain, (![C_99]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_99), true, icext(C_99, uri_rdfs_Literal), true)=true))). % 32.96/21.93 tff(c_1998, plain, (![C_95]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_95), true, icext(C_95, uri_rdf__2), true)=true))). % 32.96/21.93 tff(c_2003, plain, (![C_95]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_95), true, icext(C_95, uri_rdfs_comment), true)=true))). % 32.96/21.93 tff(c_2025, plain, (![C_95]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_95), true, icext(C_95, uri_rdfs_isDefinedBy), true)=true))). % 32.96/21.93 tff(c_18258, plain, (![X_314, Y_315]: (ifeq(iext(uri_rdf_rest, X_314, Y_315), true, icext(uri_rdf_List, Y_315), true)=true))). % 32.96/21.93 tff(c_18626, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_comment, uri_rdfs_comment)=true)). % 32.96/21.93 tff(c_18583, plain, (ip(uri_rdfs_comment)=true)). % 32.96/21.93 tff(c_18526, plain, (iext(uri_rdf_type, uri_rdfs_comment, uri_rdf_Property)=true)). % 32.96/21.93 tff(c_2385, plain, (![C_99]: (ifeq(iext(uri_rdfs_range, uri_rdfs_range, C_99), true, icext(C_99, uri_rdf_List), true)=true))). % 32.96/21.93 tff(c_18311, plain, (icext(uri_rdf_Property, uri_rdfs_comment)=true)). % 32.96/21.93 tff(c_2023, plain, (![C_95]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_95), true, icext(C_95, uri_rdfs_comment), true)=true))). % 32.96/21.93 tff(c_2322, plain, (![C_99]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_99), true, icext(C_99, uri_rdf_List), true)=true))). % 32.96/21.93 tff(c_2323, plain, (![C_99]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_99), true, icext(C_99, uri_rdfs_Datatype), true)=true))). % 32.96/21.93 tff(c_1993, plain, (![C_95]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_95), true, icext(C_95, uri_rdf_predicate), true)=true))). % 32.96/21.93 tff(c_2345, plain, (![C_99]: (ifeq(iext(uri_rdfs_range, uri_owl_someValuesFrom, C_99), true, icext(C_99, uri_ex_c), true)=true))). % 32.96/21.93 tff(c_1977, plain, (![C_95]: (ifeq(iext(uri_rdfs_domain, uri_owl_onProperty, C_95), true, icext(C_95, sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z), true)=true))). % 32.96/21.93 tff(c_2033, plain, (![C_95]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_95), true, icext(C_95, uri_rdfs_ContainerMembershipProperty), true)=true))). % 32.96/21.93 tff(c_2037, plain, (![C_95]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_95), true, icext(C_95, uri_rdf_subject), true)=true))). % 32.96/21.93 tff(c_2020, plain, (![C_95]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_95), true, icext(C_95, uri_rdf_Alt), true)=true))). % 32.96/21.93 tff(c_1984, plain, (![C_95]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_95), true, icext(C_95, uri_rdfs_subPropertyOf), true)=true))). % 32.96/21.93 tff(c_2324, plain, (![C_99]: (ifeq(iext(uri_rdfs_range, uri_rdfs_domain, C_99), true, icext(C_99, uri_rdfs_Class), true)=true))). % 32.96/21.93 tff(c_2007, plain, (![C_95]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_95), true, icext(C_95, uri_rdf__1), true)=true))). % 32.96/21.93 tff(c_17700, plain, (![X_289, Y_290]: (ifeq(iext(uri_rdfs_label, X_289, Y_290), true, icext(uri_rdfs_Literal, Y_290), true)=true))). % 32.96/21.93 tff(c_2318, plain, (![C_99]: (ifeq(iext(uri_rdfs_range, uri_owl_onProperty, C_99), true, icext(C_99, uri_ex_p), true)=true))). % 32.96/21.93 tff(c_2014, plain, (![C_95]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_95), true, icext(C_95, uri_rdf_subject), true)=true))). % 32.96/21.93 tff(c_2378, plain, (![C_99]: (ifeq(iext(uri_rdfs_range, uri_rdfs_domain, C_99), true, icext(C_99, uri_rdf_List), true)=true))). % 32.96/21.93 tff(c_1986, plain, (![C_95]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_95), true, icext(C_95, uri_rdfs_Datatype), true)=true))). % 32.96/21.93 tff(c_2344, plain, (![C_99]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_99), true, icext(C_99, uri_rdfs_seeAlso), true)=true))). % 32.96/21.93 tff(c_2370, plain, (![C_99]: (ifeq(iext(uri_rdfs_range, uri_rdfs_range, C_99), true, icext(C_99, uri_rdfs_Class), true)=true))). % 32.96/21.93 tff(c_2365, plain, (![C_99]: (ifeq(iext(uri_rdfs_range, uri_rdfs_range, C_99), true, icext(C_99, uri_rdfs_Literal), true)=true))). % 32.96/21.93 tff(c_2019, plain, (![C_95]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_95), true, icext(C_95, uri_rdfs_member), true)=true))). % 32.96/21.93 tff(c_1976, plain, (![C_95]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_95), true, icext(C_95, uri_rdfs_label), true)=true))). % 32.96/21.93 tff(c_14589, plain, (![X_33]: (ifeq(icext(uri_owl_Class, X_33), true, icext(uri_owl_Class, X_33), true)=true))). % 32.96/21.93 tff(c_15587, plain, (![X_33]: (ifeq(icext(uri_owl_ObjectProperty, X_33), true, icext(uri_owl_ObjectProperty, X_33), true)=true))). % 32.96/21.93 tff(c_15037, plain, (![X_33]: (ifeq(icext(uri_rdfs_Statement, X_33), true, icext(uri_rdfs_Statement, X_33), true)=true))). % 32.96/21.93 tff(c_15132, plain, (![X_33]: (ifeq(icext(uri_owl_Restriction, X_33), true, icext(uri_owl_Restriction, X_33), true)=true))). % 32.96/21.93 tff(c_1999, plain, (![C_95]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_95), true, icext(C_95, uri_rdfs_seeAlso), true)=true))). % 32.96/21.93 tff(c_16763, plain, (![X_33]: (ifeq(icext(uri_rdf_List, X_33), true, icext(uri_rdf_List, X_33), true)=true))). % 32.96/21.93 tff(c_11155, plain, (![X_33]: (ifeq(icext(uri_rdf_XMLLiteral, X_33), true, icext(uri_rdf_XMLLiteral, X_33), true)=true))). % 32.96/21.93 tff(c_12416, plain, (![X_33]: (ifeq(icext(uri_rdf_Property, X_33), true, icext(uri_rdf_Property, X_33), true)=true))). % 32.96/21.93 tff(c_8851, plain, (![X_33]: (ifeq(icext(uri_rdfs_Class, X_33), true, icext(uri_rdfs_Class, X_33), true)=true))). % 32.96/21.93 tff(c_5423, plain, (![X_33]: (ifeq(icext(uri_rdfs_ContainerMembershipProperty, X_33), true, icext(uri_rdfs_ContainerMembershipProperty, X_33), true)=true))). % 32.96/21.93 tff(c_16321, plain, (![X_267, Y_268]: (ifeq(iext(uri_rdfs_domain, X_267, Y_268), true, icext(uri_rdfs_Class, Y_268), true)=true))). % 32.96/21.93 tff(c_16773, plain, (iext(uri_rdfs_subClassOf, uri_rdf_List, uri_rdfs_Resource)=true)). % 32.96/21.93 tff(c_2042, plain, (![C_95]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_95), true, icext(C_95, uri_rdfs_subClassOf), true)=true))). % 32.96/21.93 tff(c_16707, plain, (iext(uri_rdfs_subClassOf, uri_rdf_List, uri_rdf_List)=true)). % 32.96/21.93 tff(c_16660, plain, (iext(uri_rdf_type, uri_rdf_List, uri_rdfs_Class)=true)). % 32.96/21.93 tff(c_16464, plain, (ic(uri_rdf_List)=true)). % 32.96/21.93 tff(c_16411, plain, (icext(uri_rdfs_Class, uri_rdf_List)=true)). % 32.96/21.93 tff(c_10940, plain, (![X_33]: (ifeq(icext(uri_rdfs_Datatype, X_33), true, icext(uri_rdfs_Datatype, X_33), true)=true))). % 32.96/21.93 tff(c_5343, plain, (![X_33]: (ifeq(icext(uri_rdfs_Seq, X_33), true, icext(uri_rdfs_Seq, X_33), true)=true))). % 32.96/21.93 tff(c_5964, plain, (![X_33]: (ifeq(icext(uri_rdfs_Literal, X_33), true, icext(uri_rdfs_Literal, X_33), true)=true))). % 32.96/21.93 tff(c_2030, plain, (![C_95]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_95), true, icext(C_95, uri_rdfs_domain), true)=true))). % 32.96/21.93 tff(c_4929, plain, (![X_33]: (ifeq(icext(uri_rdfs_Container, X_33), true, icext(uri_rdfs_Container, X_33), true)=true))). % 32.96/21.93 tff(c_5028, plain, (![X_33]: (ifeq(icext(uri_rdf_Alt, X_33), true, icext(uri_rdf_Alt, X_33), true)=true))). % 32.96/21.93 tff(c_12731, plain, (![X_33]: (ifeq(icext(uri_rdf_Bag, X_33), true, icext(uri_rdf_Bag, X_33), true)=true))). % 32.96/21.94 tff(c_16147, plain, (iext(uri_rdf_type, uri_rdfs_Resource, uri_rdfs_Class)=true)). % 32.96/21.94 tff(c_16082, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_predicate, uri_rdf_predicate)=true)). % 32.96/21.94 tff(c_1992, plain, (![C_95]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_95), true, icext(C_95, uri_rdfs_Seq), true)=true))). % 32.96/21.94 tff(c_15992, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_label, uri_rdfs_label)=true)). % 32.96/21.94 tff(c_15922, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_member, uri_rdfs_member)=true)). % 32.96/21.94 tff(c_2022, plain, (![C_95]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_95), true, icext(C_95, uri_rdfs_member), true)=true))). % 32.96/21.94 tff(c_15826, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Resource, uri_rdfs_Resource)=true)). % 32.96/21.94 tff(c_15652, plain, (icext(uri_rdf_Property, uri_rdfs_member)=true)). % 32.96/21.94 tff(c_15597, plain, (iext(uri_rdf_type, uri_rdfs_member, uri_rdf_Property)=true)). % 32.96/21.94 tff(c_15531, plain, (iext(uri_rdfs_subClassOf, uri_owl_ObjectProperty, uri_owl_ObjectProperty)=true)). % 32.96/21.94 tff(c_15322, plain, (iext(uri_rdfs_subClassOf, uri_owl_ObjectProperty, uri_rdfs_Resource)=true)). % 32.96/21.94 tff(c_15142, plain, (iext(uri_rdfs_subClassOf, uri_owl_Restriction, uri_rdfs_Resource)=true)). % 32.96/21.94 tff(c_15076, plain, (iext(uri_rdfs_subClassOf, uri_owl_Restriction, uri_owl_Restriction)=true)). % 32.96/21.94 tff(c_2017, plain, (![C_95]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_95), true, icext(C_95, uri_rdf__1), true)=true))). % 32.96/21.94 tff(c_14981, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Statement, uri_rdfs_Statement)=true)). % 32.96/21.94 tff(c_14801, plain, (iext(uri_rdfs_subClassOf, uri_owl_Class, uri_rdfs_Resource)=true)). % 32.96/21.94 tff(c_14599, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Statement, uri_rdfs_Resource)=true)). % 32.96/21.94 tff(c_2372, plain, (![C_99]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_99), true, icext(C_99, uri_rdf_Property), true)=true))). % 32.96/21.94 tff(c_14533, plain, (iext(uri_rdfs_subClassOf, uri_owl_Class, uri_owl_Class)=true)). % 32.96/21.94 tff(c_14486, plain, (iext(uri_rdf_type, uri_rdf_XMLLiteral, uri_rdfs_Class)=true)). % 32.96/21.94 tff(c_14414, plain, (iext(uri_rdf_type, uri_owl_ObjectProperty, uri_rdfs_Class)=true)). % 32.96/21.94 tff(c_2047, plain, (![C_95]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_95), true, icext(C_95, uri_rdf_value), true)=true))). % 32.96/21.94 tff(c_14279, plain, (ic(uri_owl_ObjectProperty)=true)). % 32.96/21.94 tff(c_14221, plain, (icext(uri_rdfs_Class, uri_owl_ObjectProperty)=true)). % 32.96/21.94 tff(c_2389, plain, (![C_99]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_99), true, icext(C_99, uri_owl_ObjectProperty), true)=true))). % 32.96/21.94 tff(c_14154, plain, (iext(uri_rdf_type, uri_rdfs_Seq, uri_rdfs_Class)=true)). % 32.96/21.94 tff(c_2361, plain, (![C_99]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_99), true, icext(C_99, uri_rdfs_Container), true)=true))). % 32.96/21.94 tff(c_14075, plain, (iext(uri_rdf_type, uri_rdf_Alt, uri_rdfs_Class)=true)). % 32.96/21.94 tff(c_14028, plain, (iext(uri_rdf_type, uri_rdfs_Container, uri_rdfs_Class)=true)). % 32.96/21.94 tff(c_13956, plain, (iext(uri_rdf_type, uri_rdf_Bag, uri_rdfs_Class)=true)). % 32.96/21.94 tff(c_2044, plain, (![C_95]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_95), true, icext(C_95, uri_rdf_rest), true)=true))). % 32.96/21.94 tff(c_13909, plain, (iext(uri_rdf_type, uri_rdfs_Datatype, uri_rdfs_Class)=true)). % 32.96/21.94 tff(c_13862, plain, (iext(uri_rdf_type, uri_rdfs_Class, uri_rdfs_Class)=true)). % 32.96/21.94 tff(c_13786, plain, (iext(uri_rdf_type, uri_rdfs_ContainerMembershipProperty, uri_rdfs_Class)=true)). % 32.96/21.94 tff(c_13739, plain, (iext(uri_rdf_type, uri_rdfs_Literal, uri_rdfs_Class)=true)). % 32.96/21.94 tff(c_13686, plain, (iext(uri_rdf_type, uri_owl_Class, uri_rdfs_Class)=true)). % 32.96/21.94 tff(c_13644, plain, (ip(uri_rdfs_label)=true)). % 32.96/21.94 tff(c_13566, plain, (iext(uri_rdf_type, uri_rdfs_label, uri_rdf_Property)=true)). % 32.96/21.94 tff(c_2001, plain, (![C_95]: (ifeq(iext(uri_rdfs_domain, uri_owl_someValuesFrom, C_95), true, icext(C_95, sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z), true)=true))). % 32.96/21.94 tff(c_13518, plain, (iext(uri_rdf_type, uri_rdfs_Statement, uri_rdfs_Class)=true)). % 32.96/21.94 tff(c_13476, plain, (ip(uri_rdf_predicate)=true)). % 32.96/21.94 tff(c_2045, plain, (![C_95]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_95), true, icext(C_95, uri_rdf_rest), true)=true))). % 32.96/21.94 tff(c_13394, plain, (iext(uri_rdf_type, uri_rdf_predicate, uri_rdf_Property)=true)). % 32.96/21.94 tff(c_13347, plain, (iext(uri_rdf_type, uri_owl_Restriction, uri_rdfs_Class)=true)). % 32.96/21.94 tff(c_13280, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_first, uri_rdf_first)=true)). % 32.96/21.94 tff(c_13212, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf__1, uri_rdfs_member)=true)). % 32.96/21.94 tff(c_1219, plain, (![S_5, O_6]: (ifeq(iext(uri_rdfs_domain, S_5, O_6), true, true, true)=true))). % 32.96/21.94 tff(c_1187, plain, (![S_5, O_6]: (ifeq(iext(uri_rdfs_subPropertyOf, S_5, O_6), true, true, true)=true))). % 32.96/21.94 tff(c_12991, plain, (iext(uri_rdf_type, uri_rdfs_domain, uri_rdf_Property)=true)). % 32.96/21.94 tff(c_3225, plain, (![S_5, O_6]: (ifeq(iext(uri_owl_someValuesFrom, S_5, O_6), true, true, true)=true))). % 32.96/21.94 tff(c_12811, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Container, uri_rdfs_Resource)=true)). % 32.96/21.94 tff(c_12742, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, uri_rdfs_subClassOf)=true)). % 32.96/21.94 tff(c_12674, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Bag, uri_rdf_Bag)=true)). % 32.96/21.94 tff(c_823, plain, (![S_76, O_77]: (ifeq(iext(uri_rdf_rest, S_76, O_77), true, true, true)=true))). % 32.96/21.94 tff(c_12360, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Property, uri_rdf_Property)=true)). % 32.96/21.94 tff(c_1344, plain, (![S_5, O_6]: (ifeq(iext(uri_rdfs_range, S_5, O_6), true, true, true)=true))). % 32.96/21.94 tff(c_12211, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_isDefinedBy, uri_rdfs_isDefinedBy)=true)). % 32.96/21.94 tff(c_2357, plain, (![C_99]: (ifeq(iext(uri_rdfs_range, uri_rdfs_range, C_99), true, icext(C_99, uri_rdf_Property), true)=true))). % 32.96/21.94 tff(c_11657, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Alt, uri_rdfs_Resource)=true)). % 32.96/21.94 tff(c_11589, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_object, uri_rdf_object)=true)). % 32.96/21.94 tff(c_11245, plain, (icext(uri_rdf_Property, uri_rdfs_subPropertyOf)=true)). % 32.96/21.94 tff(c_11191, plain, (iext(uri_rdf_type, uri_rdfs_subPropertyOf, uri_rdf_Property)=true)). % 32.96/21.94 tff(c_2038, plain, (![C_95]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_95), true, icext(C_95, uri_rdf_first), true)=true))). % 32.96/21.94 tff(c_11099, plain, (iext(uri_rdfs_subClassOf, uri_rdf_XMLLiteral, uri_rdf_XMLLiteral)=true)). % 32.96/21.94 tff(c_10969, plain, (icext(uri_rdf_Property, uri_rdf_predicate)=true)). % 32.96/21.94 tff(c_2036, plain, (![C_95]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_95), true, icext(C_95, uri_rdf_predicate), true)=true))). % 32.96/21.94 tff(c_10884, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, uri_rdfs_Datatype)=true)). % 32.96/21.94 tff(c_10822, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf__3, uri_rdfs_member)=true)). % 32.96/21.94 tff(c_1979, plain, (![C_95]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_95), true, icext(C_95, uri_rdf_first), true)=true))). % 32.96/21.94 tff(c_10420, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf__1, uri_rdf__1)=true)). % 32.96/21.94 tff(c_10365, plain, (iext(uri_rdf_type, uri_rdfs_isDefinedBy, uri_rdf_Property)=true)). % 32.96/21.94 tff(c_2326, plain, (![C_99]: (ifeq(iext(uri_rdfs_range, uri_rdfs_domain, C_99), true, icext(C_99, uri_rdf_Property), true)=true))). % 32.96/21.94 tff(c_10272, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_range, uri_rdfs_range)=true)). % 32.96/21.94 tff(c_9941, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Seq, uri_rdfs_Resource)=true)). % 32.96/21.94 tff(c_9660, plain, (icext(uri_rdf_Property, uri_owl_someValuesFrom)=true)). % 32.96/21.94 tff(c_9582, plain, (iext(uri_rdf_type, uri_owl_someValuesFrom, uri_rdf_Property)=true)). % 32.96/21.94 tff(c_9295, plain, (icext(uri_rdf_Property, uri_rdfs_isDefinedBy)=true)). % 32.96/21.94 tff(c_2034, plain, (![C_95]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_95), true, icext(C_95, uri_rdfs_isDefinedBy), true)=true))). % 32.96/21.94 tff(c_9212, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_seeAlso, uri_rdfs_seeAlso)=true)). % 32.96/21.94 tff(c_9097, plain, (icext(uri_rdf_Property, uri_rdfs_range)=true)). % 32.96/21.94 tff(c_9042, plain, (iext(uri_rdf_type, uri_rdfs_range, uri_rdf_Property)=true)). % 32.96/21.94 tff(c_8978, plain, (iext(uri_rdfs_subPropertyOf, uri_owl_onProperty, uri_owl_onProperty)=true)). % 32.96/21.94 tff(c_8917, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf)=true)). % 32.96/21.94 tff(c_8795, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Class, uri_rdfs_Class)=true)). % 32.96/21.94 tff(c_8732, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_type, uri_rdf_type)=true)). % 32.96/21.94 tff(c_8602, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Bag, uri_rdfs_Resource)=true)). % 32.96/21.94 tff(c_2333, plain, (![C_99]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_99), true, icext(C_99, uri_rdfs_ContainerMembershipProperty), true)=true))). % 32.96/21.94 tff(c_8405, plain, (icext(uri_rdf_Property, uri_owl_onProperty)=true)). % 32.96/21.94 tff(c_8351, plain, (iext(uri_rdf_type, uri_owl_onProperty, uri_rdf_Property)=true)). % 32.96/21.94 tff(c_2331, plain, (![C_99]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_99), true, icext(C_99, uri_rdf_Property), true)=true))). % 32.96/21.94 tff(c_8216, plain, (ic(uri_owl_Class)=true)). % 32.96/21.94 tff(c_8158, plain, (icext(uri_rdfs_Class, uri_owl_Class)=true)). % 32.96/21.94 tff(c_8078, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, uri_rdfs_domain)=true)). % 32.96/21.94 tff(c_2351, plain, (![C_99]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_99), true, icext(C_99, uri_owl_Class), true)=true))). % 32.96/21.94 tff(c_7971, plain, (icext(uri_rdf_Property, uri_rdfs_subClassOf)=true)). % 32.96/21.94 tff(c_7917, plain, (iext(uri_rdf_type, uri_rdfs_subClassOf, uri_rdf_Property)=true)). % 32.96/21.94 tff(c_2032, plain, (![C_95]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_95), true, icext(C_95, uri_rdf_type), true)=true))). % 32.96/21.94 tff(c_3175, plain, (![S_5, O_6]: (ifeq(iext(uri_rdf_object, S_5, O_6), true, true, true)=true))). % 32.96/21.94 tff(c_7657, plain, (iext(uri_rdfs_subPropertyOf, uri_owl_someValuesFrom, uri_owl_someValuesFrom)=true)). % 32.96/21.94 tff(c_2329, plain, (![C_99]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_99), true, icext(C_99, uri_rdfs_Class), true)=true))). % 32.96/21.94 tff(c_7443, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Property, uri_rdfs_Resource)=true)). % 32.96/21.94 tff(c_2043, plain, (![C_95]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_95), true, icext(C_95, uri_rdf_object), true)=true))). % 32.96/21.94 tff(c_7269, plain, (ic(uri_owl_Restriction)=true)). % 32.96/21.94 tff(c_7211, plain, (icext(uri_rdfs_Class, uri_owl_Restriction)=true)). % 32.96/21.94 tff(c_2362, plain, (![C_99]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_99), true, icext(C_99, uri_owl_Restriction), true)=true))). % 32.96/21.94 tff(c_7089, plain, (icext(uri_rdf_Property, uri_rdfs_label)=true)). % 32.96/21.94 tff(c_7052, plain, (ip(uri_rdfs_member)=true)). % 32.96/21.94 tff(c_2011, plain, (![C_95]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_95), true, icext(C_95, uri_rdfs_label), true)=true))). % 32.96/21.94 tff(c_6974, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf__2, uri_rdfs_member)=true)). % 32.96/21.94 tff(c_6830, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, uri_rdfs_Resource)=true)). % 32.96/21.94 tff(c_2013, plain, (![C_95]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_95), true, icext(C_95, uri_rdf__3), true)=true))). % 32.96/21.94 tff(c_6708, plain, (ic(uri_rdfs_Statement)=true)). % 32.96/21.94 tff(c_6654, plain, (icext(uri_rdfs_Class, uri_rdfs_Statement)=true)). % 32.96/21.94 tff(c_2377, plain, (![C_99]: (ifeq(iext(uri_rdfs_range, uri_rdfs_domain, C_99), true, icext(C_99, uri_rdfs_Statement), true)=true))). % 32.96/21.94 tff(c_6571, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf__3, uri_rdf__3)=true)). % 32.96/21.94 tff(c_6469, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf__2, uri_rdf__2)=true)). % 32.96/21.94 tff(c_3417, plain, (![S_5, O_6]: (ifeq(iext(uri_owl_onProperty, S_5, O_6), true, true, true)=true))). % 32.96/21.94 tff(c_2336, plain, (![C_99]: (ifeq(iext(uri_rdfs_range, uri_rdfs_range, C_99), true, icext(C_99, uri_rdfs_Resource), true)=true))). % 32.96/21.94 tff(c_6324, plain, (icext(uri_rdf_Property, uri_rdfs_domain)=true)). % 32.96/21.94 tff(c_6238, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_value, uri_rdf_value)=true)). % 32.96/21.94 tff(c_2015, plain, (![C_95]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_95), true, icext(C_95, uri_rdfs_domain), true)=true))). % 32.96/21.94 tff(c_6163, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Literal, uri_rdfs_Resource)=true)). % 32.96/21.94 tff(c_6073, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_rest, uri_rdf_rest)=true)). % 32.96/21.94 tff(c_5975, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_subject, uri_rdf_subject)=true)). % 32.96/21.94 tff(c_2369, plain, (![C_99]: (ifeq(iext(uri_rdfs_range, uri_rdfs_domain, C_99), true, icext(C_99, uri_rdfs_Resource), true)=true))). % 32.96/21.94 tff(c_5905, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Literal, uri_rdfs_Literal)=true)). % 32.96/21.94 tff(c_1624, plain, (![S_5, O_6]: (ifeq(iext(uri_rdfs_subClassOf, S_5, O_6), true, true, true)=true))). % 32.96/21.94 tff(c_2029, plain, (![C_95]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_95), true, icext(C_95, uri_rdf_value), true)=true))). % 32.96/21.94 tff(c_5724, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Class, uri_rdfs_Resource)=true)). % 32.96/21.94 tff(c_5632, plain, (iext(uri_rdfs_subClassOf, uri_rdf_XMLLiteral, uri_rdfs_Resource)=true)). % 32.96/21.94 tff(c_1670, plain, (![X_92]: (ifeq(icext(uri_rdf_Bag, X_92), true, icext(uri_rdfs_Container, X_92), true)=true))). % 32.96/21.94 tff(c_5578, plain, (icext(uri_rdf_Property, uri_rdfs_seeAlso)=true)). % 32.96/21.94 tff(c_5521, plain, (iext(uri_rdf_type, uri_rdfs_seeAlso, uri_rdf_Property)=true)). % 32.96/21.94 tff(c_1667, plain, (![X_92]: (ifeq(icext(uri_rdfs_Datatype, X_92), true, icext(uri_rdfs_Class, X_92), true)=true))). % 32.96/21.94 tff(c_5368, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, uri_rdfs_ContainerMembershipProperty)=true)). % 32.96/21.94 tff(c_5291, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Seq, uri_rdfs_Seq)=true)). % 32.96/21.94 tff(c_1666, plain, (![X_92]: (ifeq(icext(uri_rdf_XMLLiteral, X_92), true, icext(uri_rdfs_Literal, X_92), true)=true))). % 32.96/21.94 tff(c_5227, plain, (icext(uri_rdfs_Class, uri_rdfs_Resource)=true)). % 32.96/21.94 tff(c_1671, plain, (![X_92]: (ifeq(icext(uri_rdfs_ContainerMembershipProperty, X_92), true, icext(uri_rdf_Property, X_92), true)=true))). % 32.96/21.94 tff(c_5121, plain, (ic(uri_rdfs_Resource)=true)). % 32.96/21.94 tff(c_5060, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, uri_rdfs_Resource)=true)). % 32.96/21.94 tff(c_1668, plain, (![X_92]: (ifeq(icext(uri_rdfs_Seq, X_92), true, icext(uri_rdfs_Container, X_92), true)=true))). % 32.96/21.94 tff(c_4976, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Alt, uri_rdf_Alt)=true)). % 32.96/21.94 tff(c_4877, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Container, uri_rdfs_Container)=true)). % 32.96/21.94 tff(c_1669, plain, (![X_92]: (ifeq(icext(uri_rdf_Alt, X_92), true, icext(uri_rdfs_Container, X_92), true)=true))). % 32.96/21.94 tff(c_4812, plain, (![X_140]: (iext(uri_rdf_type, X_140, uri_rdfs_Resource)=true))). % 32.96/21.94 tff(c_2354, plain, (![X_100, Y_101]: (ifeq(iext(uri_rdf_subject, X_100, Y_101), true, true, true)=true))). % 32.96/21.94 tff(c_2031, plain, (![X_96, Y_97]: (ifeq(iext(uri_rdf_type, X_96, Y_97), true, true, true)=true))). % 32.96/21.94 tff(c_2358, plain, (![X_100, Y_101]: (ifeq(iext(uri_rdf__1, X_100, Y_101), true, true, true)=true))). % 32.96/21.94 tff(c_1975, plain, (![X_96, Y_97]: (ifeq(iext(uri_rdfs_label, X_96, Y_97), true, true, true)=true))). % 32.96/21.94 tff(c_2320, plain, (![X_100, Y_101]: (ifeq(iext(uri_rdf_first, X_100, Y_101), true, true, true)=true))). % 32.96/21.94 tff(c_2335, plain, (![X_100, Y_101]: (ifeq(iext(uri_rdf_predicate, X_100, Y_101), true, true, true)=true))). % 32.96/21.94 tff(c_2002, plain, (![X_96, Y_97]: (ifeq(iext(uri_rdfs_comment, X_96, Y_97), true, true, true)=true))). % 32.96/21.94 tff(c_2018, plain, (![X_96, Y_97]: (ifeq(iext(uri_rdfs_member, X_96, Y_97), true, true, true)=true))). % 32.96/21.94 tff(c_2028, plain, (![X_96, Y_97]: (ifeq(iext(uri_rdf_value, X_96, Y_97), true, true, true)=true))). % 32.96/21.94 tff(c_2339, plain, (![X_100, Y_101]: (ifeq(iext(uri_rdf__2, X_100, Y_101), true, true, true)=true))). % 32.96/21.94 tff(c_4610, plain, (icext(uri_rdfs_Class, uri_rdfs_Container)=true)). % 32.96/21.94 tff(c_4560, plain, (icext(uri_rdfs_Class, uri_rdf_Alt)=true)). % 32.96/21.94 tff(c_4517, plain, (icext(uri_rdfs_Class, uri_rdfs_Seq)=true)). % 32.96/21.94 tff(c_2315, plain, (![X_100, Y_101]: (ifeq(iext(uri_rdf__3, X_100, Y_101), true, true, true)=true))). % 32.96/21.94 tff(c_4461, plain, (icext(uri_rdfs_Class, uri_rdfs_Class)=true)). % 32.96/21.94 tff(c_4412, plain, (icext(uri_rdfs_Class, uri_rdfs_Datatype)=true)). % 32.96/21.94 tff(c_2024, plain, (![X_96, Y_97]: (ifeq(iext(uri_rdfs_isDefinedBy, X_96, Y_97), true, true, true)=true))). % 32.96/21.94 tff(c_4362, plain, (icext(uri_rdfs_Class, uri_rdf_XMLLiteral)=true)). % 32.96/21.94 tff(c_4314, plain, (icext(uri_rdfs_Class, uri_rdfs_Literal)=true)). % 32.96/21.94 tff(c_4264, plain, (icext(uri_rdfs_Class, uri_rdf_Bag)=true)). % 32.96/21.94 tff(c_2342, plain, (![X_100, Y_101]: (ifeq(iext(uri_rdfs_seeAlso, X_100, Y_101), true, true, true)=true))). % 32.96/21.94 tff(c_4221, plain, (icext(uri_rdfs_Class, uri_rdfs_ContainerMembershipProperty)=true)). % 32.96/21.94 tff(c_4181, plain, (icext(uri_rdf_Property, uri_rdf_type)=true)). % 32.96/21.94 tff(c_4137, plain, (icext(uri_rdfs_Datatype, uri_rdf_XMLLiteral)=true)). % 32.96/21.94 tff(c_4094, plain, (icext(uri_rdf_Property, uri_rdf_first)=true)). % 32.96/21.94 tff(c_4054, plain, (icext(sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z, uri_ex_s)=true)). % 32.96/21.94 tff(c_4012, plain, (icext(uri_rdfs_ContainerMembershipProperty, uri_rdf__2)=true)). % 32.96/21.94 tff(c_3975, plain, (icext(uri_rdf_Property, uri_rdf__2)=true)). % 32.96/21.94 tff(c_3935, plain, (icext(uri_rdf_Property, uri_rdf_object)=true)). % 32.96/21.94 tff(c_3895, plain, (icext(uri_rdf_Property, uri_rdf_rest)=true)). % 32.96/21.94 tff(c_3843, plain, (icext(uri_rdf_Property, uri_rdf_subject)=true)). % 32.96/21.94 tff(c_3798, plain, (icext(uri_rdfs_Class, uri_rdf_Property)=true)). % 32.96/21.94 tff(c_3747, plain, (icext(uri_rdf_Property, uri_rdf__3)=true)). % 32.96/21.94 tff(c_3701, plain, (icext(uri_owl_Restriction, sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z)=true)). % 32.96/21.94 tff(c_3657, plain, (icext(uri_rdfs_ContainerMembershipProperty, uri_rdf__3)=true)). % 32.96/21.94 tff(c_3620, plain, (icext(uri_owl_ObjectProperty, uri_ex_p)=true)). % 32.96/21.94 tff(c_3582, plain, (icext(uri_rdf_List, uri_rdf_nil)=true)). % 32.96/21.94 tff(c_3546, plain, (icext(uri_rdf_Property, uri_rdf__1)=true)). % 32.96/21.94 tff(c_3509, plain, (icext(uri_rdf_Property, uri_rdf_value)=true)). % 32.96/21.94 tff(c_3442, plain, (icext(uri_rdfs_ContainerMembershipProperty, uri_rdf__1)=true)). % 32.96/21.94 tff(c_3432, plain, (icext(uri_owl_Class, uri_ex_c)=true)). % 32.96/21.94 tff(c_3396, plain, (ip(uri_owl_onProperty)=true)). % 32.96/21.94 tff(c_3356, plain, (ip(uri_rdf__2)=true)). % 32.96/21.94 tff(c_3319, plain, (ic(uri_rdf_Bag)=true)). % 32.96/21.94 tff(c_3280, plain, (ic(uri_rdf_Property)=true)). % 32.96/21.94 tff(c_3244, plain, (ic(uri_rdfs_Class)=true)). % 32.96/21.94 tff(c_3204, plain, (ip(uri_owl_someValuesFrom)=true)). % 32.96/21.94 tff(c_3153, plain, (ip(uri_rdf_object)=true)). % 32.96/21.94 tff(c_3119, plain, (ic(uri_rdfs_Container)=true)). % 32.96/21.94 tff(c_3078, plain, (ip(uri_rdf__1)=true)). % 32.96/21.94 tff(c_3038, plain, (ip(uri_rdfs_isDefinedBy)=true)). % 32.96/21.94 tff(c_166, plain, (![P_47, Q_48, X_49, Y_50]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, Q_48), true, ifeq(iext(P_47, X_49, Y_50), true, iext(Q_48, X_49, Y_50), true), true)=true))). % 32.96/21.94 tff(c_2522, plain, (ip(uri_rdf_first)=true)). % 32.96/21.94 tff(c_158, plain, (![D_40, E_41, C_42]: (ifeq(iext(uri_rdfs_subClassOf, D_40, E_41), true, ifeq(iext(uri_rdfs_subClassOf, C_42, D_40), true, iext(uri_rdfs_subClassOf, C_42, E_41), true), true)=true))). % 32.96/21.94 tff(c_2419, plain, (ic(uri_rdfs_Literal)=true)). % 32.96/21.94 tff(c_172, plain, (![Q_52, R_53, P_54]: (ifeq(iext(uri_rdfs_subPropertyOf, Q_52, R_53), true, ifeq(iext(uri_rdfs_subPropertyOf, P_54, Q_52), true, iext(uri_rdfs_subPropertyOf, P_54, R_53), true), true)=true))). % 32.96/21.94 tff(c_130, plain, (![P_28, C_29, X_30, Y_31]: (ifeq(iext(uri_rdfs_range, P_28, C_29), true, ifeq(iext(P_28, X_30, Y_31), true, icext(C_29, Y_31), true), true)=true))). % 32.96/21.94 tff(c_110, plain, (![P_18, C_19, X_20, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, C_19), true, ifeq(iext(P_18, X_20, Y_21), true, icext(C_19, X_20), true), true)=true))). % 32.96/21.94 tff(c_1677, plain, (ic(uri_rdf_Alt)=true)). % 32.96/21.94 tff(c_148, plain, (![C_32, X_33, D_34]: (ifeq(icext(C_32, X_33), true, ifeq(iext(uri_rdfs_subClassOf, C_32, D_34), true, icext(D_34, X_33), true), true)=true))). % 32.96/21.94 tff(c_1603, plain, (ip(uri_rdfs_subClassOf)=true)). % 32.96/21.94 tff(c_194, plain, (![BNODE_x_55]: (tuple(iext(uri_rdf_type, BNODE_x_55, uri_ex_c), iext(uri_ex_p, uri_ex_s, BNODE_x_55))!=tuple(true, true)))). % 32.96/21.94 tff(c_54, plain, (![C_11, X_12]: (ifeq(icext(C_11, X_12), true, iext(uri_rdf_type, X_12, C_11), true)=true))). % 32.96/21.94 tff(c_1492, plain, (ip(uri_rdf__3)=true)). % 32.96/21.94 tff(c_104, plain, (![D_17]: (ifeq(icext(uri_rdfs_Datatype, D_17), true, iext(uri_rdfs_subClassOf, D_17, uri_rdfs_Literal), true)=true))). % 32.96/21.94 tff(c_56, plain, (![X_13, C_14]: (ifeq(iext(uri_rdf_type, X_13, C_14), true, icext(C_14, X_13), true)=true))). % 32.96/21.95 tff(c_72, plain, (![P_16]: (ifeq(icext(uri_rdfs_ContainerMembershipProperty, P_16), true, iext(uri_rdfs_subPropertyOf, P_16, uri_rdfs_member), true)=true))). % 32.96/21.95 tff(c_1359, plain, (ip(uri_rdfs_seeAlso)=true)). % 32.96/21.95 tff(c_1282, plain, (ip(uri_rdfs_range)=true)). % 32.96/21.95 tff(c_150, plain, (![C_35, D_36]: (ifeq(iext(uri_rdfs_subClassOf, C_35, D_36), true, ic(D_36), true)=true))). % 32.96/21.95 tff(c_162, plain, (![P_43, Q_44]: (ifeq(iext(uri_rdfs_subPropertyOf, P_43, Q_44), true, ip(Q_44), true)=true))). % 32.96/21.95 tff(c_1201, plain, (ip(uri_rdfs_domain)=true)). % 32.96/21.95 tff(c_1169, plain, (ip(uri_rdfs_subPropertyOf)=true)). % 32.96/21.95 tff(c_170, plain, (![P_51]: (ifeq(ip(P_51), true, iext(uri_rdfs_subPropertyOf, P_51, P_51), true)=true))). % 32.96/21.95 tff(c_28, plain, (![P_9]: (ifeq(ip(P_9), true, iext(uri_rdf_type, P_9, uri_rdf_Property), true)=true))). % 32.96/21.95 tff(c_1064, plain, (ip(uri_rdf_type)=true)). % 32.96/21.95 tff(c_1037, plain, (ip(uri_rdf_value)=true)). % 32.96/21.95 tff(c_4, plain, (![P_4, S_5, O_6]: (ifeq(iext(P_4, S_5, O_6), true, ip(P_4), true)=true))). % 32.96/21.95 tff(c_789, plain, (ip(uri_rdf_rest)=true)). % 32.96/21.95 tff(c_156, plain, (![C_39]: (ifeq(ic(C_39), true, iext(uri_rdfs_subClassOf, C_39, C_39), true)=true))). % 32.96/21.95 tff(c_738, plain, (ip(uri_rdf_subject)=true)). % 32.96/21.95 tff(c_679, plain, (ic(uri_rdfs_Datatype)=true)). % 32.96/21.95 tff(c_30, plain, (![P_10]: (ifeq(iext(uri_rdf_type, P_10, uri_rdf_Property), true, ip(P_10), true)=true))). % 32.96/21.95 tff(c_633, plain, (ic(uri_rdfs_Seq)=true)). % 32.96/21.95 tff(c_58, plain, (![C_15]: (ifeq(ic(C_15), true, iext(uri_rdfs_subClassOf, C_15, uri_rdfs_Resource), true)=true))). % 32.96/21.95 tff(c_607, plain, (ic(uri_rdfs_ContainerMembershipProperty)=true)). % 32.96/21.95 tff(c_164, plain, (![P_45, Q_46]: (ifeq(iext(uri_rdfs_subPropertyOf, P_45, Q_46), true, ip(P_45), true)=true))). % 32.96/21.95 tff(c_571, plain, (ic(uri_rdf_XMLLiteral)=true)). % 32.96/21.95 tff(c_152, plain, (![C_37, D_38]: (ifeq(iext(uri_rdfs_subClassOf, C_37, D_38), true, ic(C_37), true)=true))). % 32.96/21.95 tff(c_114, plain, (![X_22]: (ifeq(ic(X_22), true, icext(uri_rdfs_Class, X_22), true)=true))). % 32.96/21.95 tff(c_122, plain, (![X_26]: (ifeq(icext(uri_rdfs_Literal, X_26), true, lv(X_26), true)=true))). % 32.96/21.95 tff(c_116, plain, (![X_23]: (ifeq(icext(uri_rdfs_Class, X_23), true, ic(X_23), true)=true))). % 32.96/21.95 tff(c_502, plain, (![X_63]: (icext(uri_rdfs_Resource, X_63)=true))). % 32.96/21.95 tff(c_124, plain, (![X_27]: (ifeq(lv(X_27), true, icext(uri_rdfs_Literal, X_27), true)=true))). % 32.96/21.95 tff(c_197, plain, (![X_8]: (ifeq(lv(X_8), true, true, true)=true))). % 32.96/21.95 tff(c_2, plain, (![A_1, B_2, C_3]: (ifeq(A_1, A_1, B_2, C_3)=B_2))). % 32.96/21.95 tff(c_90, plain, (iext(uri_rdfs_range, uri_rdf__3, uri_rdfs_Resource)=true)). % 32.96/21.95 tff(c_46, plain, (iext(uri_rdfs_domain, uri_rdfs_label, uri_rdfs_Resource)=true)). % 32.96/21.95 tff(c_184, plain, (iext(uri_owl_onProperty, sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z, uri_ex_p)=true)). % 32.96/21.95 tff(c_96, plain, (iext(uri_rdf_type, uri_rdf__3, uri_rdfs_ContainerMembershipProperty)=true)). % 32.96/21.95 tff(c_62, plain, (iext(uri_rdfs_range, uri_rdf_first, uri_rdfs_Resource)=true)). % 32.96/21.95 tff(c_12, plain, (iext(uri_rdf_type, uri_rdf_nil, uri_rdf_List)=true)). % 32.96/21.95 tff(c_102, plain, (iext(uri_rdf_type, uri_rdf_XMLLiteral, uri_rdfs_Datatype)=true)). % 32.96/21.95 tff(c_146, plain, (iext(uri_rdfs_domain, uri_rdfs_subClassOf, uri_rdfs_Class)=true)). % 32.96/21.95 tff(c_100, plain, (iext(uri_rdfs_subClassOf, uri_rdf_XMLLiteral, uri_rdfs_Literal)=true)). % 32.96/21.95 tff(c_160, plain, (iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, uri_rdf_Property)=true)). % 32.96/21.95 tff(c_14, plain, (iext(uri_rdf_type, uri_rdf_rest, uri_rdf_Property)=true)). % 32.96/21.95 tff(c_106, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, uri_rdfs_Class)=true)). % 32.96/21.95 tff(c_126, plain, (iext(uri_rdf_type, uri_rdf_Property, uri_rdfs_Class)=true)). % 32.96/21.95 tff(c_190, plain, (iext(uri_rdf_type, uri_ex_s, sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z)=true)). % 32.96/21.95 tff(c_20, plain, (iext(uri_rdf_type, uri_rdf__3, uri_rdf_Property)=true)). % 32.96/21.95 tff(c_34, plain, (iext(uri_rdf_type, uri_rdf_type, uri_rdf_Property)=true)). % 32.96/21.95 tff(c_92, plain, (iext(uri_rdf_type, uri_rdf__1, uri_rdfs_ContainerMembershipProperty)=true)). % 32.96/21.95 tff(c_98, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Seq, uri_rdfs_Container)=true)). % 32.96/21.95 tff(c_140, plain, (iext(uri_rdfs_range, uri_rdf_predicate, uri_rdfs_Resource)=true)). % 32.96/21.95 tff(c_22, plain, (iext(uri_rdf_type, uri_rdf_object, uri_rdf_Property)=true)). % 32.96/21.95 tff(c_16, plain, (iext(uri_rdf_type, uri_rdf__1, uri_rdf_Property)=true)). % 32.96/21.95 tff(c_88, plain, (iext(uri_rdfs_range, uri_rdf__2, uri_rdfs_Resource)=true)). % 32.96/21.95 tff(c_82, plain, (iext(uri_rdfs_domain, uri_rdf__2, uri_rdfs_Resource)=true)). % 32.96/21.95 tff(c_52, plain, (iext(uri_rdfs_range, uri_rdfs_seeAlso, uri_rdfs_Resource)=true)). % 32.96/21.95 tff(c_44, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_isDefinedBy, uri_rdfs_seeAlso)=true)). % 32.96/21.95 tff(c_182, plain, (iext(uri_owl_someValuesFrom, sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z, uri_ex_c)=true)). % 32.96/21.95 tff(c_36, plain, (iext(uri_rdfs_domain, uri_rdfs_comment, uri_rdfs_Resource)=true)). % 32.96/21.95 tff(c_50, plain, (iext(uri_rdfs_domain, uri_rdfs_seeAlso, uri_rdfs_Resource)=true)). % 32.96/21.95 tff(c_80, plain, (iext(uri_rdfs_domain, uri_rdf__1, uri_rdfs_Resource)=true)). % 32.96/21.95 tff(c_24, plain, (iext(uri_rdf_type, uri_rdf_value, uri_rdf_Property)=true)). % 32.96/21.95 tff(c_94, plain, (iext(uri_rdf_type, uri_rdf__2, uri_rdfs_ContainerMembershipProperty)=true)). % 32.96/21.95 tff(c_188, plain, (iext(uri_rdf_type, uri_ex_c, uri_owl_Class)=true)). % 32.96/21.95 tff(c_48, plain, (iext(uri_rdfs_range, uri_rdfs_label, uri_rdfs_Literal)=true)). % 32.96/21.95 tff(c_84, plain, (iext(uri_rdfs_domain, uri_rdf__3, uri_rdfs_Resource)=true)). % 32.96/21.95 tff(c_144, plain, (iext(uri_rdfs_range, uri_rdf_subject, uri_rdfs_Resource)=true)). % 32.96/21.95 tff(c_108, plain, (iext(uri_rdfs_domain, uri_rdfs_domain, uri_rdf_Property)=true)). % 32.96/21.95 tff(c_168, plain, (iext(uri_rdfs_range, uri_rdfs_subPropertyOf, uri_rdf_Property)=true)). % 32.96/21.95 tff(c_86, plain, (iext(uri_rdfs_range, uri_rdf__1, uri_rdfs_Resource)=true)). % 32.96/21.95 tff(c_76, plain, (iext(uri_rdfs_domain, uri_rdfs_member, uri_rdfs_Resource)=true)). % 32.96/21.95 tff(c_68, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Alt, uri_rdfs_Container)=true)). % 32.96/21.95 tff(c_186, plain, (iext(uri_rdf_type, sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z, uri_owl_Restriction)=true)). % 32.96/21.95 tff(c_78, plain, (iext(uri_rdfs_range, uri_rdfs_member, uri_rdfs_Resource)=true)). % 32.96/21.95 tff(c_38, plain, (iext(uri_rdfs_range, uri_rdfs_comment, uri_rdfs_Literal)=true)). % 32.96/21.95 tff(c_40, plain, (iext(uri_rdfs_domain, uri_rdfs_isDefinedBy, uri_rdfs_Resource)=true)). % 32.96/21.95 tff(c_176, plain, (iext(uri_rdfs_range, uri_rdf_type, uri_rdfs_Class)=true)). % 32.96/21.95 tff(c_70, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Bag, uri_rdfs_Container)=true)). % 32.96/21.95 tff(c_178, plain, (iext(uri_rdfs_domain, uri_rdf_value, uri_rdfs_Resource)=true)). % 32.96/21.95 tff(c_112, plain, (iext(uri_rdfs_range, uri_rdfs_domain, uri_rdfs_Class)=true)). % 32.96/21.95 tff(c_174, plain, (iext(uri_rdfs_domain, uri_rdf_type, uri_rdfs_Resource)=true)). % 32.96/21.95 tff(c_74, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, uri_rdf_Property)=true)). % 32.96/21.95 tff(c_42, plain, (iext(uri_rdfs_range, uri_rdfs_isDefinedBy, uri_rdfs_Resource)=true)). % 32.96/21.95 tff(c_18, plain, (iext(uri_rdf_type, uri_rdf__2, uri_rdf_Property)=true)). % 32.96/21.95 tff(c_138, plain, (iext(uri_rdfs_domain, uri_rdf_predicate, uri_rdfs_Statement)=true)). % 32.96/21.95 tff(c_142, plain, (iext(uri_rdfs_domain, uri_rdf_subject, uri_rdfs_Statement)=true)). % 32.96/21.95 tff(c_60, plain, (iext(uri_rdfs_domain, uri_rdf_first, uri_rdf_List)=true)). % 32.96/21.95 tff(c_132, plain, (iext(uri_rdfs_range, uri_rdfs_range, uri_rdfs_Class)=true)). % 32.96/21.95 tff(c_10, plain, (iext(uri_rdf_type, uri_rdf_first, uri_rdf_Property)=true)). % 32.96/21.95 tff(c_26, plain, (iext(uri_rdf_type, uri_rdf_subject, uri_rdf_Property)=true)). % 32.96/21.95 tff(c_154, plain, (iext(uri_rdfs_range, uri_rdfs_subClassOf, uri_rdfs_Class)=true)). % 32.96/21.95 tff(c_134, plain, (iext(uri_rdfs_domain, uri_rdf_object, uri_rdfs_Statement)=true)). % 32.96/21.95 tff(c_64, plain, (iext(uri_rdfs_domain, uri_rdf_rest, uri_rdf_List)=true)). % 32.96/21.95 tff(c_66, plain, (iext(uri_rdfs_range, uri_rdf_rest, uri_rdf_List)=true)). % 32.96/21.95 tff(c_128, plain, (iext(uri_rdfs_domain, uri_rdfs_range, uri_rdf_Property)=true)). % 32.96/21.95 tff(c_180, plain, (iext(uri_rdfs_range, uri_rdf_value, uri_rdfs_Resource)=true)). % 32.96/21.95 tff(c_192, plain, (iext(uri_rdf_type, uri_ex_p, uri_owl_ObjectProperty)=true)). % 32.96/21.95 tff(c_6, plain, (![X_7]: (ir(X_7)=true))). % 32.96/21.95 % SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 32.96/21.95 %------------------------------------------------------------------------------