%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : SWB026-10 : TPTP v9.0.0. Released v7.3.0. % Transfm : none % Format : tptp:raw % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % Computer : n014.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Wed Apr 9 09:15:56 PM UTC 2025 % Result : Satisfiable 33.03s 22.12s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.04/0.12 % Problem : SWB026-10 : TPTP v9.0.0. Released v7.3.0. % 0.04/0.13 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % 0.13/0.34 % Computer : n014.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 300 % 0.13/0.34 % DateTime : Wed Apr 9 01:02:19 EDT 2025 % 0.13/0.34 % CPUTime : % 33.03/22.11 % 33.03/22.12 % SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 33.03/22.12 % 33.03/22.12 % SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 33.13/22.13 %$ ifeq > iext > 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_oneOf > uri_owl_InverseFunctionalProperty > uri_ex_w > uri_ex_u > uri_ex_p > true > sK4_testcase_premise_fullish_026_Inferred_Property_Characteristics_I_BNODE_l1 > sK3_testcase_premise_fullish_026_Inferred_Property_Characteristics_I_BNODE_x1 > sK2_testcase_premise_fullish_026_Inferred_Property_Characteristics_I_BNODE_l2 > sK1_testcase_premise_fullish_026_Inferred_Property_Characteristics_I_BNODE_x2 % 33.13/22.13 % 33.13/22.13 %Foreground sorts: % 33.13/22.13 % 33.13/22.13 % 33.13/22.13 %Background operators: % 33.13/22.13 % 33.13/22.13 % 33.13/22.13 %Foreground operators: % 33.13/22.13 tff(uri_owl_InverseFunctionalProperty, type, uri_owl_InverseFunctionalProperty: $i). % 33.13/22.13 tff(uri_rdfs_Datatype, type, uri_rdfs_Datatype: $i). % 33.13/22.13 tff(uri_rdfs_ContainerMembershipProperty, type, uri_rdfs_ContainerMembershipProperty: $i). % 33.13/22.13 tff(uri_owl_oneOf, type, uri_owl_oneOf: $i). % 33.13/22.13 tff(uri_rdfs_Resource, type, uri_rdfs_Resource: $i). % 33.13/22.13 tff(uri_rdf_Property, type, uri_rdf_Property: $i). % 33.13/22.13 tff(uri_rdf_subject, type, uri_rdf_subject: $i). % 33.13/22.13 tff(uri_rdf_type, type, uri_rdf_type: $i). % 33.13/22.13 tff(uri_rdfs_subPropertyOf, type, uri_rdfs_subPropertyOf: $i). % 33.13/22.13 tff(uri_ex_u, type, uri_ex_u: $i). % 33.13/22.13 tff(uri_rdfs_seeAlso, type, uri_rdfs_seeAlso: $i). % 33.13/22.13 tff(icext, type, icext: ($i * $i) > $i). % 33.13/22.13 tff(uri_rdfs_range, type, uri_rdfs_range: $i). % 33.13/22.13 tff(uri_rdf_XMLLiteral, type, uri_rdf_XMLLiteral: $i). % 33.13/22.13 tff(sK2_testcase_premise_fullish_026_Inferred_Property_Characteristics_I_BNODE_l2, type, sK2_testcase_premise_fullish_026_Inferred_Property_Characteristics_I_BNODE_l2: $i). % 33.13/22.13 tff(uri_rdf_List, type, uri_rdf_List: $i). % 33.13/22.13 tff(uri_rdf_first, type, uri_rdf_first: $i). % 33.13/22.13 tff(uri_rdf_predicate, type, uri_rdf_predicate: $i). % 33.13/22.13 tff(ir, type, ir: $i > $i). % 33.13/22.13 tff(lv, type, lv: $i > $i). % 33.13/22.13 tff(uri_rdf__3, type, uri_rdf__3: $i). % 33.13/22.13 tff(uri_rdf_value, type, uri_rdf_value: $i). % 33.13/22.13 tff(sK1_testcase_premise_fullish_026_Inferred_Property_Characteristics_I_BNODE_x2, type, sK1_testcase_premise_fullish_026_Inferred_Property_Characteristics_I_BNODE_x2: $i). % 33.13/22.13 tff(ic, type, ic: $i > $i). % 33.13/22.13 tff(uri_rdfs_Statement, type, uri_rdfs_Statement: $i). % 33.13/22.13 tff(uri_ex_p, type, uri_ex_p: $i). % 33.13/22.13 tff(uri_rdf__1, type, uri_rdf__1: $i). % 33.13/22.13 tff(iext, type, iext: ($i * $i * $i) > $i). % 33.13/22.13 tff(uri_ex_w, type, uri_ex_w: $i). % 33.13/22.13 tff(uri_rdf_rest, type, uri_rdf_rest: $i). % 33.13/22.13 tff(uri_rdfs_label, type, uri_rdfs_label: $i). % 33.13/22.13 tff(uri_rdfs_Container, type, uri_rdfs_Container: $i). % 33.13/22.13 tff(sK3_testcase_premise_fullish_026_Inferred_Property_Characteristics_I_BNODE_x1, type, sK3_testcase_premise_fullish_026_Inferred_Property_Characteristics_I_BNODE_x1: $i). % 33.13/22.13 tff(uri_rdfs_subClassOf, type, uri_rdfs_subClassOf: $i). % 33.13/22.13 tff(uri_rdf_object, type, uri_rdf_object: $i). % 33.13/22.13 tff(ip, type, ip: $i > $i). % 33.13/22.13 tff(uri_rdfs_Class, type, uri_rdfs_Class: $i). % 33.13/22.13 tff(uri_rdfs_Seq, type, uri_rdfs_Seq: $i). % 33.13/22.13 tff(uri_rdfs_member, type, uri_rdfs_member: $i). % 33.13/22.13 tff(uri_rdf_Bag, type, uri_rdf_Bag: $i). % 33.13/22.13 tff(uri_rdf__2, type, uri_rdf__2: $i). % 33.13/22.13 tff(uri_rdfs_comment, type, uri_rdfs_comment: $i). % 33.13/22.13 tff(uri_rdfs_Literal, type, uri_rdfs_Literal: $i). % 33.13/22.13 tff(sK4_testcase_premise_fullish_026_Inferred_Property_Characteristics_I_BNODE_l1, type, sK4_testcase_premise_fullish_026_Inferred_Property_Characteristics_I_BNODE_l1: $i). % 33.13/22.13 tff(true, type, true: $i). % 33.13/22.13 tff(uri_rdf_Alt, type, uri_rdf_Alt: $i). % 33.13/22.13 tff(uri_rdf_nil, type, uri_rdf_nil: $i). % 33.13/22.13 tff(uri_rdfs_isDefinedBy, type, uri_rdfs_isDefinedBy: $i). % 33.13/22.13 tff(uri_rdfs_domain, type, uri_rdfs_domain: $i). % 33.13/22.13 tff(ifeq, type, ifeq: ($i * $i * $i * $i) > $i). % 33.13/22.13 % 33.13/22.13 %Saturated clause set: % 33.13/22.14 tff(c_13559, 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))). % 33.13/22.14 tff(c_13556, 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))). % 33.13/22.14 tff(c_14110, 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))). % 33.13/22.14 tff(c_13958, 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))). % 33.13/22.14 tff(c_72394, plain, (![X_1251, Y_1252]: (ifeq(iext(uri_rdfs_label, X_1251, Y_1252), true, iext(uri_rdfs_label, X_1251, Y_1252), true)=true))). % 33.13/22.14 tff(c_13893, 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))). % 33.13/22.14 tff(c_13820, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subPropertyOf), true, ifeq(iext(P_47, uri_ex_p, uri_ex_p), true, true, true), true)=true))). % 33.13/22.14 tff(c_72124, plain, (![X_1245, Y_1246]: (ifeq(iext(uri_ex_p, X_1245, Y_1246), true, iext(uri_ex_p, X_1245, Y_1246), true)=true))). % 33.13/22.14 tff(c_72097, plain, (![X_1241, Y_1242]: (ifeq(iext(uri_rdfs_comment, X_1241, Y_1242), true, iext(uri_rdfs_comment, X_1241, Y_1242), true)=true))). % 33.13/22.14 tff(c_14023, 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))). % 33.13/22.14 tff(c_71949, plain, (![X_1236, Y_1237]: (ifeq(iext(uri_rdf_predicate, X_1236, Y_1237), true, iext(uri_rdf_predicate, X_1236, Y_1237), true)=true))). % 33.13/22.14 tff(c_4915, 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))). % 33.13/22.14 tff(c_13502, 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))). % 33.13/22.14 tff(c_13751, 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))). % 33.13/22.14 tff(c_71408, plain, (![X_1228, Y_1229]: (ifeq(iext(uri_rdfs_member, X_1228, Y_1229), true, iext(uri_rdfs_member, X_1228, Y_1229), true)=true))). % 33.13/22.14 tff(c_4918, 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))). % 33.13/22.14 tff(c_13439, 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))). % 33.13/22.14 tff(c_70999, plain, (![C_1223]: (ifeq(iext(uri_rdfs_subClassOf, C_1223, sK3_testcase_premise_fullish_026_Inferred_Property_Characteristics_I_BNODE_x1), true, iext(uri_rdfs_subClassOf, C_1223, uri_rdfs_Resource), true)=true))). % 33.13/22.14 tff(c_12810, 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))). % 33.13/22.14 tff(c_13303, 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))). % 33.13/22.14 tff(c_13212, 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))). % 33.13/22.14 tff(c_13145, 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))). % 33.13/22.14 tff(c_70351, plain, (![C_1217]: (ifeq(iext(uri_rdfs_subClassOf, C_1217, sK1_testcase_premise_fullish_026_Inferred_Property_Characteristics_I_BNODE_x2), true, iext(uri_rdfs_subClassOf, C_1217, uri_rdfs_Resource), true)=true))). % 33.13/22.14 tff(c_70195, plain, (![C_1215]: (ifeq(iext(uri_rdfs_subClassOf, C_1215, uri_rdfs_Statement), true, iext(uri_rdfs_subClassOf, C_1215, uri_rdfs_Resource), true)=true))). % 33.13/22.14 tff(c_13054, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subClassOf), true, ifeq(iext(P_47, sK1_testcase_premise_fullish_026_Inferred_Property_Characteristics_I_BNODE_x2, sK1_testcase_premise_fullish_026_Inferred_Property_Characteristics_I_BNODE_x2), true, true, true), true)=true))). % 33.13/22.14 tff(c_14745, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subClassOf), true, ifeq(iext(P_47, sK3_testcase_premise_fullish_026_Inferred_Property_Characteristics_I_BNODE_x1, uri_rdfs_Resource), true, true, true), true)=true))). % 33.13/22.14 tff(c_12932, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subClassOf), true, ifeq(iext(P_47, sK1_testcase_premise_fullish_026_Inferred_Property_Characteristics_I_BNODE_x2, uri_rdfs_Resource), true, true, true), true)=true))). % 33.13/22.14 tff(c_69670, plain, (![C_1210]: (ifeq(iext(uri_rdfs_subClassOf, C_1210, uri_rdf_List), true, iext(uri_rdfs_subClassOf, C_1210, uri_rdfs_Resource), true)=true))). % 33.13/22.14 tff(c_14679, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subClassOf), true, ifeq(iext(P_47, sK3_testcase_premise_fullish_026_Inferred_Property_Characteristics_I_BNODE_x1, sK3_testcase_premise_fullish_026_Inferred_Property_Characteristics_I_BNODE_x1), true, true, true), true)=true))). % 33.13/22.14 tff(c_7778, 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))). % 33.13/22.14 tff(c_5072, 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))). % 33.13/22.14 tff(c_12635, 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))). % 33.13/22.14 tff(c_12754, 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))). % 33.13/22.14 tff(c_6779, 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))). % 33.13/22.14 tff(c_12587, 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))). % 33.13/22.14 tff(c_12235, 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))). % 33.13/22.14 tff(c_5069, 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))). % 33.13/22.14 tff(c_12186, 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))). % 33.13/22.14 tff(c_8373, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdf_Property), true, ifeq(iext(P_28, X_30, uri_owl_oneOf), true, true, true), true)=true))). % 33.13/22.14 tff(c_12707, 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))). % 33.13/22.15 tff(c_8376, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdf_Property), true, ifeq(iext(P_18, uri_owl_oneOf, Y_21), true, true, true), true)=true))). % 33.13/22.15 tff(c_7781, 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))). % 33.13/22.15 tff(c_12139, 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))). % 33.13/22.15 tff(c_12539, 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))). % 33.13/22.15 tff(c_6776, 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))). % 33.13/22.15 tff(c_12288, 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))). % 33.13/22.15 tff(c_11451, 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))). % 33.13/22.15 tff(c_11567, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, uri_ex_p, uri_rdf_Property), true, true, true), true)=true))). % 33.13/22.15 tff(c_11852, 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))). % 33.13/22.15 tff(c_12067, 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))). % 33.13/22.15 tff(c_11660, 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))). % 33.13/22.15 tff(c_14623, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, sK3_testcase_premise_fullish_026_Inferred_Property_Characteristics_I_BNODE_x1, uri_rdfs_Class), true, true, true), true)=true))). % 33.13/22.15 tff(c_12019, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, sK1_testcase_premise_fullish_026_Inferred_Property_Characteristics_I_BNODE_x2, uri_rdfs_Class), true, true, true), true)=true))). % 33.13/22.15 tff(c_12396, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, sK2_testcase_premise_fullish_026_Inferred_Property_Characteristics_I_BNODE_l2, uri_rdf_List), true, true, true), true)=true))). % 33.13/22.15 tff(c_11899, 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))). % 33.13/22.15 tff(c_11780, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, sK4_testcase_premise_fullish_026_Inferred_Property_Characteristics_I_BNODE_l1, uri_rdf_List), true, true, true), true)=true))). % 33.13/22.15 tff(c_4308, 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))). % 33.13/22.15 tff(c_4154, 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))). % 33.13/22.15 tff(c_65194, plain, (![X_1166, Y_1167]: (ifeq(iext(uri_rdf_type, X_1166, Y_1167), true, iext(uri_rdf_type, X_1166, Y_1167), true)=true))). % 33.13/22.15 tff(c_8966, 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))). % 33.13/22.15 tff(c_5005, 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))). % 33.13/22.15 tff(c_10724, 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))). % 33.13/22.15 tff(c_64663, plain, (![C_1161]: (ifeq(iext(uri_rdfs_subClassOf, C_1161, uri_rdf_XMLLiteral), true, iext(uri_rdfs_subClassOf, C_1161, uri_rdfs_Resource), true)=true))). % 33.13/22.15 tff(c_64636, plain, (![X_1157, Y_1158]: (ifeq(iext(uri_rdf_value, X_1157, Y_1158), true, iext(uri_rdf_value, X_1157, Y_1158), true)=true))). % 33.13/22.15 tff(c_4157, 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))). % 33.13/22.15 tff(c_6344, 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))). % 33.13/22.15 tff(c_64319, plain, (![X_1150, Y_1151]: (ifeq(iext(uri_rdf_rest, X_1150, Y_1151), true, iext(uri_rdf_rest, X_1150, Y_1151), true)=true))). % 33.13/22.15 tff(c_64290, plain, (![X_1146, Y_1147]: (ifeq(iext(uri_rdf__2, X_1146, Y_1147), true, iext(uri_rdfs_member, X_1146, Y_1147), true)=true))). % 33.13/22.15 tff(c_64136, plain, (![C_1144]: (ifeq(iext(uri_rdfs_subClassOf, C_1144, uri_rdf_Alt), true, iext(uri_rdfs_subClassOf, C_1144, uri_rdfs_Resource), true)=true))). % 33.13/22.15 tff(c_63803, plain, (![X_1140, Y_1141]: (ifeq(iext(uri_rdfs_range, X_1140, Y_1141), true, iext(uri_rdfs_range, X_1140, Y_1141), true)=true))). % 33.13/22.15 tff(c_63603, plain, (![P_1136]: (ifeq(iext(uri_rdfs_subPropertyOf, P_1136, uri_rdf__1), true, iext(uri_rdfs_subPropertyOf, P_1136, uri_rdfs_member), true)=true))). % 33.13/22.15 tff(c_4112, 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))). % 33.13/22.15 tff(c_4360, 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))). % 33.13/22.15 tff(c_63435, plain, (![X_1130, Y_1131]: (ifeq(iext(uri_rdfs_isDefinedBy, X_1130, Y_1131), true, iext(uri_rdfs_isDefinedBy, X_1130, Y_1131), true)=true))). % 33.13/22.15 tff(c_6595, 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))). % 33.13/22.15 tff(c_63287, plain, (![X_1125, Y_1126]: (ifeq(iext(uri_rdf__2, X_1125, Y_1126), true, iext(uri_rdf__2, X_1125, Y_1126), true)=true))). % 33.13/22.15 tff(c_62605, plain, (![X_1121, Y_1122]: (ifeq(iext(uri_rdfs_subClassOf, X_1121, Y_1122), true, iext(uri_rdfs_subClassOf, X_1121, Y_1122), true)=true))). % 33.13/22.15 tff(c_7556, 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))). % 33.13/22.15 tff(c_10477, 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))). % 33.13/22.15 tff(c_61955, plain, (![C_1115]: (ifeq(iext(uri_rdfs_subClassOf, C_1115, uri_rdf_Property), true, iext(uri_rdfs_subClassOf, C_1115, uri_rdfs_Resource), true)=true))). % 33.13/22.15 tff(c_4510, 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))). % 33.13/22.15 tff(c_8294, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, uri_owl_oneOf, uri_rdf_Property), true, true, true), true)=true))). % 33.13/22.15 tff(c_61355, plain, (![X_1108, Y_1109]: (ifeq(iext(uri_rdfs_domain, X_1108, Y_1109), true, iext(uri_rdfs_domain, X_1108, Y_1109), true)=true))). % 33.13/22.15 tff(c_6454, 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))). % 33.13/22.15 tff(c_60951, plain, (![C_1104]: (ifeq(iext(uri_rdfs_subClassOf, C_1104, uri_rdfs_Class), true, iext(uri_rdfs_subClassOf, C_1104, uri_rdfs_Resource), true)=true))). % 33.13/22.15 tff(c_8101, 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))). % 33.13/22.15 tff(c_10050, 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))). % 33.13/22.15 tff(c_60799, plain, (![X_1099, Y_1100]: (ifeq(iext(uri_rdf_object, X_1099, Y_1100), true, iext(uri_rdf_object, X_1099, Y_1100), true)=true))). % 33.13/22.15 tff(c_60636, plain, (![C_1097]: (ifeq(iext(uri_rdfs_subClassOf, C_1097, uri_rdfs_Literal), true, iext(uri_rdfs_subClassOf, C_1097, uri_rdfs_Resource), true)=true))). % 33.13/22.15 tff(c_4507, 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))). % 33.13/22.15 tff(c_6150, 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))). % 33.13/22.15 tff(c_4069, 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))). % 33.13/22.15 tff(c_5507, 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))). % 33.13/22.15 tff(c_60083, plain, (![X_1087, Y_1088]: (ifeq(iext(uri_rdf__3, X_1087, Y_1088), true, iext(uri_rdfs_member, X_1087, Y_1088), true)=true))). % 33.13/22.15 tff(c_4109, 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))). % 33.13/22.15 tff(c_59784, plain, (![C_1083]: (ifeq(iext(uri_rdfs_subClassOf, C_1083, uri_rdf_Bag), true, iext(uri_rdfs_subClassOf, C_1083, uri_rdfs_Resource), true)=true))). % 33.13/22.15 tff(c_5247, 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))). % 33.13/22.15 tff(c_4252, 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))). % 33.13/22.15 tff(c_59351, plain, (![C_1078]: (ifeq(iext(uri_rdfs_subClassOf, C_1078, uri_rdfs_Container), true, iext(uri_rdfs_subClassOf, C_1078, uri_rdfs_Resource), true)=true))). % 33.13/22.15 tff(c_6996, 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))). % 33.13/22.15 tff(c_5438, 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))). % 33.13/22.15 tff(c_59082, plain, (![X_1072, Y_1073]: (ifeq(iext(uri_rdf__3, X_1072, Y_1073), true, iext(uri_rdf__3, X_1072, Y_1073), true)=true))). % 33.13/22.15 tff(c_7724, 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))). % 33.13/22.16 tff(c_5601, 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))). % 33.13/22.16 tff(c_10315, 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))). % 33.13/22.16 tff(c_58662, plain, (![X_1065, Y_1066]: (ifeq(iext(uri_owl_oneOf, X_1065, Y_1066), true, iext(uri_owl_oneOf, X_1065, Y_1066), true)=true))). % 33.13/22.16 tff(c_4249, 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))). % 33.13/22.16 tff(c_58191, plain, (![X_1057, Y_1058]: (ifeq(iext(uri_rdf__1, X_1057, Y_1058), true, iext(uri_rdfs_member, X_1057, Y_1058), true)=true))). % 33.13/22.16 tff(c_8416, 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))). % 33.13/22.16 tff(c_9419, 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))). % 33.13/22.16 tff(c_7159, 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))). % 33.13/22.16 tff(c_8624, 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))). % 33.13/22.16 tff(c_4460, 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))). % 33.13/22.16 tff(c_4414, 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))). % 33.13/22.16 tff(c_57278, plain, (![C_1047]: (ifeq(iext(uri_rdfs_subClassOf, C_1047, uri_rdfs_Datatype), true, iext(uri_rdfs_subClassOf, C_1047, uri_rdfs_Resource), true)=true))). % 33.13/22.16 tff(c_57210, plain, (![P_1045]: (ifeq(iext(uri_rdfs_subPropertyOf, P_1045, uri_rdf__3), true, iext(uri_rdfs_subPropertyOf, P_1045, uri_rdfs_member), true)=true))). % 33.13/22.16 tff(c_5874, 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))). % 33.13/22.16 tff(c_11297, 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))). % 33.13/22.16 tff(c_7088, 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))). % 33.13/22.16 tff(c_56447, plain, (![C_1038]: (ifeq(iext(uri_rdfs_subClassOf, C_1038, uri_rdfs_ContainerMembershipProperty), true, iext(uri_rdfs_subClassOf, C_1038, uri_rdfs_Resource), true)=true))). % 33.13/22.16 tff(c_4311, 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))). % 33.13/22.16 tff(c_6927, 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))). % 33.13/22.16 tff(c_55626, plain, (![X_1031, Y_1032]: (ifeq(iext(uri_rdfs_subPropertyOf, X_1031, Y_1032), true, iext(uri_rdfs_subPropertyOf, X_1031, Y_1032), true)=true))). % 33.13/22.16 tff(c_4417, 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))). % 33.13/22.16 tff(c_9686, 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))). % 33.13/22.16 tff(c_5774, 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))). % 33.13/22.16 tff(c_8186, 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))). % 33.13/22.16 tff(c_4782, 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))). % 33.13/22.16 tff(c_4357, 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))). % 33.13/22.16 tff(c_54111, plain, (![C_1017]: (ifeq(iext(uri_rdfs_subClassOf, C_1017, uri_rdfs_Seq), true, iext(uri_rdfs_subClassOf, C_1017, uri_rdfs_Resource), true)=true))). % 33.13/22.16 tff(c_7341, 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))). % 33.13/22.16 tff(c_9139, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subPropertyOf), true, ifeq(iext(P_47, uri_owl_oneOf, uri_owl_oneOf), true, true, true), true)=true))). % 33.13/22.16 tff(c_8482, 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))). % 33.13/22.16 tff(c_53122, plain, (![X_1006, Y_1007]: (ifeq(iext(uri_rdfs_seeAlso, X_1006, Y_1007), true, iext(uri_rdfs_seeAlso, X_1006, Y_1007), true)=true))). % 33.13/22.16 tff(c_8034, 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))). % 33.13/22.16 tff(c_52644, plain, (![X_999, Y_1000]: (ifeq(iext(uri_rdf_first, X_999, Y_1000), true, iext(uri_rdf_first, X_999, Y_1000), true)=true))). % 33.13/22.16 tff(c_52390, plain, (![X_993, Y_994]: (ifeq(iext(uri_rdf__1, X_993, Y_994), true, iext(uri_rdf__1, X_993, Y_994), true)=true))). % 33.13/22.16 tff(c_9233, 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))). % 33.13/22.16 tff(c_4708, 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))). % 33.13/22.16 tff(c_9074, 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))). % 33.13/22.16 tff(c_5181, 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))). % 33.13/22.16 tff(c_8795, 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))). % 33.13/22.16 tff(c_51139, plain, (![P_982]: (ifeq(iext(uri_rdfs_subPropertyOf, P_982, uri_rdf__2), true, iext(uri_rdfs_subPropertyOf, P_982, uri_rdfs_member), true)=true))). % 33.13/22.16 tff(c_7660, 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))). % 33.13/22.16 tff(c_11099, 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))). % 33.13/22.16 tff(c_7489, 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))). % 33.13/22.16 tff(c_50142, plain, (![X_971, Y_972]: (ifeq(iext(uri_rdf_subject, X_971, Y_972), true, iext(uri_rdf_subject, X_971, Y_972), true)=true))). % 33.13/22.16 tff(c_9979, 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))). % 33.13/22.16 tff(c_5672, 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))). % 33.13/22.16 tff(c_4463, 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))). % 33.13/22.16 tff(c_4066, 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))). % 33.13/22.16 tff(c_6513, 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))). % 33.13/22.16 tff(c_12356, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdf_List), true, ifeq(iext(P_18, sK2_testcase_premise_fullish_026_Inferred_Property_Characteristics_I_BNODE_l2, Y_21), true, true, true), true)=true))). % 33.13/22.16 tff(c_14381, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdfs_Class), true, ifeq(iext(P_28, X_30, sK3_testcase_premise_fullish_026_Inferred_Property_Characteristics_I_BNODE_x1), true, true, true), true)=true))). % 33.28/22.16 tff(c_7240, 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))). % 33.28/22.16 tff(c_11048, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdf_List), true, ifeq(iext(P_18, sK4_testcase_premise_fullish_026_Inferred_Property_Characteristics_I_BNODE_l1, Y_21), true, true, true), true)=true))). % 33.28/22.16 tff(c_10807, 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))). % 33.28/22.16 tff(c_7851, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdfs_Class), true, ifeq(iext(P_18, sK1_testcase_premise_fullish_026_Inferred_Property_Characteristics_I_BNODE_x2, Y_21), true, true, true), true)=true))). % 33.28/22.16 tff(c_14384, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdfs_Class), true, ifeq(iext(P_18, sK3_testcase_premise_fullish_026_Inferred_Property_Characteristics_I_BNODE_x1, Y_21), true, true, true), true)=true))). % 33.28/22.16 tff(c_6651, 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))). % 33.28/22.16 tff(c_9480, 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))). % 33.28/22.16 tff(c_6030, 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))). % 33.28/22.16 tff(c_6302, 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))). % 33.28/22.16 tff(c_10804, 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))). % 33.28/22.16 tff(c_8857, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdf_Property), true, ifeq(iext(P_18, uri_ex_p, Y_21), true, true, true), true)=true))). % 33.28/22.16 tff(c_7848, 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_026_Inferred_Property_Characteristics_I_BNODE_x2), true, true, true), true)=true))). % 33.28/22.16 tff(c_6882, 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))). % 33.28/22.16 tff(c_7237, 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))). % 33.28/22.16 tff(c_12353, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdf_List), true, ifeq(iext(P_28, X_30, sK2_testcase_premise_fullish_026_Inferred_Property_Characteristics_I_BNODE_l2), true, true, true), true)=true))). % 33.28/22.17 tff(c_9749, 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))). % 33.28/22.17 tff(c_9477, 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))). % 33.28/22.17 tff(c_6299, 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))). % 33.28/22.17 tff(c_11045, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdf_List), true, ifeq(iext(P_28, X_30, sK4_testcase_premise_fullish_026_Inferred_Property_Characteristics_I_BNODE_l1), true, true, true), true)=true))). % 33.28/22.17 tff(c_8854, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdf_Property), true, ifeq(iext(P_28, X_30, uri_ex_p), true, true, true), true)=true))). % 33.28/22.17 tff(c_6885, 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))). % 33.28/22.17 tff(c_9746, 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))). % 33.28/22.17 tff(c_6654, 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))). % 33.28/22.17 tff(c_6027, 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))). % 33.28/22.17 tff(c_4635, plain, (![P_47, X_132]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, X_132, uri_rdfs_Resource), true, true, true), true)=true))). % 33.28/22.17 tff(c_3694, 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))). % 33.28/22.17 tff(c_3697, 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))). % 33.28/22.17 tff(c_3486, 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))). % 33.28/22.17 tff(c_3976, 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))). % 33.28/22.17 tff(c_3457, 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))). % 33.28/22.17 tff(c_3890, 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))). % 33.28/22.17 tff(c_3929, 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))). % 33.28/22.17 tff(c_3774, 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))). % 33.28/22.17 tff(c_3849, 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))). % 33.28/22.17 tff(c_3611, 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))). % 33.28/22.17 tff(c_3736, 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))). % 33.28/22.17 tff(c_3534, 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))). % 33.28/22.17 tff(c_3733, 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))). % 33.28/22.17 tff(c_3483, 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))). % 33.28/22.17 tff(c_4016, 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))). % 33.28/22.17 tff(c_3656, 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))). % 33.28/22.17 tff(c_3815, 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))). % 33.28/22.17 tff(c_3568, 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))). % 33.28/22.17 tff(c_3531, 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))). % 33.28/22.17 tff(c_4013, 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))). % 33.28/22.17 tff(c_3979, 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))). % 33.28/22.17 tff(c_3887, 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))). % 33.28/22.17 tff(c_3852, 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))). % 33.28/22.17 tff(c_3812, 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))). % 33.28/22.17 tff(c_3777, 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))). % 33.28/22.17 tff(c_3608, 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))). % 33.28/22.17 tff(c_3571, 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))). % 33.28/22.17 tff(c_3932, 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))). % 33.28/22.17 tff(c_3460, 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))). % 33.28/22.17 tff(c_3653, 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))). % 33.28/22.17 tff(c_2089, plain, (![P_95, X_97, X_60]: (ifeq(iext(uri_rdfs_range, P_95, uri_rdfs_Resource), true, ifeq(iext(P_95, X_97, X_60), true, true, true), true)=true))). % 33.28/22.17 tff(c_1668, plain, (![P_91, X_60, Y_94]: (ifeq(iext(uri_rdfs_domain, P_91, uri_rdfs_Resource), true, ifeq(iext(P_91, X_60, Y_94), true, true, true), true)=true))). % 33.28/22.17 tff(c_2682, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_range), true, ifeq(iext(P_102, uri_rdf_subject, uri_rdfs_Resource), true, true, true), true)=true))). % 33.28/22.17 tff(c_2853, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_range), true, ifeq(iext(P_102, uri_rdf__1, uri_rdfs_Resource), true, true, true), true)=true))). % 33.28/22.17 tff(c_2676, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_domain), true, ifeq(iext(P_102, uri_rdfs_comment, uri_rdfs_Resource), true, true, true), true)=true))). % 33.28/22.17 tff(c_2532, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_domain), true, ifeq(iext(P_102, uri_rdf_type, uri_rdfs_Resource), true, true, true), true)=true))). % 33.28/22.17 tff(c_2604, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdf_type), true, ifeq(iext(P_102, uri_rdf__1, uri_rdf_Property), true, true, true), true)=true))). % 33.28/22.17 tff(c_2634, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_domain), true, ifeq(iext(P_102, uri_ex_p, sK3_testcase_premise_fullish_026_Inferred_Property_Characteristics_I_BNODE_x1), true, true, true), true)=true))). % 33.28/22.17 tff(c_38471, plain, (![C_828]: (ifeq(iext(uri_rdfs_subClassOf, C_828, uri_rdf_Bag), true, iext(uri_rdfs_subClassOf, C_828, uri_rdfs_Container), true)=true))). % 33.28/22.17 tff(c_2769, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_domain), true, ifeq(iext(P_102, uri_rdf__2, uri_rdfs_Resource), true, true, true), true)=true))). % 33.28/22.17 tff(c_2895, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_subClassOf), true, ifeq(iext(P_102, uri_rdf_Alt, uri_rdfs_Container), true, true, true), true)=true))). % 33.28/22.17 tff(c_2865, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_range), true, ifeq(iext(P_102, uri_rdf_rest, uri_rdf_List), true, true, true), true)=true))). % 33.28/22.17 tff(c_2829, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_domain), true, ifeq(iext(P_102, uri_rdf__1, uri_rdfs_Resource), true, true, true), true)=true))). % 33.28/22.17 tff(c_2739, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdf_rest), true, ifeq(iext(P_102, sK2_testcase_premise_fullish_026_Inferred_Property_Characteristics_I_BNODE_l2, uri_rdf_nil), true, true, true), true)=true))). % 33.28/22.17 tff(c_2610, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdf_type), true, ifeq(iext(P_102, uri_rdf_object, uri_rdf_Property), true, true, true), true)=true))). % 33.28/22.17 tff(c_2781, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_domain), true, ifeq(iext(P_102, uri_rdfs_member, uri_rdfs_Resource), true, true, true), true)=true))). % 33.28/22.17 tff(c_2550, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdf_first), true, ifeq(iext(P_102, sK2_testcase_premise_fullish_026_Inferred_Property_Characteristics_I_BNODE_l2, uri_ex_u), true, true, true), true)=true))). % 33.28/22.17 tff(c_2817, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_range), true, ifeq(iext(P_102, uri_rdf_value, uri_rdfs_Resource), true, true, true), true)=true))). % 33.28/22.17 tff(c_2787, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_subClassOf), true, ifeq(iext(P_102, uri_rdfs_ContainerMembershipProperty, uri_rdf_Property), true, true, true), true)=true))). % 33.28/22.17 tff(c_2718, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdf_type), true, ifeq(iext(P_102, uri_rdf_XMLLiteral, uri_rdfs_Datatype), true, true, true), true)=true))). % 33.28/22.17 tff(c_2775, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_range), true, ifeq(iext(P_102, uri_ex_p, sK1_testcase_premise_fullish_026_Inferred_Property_Characteristics_I_BNODE_x2), true, true, true), true)=true))). % 33.28/22.17 tff(c_2694, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_domain), true, ifeq(iext(P_102, uri_rdfs_domain, uri_rdf_Property), true, true, true), true)=true))). % 33.28/22.17 tff(c_2670, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdf_type), true, ifeq(iext(P_102, uri_rdf__3, uri_rdfs_ContainerMembershipProperty), true, true, true), true)=true))). % 33.28/22.17 tff(c_2733, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_subPropertyOf), true, ifeq(iext(P_102, uri_rdfs_isDefinedBy, uri_rdfs_seeAlso), true, true, true), true)=true))). % 33.28/22.17 tff(c_2562, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdf_type), true, ifeq(iext(P_102, uri_rdf_nil, uri_rdf_List), true, true, true), true)=true))). % 33.28/22.17 tff(c_36330, plain, (![C_809]: (ifeq(iext(uri_rdfs_subClassOf, C_809, uri_rdfs_ContainerMembershipProperty), true, iext(uri_rdfs_subClassOf, C_809, uri_rdf_Property), true)=true))). % 33.28/22.17 tff(c_2847, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_range), true, ifeq(iext(P_102, uri_rdf_predicate, uri_rdfs_Resource), true, true, true), true)=true))). % 33.28/22.17 tff(c_2751, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_domain), true, ifeq(iext(P_102, uri_rdfs_isDefinedBy, uri_rdfs_Resource), true, true, true), true)=true))). % 33.28/22.17 tff(c_36172, plain, (![X_804, Y_805]: (ifeq(iext(uri_rdfs_isDefinedBy, X_804, Y_805), true, iext(uri_rdfs_seeAlso, X_804, Y_805), true)=true))). % 33.28/22.17 tff(c_2931, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdf_rest), true, ifeq(iext(P_102, sK4_testcase_premise_fullish_026_Inferred_Property_Characteristics_I_BNODE_l1, uri_rdf_nil), true, true, true), true)=true))). % 33.28/22.17 tff(c_2706, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_subClassOf), true, ifeq(iext(P_102, uri_rdfs_Seq, uri_rdfs_Container), true, true, true), true)=true))). % 33.28/22.17 tff(c_2646, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_owl_oneOf), true, ifeq(iext(P_102, sK1_testcase_premise_fullish_026_Inferred_Property_Characteristics_I_BNODE_x2, sK2_testcase_premise_fullish_026_Inferred_Property_Characteristics_I_BNODE_l2), true, true, true), true)=true))). % 33.28/22.17 tff(c_2658, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_domain), true, ifeq(iext(P_102, uri_rdf__3, uri_rdfs_Resource), true, true, true), true)=true))). % 33.28/22.17 tff(c_35616, plain, (![C_798]: (ifeq(iext(uri_rdfs_subClassOf, C_798, uri_rdf_Alt), true, iext(uri_rdfs_subClassOf, C_798, uri_rdfs_Container), true)=true))). % 33.28/22.17 tff(c_2640, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_domain), true, ifeq(iext(P_102, uri_rdfs_subPropertyOf, uri_rdf_Property), true, true, true), true)=true))). % 33.28/22.17 tff(c_2883, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_domain), true, ifeq(iext(P_102, uri_rdf_predicate, uri_rdfs_Statement), true, true, true), true)=true))). % 33.28/22.17 tff(c_2688, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_range), true, ifeq(iext(P_102, uri_rdfs_isDefinedBy, uri_rdfs_Resource), true, true, true), true)=true))). % 33.28/22.17 tff(c_35052, plain, (![C_792]: (ifeq(iext(uri_rdfs_subClassOf, C_792, uri_rdfs_Seq), true, iext(uri_rdfs_subClassOf, C_792, uri_rdfs_Container), true)=true))). % 33.28/22.17 tff(c_2568, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdf_type), true, ifeq(iext(P_102, uri_rdf_first, uri_rdf_Property), true, true, true), true)=true))). % 33.28/22.17 tff(c_2724, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_subClassOf), true, ifeq(iext(P_102, uri_rdf_Bag, uri_rdfs_Container), true, true, true), true)=true))). % 33.28/22.17 tff(c_34881, plain, (![P_789]: (ifeq(iext(uri_rdfs_subPropertyOf, P_789, uri_rdfs_isDefinedBy), true, iext(uri_rdfs_subPropertyOf, P_789, uri_rdfs_seeAlso), true)=true))). % 33.28/22.17 tff(c_2664, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_domain), true, ifeq(iext(P_102, uri_rdfs_range, uri_rdf_Property), true, true, true), true)=true))). % 33.28/22.17 tff(c_2556, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_subClassOf), true, ifeq(iext(P_102, uri_rdf_XMLLiteral, uri_rdfs_Literal), true, true, true), true)=true))). % 33.28/22.17 tff(c_2859, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdf_type), true, ifeq(iext(P_102, uri_rdf__2, uri_rdfs_ContainerMembershipProperty), true, true, true), true)=true))). % 33.28/22.17 tff(c_2586, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_domain), true, ifeq(iext(P_102, uri_rdf_value, uri_rdfs_Resource), true, true, true), true)=true))). % 33.28/22.18 tff(c_2835, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_range), true, ifeq(iext(P_102, uri_rdf__2, uri_rdfs_Resource), true, true, true), true)=true))). % 33.28/22.18 tff(c_2871, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdf_type), true, ifeq(iext(P_102, uri_rdf_rest, uri_rdf_Property), true, true, true), true)=true))). % 33.28/22.18 tff(c_2913, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_domain), true, ifeq(iext(P_102, uri_rdf_object, uri_rdfs_Statement), true, true, true), true)=true))). % 33.28/22.18 tff(c_2757, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdf_type), true, ifeq(iext(P_102, uri_rdf__1, uri_rdfs_ContainerMembershipProperty), true, true, true), true)=true))). % 33.28/22.18 tff(c_33832, plain, (![D_779]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_779), true, icext(D_779, uri_rdfs_member), true)=true))). % 33.28/22.18 tff(c_33637, plain, (![D_776]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_776), true, icext(D_776, uri_rdfs_Resource), true)=true))). % 33.28/22.18 tff(c_2745, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_range), true, ifeq(iext(P_102, uri_rdf__3, uri_rdfs_Resource), true, true, true), true)=true))). % 33.28/22.18 tff(c_33569, plain, (![D_774]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_774), true, icext(D_774, uri_owl_oneOf), true)=true))). % 33.28/22.18 tff(c_33503, plain, (![D_772]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_772), true, icext(D_772, uri_rdfs_subPropertyOf), true)=true))). % 33.28/22.18 tff(c_2793, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_domain), true, ifeq(iext(P_102, uri_rdfs_label, uri_rdfs_Resource), true, true, true), true)=true))). % 33.28/22.18 tff(c_33310, plain, (![D_769]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_769), true, icext(D_769, uri_rdfs_isDefinedBy), true)=true))). % 33.28/22.18 tff(c_33243, plain, (![D_767]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_767), true, icext(D_767, uri_rdfs_seeAlso), true)=true))). % 33.28/22.18 tff(c_2652, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_range), true, ifeq(iext(P_102, uri_rdf_type, uri_rdfs_Class), true, true, true), true)=true))). % 33.28/22.18 tff(c_33057, plain, (![D_764]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_764), true, icext(D_764, uri_rdfs_Container), true)=true))). % 33.28/22.18 tff(c_32991, plain, (![D_762]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_762), true, icext(D_762, uri_rdfs_ContainerMembershipProperty), true)=true))). % 33.28/22.18 tff(c_32925, plain, (![D_760]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_760), true, icext(D_760, uri_rdfs_Seq), true)=true))). % 33.28/22.18 tff(c_2616, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdf_type), true, ifeq(iext(P_102, uri_rdf__3, uri_rdf_Property), true, true, true), true)=true))). % 33.28/22.18 tff(c_32739, plain, (![D_757]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_757), true, icext(D_757, uri_rdf_Alt), true)=true))). % 33.28/22.18 tff(c_32665, plain, (![D_755]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_755), true, icext(D_755, uri_rdf_XMLLiteral), true)=true))). % 33.28/22.18 tff(c_2580, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_range), true, ifeq(iext(P_102, uri_rdfs_subClassOf, uri_rdfs_Class), true, true, true), true)=true))). % 33.28/22.18 tff(c_32473, plain, (![D_752]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_752), true, icext(D_752, uri_rdfs_Literal), true)=true))). % 33.28/22.18 tff(c_32407, plain, (![D_750]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_750), true, icext(D_750, uri_rdf_Bag), true)=true))). % 33.28/22.18 tff(c_32215, plain, (![D_747]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_747), true, icext(D_747, uri_rdfs_Datatype), true)=true))). % 33.28/22.18 tff(c_2901, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_subClassOf), true, ifeq(iext(P_102, uri_rdfs_Datatype, uri_rdfs_Class), true, true, true), true)=true))). % 33.28/22.18 tff(c_32118, plain, (![D_745]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_745), true, icext(D_745, uri_rdfs_Class), true)=true))). % 33.28/22.18 tff(c_2823, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_range), true, ifeq(iext(P_102, uri_rdfs_member, uri_rdfs_Resource), true, true, true), true)=true))). % 33.28/22.18 tff(c_31919, plain, (![D_742]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_742), true, icext(D_742, uri_rdfs_range), true)=true))). % 33.28/22.18 tff(c_31853, plain, (![D_740]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_740), true, icext(D_740, uri_rdfs_label), true)=true))). % 33.28/22.18 tff(c_2907, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_domain), true, ifeq(iext(P_102, uri_rdf_subject, uri_rdfs_Statement), true, true, true), true)=true))). % 33.28/22.18 tff(c_31665, plain, (![D_737]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_737), true, icext(D_737, uri_rdfs_comment), true)=true))). % 33.28/22.18 tff(c_31599, plain, (![D_735]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_735), true, icext(D_735, uri_rdfs_Statement), true)=true))). % 33.28/22.18 tff(c_31409, plain, (![D_732]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_List, D_732), true, icext(D_732, sK4_testcase_premise_fullish_026_Inferred_Property_Characteristics_I_BNODE_l1), true)=true))). % 33.28/22.18 tff(c_2538, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_domain), true, ifeq(iext(P_102, uri_rdfs_subClassOf, uri_rdfs_Class), true, true, true), true)=true))). % 33.28/22.18 tff(c_31342, plain, (![D_730]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_List, D_730), true, icext(D_730, sK2_testcase_premise_fullish_026_Inferred_Property_Characteristics_I_BNODE_l2), true)=true))). % 33.28/22.18 tff(c_31276, plain, (![D_728]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_728), true, icext(D_728, uri_ex_p), true)=true))). % 33.28/22.18 tff(c_2628, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_domain), true, ifeq(iext(P_102, uri_rdf_first, uri_rdf_List), true, true, true), true)=true))). % 33.28/22.18 tff(c_31090, plain, (![D_725]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_725), true, icext(D_725, sK1_testcase_premise_fullish_026_Inferred_Property_Characteristics_I_BNODE_x2), true)=true))). % 33.28/22.18 tff(c_31024, plain, (![D_723]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_723), true, icext(D_723, sK3_testcase_premise_fullish_026_Inferred_Property_Characteristics_I_BNODE_x1), true)=true))). % 33.28/22.18 tff(c_30958, plain, (![D_721]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_721), true, icext(D_721, uri_rdf_List), true)=true))). % 33.28/22.18 tff(c_2811, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_range), true, ifeq(iext(P_102, uri_rdf_first, uri_rdfs_Resource), true, true, true), true)=true))). % 33.28/22.18 tff(c_30767, plain, (![D_718]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_718), true, icext(D_718, uri_rdfs_domain), true)=true))). % 33.28/22.18 tff(c_14129, 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))). % 33.28/22.18 tff(c_30686, plain, (![D_715]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_715), true, icext(D_715, uri_rdfs_subClassOf), true)=true))). % 33.28/22.18 tff(c_14054, 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))). % 33.28/22.18 tff(c_13924, 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))). % 33.28/22.18 tff(c_2700, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_range), true, ifeq(iext(P_102, uri_rdfs_domain, uri_rdfs_Class), true, true, true), true)=true))). % 33.28/22.18 tff(c_13989, 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))). % 33.28/22.18 tff(c_13851, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_48), true, iext(Q_48, uri_ex_p, uri_ex_p), true)=true))). % 33.28/22.18 tff(c_13527, 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))). % 33.28/22.18 tff(c_13469, 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))). % 33.28/22.18 tff(c_2889, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdf_type), true, ifeq(iext(P_102, uri_rdf_type, uri_rdf_Property), true, true, true), true)=true))). % 33.28/22.18 tff(c_13785, 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))). % 33.28/22.18 tff(c_14772, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_48), true, iext(Q_48, sK3_testcase_premise_fullish_026_Inferred_Property_Characteristics_I_BNODE_x1, uri_rdfs_Resource), true)=true))). % 33.28/22.18 tff(c_30111, plain, (![D_697]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_697), true, icext(D_697, uri_rdf_predicate), true)=true))). % 33.28/22.18 tff(c_13328, 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))). % 33.28/22.18 tff(c_12835, 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))). % 33.28/22.18 tff(c_2622, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_domain), true, ifeq(iext(P_102, uri_rdf_rest, uri_rdf_List), true, true, true), true)=true))). % 33.28/22.18 tff(c_14770, plain, (![E_41]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Resource, E_41), true, iext(uri_rdfs_subClassOf, sK3_testcase_premise_fullish_026_Inferred_Property_Characteristics_I_BNODE_x1, E_41), true)=true))). % 33.28/22.18 tff(c_13239, 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))). % 33.28/22.18 tff(c_13330, 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))). % 33.28/22.18 tff(c_12957, plain, (![E_41]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Resource, E_41), true, iext(uri_rdfs_subClassOf, sK1_testcase_premise_fullish_026_Inferred_Property_Characteristics_I_BNODE_x2, E_41), true)=true))). % 33.28/22.18 tff(c_12837, 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))). % 33.28/22.18 tff(c_12959, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_48), true, iext(Q_48, sK1_testcase_premise_fullish_026_Inferred_Property_Characteristics_I_BNODE_x2, uri_rdfs_Resource), true)=true))). % 33.28/22.18 tff(c_13172, 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))). % 33.28/22.18 tff(c_14706, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_48), true, iext(Q_48, sK3_testcase_premise_fullish_026_Inferred_Property_Characteristics_I_BNODE_x1, sK3_testcase_premise_fullish_026_Inferred_Property_Characteristics_I_BNODE_x1), true)=true))). % 33.28/22.18 tff(c_13081, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_48), true, iext(Q_48, sK1_testcase_premise_fullish_026_Inferred_Property_Characteristics_I_BNODE_x2, sK1_testcase_premise_fullish_026_Inferred_Property_Characteristics_I_BNODE_x2), true)=true))). % 33.28/22.18 tff(c_12773, 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))). % 33.28/22.18 tff(c_12205, 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))). % 33.28/22.18 tff(c_29583, plain, (![C_677]: (ifeq(iext(uri_rdfs_subClassOf, C_677, uri_rdfs_Datatype), true, iext(uri_rdfs_subClassOf, C_677, uri_rdfs_Class), true)=true))). % 33.28/22.18 tff(c_12558, 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))). % 33.28/22.18 tff(c_12254, 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))). % 33.28/22.18 tff(c_12726, 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))). % 33.28/22.18 tff(c_12606, 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))). % 33.28/22.18 tff(c_12158, 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))). % 33.28/22.18 tff(c_12654, 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))). % 33.28/22.18 tff(c_12307, 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))). % 33.28/22.18 tff(c_11685, 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))). % 33.28/22.18 tff(c_2544, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_range), true, ifeq(iext(P_102, uri_rdfs_seeAlso, uri_rdfs_Resource), true, true, true), true)=true))). % 33.28/22.18 tff(c_11871, 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))). % 33.28/22.18 tff(c_11924, 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))). % 33.28/22.18 tff(c_12086, 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))). % 33.28/22.18 tff(c_29214, plain, (![D_663]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_List, D_663), true, icext(D_663, uri_rdf_nil), true)=true))). % 33.28/22.18 tff(c_11476, 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))). % 33.28/22.18 tff(c_12038, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, sK1_testcase_premise_fullish_026_Inferred_Property_Characteristics_I_BNODE_x2, uri_rdfs_Class), true)=true))). % 33.28/22.18 tff(c_12415, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, sK2_testcase_premise_fullish_026_Inferred_Property_Characteristics_I_BNODE_l2, uri_rdf_List), true)=true))). % 33.28/22.18 tff(c_2841, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdf_first), true, ifeq(iext(P_102, sK4_testcase_premise_fullish_026_Inferred_Property_Characteristics_I_BNODE_l1, uri_ex_w), true, true, true), true)=true))). % 33.28/22.18 tff(c_11799, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, sK4_testcase_premise_fullish_026_Inferred_Property_Characteristics_I_BNODE_l1, uri_rdf_List), true)=true))). % 33.28/22.18 tff(c_14642, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, sK3_testcase_premise_fullish_026_Inferred_Property_Characteristics_I_BNODE_x1, uri_rdfs_Class), true)=true))). % 33.28/22.18 tff(c_11592, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, uri_ex_p, uri_rdf_Property), true)=true))). % 33.28/22.18 tff(c_28938, plain, (![D_654]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_654), true, icext(D_654, uri_rdf_object), true)=true))). % 33.28/22.18 tff(c_6375, 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))). % 33.28/22.18 tff(c_11127, 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))). % 33.28/22.18 tff(c_5030, 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))). % 33.28/22.18 tff(c_2799, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_range), true, ifeq(iext(P_102, uri_rdfs_label, uri_rdfs_Literal), true, true, true), true)=true))). % 33.28/22.18 tff(c_4807, 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))). % 33.28/22.18 tff(c_5905, 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))). % 33.28/22.18 tff(c_28633, plain, (![D_645]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_645), true, icext(D_645, uri_rdf_subject), true)=true))). % 33.28/22.18 tff(c_8651, 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))). % 33.28/22.18 tff(c_10075, 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))). % 33.28/22.18 tff(c_7691, 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))). % 33.28/22.18 tff(c_2925, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_owl_oneOf), true, ifeq(iext(P_102, sK3_testcase_premise_fullish_026_Inferred_Property_Characteristics_I_BNODE_x1, sK4_testcase_premise_fullish_026_Inferred_Property_Characteristics_I_BNODE_l1), true, true, true), true)=true))). % 33.28/22.18 tff(c_4806, 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))). % 33.28/22.18 tff(c_7119, 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))). % 33.28/22.18 tff(c_28300, plain, (![D_636]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, D_636), true, icext(D_636, uri_rdf__1), true)=true))). % 33.28/22.18 tff(c_10502, 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))). % 33.28/22.18 tff(c_5805, 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))). % 33.28/22.19 tff(c_2763, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdf_type), true, ifeq(iext(P_102, uri_rdf_subject, uri_rdf_Property), true, true, true), true)=true))). % 33.28/22.19 tff(c_8217, 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))). % 33.28/22.19 tff(c_5469, 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))). % 33.28/22.19 tff(c_27972, plain, (![D_627]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, D_627), true, icext(D_627, uri_rdf__2), true)=true))). % 33.28/22.19 tff(c_7587, 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))). % 33.28/22.19 tff(c_7184, 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))). % 33.28/22.19 tff(c_2598, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_range), true, ifeq(iext(P_102, uri_rdfs_range, uri_rdfs_Class), true, true, true), true)=true))). % 33.28/22.19 tff(c_11324, 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))). % 33.28/22.19 tff(c_10347, 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))). % 33.28/22.19 tff(c_9444, 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))). % 33.28/22.19 tff(c_6544, 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))). % 33.28/22.19 tff(c_8441, 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))). % 33.28/22.19 tff(c_9106, 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))). % 33.28/22.19 tff(c_8821, 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))). % 33.28/22.19 tff(c_5205, 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))). % 33.28/22.19 tff(c_6479, 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))). % 33.28/22.19 tff(c_27501, plain, (![D_610]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_610), true, icext(D_610, uri_rdf_Property), true)=true))). % 33.28/22.19 tff(c_7520, 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))). % 33.28/22.19 tff(c_8649, 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))). % 33.28/22.19 tff(c_4738, 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))). % 33.28/22.19 tff(c_9258, 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))). % 33.28/22.19 tff(c_27289, plain, (![D_602]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_602), true, icext(D_602, uri_rdf_first), true)=true))). % 33.28/22.19 tff(c_7588, 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))). % 33.28/22.19 tff(c_2592, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_domain), true, ifeq(iext(P_102, uri_rdfs_seeAlso, uri_rdfs_Resource), true, true, true), true)=true))). % 33.28/22.19 tff(c_9170, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_48), true, iext(Q_48, uri_owl_oneOf, uri_owl_oneOf), true)=true))). % 33.28/22.19 tff(c_10010, 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))). % 33.28/22.19 tff(c_8993, 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))). % 33.28/22.19 tff(c_5698, 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))). % 33.28/22.19 tff(c_8510, 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))). % 33.28/22.19 tff(c_8128, 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))). % 33.28/22.19 tff(c_2805, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdf_type), true, ifeq(iext(P_102, uri_rdf_value, uri_rdf_Property), true, true, true), true)=true))). % 33.28/22.19 tff(c_11322, 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))). % 33.28/22.19 tff(c_10346, 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))). % 33.28/22.19 tff(c_26674, plain, (![D_584]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_584), true, icext(D_584, uri_rdf__2), true)=true))). % 33.28/22.19 tff(c_10077, 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))). % 33.28/22.19 tff(c_2919, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_range), true, ifeq(iext(P_102, uri_rdfs_subPropertyOf, uri_rdf_Property), true, true, true), true)=true))). % 33.28/22.19 tff(c_7366, 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))). % 33.28/22.19 tff(c_10751, 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))). % 33.28/22.19 tff(c_26341, plain, (![D_575]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_575), true, icext(D_575, uri_rdf__1), true)=true))). % 33.28/22.19 tff(c_6958, 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))). % 33.28/22.19 tff(c_9105, 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))). % 33.28/22.19 tff(c_7749, 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))). % 33.28/22.19 tff(c_2574, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdf_type), true, ifeq(iext(P_102, uri_rdf__2, uri_rdf_Property), true, true, true), true)=true))). % 33.28/22.19 tff(c_9711, 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))). % 33.28/22.19 tff(c_8062, 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))). % 33.28/22.19 tff(c_5272, 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))). % 33.28/22.19 tff(c_5531, 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))). % 33.28/22.19 tff(c_9713, 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))). % 33.28/22.19 tff(c_6620, 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))). % 33.28/22.19 tff(c_26017, plain, (![C_563]: (ifeq(iext(uri_rdfs_subClassOf, C_563, uri_rdf_XMLLiteral), true, iext(uri_rdfs_subClassOf, C_563, uri_rdfs_Literal), true)=true))). % 33.28/22.19 tff(c_9257, 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))). % 33.28/22.19 tff(c_8991, 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))). % 33.28/22.19 tff(c_6181, 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))). % 33.28/22.19 tff(c_8319, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, uri_owl_oneOf, uri_rdf_Property), true)=true))). % 33.28/22.19 tff(c_2877, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_range), true, ifeq(iext(P_102, uri_rdfs_comment, uri_rdfs_Literal), true, true, true), true)=true))). % 33.28/22.19 tff(c_7186, 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))). % 33.28/22.19 tff(c_7027, 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))). % 33.28/22.19 tff(c_5632, 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))). % 33.28/22.19 tff(c_5206, 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))). % 33.28/22.19 tff(c_2712, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdf_type), true, ifeq(iext(P_102, uri_rdf_Property, uri_rdfs_Class), true, true, true), true)=true))). % 33.28/22.19 tff(c_5532, 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))). % 33.28/22.19 tff(c_4655, plain, (![Q_48, X_132]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, X_132, uri_rdfs_Resource), true)=true))). % 33.28/22.19 tff(c_2947, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_103), true, iext(Q_103, uri_rdfs_range, uri_rdfs_Class), true)=true))). % 33.28/22.19 tff(c_2948, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_103), true, iext(Q_103, uri_rdf__1, uri_rdf_Property), true)=true))). % 33.28/22.19 tff(c_2961, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_103), true, iext(Q_103, uri_rdf_subject, uri_rdfs_Resource), true)=true))). % 33.28/22.19 tff(c_2999, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_103), true, iext(Q_103, uri_rdf_object, uri_rdfs_Statement), true)=true))). % 33.28/22.19 tff(c_3001, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_owl_oneOf, Q_103), true, iext(Q_103, sK3_testcase_premise_fullish_026_Inferred_Property_Characteristics_I_BNODE_x1, sK4_testcase_premise_fullish_026_Inferred_Property_Characteristics_I_BNODE_l1), true)=true))). % 33.28/22.19 tff(c_2940, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_103), true, iext(Q_103, uri_rdf_XMLLiteral, uri_rdfs_Literal), true)=true))). % 33.28/22.19 tff(c_2968, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_103), true, iext(Q_103, uri_rdf_Bag, uri_rdfs_Container), true)=true))). % 33.28/22.19 tff(c_2959, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_103), true, iext(Q_103, uri_rdf__3, uri_rdfs_ContainerMembershipProperty), true)=true))). % 33.28/22.19 tff(c_3104, plain, (![E_107]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Container, E_107), true, iext(uri_rdfs_subClassOf, uri_rdfs_Seq, E_107), true)=true))). % 33.28/22.19 tff(c_24952, plain, (![D_530]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_530), true, icext(D_530, uri_rdf_type), true)=true))). % 33.28/22.19 tff(c_2936, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_103), true, iext(Q_103, uri_rdf_type, uri_rdfs_Resource), true)=true))). % 33.28/22.19 tff(c_2994, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_103), true, iext(Q_103, uri_rdf_predicate, uri_rdfs_Statement), true)=true))). % 33.28/22.19 tff(c_2991, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_103), true, iext(Q_103, uri_rdf_rest, uri_rdf_List), true)=true))). % 33.28/22.19 tff(c_2967, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_103), true, iext(Q_103, uri_rdf_XMLLiteral, uri_rdfs_Datatype), true)=true))). % 33.28/22.19 tff(c_2937, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_103), true, iext(Q_103, uri_rdfs_subClassOf, uri_rdfs_Class), true)=true))). % 33.28/22.19 tff(c_2970, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_rest, Q_103), true, iext(Q_103, sK2_testcase_premise_fullish_026_Inferred_Property_Characteristics_I_BNODE_l2, uri_rdf_nil), true)=true))). % 33.28/22.19 tff(c_3108, plain, (![E_107]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, E_107), true, iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, E_107), true)=true))). % 33.28/22.19 tff(c_2951, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_103), true, iext(Q_103, uri_rdf_rest, uri_rdf_List), true)=true))). % 33.28/22.19 tff(c_2958, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_103), true, iext(Q_103, uri_rdfs_range, uri_rdf_Property), true)=true))). % 33.28/22.19 tff(c_2976, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_103), true, iext(Q_103, uri_ex_p, sK1_testcase_premise_fullish_026_Inferred_Property_Characteristics_I_BNODE_x2), true)=true))). % 33.28/22.19 tff(c_3103, plain, (![E_107]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Literal, E_107), true, iext(uri_rdfs_subClassOf, uri_rdf_XMLLiteral, E_107), true)=true))). % 33.28/22.19 tff(c_2990, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_103), true, iext(Q_103, uri_rdf__2, uri_rdfs_ContainerMembershipProperty), true)=true))). % 33.28/22.19 tff(c_2998, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_103), true, iext(Q_103, uri_rdf_subject, uri_rdfs_Statement), true)=true))). % 33.28/22.19 tff(c_2980, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_103), true, iext(Q_103, uri_rdfs_label, uri_rdfs_Literal), true)=true))). % 33.28/22.19 tff(c_2478, plain, (![R_100]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_seeAlso, R_100), true, iext(uri_rdfs_subPropertyOf, uri_rdfs_isDefinedBy, R_100), true)=true))). % 33.28/22.19 tff(c_2953, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_103), true, iext(Q_103, uri_ex_p, sK3_testcase_premise_fullish_026_Inferred_Property_Characteristics_I_BNODE_x1), true)=true))). % 33.28/22.19 tff(c_2987, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_first, Q_103), true, iext(Q_103, sK4_testcase_premise_fullish_026_Inferred_Property_Characteristics_I_BNODE_l1, uri_ex_w), true)=true))). % 33.28/22.19 tff(c_2944, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_103), true, iext(Q_103, uri_rdfs_subClassOf, uri_rdfs_Class), true)=true))). % 33.28/22.19 tff(c_3107, plain, (![E_107]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Container, E_107), true, iext(uri_rdfs_subClassOf, uri_rdf_Alt, E_107), true)=true))). % 33.28/22.19 tff(c_2996, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_103), true, iext(Q_103, uri_rdf_Alt, uri_rdfs_Container), true)=true))). % 33.28/22.19 tff(c_2979, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_103), true, iext(Q_103, uri_rdfs_label, uri_rdfs_Resource), true)=true))). % 33.28/22.19 tff(c_2997, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_103), true, iext(Q_103, uri_rdfs_Datatype, uri_rdfs_Class), true)=true))). % 33.28/22.19 tff(c_2983, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_103), true, iext(Q_103, uri_rdf_value, uri_rdfs_Resource), true)=true))). % 33.28/22.19 tff(c_3002, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_rest, Q_103), true, iext(Q_103, sK4_testcase_premise_fullish_026_Inferred_Property_Characteristics_I_BNODE_l1, uri_rdf_nil), true)=true))). % 33.28/22.19 tff(c_2993, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_103), true, iext(Q_103, uri_rdfs_comment, uri_rdfs_Literal), true)=true))). % 33.28/22.19 tff(c_24410, plain, (![D_503]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, D_503), true, icext(D_503, uri_rdf_XMLLiteral), true)=true))). % 33.28/22.19 tff(c_2946, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_103), true, iext(Q_103, uri_rdfs_seeAlso, uri_rdfs_Resource), true)=true))). % 33.28/22.19 tff(c_2963, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_103), true, iext(Q_103, uri_rdfs_domain, uri_rdf_Property), true)=true))). % 33.28/22.19 tff(c_2962, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_103), true, iext(Q_103, uri_rdfs_isDefinedBy, uri_rdfs_Resource), true)=true))). % 33.28/22.19 tff(c_2952, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_103), true, iext(Q_103, uri_rdf_first, uri_rdf_List), true)=true))). % 33.28/22.19 tff(c_2982, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_103), true, iext(Q_103, uri_rdf_first, uri_rdfs_Resource), true)=true))). % 33.28/22.19 tff(c_2943, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_103), true, iext(Q_103, uri_rdf__2, uri_rdf_Property), true)=true))). % 33.28/22.19 tff(c_2941, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_103), true, iext(Q_103, uri_rdf_nil, uri_rdf_List), true)=true))). % 33.28/22.19 tff(c_2938, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_103), true, iext(Q_103, uri_rdfs_seeAlso, uri_rdfs_Resource), true)=true))). % 33.28/22.19 tff(c_2955, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_owl_oneOf, Q_103), true, iext(Q_103, sK1_testcase_premise_fullish_026_Inferred_Property_Characteristics_I_BNODE_x2, sK2_testcase_premise_fullish_026_Inferred_Property_Characteristics_I_BNODE_l2), true)=true))). % 33.28/22.19 tff(c_2966, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_103), true, iext(Q_103, uri_rdf_Property, uri_rdfs_Class), true)=true))). % 33.28/22.19 tff(c_2950, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_103), true, iext(Q_103, uri_rdf__3, uri_rdf_Property), true)=true))). % 33.28/22.19 tff(c_2995, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_103), true, iext(Q_103, uri_rdf_type, uri_rdf_Property), true)=true))). % 33.28/22.19 tff(c_2957, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_103), true, iext(Q_103, uri_rdf__3, uri_rdfs_Resource), true)=true))). % 33.28/22.19 tff(c_2972, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_103), true, iext(Q_103, uri_rdfs_isDefinedBy, uri_rdfs_Resource), true)=true))). % 33.28/22.19 tff(c_2954, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_103), true, iext(Q_103, uri_rdfs_subPropertyOf, uri_rdf_Property), true)=true))). % 33.28/22.19 tff(c_2956, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_103), true, iext(Q_103, uri_rdf_type, uri_rdfs_Class), true)=true))). % 33.28/22.19 tff(c_24021, plain, (![D_485]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_485), true, icext(D_485, uri_rdf_rest), true)=true))). % 33.28/22.19 tff(c_13992, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_predicate), true)=true))). % 33.28/22.19 tff(c_2984, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_103), true, iext(Q_103, uri_rdfs_member, uri_rdfs_Resource), true)=true))). % 33.28/22.19 tff(c_13993, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_predicate), true)=true))). % 33.28/22.19 tff(c_13855, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_ex_p), true)=true))). % 33.28/22.19 tff(c_13854, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_ex_p), true)=true))). % 33.28/22.19 tff(c_13927, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_comment), true)=true))). % 33.28/22.19 tff(c_13928, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_comment), true)=true))). % 33.28/22.19 tff(c_14057, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_label), true)=true))). % 33.28/22.20 tff(c_14058, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_label), true)=true))). % 33.28/22.20 tff(c_13789, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_member), true)=true))). % 33.28/22.20 tff(c_2971, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_103), true, iext(Q_103, uri_rdf__3, uri_rdfs_Resource), true)=true))). % 33.28/22.20 tff(c_13471, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdfs_Resource), true)=true))). % 33.28/22.20 tff(c_2964, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_103), true, iext(Q_103, uri_rdfs_domain, uri_rdfs_Class), true)=true))). % 33.28/22.20 tff(c_13173, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdfs_Statement), true)=true))). % 33.28/22.20 tff(c_13240, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdf_List), true)=true))). % 33.28/22.20 tff(c_23572, plain, (![D_468]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_468), true, icext(D_468, uri_rdf__3), true)=true))). % 33.28/22.20 tff(c_14774, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, sK3_testcase_premise_fullish_026_Inferred_Property_Characteristics_I_BNODE_x1), true)=true))). % 33.28/22.20 tff(c_13241, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdf_List), true)=true))). % 33.28/22.20 tff(c_2965, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_103), true, iext(Q_103, uri_rdfs_Seq, uri_rdfs_Container), true)=true))). % 33.28/22.20 tff(c_13083, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, sK1_testcase_premise_fullish_026_Inferred_Property_Characteristics_I_BNODE_x2), true)=true))). % 33.28/22.20 tff(c_13082, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, sK1_testcase_premise_fullish_026_Inferred_Property_Characteristics_I_BNODE_x2), true)=true))). % 33.28/22.20 tff(c_14707, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, sK3_testcase_premise_fullish_026_Inferred_Property_Characteristics_I_BNODE_x1), true)=true))). % 33.28/22.20 tff(c_13174, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdfs_Statement), true)=true))). % 33.28/22.20 tff(c_2977, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_103), true, iext(Q_103, uri_rdfs_member, uri_rdfs_Resource), true)=true))). % 33.28/22.20 tff(c_23292, plain, (![D_458]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, D_458), true, icext(D_458, uri_rdf__3), true)=true))). % 33.28/22.20 tff(c_2978, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_103), true, iext(Q_103, uri_rdfs_ContainerMembershipProperty, uri_rdf_Property), true)=true))). % 33.28/22.20 tff(c_23205, plain, (![D_455]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_455), true, icext(D_455, uri_rdf_value), true)=true))). % 33.28/22.20 tff(c_2939, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_first, Q_103), true, iext(Q_103, sK2_testcase_premise_fullish_026_Inferred_Property_Characteristics_I_BNODE_l2, uri_ex_u), true)=true))). % 33.28/22.20 tff(c_22763, plain, (![D_450, X_451]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Resource, D_450), true, icext(D_450, X_451), true)=true))). % 33.28/22.20 tff(c_2981, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_103), true, iext(Q_103, uri_rdf_value, uri_rdf_Property), true)=true))). % 33.28/22.20 tff(c_22571, plain, (![C_88, X_60]: (ifeq(icext(C_88, X_60), true, true, true)=true))). % 33.28/22.20 tff(c_3105, plain, (![E_107]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Container, E_107), true, iext(uri_rdfs_subClassOf, uri_rdf_Bag, E_107), true)=true))). % 33.28/22.20 tff(c_22511, plain, (![X_442, Y_443]: (ifeq(iext(uri_rdf_subject, X_442, Y_443), true, icext(uri_rdfs_Statement, X_442), true)=true))). % 33.28/22.20 tff(c_2974, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_103), true, iext(Q_103, uri_rdf_subject, uri_rdf_Property), true)=true))). % 33.28/22.20 tff(c_7123, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_rest), true)=true))). % 33.28/22.20 tff(c_22434, plain, (![X_436, Y_437]: (ifeq(iext(uri_ex_p, X_436, Y_437), true, icext(sK3_testcase_premise_fullish_026_Inferred_Property_Characteristics_I_BNODE_x1, X_436), true)=true))). % 33.28/22.20 tff(c_8130, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdf_Property), true)=true))). % 33.28/22.20 tff(c_2973, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_103), true, iext(Q_103, uri_rdf__1, uri_rdfs_ContainerMembershipProperty), true)=true))). % 33.28/22.20 tff(c_7523, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_first), true)=true))). % 33.28/22.20 tff(c_22001, plain, (![X_429, Y_430]: (ifeq(iext(uri_rdfs_range, X_429, Y_430), true, icext(uri_rdf_Property, X_429), true)=true))). % 33.28/22.20 tff(c_8063, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdf_Alt), true)=true))). % 33.28/22.20 tff(c_2969, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_103), true, iext(Q_103, uri_rdfs_isDefinedBy, uri_rdfs_seeAlso), true)=true))). % 33.28/22.20 tff(c_6548, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_range), true)=true))). % 33.28/22.20 tff(c_21580, plain, (![X_422, Y_423]: (ifeq(iext(uri_rdfs_range, X_422, Y_423), true, icext(uri_rdfs_Class, Y_423), true)=true))). % 33.28/22.20 tff(c_5808, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_subClassOf), true)=true))). % 33.28/22.20 tff(c_3106, plain, (![E_107]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, E_107), true, iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, E_107), true)=true))). % 33.28/22.20 tff(c_7368, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdfs_Class), true)=true))). % 33.28/22.20 tff(c_21407, plain, (![X_415, Y_416]: (ifeq(iext(uri_rdf_rest, X_415, Y_416), true, icext(uri_rdf_List, Y_416), true)=true))). % 33.28/22.20 tff(c_5809, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_subClassOf), true)=true))). % 33.28/22.20 tff(c_6962, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_object), true)=true))). % 33.28/22.20 tff(c_2988, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_103), true, iext(Q_103, uri_rdf_predicate, uri_rdfs_Resource), true)=true))). % 33.28/22.20 tff(c_20817, plain, (![X_408, Y_409]: (ifeq(iext(uri_rdf_type, X_408, Y_409), true, icext(uri_rdfs_Class, Y_409), true)=true))). % 33.28/22.20 tff(c_6547, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_range), true)=true))). % 33.28/22.20 tff(c_2975, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_103), true, iext(Q_103, uri_rdf__2, uri_rdfs_Resource), true)=true))). % 33.28/22.20 tff(c_7694, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_isDefinedBy), true)=true))). % 33.28/22.20 tff(c_20707, plain, (![X_401, Y_402]: (ifeq(iext(uri_rdf_predicate, X_401, Y_402), true, icext(uri_rdfs_Statement, X_401), true)=true))). % 33.28/22.20 tff(c_2960, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_103), true, iext(Q_103, uri_rdfs_comment, uri_rdfs_Resource), true)=true))). % 33.28/22.20 tff(c_7524, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_first), true)=true))). % 33.28/22.20 tff(c_20585, plain, (![X_395, Y_396]: (ifeq(iext(uri_rdf_first, X_395, Y_396), true, icext(uri_rdf_List, X_395), true)=true))). % 33.28/22.20 tff(c_8822, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdfs_Datatype), true)=true))). % 33.28/22.20 tff(c_2949, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_103), true, iext(Q_103, uri_rdf_object, uri_rdf_Property), true)=true))). % 33.28/22.20 tff(c_10752, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdfs_Seq), true)=true))). % 33.28/22.20 tff(c_20484, plain, (![X_388, Y_389]: (ifeq(iext(uri_rdf_object, X_388, Y_389), true, icext(uri_rdfs_Statement, X_388), true)=true))). % 33.28/22.20 tff(c_8221, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_seeAlso), true)=true))). % 33.28/22.20 tff(c_6185, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_subject), true)=true))). % 33.28/22.20 tff(c_5472, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_domain), true)=true))). % 33.28/22.20 tff(c_2942, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_103), true, iext(Q_103, uri_rdf_first, uri_rdf_Property), true)=true))). % 33.28/22.20 tff(c_5473, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_domain), true)=true))). % 33.28/22.20 tff(c_10013, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_type), true)=true))). % 33.28/22.20 tff(c_20311, plain, (![X_378, Y_379]: (ifeq(iext(uri_rdfs_label, X_378, Y_379), true, icext(uri_rdfs_Literal, Y_379), true)=true))). % 33.28/22.20 tff(c_4809, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdfs_Literal), true)=true))). % 33.28/22.20 tff(c_7122, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_rest), true)=true))). % 33.28/22.20 tff(c_6379, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_value), true)=true))). % 33.28/22.20 tff(c_2985, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_103), true, iext(Q_103, uri_rdf__1, uri_rdfs_Resource), true)=true))). % 33.28/22.20 tff(c_9174, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_owl_oneOf), true)=true))). % 33.28/22.20 tff(c_5909, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf__3), true)=true))). % 33.28/22.20 tff(c_4740, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_subPropertyOf), true)=true))). % 33.28/22.20 tff(c_19717, plain, (![X_367, Y_368]: (ifeq(iext(uri_rdfs_subPropertyOf, X_367, Y_368), true, icext(uri_rdf_Property, X_367), true)=true))). % 33.28/22.20 tff(c_7030, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf__1), true)=true))). % 33.28/22.20 tff(c_9173, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_owl_oneOf), true)=true))). % 33.28/22.20 tff(c_5908, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf__3), true)=true))). % 33.28/22.20 tff(c_2989, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_103), true, iext(Q_103, uri_rdf__1, uri_rdfs_Resource), true)=true))). % 33.28/22.20 tff(c_5635, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf__2), true)=true))). % 33.28/22.20 tff(c_6480, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdfs_ContainerMembershipProperty), true)=true))). % 33.28/22.20 tff(c_6378, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_value), true)=true))). % 33.28/22.20 tff(c_19207, plain, (![X_356, Y_357]: (ifeq(iext(uri_rdfs_domain, X_356, Y_357), true, icext(uri_rdfs_Class, Y_357), true)=true))). % 33.28/22.20 tff(c_5273, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdf_Bag), true)=true))). % 33.28/22.20 tff(c_7031, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf__1), true)=true))). % 33.28/22.20 tff(c_3000, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_103), true, iext(Q_103, uri_rdfs_subPropertyOf, uri_rdf_Property), true)=true))). % 33.28/22.20 tff(c_6961, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_object), true)=true))). % 33.28/22.20 tff(c_6184, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_subject), true)=true))). % 33.28/22.20 tff(c_18670, plain, (![X_347, Y_348]: (ifeq(iext(uri_rdfs_domain, X_347, Y_348), true, icext(uri_rdf_Property, X_347), true)=true))). % 33.28/22.20 tff(c_2986, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_103), true, iext(Q_103, uri_rdf__2, uri_rdfs_Resource), true)=true))). % 33.28/22.20 tff(c_7590, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_member), true)=true))). % 33.28/22.20 tff(c_11128, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdf_XMLLiteral), true)=true))). % 33.28/22.20 tff(c_18516, plain, (![X_340, Y_341]: (ifeq(iext(uri_rdf_rest, X_340, Y_341), true, icext(uri_rdf_List, X_340), true)=true))). % 33.28/22.20 tff(c_2945, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_103), true, iext(Q_103, uri_rdf_value, uri_rdfs_Resource), true)=true))). % 33.28/22.20 tff(c_5700, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdfs_Container), true)=true))). % 33.28/22.20 tff(c_10014, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_type), true)=true))). % 33.28/22.20 tff(c_18038, plain, (![X_333, Y_334]: (ifeq(iext(uri_rdfs_subPropertyOf, X_333, Y_334), true, icext(uri_rdf_Property, Y_334), true)=true))). % 33.28/22.20 tff(c_4741, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_subPropertyOf), true)=true))). % 33.28/22.20 tff(c_10350, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf__2), true)=true))). % 33.28/22.20 tff(c_11325, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdfs_Resource), true)=true))). % 33.28/22.20 tff(c_2992, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_103), true, iext(Q_103, uri_rdf_rest, uri_rdf_Property), true)=true))). % 33.28/22.20 tff(c_4656, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_29), true, icext(C_29, uri_rdfs_Resource), true)=true))). % 33.28/22.20 tff(c_4657, plain, (![C_19, X_132]: (ifeq(iext(uri_rdfs_domain, uri_rdf_type, C_19), true, icext(C_19, X_132), true)=true))). % 33.28/22.20 tff(c_1969, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_92), true, icext(C_92, uri_rdf_Bag), true)=true))). % 33.28/22.20 tff(c_1941, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_92), true, icext(C_92, uri_rdfs_subClassOf), true)=true))). % 33.28/22.20 tff(c_2370, plain, (![C_96]: (ifeq(iext(uri_rdfs_range, uri_owl_oneOf, C_96), true, icext(C_96, sK2_testcase_premise_fullish_026_Inferred_Property_Characteristics_I_BNODE_l2), true)=true))). % 33.28/22.20 tff(c_2396, plain, (![C_96]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_96), true, icext(C_96, uri_rdf_Property), true)=true))). % 33.28/22.20 tff(c_2003, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_92), true, icext(C_92, uri_rdfs_Datatype), true)=true))). % 33.28/22.20 tff(c_1978, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_92), true, icext(C_92, uri_rdf__2), true)=true))). % 33.28/22.20 tff(c_16960, plain, (![X_312, Y_313]: (ifeq(iext(uri_rdfs_subClassOf, X_312, Y_313), true, icext(uri_rdfs_Class, X_312), true)=true))). % 33.28/22.20 tff(c_1993, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdf_first, C_92), true, icext(C_92, sK4_testcase_premise_fullish_026_Inferred_Property_Characteristics_I_BNODE_l1), true)=true))). % 33.28/22.20 tff(c_1981, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_92), true, icext(C_92, uri_rdfs_member), true)=true))). % 33.28/22.20 tff(c_1957, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_92), true, icext(C_92, uri_rdf__3), true)=true))). % 33.28/22.20 tff(c_1954, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_owl_oneOf, C_92), true, icext(C_92, sK1_testcase_premise_fullish_026_Inferred_Property_Characteristics_I_BNODE_x2), true)=true))). % 33.28/22.20 tff(c_2002, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_92), true, icext(C_92, uri_rdf_Alt), true)=true))). % 33.28/22.20 tff(c_1964, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_92), true, icext(C_92, uri_rdfs_domain), true)=true))). % 33.28/22.20 tff(c_2005, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_92), true, icext(C_92, uri_rdf_object), true)=true))). % 33.28/22.20 tff(c_1937, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_92), true, icext(C_92, uri_rdf_XMLLiteral), true)=true))). % 33.28/22.20 tff(c_1992, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_92), true, icext(C_92, uri_rdf__2), true)=true))). % 33.28/22.20 tff(c_1994, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_92), true, icext(C_92, uri_rdf_predicate), true)=true))). % 33.28/22.20 tff(c_1935, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_92), true, icext(C_92, uri_rdfs_seeAlso), true)=true))). % 33.28/22.20 tff(c_1988, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_92), true, icext(C_92, uri_rdf_value), true)=true))). % 33.28/22.20 tff(c_2425, plain, (![C_96]: (ifeq(iext(uri_rdfs_range, uri_owl_oneOf, C_96), true, icext(C_96, sK4_testcase_premise_fullish_026_Inferred_Property_Characteristics_I_BNODE_l1), true)=true))). % 33.28/22.20 tff(c_1966, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_92), true, icext(C_92, uri_rdfs_Seq), true)=true))). % 33.28/22.20 tff(c_16326, plain, (![X_290, Y_291]: (ifeq(iext(uri_rdfs_comment, X_290, Y_291), true, icext(uri_rdfs_Literal, Y_291), true)=true))). % 33.28/22.20 tff(c_2355, plain, (![C_96]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_96), true, icext(C_96, uri_rdfs_Literal), true)=true))). % 33.28/22.20 tff(c_1933, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_92), true, icext(C_92, uri_rdf_type), true)=true))). % 33.28/22.20 tff(c_1955, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_92), true, icext(C_92, uri_rdf_type), true)=true))). % 33.28/22.20 tff(c_2398, plain, (![C_96]: (ifeq(iext(uri_rdfs_range, uri_rdfs_range, C_96), true, icext(C_96, uri_rdfs_Literal), true)=true))). % 33.28/22.20 tff(c_1985, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_92), true, icext(C_92, uri_rdfs_label), true)=true))). % 33.28/22.20 tff(c_1995, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_92), true, icext(C_92, uri_rdf__1), true)=true))). % 33.28/22.20 tff(c_1961, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_92), true, icext(C_92, uri_rdfs_comment), true)=true))). % 33.28/22.20 tff(c_2387, plain, (![C_96]: (ifeq(iext(uri_rdfs_range, uri_rdf_rest, C_96), true, icext(C_96, uri_rdf_nil), true)=true))). % 33.28/22.20 tff(c_1936, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdf_first, C_92), true, icext(C_92, sK2_testcase_premise_fullish_026_Inferred_Property_Characteristics_I_BNODE_l2), true)=true))). % 33.28/22.20 tff(c_15526, plain, (![X_271, Y_272]: (ifeq(iext(uri_rdfs_subClassOf, X_271, Y_272), true, icext(uri_rdfs_Class, Y_272), true)=true))). % 33.28/22.20 tff(c_1989, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_92), true, icext(C_92, uri_rdfs_member), true)=true))). % 33.28/22.20 tff(c_2415, plain, (![C_96]: (ifeq(iext(uri_rdfs_range, uri_rdfs_range, C_96), true, icext(C_96, uri_rdf_List), true)=true))). % 33.28/22.20 tff(c_2006, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_92), true, icext(C_92, uri_rdfs_subPropertyOf), true)=true))). % 33.28/22.20 tff(c_2354, plain, (![C_96]: (ifeq(iext(uri_rdfs_range, uri_rdf_first, C_96), true, icext(C_96, uri_ex_u), true)=true))). % 33.28/22.20 tff(c_2382, plain, (![C_96]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_96), true, icext(C_96, uri_rdfs_Container), true)=true))). % 33.28/22.20 tff(c_1972, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_92), true, icext(C_92, uri_rdf__3), true)=true))). % 33.28/22.20 tff(c_1945, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_92), true, icext(C_92, uri_rdfs_seeAlso), true)=true))). % 33.28/22.20 tff(c_1970, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_92), true, icext(C_92, uri_rdfs_isDefinedBy), true)=true))). % 33.28/22.20 tff(c_1963, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_92), true, icext(C_92, uri_rdfs_isDefinedBy), true)=true))). % 33.28/22.20 tff(c_1946, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_92), true, icext(C_92, uri_rdfs_range), true)=true))). % 33.28/22.20 tff(c_2383, plain, (![C_96]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_96), true, icext(C_96, uri_rdfs_Class), true)=true))). % 33.28/22.20 tff(c_2409, plain, (![C_96]: (ifeq(iext(uri_rdfs_range, uri_rdf_first, C_96), true, icext(C_96, uri_ex_w), true)=true))). % 33.28/22.20 tff(c_2424, plain, (![C_96]: (ifeq(iext(uri_rdfs_range, uri_rdfs_range, C_96), true, icext(C_96, uri_rdf_Property), true)=true))). % 33.28/22.20 tff(c_2351, plain, (![C_96]: (ifeq(iext(uri_rdfs_range, uri_rdfs_domain, C_96), true, icext(C_96, uri_rdfs_Class), true)=true))). % 33.28/22.21 tff(c_14709, plain, (![X_33]: (ifeq(icext(sK3_testcase_premise_fullish_026_Inferred_Property_Characteristics_I_BNODE_x1, X_33), true, icext(sK3_testcase_premise_fullish_026_Inferred_Property_Characteristics_I_BNODE_x1, X_33), true)=true))). % 33.28/22.21 tff(c_13084, plain, (![X_33]: (ifeq(icext(sK1_testcase_premise_fullish_026_Inferred_Property_Characteristics_I_BNODE_x2, X_33), true, icext(sK1_testcase_premise_fullish_026_Inferred_Property_Characteristics_I_BNODE_x2, X_33), true)=true))). % 33.28/22.21 tff(c_13175, plain, (![X_33]: (ifeq(icext(uri_rdfs_Statement, X_33), true, icext(uri_rdfs_Statement, X_33), true)=true))). % 33.28/22.21 tff(c_13242, plain, (![X_33]: (ifeq(icext(uri_rdf_List, X_33), true, icext(uri_rdf_List, X_33), true)=true))). % 33.28/22.21 tff(c_8065, plain, (![X_33]: (ifeq(icext(uri_rdf_Alt, X_33), true, icext(uri_rdf_Alt, X_33), true)=true))). % 33.28/22.21 tff(c_8131, plain, (![X_33]: (ifeq(icext(uri_rdf_Property, X_33), true, icext(uri_rdf_Property, X_33), true)=true))). % 33.28/22.21 tff(c_14147, plain, (![X_239, Y_240]: (ifeq(iext(uri_ex_p, X_239, Y_240), true, icext(sK1_testcase_premise_fullish_026_Inferred_Property_Characteristics_I_BNODE_x2, Y_240), true)=true))). % 33.28/22.21 tff(c_8513, plain, (![X_33]: (ifeq(icext(uri_rdfs_Literal, X_33), true, icext(uri_rdfs_Literal, X_33), true)=true))). % 33.28/22.21 tff(c_5275, plain, (![X_33]: (ifeq(icext(uri_rdf_Bag, X_33), true, icext(uri_rdf_Bag, X_33), true)=true))). % 33.28/22.21 tff(c_10754, plain, (![X_33]: (ifeq(icext(uri_rdfs_Seq, X_33), true, icext(uri_rdfs_Seq, X_33), true)=true))). % 33.28/22.21 tff(c_14719, plain, (iext(uri_rdfs_subClassOf, sK3_testcase_premise_fullish_026_Inferred_Property_Characteristics_I_BNODE_x1, uri_rdfs_Resource)=true)). % 33.28/22.21 tff(c_14653, plain, (iext(uri_rdfs_subClassOf, sK3_testcase_premise_fullish_026_Inferred_Property_Characteristics_I_BNODE_x1, sK3_testcase_premise_fullish_026_Inferred_Property_Characteristics_I_BNODE_x1)=true)). % 33.28/22.21 tff(c_14581, plain, (iext(uri_rdf_type, sK3_testcase_premise_fullish_026_Inferred_Property_Characteristics_I_BNODE_x1, uri_rdfs_Class)=true)). % 33.28/22.21 tff(c_2356, plain, (![C_96]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_96), true, icext(C_96, uri_rdf_List), true)=true))). % 33.28/22.21 tff(c_14422, plain, (ic(sK3_testcase_premise_fullish_026_Inferred_Property_Characteristics_I_BNODE_x1)=true)). % 33.28/22.21 tff(c_14352, plain, (icext(uri_rdfs_Class, sK3_testcase_premise_fullish_026_Inferred_Property_Characteristics_I_BNODE_x1)=true)). % 33.28/22.21 tff(c_2368, plain, (![C_96]: (ifeq(iext(uri_rdfs_range, uri_rdfs_domain, C_96), true, icext(C_96, sK3_testcase_premise_fullish_026_Inferred_Property_Characteristics_I_BNODE_x1), true)=true))). % 33.28/22.21 tff(c_6482, plain, (![X_33]: (ifeq(icext(uri_rdfs_ContainerMembershipProperty, X_33), true, icext(uri_rdfs_ContainerMembershipProperty, X_33), true)=true))). % 33.28/22.21 tff(c_7369, plain, (![X_33]: (ifeq(icext(uri_rdfs_Class, X_33), true, icext(uri_rdfs_Class, X_33), true)=true))). % 33.28/22.21 tff(c_11130, plain, (![X_33]: (ifeq(icext(uri_rdf_XMLLiteral, X_33), true, icext(uri_rdf_XMLLiteral, X_33), true)=true))). % 33.28/22.21 tff(c_5701, plain, (![X_33]: (ifeq(icext(uri_rdfs_Container, X_33), true, icext(uri_rdfs_Container, X_33), true)=true))). % 33.28/22.21 tff(c_8824, plain, (![X_33]: (ifeq(icext(uri_rdfs_Datatype, X_33), true, icext(uri_rdfs_Datatype, X_33), true)=true))). % 33.28/22.21 tff(c_14093, plain, (iext(uri_rdf_type, uri_rdfs_Resource, uri_rdfs_Class)=true)). % 33.28/22.21 tff(c_1943, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_92), true, icext(C_92, uri_rdf_value), true)=true))). % 33.28/22.21 tff(c_14003, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_label, uri_rdfs_label)=true)). % 33.28/22.21 tff(c_13938, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_predicate, uri_rdf_predicate)=true)). % 33.28/22.21 tff(c_13873, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_comment, uri_rdfs_comment)=true)). % 33.28/22.21 tff(c_11615, plain, (![S_5, O_6]: (ifeq(iext(uri_ex_p, S_5, O_6), true, true, true)=true))). % 33.28/22.21 tff(c_13800, plain, (iext(uri_rdfs_subPropertyOf, uri_ex_p, uri_ex_p)=true)). % 33.28/22.21 tff(c_13731, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_member, uri_rdfs_member)=true)). % 33.28/22.21 tff(c_1991, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_92), true, icext(C_92, uri_rdf__1), true)=true))). % 33.28/22.21 tff(c_13539, plain, (icext(uri_rdf_Property, uri_rdfs_member)=true)). % 33.28/22.21 tff(c_13485, plain, (iext(uri_rdf_type, uri_rdfs_member, uri_rdf_Property)=true)). % 33.28/22.21 tff(c_13412, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Resource, uri_rdfs_Resource)=true)). % 33.28/22.21 tff(c_13252, plain, (iext(uri_rdfs_subClassOf, uri_rdf_List, uri_rdfs_Resource)=true)). % 33.28/22.21 tff(c_2369, plain, (![C_96]: (ifeq(iext(uri_rdfs_range, uri_rdfs_domain, C_96), true, icext(C_96, uri_rdf_Property), true)=true))). % 33.28/22.21 tff(c_13186, plain, (iext(uri_rdfs_subClassOf, uri_rdf_List, uri_rdf_List)=true)). % 33.28/22.21 tff(c_13119, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Statement, uri_rdfs_Statement)=true)). % 33.28/22.21 tff(c_2004, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_92), true, icext(C_92, uri_rdf_subject), true)=true))). % 33.28/22.21 tff(c_13028, plain, (iext(uri_rdfs_subClassOf, sK1_testcase_premise_fullish_026_Inferred_Property_Characteristics_I_BNODE_x2, sK1_testcase_premise_fullish_026_Inferred_Property_Characteristics_I_BNODE_x2)=true)). % 33.28/22.21 tff(c_12906, plain, (iext(uri_rdfs_subClassOf, sK1_testcase_premise_fullish_026_Inferred_Property_Characteristics_I_BNODE_x2, uri_rdfs_Resource)=true)). % 33.28/22.21 tff(c_12784, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Statement, uri_rdfs_Resource)=true)). % 33.28/22.21 tff(c_12737, plain, (iext(uri_rdf_type, uri_rdfs_Container, uri_rdfs_Class)=true)). % 33.28/22.21 tff(c_12690, plain, (iext(uri_rdf_type, uri_rdfs_Class, uri_rdfs_Class)=true)). % 33.28/22.21 tff(c_2381, plain, (![C_96]: (ifeq(iext(uri_rdfs_range, uri_rdfs_range, C_96), true, icext(C_96, uri_rdfs_Class), true)=true))). % 33.28/22.21 tff(c_12618, plain, (iext(uri_rdf_type, uri_rdfs_Datatype, uri_rdfs_Class)=true)). % 33.28/22.21 tff(c_12570, plain, (iext(uri_rdf_type, uri_rdf_Bag, uri_rdfs_Class)=true)). % 33.28/22.21 tff(c_12521, plain, (iext(uri_rdf_type, uri_rdf_XMLLiteral, uri_rdfs_Class)=true)). % 33.28/22.21 tff(c_12379, plain, (iext(uri_rdf_type, sK2_testcase_premise_fullish_026_Inferred_Property_Characteristics_I_BNODE_l2, uri_rdf_List)=true)). % 33.28/22.21 tff(c_12338, plain, (icext(uri_rdf_List, sK2_testcase_premise_fullish_026_Inferred_Property_Characteristics_I_BNODE_l2)=true)). % 33.28/22.21 tff(c_1971, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdf_rest, C_92), true, icext(C_92, sK2_testcase_premise_fullish_026_Inferred_Property_Characteristics_I_BNODE_l2), true)=true))). % 33.28/22.21 tff(c_12271, plain, (iext(uri_rdf_type, uri_rdfs_Literal, uri_rdfs_Class)=true)). % 33.28/22.21 tff(c_12218, plain, (iext(uri_rdf_type, uri_rdf_Alt, uri_rdfs_Class)=true)). % 33.28/22.21 tff(c_12169, plain, (iext(uri_rdf_type, uri_rdfs_Seq, uri_rdfs_Class)=true)). % 33.28/22.21 tff(c_12097, plain, (iext(uri_rdf_type, uri_rdfs_ContainerMembershipProperty, uri_rdfs_Class)=true)). % 33.28/22.21 tff(c_1987, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_92), true, icext(C_92, uri_rdf_first), true)=true))). % 33.28/22.21 tff(c_12050, plain, (iext(uri_rdf_type, uri_rdf_List, uri_rdfs_Class)=true)). % 33.28/22.21 tff(c_12002, plain, (iext(uri_rdf_type, sK1_testcase_premise_fullish_026_Inferred_Property_Characteristics_I_BNODE_x2, uri_rdfs_Class)=true)). % 33.28/22.21 tff(c_11935, plain, (ip(uri_rdfs_comment)=true)). % 33.28/22.21 tff(c_11882, plain, (iext(uri_rdf_type, uri_rdfs_comment, uri_rdf_Property)=true)). % 33.28/22.21 tff(c_11810, plain, (iext(uri_rdf_type, uri_rdfs_Statement, uri_rdfs_Class)=true)). % 33.28/22.21 tff(c_1952, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_92), true, icext(C_92, uri_ex_p), true)=true))). % 33.28/22.21 tff(c_11763, plain, (iext(uri_rdf_type, sK4_testcase_premise_fullish_026_Inferred_Property_Characteristics_I_BNODE_l1, uri_rdf_List)=true)). % 33.28/22.21 tff(c_11721, plain, (ip(uri_rdf_predicate)=true)). % 33.28/22.21 tff(c_1950, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_92), true, icext(C_92, uri_rdf_rest), true)=true))). % 33.28/22.21 tff(c_11643, plain, (iext(uri_rdf_type, uri_rdf_predicate, uri_rdf_Property)=true)). % 33.28/22.21 tff(c_11603, plain, (ip(uri_ex_p)=true)). % 33.28/22.21 tff(c_11533, plain, (iext(uri_rdf_type, uri_ex_p, uri_rdf_Property)=true)). % 33.28/22.21 tff(c_2007, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_owl_oneOf, C_92), true, icext(C_92, sK3_testcase_premise_fullish_026_Inferred_Property_Characteristics_I_BNODE_x1), true)=true))). % 33.28/22.21 tff(c_11491, plain, (ip(uri_rdfs_label)=true)). % 33.28/22.21 tff(c_11434, plain, (iext(uri_rdf_type, uri_rdfs_label, uri_rdf_Property)=true)). % 33.28/22.21 tff(c_1974, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_92), true, icext(C_92, uri_rdfs_isDefinedBy), true)=true))). % 33.28/22.21 tff(c_11271, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, uri_rdfs_Resource)=true)). % 33.28/22.21 tff(c_1637, plain, (![S_5, O_6]: (ifeq(iext(uri_rdfs_subClassOf, S_5, O_6), true, true, true)=true))). % 33.28/22.21 tff(c_2384, plain, (![C_96]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_96), true, icext(C_96, uri_rdfs_Datatype), true)=true))). % 33.28/22.21 tff(c_11071, plain, (iext(uri_rdfs_subClassOf, uri_rdf_XMLLiteral, uri_rdf_XMLLiteral)=true)). % 33.28/22.21 tff(c_11030, plain, (icext(uri_rdf_List, sK4_testcase_premise_fullish_026_Inferred_Property_Characteristics_I_BNODE_l1)=true)). % 33.28/22.21 tff(c_2008, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdf_rest, C_92), true, icext(C_92, sK4_testcase_premise_fullish_026_Inferred_Property_Characteristics_I_BNODE_l1), true)=true))). % 33.28/22.21 tff(c_10784, plain, (icext(uri_rdf_Property, uri_rdfs_label)=true)). % 33.28/22.21 tff(c_1984, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_92), true, icext(C_92, uri_rdfs_label), true)=true))). % 33.28/22.21 tff(c_10698, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Seq, uri_rdfs_Seq)=true)). % 33.28/22.21 tff(c_10435, plain, (iext(uri_rdf_type, uri_rdfs_range, uri_rdf_Property)=true)). % 33.28/22.21 tff(c_2421, plain, (![C_96]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_96), true, icext(C_96, uri_rdfs_Class), true)=true))). % 33.28/22.21 tff(c_10295, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf__2, uri_rdfs_member)=true)). % 33.28/22.21 tff(c_1446, plain, (![S_5, O_6]: (ifeq(iext(uri_rdfs_domain, S_5, O_6), true, true, true)=true))). % 33.28/22.21 tff(c_2403, plain, (![C_96]: (ifeq(iext(uri_rdfs_range, uri_rdfs_range, C_96), true, icext(C_96, uri_rdfs_Resource), true)=true))). % 33.28/22.21 tff(c_10024, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Bag, uri_rdfs_Resource)=true)). % 33.28/22.21 tff(c_9959, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_type, uri_rdf_type)=true)). % 33.28/22.21 tff(c_9726, plain, (icext(uri_rdf_Property, uri_rdfs_comment)=true)). % 33.28/22.21 tff(c_9640, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Container, uri_rdfs_Resource)=true)). % 33.28/22.21 tff(c_1999, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_92), true, icext(C_92, uri_rdfs_comment), true)=true))). % 33.28/22.21 tff(c_9457, plain, (icext(uri_rdf_Property, uri_rdfs_range)=true)). % 33.28/22.21 tff(c_9382, plain, (iext(uri_rdf_type, uri_rdfs_domain, uri_rdf_Property)=true)). % 33.28/22.21 tff(c_1958, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_92), true, icext(C_92, uri_rdfs_range), true)=true))). % 33.28/22.21 tff(c_9184, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, uri_rdfs_Resource)=true)). % 33.28/22.21 tff(c_9119, plain, (iext(uri_rdfs_subPropertyOf, uri_owl_oneOf, uri_owl_oneOf)=true)). % 33.28/22.21 tff(c_9054, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf__1, uri_rdfs_member)=true)). % 33.28/22.21 tff(c_2386, plain, (![C_96]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_96), true, icext(C_96, uri_rdfs_seeAlso), true)=true))). % 33.28/22.21 tff(c_8940, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Alt, uri_rdfs_Resource)=true)). % 33.28/22.21 tff(c_8834, plain, (icext(uri_rdf_Property, uri_ex_p)=true)). % 33.28/22.21 tff(c_8749, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, uri_rdfs_Datatype)=true)). % 33.28/22.21 tff(c_1979, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_92), true, icext(C_92, uri_ex_p), true)=true))). % 33.28/22.21 tff(c_8598, plain, (iext(uri_rdfs_subClassOf, uri_rdf_XMLLiteral, uri_rdfs_Resource)=true)). % 33.28/22.21 tff(c_8458, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Literal, uri_rdfs_Literal)=true)). % 33.28/22.21 tff(c_8399, plain, (iext(uri_rdf_type, uri_rdfs_subClassOf, uri_rdf_Property)=true)). % 33.28/22.21 tff(c_8356, plain, (icext(uri_rdf_Property, uri_owl_oneOf)=true)). % 33.28/22.21 tff(c_1962, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_92), true, icext(C_92, uri_rdf_subject), true)=true))). % 33.28/22.21 tff(c_8277, plain, (iext(uri_rdf_type, uri_owl_oneOf, uri_rdf_Property)=true)). % 33.28/22.21 tff(c_8166, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_seeAlso, uri_rdfs_seeAlso)=true)). % 33.28/22.21 tff(c_2391, plain, (![C_96]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_96), true, icext(C_96, uri_rdfs_ContainerMembershipProperty), true)=true))). % 33.28/22.21 tff(c_8075, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Property, uri_rdf_Property)=true)). % 33.28/22.21 tff(c_8006, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Alt, uri_rdf_Alt)=true)). % 33.28/22.21 tff(c_1982, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_92), true, icext(C_92, uri_rdfs_ContainerMembershipProperty), true)=true))). % 33.28/22.21 tff(c_7885, plain, (ic(sK1_testcase_premise_fullish_026_Inferred_Property_Characteristics_I_BNODE_x2)=true)). % 33.28/22.21 tff(c_7828, plain, (icext(uri_rdfs_Class, sK1_testcase_premise_fullish_026_Inferred_Property_Characteristics_I_BNODE_x2)=true)). % 33.28/22.21 tff(c_2394, plain, (![C_96]: (ifeq(iext(uri_rdfs_range, uri_rdfs_range, C_96), true, icext(C_96, sK1_testcase_premise_fullish_026_Inferred_Property_Characteristics_I_BNODE_x2), true)=true))). % 33.28/22.21 tff(c_7761, plain, (icext(uri_rdf_Property, uri_rdfs_seeAlso)=true)). % 33.28/22.21 tff(c_7707, plain, (iext(uri_rdf_type, uri_rdfs_seeAlso, uri_rdf_Property)=true)). % 33.28/22.21 tff(c_7640, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_isDefinedBy, uri_rdfs_isDefinedBy)=true)). % 33.28/22.21 tff(c_7600, plain, (ip(uri_rdfs_member)=true)). % 33.28/22.21 tff(c_7536, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf__3, uri_rdfs_member)=true)). % 33.28/22.21 tff(c_7469, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_first, uri_rdf_first)=true)). % 33.28/22.21 tff(c_7317, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Class, uri_rdfs_Class)=true)). % 33.28/22.21 tff(c_7219, plain, (icext(uri_rdf_Property, uri_rdf_predicate)=true)). % 33.28/22.21 tff(c_2000, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_92), true, icext(C_92, uri_rdf_predicate), true)=true))). % 33.28/22.21 tff(c_7133, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Property, uri_rdfs_Resource)=true)). % 33.28/22.21 tff(c_7068, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_rest, uri_rdf_rest)=true)). % 33.28/22.21 tff(c_1997, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_92), true, icext(C_92, uri_rdf_rest), true)=true))). % 33.28/22.21 tff(c_6976, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf__1, uri_rdf__1)=true)). % 33.28/22.21 tff(c_6907, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_object, uri_rdf_object)=true)). % 33.28/22.21 tff(c_6864, plain, (icext(uri_rdf_Property, uri_rdfs_subClassOf)=true)). % 33.28/22.21 tff(c_1934, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_92), true, icext(C_92, uri_rdfs_subClassOf), true)=true))). % 33.28/22.21 tff(c_6759, plain, (icext(uri_rdf_Property, uri_rdfs_isDefinedBy)=true)). % 33.28/22.21 tff(c_2361, plain, (![C_96]: (ifeq(iext(uri_rdfs_range, uri_rdfs_domain, C_96), true, icext(C_96, uri_rdfs_Resource), true)=true))). % 33.28/22.21 tff(c_6687, plain, (ic(uri_rdf_List)=true)). % 33.28/22.21 tff(c_6631, plain, (icext(uri_rdfs_Class, uri_rdf_List)=true)). % 33.28/22.21 tff(c_6558, plain, (iext(uri_rdf_type, uri_rdfs_isDefinedBy, uri_rdf_Property)=true)). % 33.28/22.21 tff(c_2366, plain, (![C_96]: (ifeq(iext(uri_rdfs_range, uri_rdfs_domain, C_96), true, icext(C_96, uri_rdf_List), true)=true))). % 33.28/22.21 tff(c_6493, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_range, uri_rdfs_range)=true)). % 33.28/22.21 tff(c_6430, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, uri_rdfs_ContainerMembershipProperty)=true)). % 33.28/22.21 tff(c_1073, plain, (![S_80, O_81]: (ifeq(iext(uri_rdf_object, S_80, O_81), true, true, true)=true))). % 33.28/22.21 tff(c_1951, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_92), true, icext(C_92, uri_rdf_first), true)=true))). % 33.28/22.21 tff(c_6324, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_value, uri_rdf_value)=true)). % 33.28/22.21 tff(c_6281, plain, (icext(uri_rdf_Property, uri_rdfs_domain)=true)). % 33.28/22.21 tff(c_1965, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_92), true, icext(C_92, uri_rdfs_domain), true)=true))). % 33.28/22.21 tff(c_2059, plain, (![S_5, O_6]: (ifeq(iext(uri_owl_oneOf, S_5, O_6), true, true, true)=true))). % 33.28/22.21 tff(c_1079, plain, (![S_80, O_81]: (ifeq(iext(uri_rdf_rest, S_80, O_81), true, true, true)=true))). % 33.28/22.21 tff(c_6106, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_subject, uri_rdf_subject)=true)). % 33.28/22.21 tff(c_1953, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_92), true, icext(C_92, uri_rdfs_subPropertyOf), true)=true))). % 33.28/22.21 tff(c_6063, plain, (ic(uri_rdfs_Statement)=true)). % 33.28/22.21 tff(c_6007, plain, (icext(uri_rdfs_Class, uri_rdfs_Statement)=true)). % 33.28/22.21 tff(c_2422, plain, (![C_96]: (ifeq(iext(uri_rdfs_range, uri_rdfs_domain, C_96), true, icext(C_96, uri_rdfs_Statement), true)=true))). % 33.28/22.21 tff(c_1401, plain, (![S_5, O_6]: (ifeq(iext(uri_rdfs_range, S_5, O_6), true, true, true)=true))). % 33.28/22.21 tff(c_5854, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf__3, uri_rdf__3)=true)). % 33.28/22.21 tff(c_5726, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, uri_rdfs_subClassOf)=true)). % 33.28/22.21 tff(c_5646, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Container, uri_rdfs_Container)=true)). % 33.28/22.21 tff(c_5581, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf__2, uri_rdf__2)=true)). % 33.28/22.21 tff(c_2363, plain, (![C_96]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_96), true, icext(C_96, uri_rdf_Property), true)=true))). % 33.28/22.21 tff(c_5483, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Seq, uri_rdfs_Resource)=true)). % 33.28/22.21 tff(c_5418, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, uri_rdfs_domain)=true)). % 33.28/22.21 tff(c_1630, plain, (![X_89]: (ifeq(icext(uri_rdf_Alt, X_89), true, icext(uri_rdfs_Container, X_89), true)=true))). % 33.28/22.21 tff(c_1626, plain, (![X_89]: (ifeq(icext(uri_rdf_XMLLiteral, X_89), true, icext(uri_rdfs_Literal, X_89), true)=true))). % 33.28/22.21 tff(c_5223, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Bag, uri_rdf_Bag)=true)). % 33.28/22.21 tff(c_5112, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Class, uri_rdfs_Resource)=true)). % 33.28/22.21 tff(c_1631, plain, (![X_89]: (ifeq(icext(uri_rdfs_Datatype, X_89), true, icext(uri_rdfs_Class, X_89), true)=true))). % 33.28/22.21 tff(c_3198, plain, (![S_5, O_6]: (ifeq(iext(uri_rdfs_subPropertyOf, S_5, O_6), true, true, true)=true))). % 33.28/22.21 tff(c_5052, plain, (icext(uri_rdf_Property, uri_rdfs_subPropertyOf)=true)). % 33.28/22.21 tff(c_1627, plain, (![X_89]: (ifeq(icext(uri_rdfs_Seq, X_89), true, icext(uri_rdfs_Container, X_89), true)=true))). % 33.28/22.21 tff(c_4988, plain, (iext(uri_rdf_type, uri_rdfs_subPropertyOf, uri_rdf_Property)=true)). % 33.28/22.21 tff(c_1628, plain, (![X_89]: (ifeq(icext(uri_rdf_Bag, X_89), true, icext(uri_rdfs_Container, X_89), true)=true))). % 33.28/22.21 tff(c_4903, plain, (icext(uri_rdfs_Class, uri_rdfs_Resource)=true)). % 33.28/22.21 tff(c_4868, plain, (ic(uri_rdfs_Resource)=true)). % 33.28/22.21 tff(c_1629, plain, (![X_89]: (ifeq(icext(uri_rdfs_ContainerMembershipProperty, X_89), true, icext(uri_rdf_Property, X_89), true)=true))). % 33.28/22.21 tff(c_4758, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Literal, uri_rdfs_Resource)=true)). % 33.28/22.21 tff(c_4690, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf)=true)). % 33.28/22.21 tff(c_2410, plain, (![X_97, Y_98]: (ifeq(iext(uri_rdf_predicate, X_97, Y_98), true, true, true)=true))). % 33.28/22.21 tff(c_1960, plain, (![X_93, Y_94]: (ifeq(iext(uri_rdfs_comment, X_93, Y_94), true, true, true)=true))). % 33.28/22.21 tff(c_2404, plain, (![X_97, Y_98]: (ifeq(iext(uri_rdfs_member, X_97, Y_98), true, true, true)=true))). % 33.28/22.21 tff(c_4615, plain, (![X_131]: (iext(uri_rdf_type, X_131, uri_rdfs_Resource)=true))). % 33.28/22.21 tff(c_1944, plain, (![X_93, Y_94]: (ifeq(iext(uri_rdfs_seeAlso, X_93, Y_94), true, true, true)=true))). % 33.28/22.21 tff(c_2376, plain, (![X_97, Y_98]: (ifeq(iext(uri_rdf_subject, X_97, Y_98), true, true, true)=true))). % 33.28/22.21 tff(c_1956, plain, (![X_93, Y_94]: (ifeq(iext(uri_rdf__3, X_93, Y_94), true, true, true)=true))). % 33.28/22.21 tff(c_2407, plain, (![X_97, Y_98]: (ifeq(iext(uri_rdf__2, X_97, Y_98), true, true, true)=true))). % 33.28/22.21 tff(c_2400, plain, (![X_97, Y_98]: (ifeq(iext(uri_rdf_first, X_97, Y_98), true, true, true)=true))). % 33.28/22.21 tff(c_1983, plain, (![X_93, Y_94]: (ifeq(iext(uri_rdfs_label, X_93, Y_94), true, true, true)=true))). % 33.28/22.21 tff(c_4493, plain, (icext(uri_rdfs_Class, uri_rdfs_Container)=true)). % 33.28/22.21 tff(c_4446, plain, (icext(uri_rdfs_Class, uri_rdf_Bag)=true)). % 33.28/22.21 tff(c_4393, plain, (icext(uri_rdfs_Class, uri_rdfs_Seq)=true)). % 33.28/22.21 tff(c_2378, plain, (![X_97, Y_98]: (ifeq(iext(uri_rdfs_isDefinedBy, X_97, Y_98), true, true, true)=true))). % 33.28/22.21 tff(c_4345, plain, (icext(uri_rdfs_Class, uri_rdf_XMLLiteral)=true)). % 33.28/22.21 tff(c_4289, plain, (icext(uri_rdfs_Class, uri_rdf_Alt)=true)). % 33.28/22.21 tff(c_1942, plain, (![X_93, Y_94]: (ifeq(iext(uri_rdf_value, X_93, Y_94), true, true, true)=true))). % 33.28/22.21 tff(c_4237, plain, (icext(uri_rdfs_Class, uri_rdfs_Class)=true)). % 33.28/22.21 tff(c_1932, plain, (![X_93, Y_94]: (ifeq(iext(uri_rdf_type, X_93, Y_94), true, true, true)=true))). % 33.28/22.21 tff(c_4140, plain, (icext(uri_rdfs_Class, uri_rdfs_ContainerMembershipProperty)=true)). % 33.28/22.21 tff(c_4097, plain, (icext(uri_rdfs_Class, uri_rdfs_Literal)=true)). % 33.28/22.21 tff(c_4054, plain, (icext(uri_rdfs_Class, uri_rdfs_Datatype)=true)). % 33.28/22.21 tff(c_1990, plain, (![X_93, Y_94]: (ifeq(iext(uri_rdf__1, X_93, Y_94), true, true, true)=true))). % 33.28/22.21 tff(c_4000, plain, (icext(uri_rdf_Property, uri_rdf_object)=true)). % 33.28/22.21 tff(c_3962, plain, (icext(uri_rdf_Property, uri_rdf__2)=true)). % 33.28/22.21 tff(c_3915, plain, (icext(uri_rdf_Property, uri_rdf_rest)=true)). % 33.28/22.22 tff(c_3875, plain, (icext(uri_rdfs_ContainerMembershipProperty, uri_rdf__2)=true)). % 33.28/22.22 tff(c_3837, plain, (icext(uri_rdf_Property, uri_rdf__3)=true)). % 33.28/22.22 tff(c_3800, plain, (icext(uri_rdf_Property, uri_rdf__1)=true)). % 33.28/22.22 tff(c_3762, plain, (icext(uri_rdf_Property, uri_rdf_type)=true)). % 33.28/22.22 tff(c_3719, plain, (icext(uri_rdfs_Datatype, uri_rdf_XMLLiteral)=true)). % 33.28/22.22 tff(c_3681, plain, (icext(uri_rdf_Property, uri_rdf_subject)=true)). % 33.28/22.22 tff(c_3641, plain, (icext(uri_rdfs_ContainerMembershipProperty, uri_rdf__3)=true)). % 33.28/22.22 tff(c_3596, plain, (icext(uri_rdfs_Class, uri_rdf_Property)=true)). % 33.28/22.22 tff(c_3556, plain, (icext(uri_rdfs_ContainerMembershipProperty, uri_rdf__1)=true)). % 33.28/22.22 tff(c_3517, plain, (icext(uri_rdf_List, uri_rdf_nil)=true)). % 33.28/22.22 tff(c_3445, plain, (icext(uri_rdf_Property, uri_rdf_value)=true)). % 33.28/22.22 tff(c_3435, plain, (icext(uri_rdf_Property, uri_rdf_first)=true)). % 33.28/22.22 tff(c_3383, plain, (ip(uri_rdfs_seeAlso)=true)). % 33.28/22.22 tff(c_3342, plain, (ic(uri_rdf_Alt)=true)). % 33.28/22.22 tff(c_3304, plain, (ic(uri_rdfs_Class)=true)). % 33.28/22.22 tff(c_3266, plain, (ic(uri_rdfs_Seq)=true)). % 33.28/22.22 tff(c_3230, plain, (ip(uri_rdfs_isDefinedBy)=true)). % 33.28/22.22 tff(c_3186, plain, (ip(uri_rdfs_subPropertyOf)=true)). % 33.28/22.22 tff(c_3126, plain, (ic(uri_rdfs_Literal)=true)). % 33.28/22.22 tff(c_3116, plain, (ic(uri_rdfs_Datatype)=true)). % 33.28/22.22 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))). % 33.28/22.22 tff(c_3007, plain, (ip(uri_rdf_first)=true)). % 33.28/22.22 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))). % 33.28/22.22 tff(c_2483, plain, (ic(uri_rdfs_ContainerMembershipProperty)=true)). % 33.28/22.22 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))). % 33.28/22.22 tff(c_2431, plain, (ic(uri_rdf_Property)=true)). % 33.28/22.22 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))). % 33.28/22.22 tff(c_2047, plain, (ip(uri_owl_oneOf)=true)). % 33.28/22.22 tff(c_2012, plain, (ic(uri_rdf_Bag)=true)). % 33.28/22.22 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))). % 33.28/22.22 tff(c_1588, plain, (ip(uri_rdfs_subClassOf)=true)). % 33.28/22.22 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))). % 33.28/22.22 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))). % 33.28/22.22 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))). % 33.28/22.22 tff(c_1434, plain, (ip(uri_rdfs_domain)=true)). % 33.28/22.22 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))). % 33.28/22.22 tff(c_1389, plain, (ip(uri_rdfs_range)=true)). % 33.28/22.22 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))). % 33.28/22.22 tff(c_1345, plain, (ip(uri_rdf_subject)=true)). % 33.28/22.22 tff(c_1041, plain, (ip(uri_rdf__3)=true)). % 33.28/22.22 tff(c_4, plain, (![P_4, S_5, O_6]: (ifeq(iext(P_4, S_5, O_6), true, ip(P_4), true)=true))). % 33.28/22.22 tff(c_970, plain, (ic(uri_rdfs_Container)=true)). % 33.28/22.22 tff(c_164, plain, (![P_45, Q_46]: (ifeq(iext(uri_rdfs_subPropertyOf, P_45, Q_46), true, ip(P_45), true)=true))). % 33.28/22.22 tff(c_939, plain, (ip(uri_rdf_value)=true)). % 33.28/22.22 tff(c_150, plain, (![C_35, D_36]: (ifeq(iext(uri_rdfs_subClassOf, C_35, D_36), true, ic(D_36), true)=true))). % 33.28/22.22 tff(c_871, plain, (ic(uri_rdf_XMLLiteral)=true)). % 33.28/22.22 tff(c_152, plain, (![C_37, D_38]: (ifeq(iext(uri_rdfs_subClassOf, C_37, D_38), true, ic(C_37), true)=true))). % 33.28/22.22 tff(c_813, plain, (ip(uri_rdf__1)=true)). % 33.28/22.22 tff(c_780, plain, (ip(uri_rdf_object)=true)). % 33.28/22.22 tff(c_162, plain, (![P_43, Q_44]: (ifeq(iext(uri_rdfs_subPropertyOf, P_43, Q_44), true, ip(Q_44), true)=true))). % 33.28/22.22 tff(c_731, plain, (ip(uri_rdf_rest)=true)). % 33.28/22.22 tff(c_58, plain, (![C_15]: (ifeq(ic(C_15), true, iext(uri_rdfs_subClassOf, C_15, uri_rdfs_Resource), true)=true))). % 33.28/22.22 tff(c_682, plain, (ip(uri_rdf__2)=true)). % 33.28/22.22 tff(c_156, plain, (![C_39]: (ifeq(ic(C_39), true, iext(uri_rdfs_subClassOf, C_39, C_39), true)=true))). % 33.28/22.22 tff(c_645, plain, (ip(uri_rdf_type)=true)). % 33.28/22.22 tff(c_30, plain, (![P_10]: (ifeq(iext(uri_rdf_type, P_10, uri_rdf_Property), true, ip(P_10), true)=true))). % 33.28/22.22 tff(c_28, plain, (![P_9]: (ifeq(ip(P_9), true, iext(uri_rdf_type, P_9, uri_rdf_Property), true)=true))). % 33.28/22.22 tff(c_170, plain, (![P_51]: (ifeq(ip(P_51), true, iext(uri_rdfs_subPropertyOf, P_51, P_51), true)=true))). % 33.28/22.22 tff(c_114, plain, (![X_22]: (ifeq(ic(X_22), true, icext(uri_rdfs_Class, X_22), true)=true))). % 33.28/22.22 tff(c_116, plain, (![X_23]: (ifeq(icext(uri_rdfs_Class, X_23), true, ic(X_23), true)=true))). % 33.28/22.22 tff(c_122, plain, (![X_26]: (ifeq(icext(uri_rdfs_Literal, X_26), true, lv(X_26), true)=true))). % 33.28/22.22 tff(c_124, plain, (![X_27]: (ifeq(lv(X_27), true, icext(uri_rdfs_Literal, X_27), true)=true))). % 33.28/22.22 tff(c_500, plain, (![X_60]: (icext(uri_rdfs_Resource, X_60)=true))). % 33.28/22.22 tff(c_201, plain, (![X_8]: (ifeq(lv(X_8), true, true, true)=true))). % 33.28/22.22 tff(c_2, plain, (![A_1, B_2, C_3]: (ifeq(A_1, A_1, B_2, C_3)=B_2))). % 33.28/22.22 tff(c_174, plain, (iext(uri_rdfs_domain, uri_rdf_type, uri_rdfs_Resource)=true)). % 33.28/22.22 tff(c_146, plain, (iext(uri_rdfs_domain, uri_rdfs_subClassOf, uri_rdfs_Class)=true)). % 33.28/22.22 tff(c_52, plain, (iext(uri_rdfs_range, uri_rdfs_seeAlso, uri_rdfs_Resource)=true)). % 33.28/22.22 tff(c_194, plain, (iext(uri_rdf_first, sK2_testcase_premise_fullish_026_Inferred_Property_Characteristics_I_BNODE_l2, uri_ex_u)=true)). % 33.28/22.22 tff(c_100, plain, (iext(uri_rdfs_subClassOf, uri_rdf_XMLLiteral, uri_rdfs_Literal)=true)). % 33.28/22.22 tff(c_12, plain, (iext(uri_rdf_type, uri_rdf_nil, uri_rdf_List)=true)). % 33.28/22.22 tff(c_10, plain, (iext(uri_rdf_type, uri_rdf_first, uri_rdf_Property)=true)). % 33.28/22.22 tff(c_18, plain, (iext(uri_rdf_type, uri_rdf__2, uri_rdf_Property)=true)). % 33.28/22.22 tff(c_154, plain, (iext(uri_rdfs_range, uri_rdfs_subClassOf, uri_rdfs_Class)=true)). % 33.28/22.22 tff(c_178, plain, (iext(uri_rdfs_domain, uri_rdf_value, uri_rdfs_Resource)=true)). % 33.28/22.22 tff(c_50, plain, (iext(uri_rdfs_domain, uri_rdfs_seeAlso, uri_rdfs_Resource)=true)). % 33.28/22.22 tff(c_132, plain, (iext(uri_rdfs_range, uri_rdfs_range, uri_rdfs_Class)=true)). % 33.28/22.22 tff(c_16, plain, (iext(uri_rdf_type, uri_rdf__1, uri_rdf_Property)=true)). % 33.28/22.22 tff(c_22, plain, (iext(uri_rdf_type, uri_rdf_object, uri_rdf_Property)=true)). % 33.28/22.22 tff(c_20, plain, (iext(uri_rdf_type, uri_rdf__3, uri_rdf_Property)=true)). % 33.28/22.22 tff(c_64, plain, (iext(uri_rdfs_domain, uri_rdf_rest, uri_rdf_List)=true)). % 33.28/22.22 tff(c_60, plain, (iext(uri_rdfs_domain, uri_rdf_first, uri_rdf_List)=true)). % 33.28/22.22 tff(c_188, plain, (iext(uri_rdfs_domain, uri_ex_p, sK3_testcase_premise_fullish_026_Inferred_Property_Characteristics_I_BNODE_x1)=true)). % 33.28/22.22 tff(c_160, plain, (iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, uri_rdf_Property)=true)). % 33.28/22.22 tff(c_182, plain, (iext(uri_owl_oneOf, sK1_testcase_premise_fullish_026_Inferred_Property_Characteristics_I_BNODE_x2, sK2_testcase_premise_fullish_026_Inferred_Property_Characteristics_I_BNODE_l2)=true)). % 33.28/22.22 tff(c_176, plain, (iext(uri_rdfs_range, uri_rdf_type, uri_rdfs_Class)=true)). % 33.28/22.22 tff(c_84, plain, (iext(uri_rdfs_domain, uri_rdf__3, uri_rdfs_Resource)=true)). % 33.28/22.22 tff(c_128, plain, (iext(uri_rdfs_domain, uri_rdfs_range, uri_rdf_Property)=true)). % 33.28/22.22 tff(c_96, plain, (iext(uri_rdf_type, uri_rdf__3, uri_rdfs_ContainerMembershipProperty)=true)). % 33.28/22.22 tff(c_36, plain, (iext(uri_rdfs_domain, uri_rdfs_comment, uri_rdfs_Resource)=true)). % 33.28/22.22 tff(c_144, plain, (iext(uri_rdfs_range, uri_rdf_subject, uri_rdfs_Resource)=true)). % 33.28/22.22 tff(c_42, plain, (iext(uri_rdfs_range, uri_rdfs_isDefinedBy, uri_rdfs_Resource)=true)). % 33.28/22.22 tff(c_108, plain, (iext(uri_rdfs_domain, uri_rdfs_domain, uri_rdf_Property)=true)). % 33.28/22.22 tff(c_112, plain, (iext(uri_rdfs_range, uri_rdfs_domain, uri_rdfs_Class)=true)). % 33.28/22.22 tff(c_98, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Seq, uri_rdfs_Container)=true)). % 33.28/22.22 tff(c_126, plain, (iext(uri_rdf_type, uri_rdf_Property, uri_rdfs_Class)=true)). % 33.28/22.22 tff(c_102, plain, (iext(uri_rdf_type, uri_rdf_XMLLiteral, uri_rdfs_Datatype)=true)). % 33.28/22.22 tff(c_70, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Bag, uri_rdfs_Container)=true)). % 33.28/22.22 tff(c_44, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_isDefinedBy, uri_rdfs_seeAlso)=true)). % 33.28/22.22 tff(c_190, plain, (iext(uri_rdf_rest, sK2_testcase_premise_fullish_026_Inferred_Property_Characteristics_I_BNODE_l2, uri_rdf_nil)=true)). % 33.28/22.22 tff(c_90, plain, (iext(uri_rdfs_range, uri_rdf__3, uri_rdfs_Resource)=true)). % 33.28/22.22 tff(c_40, plain, (iext(uri_rdfs_domain, uri_rdfs_isDefinedBy, uri_rdfs_Resource)=true)). % 33.28/22.22 tff(c_92, plain, (iext(uri_rdf_type, uri_rdf__1, uri_rdfs_ContainerMembershipProperty)=true)). % 33.28/22.22 tff(c_26, plain, (iext(uri_rdf_type, uri_rdf_subject, uri_rdf_Property)=true)). % 33.28/22.22 tff(c_82, plain, (iext(uri_rdfs_domain, uri_rdf__2, uri_rdfs_Resource)=true)). % 33.28/22.22 tff(c_186, plain, (iext(uri_rdfs_range, uri_ex_p, sK1_testcase_premise_fullish_026_Inferred_Property_Characteristics_I_BNODE_x2)=true)). % 33.28/22.22 tff(c_76, plain, (iext(uri_rdfs_domain, uri_rdfs_member, uri_rdfs_Resource)=true)). % 33.28/22.22 tff(c_74, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, uri_rdf_Property)=true)). % 33.28/22.22 tff(c_46, plain, (iext(uri_rdfs_domain, uri_rdfs_label, uri_rdfs_Resource)=true)). % 33.28/22.22 tff(c_48, plain, (iext(uri_rdfs_range, uri_rdfs_label, uri_rdfs_Literal)=true)). % 33.28/22.22 tff(c_24, plain, (iext(uri_rdf_type, uri_rdf_value, uri_rdf_Property)=true)). % 33.28/22.22 tff(c_62, plain, (iext(uri_rdfs_range, uri_rdf_first, uri_rdfs_Resource)=true)). % 33.28/22.22 tff(c_180, plain, (iext(uri_rdfs_range, uri_rdf_value, uri_rdfs_Resource)=true)). % 33.28/22.22 tff(c_78, plain, (iext(uri_rdfs_range, uri_rdfs_member, uri_rdfs_Resource)=true)). % 33.28/22.22 tff(c_80, plain, (iext(uri_rdfs_domain, uri_rdf__1, uri_rdfs_Resource)=true)). % 33.28/22.22 tff(c_88, plain, (iext(uri_rdfs_range, uri_rdf__2, uri_rdfs_Resource)=true)). % 33.28/22.22 tff(c_196, plain, (iext(uri_rdf_first, sK4_testcase_premise_fullish_026_Inferred_Property_Characteristics_I_BNODE_l1, uri_ex_w)=true)). % 33.28/22.22 tff(c_140, plain, (iext(uri_rdfs_range, uri_rdf_predicate, uri_rdfs_Resource)=true)). % 33.28/22.22 tff(c_86, plain, (iext(uri_rdfs_range, uri_rdf__1, uri_rdfs_Resource)=true)). % 33.28/22.22 tff(c_94, plain, (iext(uri_rdf_type, uri_rdf__2, uri_rdfs_ContainerMembershipProperty)=true)). % 33.28/22.22 tff(c_66, plain, (iext(uri_rdfs_range, uri_rdf_rest, uri_rdf_List)=true)). % 33.28/22.22 tff(c_14, plain, (iext(uri_rdf_type, uri_rdf_rest, uri_rdf_Property)=true)). % 33.28/22.22 tff(c_38, plain, (iext(uri_rdfs_range, uri_rdfs_comment, uri_rdfs_Literal)=true)). % 33.28/22.22 tff(c_138, plain, (iext(uri_rdfs_domain, uri_rdf_predicate, uri_rdfs_Statement)=true)). % 33.28/22.22 tff(c_34, plain, (iext(uri_rdf_type, uri_rdf_type, uri_rdf_Property)=true)). % 33.28/22.22 tff(c_68, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Alt, uri_rdfs_Container)=true)). % 33.28/22.22 tff(c_106, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, uri_rdfs_Class)=true)). % 33.28/22.22 tff(c_142, plain, (iext(uri_rdfs_domain, uri_rdf_subject, uri_rdfs_Statement)=true)). % 33.28/22.22 tff(c_134, plain, (iext(uri_rdfs_domain, uri_rdf_object, uri_rdfs_Statement)=true)). % 33.28/22.22 tff(c_168, plain, (iext(uri_rdfs_range, uri_rdfs_subPropertyOf, uri_rdf_Property)=true)). % 33.28/22.22 tff(c_184, plain, (iext(uri_owl_oneOf, sK3_testcase_premise_fullish_026_Inferred_Property_Characteristics_I_BNODE_x1, sK4_testcase_premise_fullish_026_Inferred_Property_Characteristics_I_BNODE_l1)=true)). % 33.28/22.22 tff(c_192, plain, (iext(uri_rdf_rest, sK4_testcase_premise_fullish_026_Inferred_Property_Characteristics_I_BNODE_l1, uri_rdf_nil)=true)). % 33.28/22.22 tff(c_198, plain, (iext(uri_rdf_type, uri_ex_p, uri_owl_InverseFunctionalProperty)!=true)). % 33.28/22.22 tff(c_6, plain, (![X_7]: (ir(X_7)=true))). % 33.28/22.22 % SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 33.28/22.22 %------------------------------------------------------------------------------