%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : SWB028-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/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % Computer : n011.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:57 PM UTC 2025 % Result : Satisfiable 33.88s 20.99s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.02/0.10 % Problem : SWB028-10 : TPTP v9.0.0. Released v7.3.0. % 0.11/0.11 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % 0.11/0.32 % Computer : n011.cluster.edu % 0.11/0.32 % Model : x86_64 x86_64 % 0.11/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.11/0.32 % Memory : 8042.1875MB % 0.11/0.32 % OS : Linux 3.10.0-693.el7.x86_64 % 0.11/0.32 % CPULimit : 300 % 0.11/0.32 % WCLimit : 300 % 0.11/0.32 % DateTime : Wed Apr 9 01:03:33 EDT 2025 % 0.11/0.33 % CPUTime : % 33.88/20.99 % 33.88/20.99 % SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 33.88/20.99 % 33.88/20.99 % SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 33.92/21.01 %$ 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_someValuesFrom > uri_owl_onProperty > uri_owl_inverseOf > uri_owl_equivalentClass > uri_owl_Restriction > uri_owl_InverseFunctionalProperty > uri_owl_FunctionalProperty > uri_ex_InversesOfFunctionalProperties > true > sK1_testcase_premise_fullish_028_Inferred_Property_Characteristics_III_BNODE_z % 33.92/21.01 % 33.92/21.01 %Foreground sorts: % 33.92/21.01 % 33.92/21.01 % 33.92/21.01 %Background operators: % 33.92/21.01 % 33.92/21.01 % 33.92/21.01 %Foreground operators: % 33.92/21.01 tff(uri_owl_InverseFunctionalProperty, type, uri_owl_InverseFunctionalProperty: $i). % 33.92/21.01 tff(uri_rdfs_Datatype, type, uri_rdfs_Datatype: $i). % 33.92/21.01 tff(uri_rdfs_ContainerMembershipProperty, type, uri_rdfs_ContainerMembershipProperty: $i). % 33.92/21.01 tff(uri_rdfs_Resource, type, uri_rdfs_Resource: $i). % 33.92/21.01 tff(uri_rdf_Property, type, uri_rdf_Property: $i). % 33.92/21.01 tff(uri_rdf_subject, type, uri_rdf_subject: $i). % 33.92/21.01 tff(uri_owl_equivalentClass, type, uri_owl_equivalentClass: $i). % 33.92/21.01 tff(uri_rdf_type, type, uri_rdf_type: $i). % 33.92/21.01 tff(uri_owl_onProperty, type, uri_owl_onProperty: $i). % 33.92/21.01 tff(uri_rdfs_subPropertyOf, type, uri_rdfs_subPropertyOf: $i). % 33.92/21.01 tff(uri_rdfs_seeAlso, type, uri_rdfs_seeAlso: $i). % 33.92/21.01 tff(icext, type, icext: ($i * $i) > $i). % 33.92/21.01 tff(uri_rdfs_range, type, uri_rdfs_range: $i). % 33.92/21.01 tff(uri_rdf_XMLLiteral, type, uri_rdf_XMLLiteral: $i). % 33.92/21.01 tff(uri_rdf_List, type, uri_rdf_List: $i). % 33.92/21.01 tff(uri_ex_InversesOfFunctionalProperties, type, uri_ex_InversesOfFunctionalProperties: $i). % 33.92/21.01 tff(uri_rdf_first, type, uri_rdf_first: $i). % 33.92/21.01 tff(uri_rdf_predicate, type, uri_rdf_predicate: $i). % 33.92/21.01 tff(ir, type, ir: $i > $i). % 33.92/21.01 tff(lv, type, lv: $i > $i). % 33.92/21.01 tff(uri_owl_inverseOf, type, uri_owl_inverseOf: $i). % 33.92/21.01 tff(uri_rdf__3, type, uri_rdf__3: $i). % 33.92/21.01 tff(uri_rdf_value, type, uri_rdf_value: $i). % 33.92/21.01 tff(uri_owl_FunctionalProperty, type, uri_owl_FunctionalProperty: $i). % 33.92/21.01 tff(ic, type, ic: $i > $i). % 33.92/21.01 tff(uri_rdfs_Statement, type, uri_rdfs_Statement: $i). % 33.92/21.01 tff(uri_rdf__1, type, uri_rdf__1: $i). % 33.92/21.01 tff(iext, type, iext: ($i * $i * $i) > $i). % 33.92/21.01 tff(uri_owl_Restriction, type, uri_owl_Restriction: $i). % 33.92/21.01 tff(uri_rdf_rest, type, uri_rdf_rest: $i). % 33.92/21.01 tff(uri_rdfs_label, type, uri_rdfs_label: $i). % 33.92/21.01 tff(uri_rdfs_Container, type, uri_rdfs_Container: $i). % 33.92/21.01 tff(uri_rdfs_subClassOf, type, uri_rdfs_subClassOf: $i). % 33.92/21.01 tff(uri_rdf_object, type, uri_rdf_object: $i). % 33.92/21.01 tff(ip, type, ip: $i > $i). % 33.92/21.01 tff(uri_rdfs_Class, type, uri_rdfs_Class: $i). % 33.92/21.01 tff(uri_rdfs_Seq, type, uri_rdfs_Seq: $i). % 33.92/21.01 tff(uri_rdfs_member, type, uri_rdfs_member: $i). % 33.92/21.01 tff(uri_rdf_Bag, type, uri_rdf_Bag: $i). % 33.92/21.01 tff(uri_rdf__2, type, uri_rdf__2: $i). % 33.92/21.01 tff(uri_rdfs_comment, type, uri_rdfs_comment: $i). % 33.92/21.01 tff(uri_rdfs_Literal, type, uri_rdfs_Literal: $i). % 33.92/21.01 tff(true, type, true: $i). % 33.92/21.01 tff(uri_owl_someValuesFrom, type, uri_owl_someValuesFrom: $i). % 33.92/21.01 tff(uri_rdf_Alt, type, uri_rdf_Alt: $i). % 33.92/21.01 tff(uri_rdf_nil, type, uri_rdf_nil: $i). % 33.92/21.01 tff(sK1_testcase_premise_fullish_028_Inferred_Property_Characteristics_III_BNODE_z, type, sK1_testcase_premise_fullish_028_Inferred_Property_Characteristics_III_BNODE_z: $i). % 33.92/21.01 tff(uri_rdfs_isDefinedBy, type, uri_rdfs_isDefinedBy: $i). % 33.92/21.01 tff(uri_rdfs_domain, type, uri_rdfs_domain: $i). % 33.92/21.01 tff(ifeq, type, ifeq: ($i * $i * $i * $i) > $i). % 33.92/21.01 % 33.92/21.01 %Saturated clause set: % 33.92/21.02 tff(c_69484, plain, (![X_1222, Y_1223]: (ifeq(iext(uri_rdf_predicate, X_1222, Y_1223), true, iext(uri_rdf_predicate, X_1222, Y_1223), true)=true))). % 33.92/21.02 tff(c_15591, 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.92/21.02 tff(c_69332, plain, (![X_1217, Y_1218]: (ifeq(iext(uri_rdfs_comment, X_1217, Y_1218), true, iext(uri_rdfs_comment, X_1217, Y_1218), true)=true))). % 33.92/21.02 tff(c_14198, 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.92/21.02 tff(c_15084, 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.92/21.02 tff(c_69055, plain, (![X_1211, Y_1212]: (ifeq(iext(uri_rdfs_label, X_1211, Y_1212), true, iext(uri_rdfs_label, X_1211, Y_1212), true)=true))). % 33.92/21.02 tff(c_69025, plain, (![X_1207, Y_1208]: (ifeq(iext(uri_rdfs_member, X_1207, Y_1208), true, iext(uri_rdfs_member, X_1207, Y_1208), true)=true))). % 33.92/21.02 tff(c_13335, 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.92/21.02 tff(c_13938, 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.92/21.02 tff(c_68626, plain, (![C_1203]: (ifeq(iext(uri_rdfs_subClassOf, C_1203, uri_rdf_List), true, iext(uri_rdfs_subClassOf, C_1203, uri_rdfs_Resource), true)=true))). % 33.92/21.02 tff(c_13164, 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.92/21.02 tff(c_68349, plain, (![C_1200]: (ifeq(iext(uri_rdfs_subClassOf, C_1200, uri_rdfs_Statement), true, iext(uri_rdfs_subClassOf, C_1200, uri_rdfs_Resource), true)=true))). % 33.92/21.02 tff(c_14029, 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.92/21.02 tff(c_13092, 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.92/21.02 tff(c_16578, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subClassOf), true, ifeq(iext(P_47, uri_owl_Restriction, uri_rdfs_Resource), true, true, true), true)=true))). % 33.92/21.02 tff(c_13026, 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.92/21.02 tff(c_16512, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subClassOf), true, ifeq(iext(P_47, uri_owl_Restriction, uri_owl_Restriction), true, true, true), true)=true))). % 33.92/21.02 tff(c_67560, plain, (![C_1193]: (ifeq(iext(uri_rdfs_subClassOf, C_1193, uri_owl_Restriction), true, iext(uri_rdfs_subClassOf, C_1193, uri_rdfs_Resource), true)=true))). % 33.92/21.02 tff(c_11755, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdf_Property), true, ifeq(iext(P_18, uri_owl_someValuesFrom, Y_21), true, true, true), true)=true))). % 33.92/21.02 tff(c_5356, 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.92/21.02 tff(c_12296, 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.92/21.02 tff(c_4821, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdf_Property), true, ifeq(iext(P_18, uri_owl_equivalentClass, Y_21), true, true, true), true)=true))). % 33.92/21.02 tff(c_12952, 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.92/21.02 tff(c_7615, 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.92/21.02 tff(c_4818, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdf_Property), true, ifeq(iext(P_28, X_30, uri_owl_equivalentClass), true, true, true), true)=true))). % 33.92/21.02 tff(c_12905, 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.92/21.02 tff(c_12857, 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.92/21.02 tff(c_7300, 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.92/21.02 tff(c_8671, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdf_Property), true, ifeq(iext(P_28, X_30, uri_owl_onProperty), true, true, true), true)=true))). % 33.92/21.02 tff(c_11132, 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.92/21.02 tff(c_7297, 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.92/21.02 tff(c_12510, 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.92/21.02 tff(c_12443, 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.92/21.02 tff(c_8674, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdf_Property), true, ifeq(iext(P_18, uri_owl_onProperty, Y_21), true, true, true), true)=true))). % 33.92/21.02 tff(c_6243, 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.92/21.02 tff(c_6246, 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.92/21.02 tff(c_7618, 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.92/21.02 tff(c_12343, 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.92/21.02 tff(c_11752, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdf_Property), true, ifeq(iext(P_28, X_30, uri_owl_someValuesFrom), true, true, true), true)=true))). % 33.92/21.02 tff(c_12785, 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.92/21.02 tff(c_12396, 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.92/21.02 tff(c_11135, 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.92/21.02 tff(c_5353, 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.92/21.02 tff(c_13891, 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.92/21.02 tff(c_14958, 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.92/21.03 tff(c_12248, 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.92/21.03 tff(c_12699, 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.92/21.03 tff(c_16465, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, uri_owl_Restriction, uri_rdfs_Class), true, true, true), true)=true))). % 33.92/21.03 tff(c_13551, 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.92/21.03 tff(c_15464, 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.92/21.03 tff(c_12200, 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.92/21.03 tff(c_5593, 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.92/21.03 tff(c_7220, 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.92/21.03 tff(c_62819, plain, (![C_1140]: (ifeq(iext(uri_rdfs_subClassOf, C_1140, uri_rdfs_Container), true, iext(uri_rdfs_subClassOf, C_1140, uri_rdfs_Resource), true)=true))). % 33.92/21.03 tff(c_8506, 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.92/21.03 tff(c_62666, plain, (![X_1135, Y_1136]: (ifeq(iext(uri_rdf__3, X_1135, Y_1136), true, iext(uri_rdf__3, X_1135, Y_1136), true)=true))). % 33.92/21.03 tff(c_62638, plain, (![X_1131, Y_1132]: (ifeq(iext(uri_rdf__1, X_1131, Y_1132), true, iext(uri_rdf__1, X_1131, Y_1132), true)=true))). % 33.92/21.03 tff(c_4393, 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))). % 34.07/21.03 tff(c_62473, plain, (![X_1125, Y_1126]: (ifeq(iext(uri_rdf_first, X_1125, Y_1126), true, iext(uri_rdf_first, X_1125, Y_1126), true)=true))). % 34.07/21.03 tff(c_5903, 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))). % 34.07/21.03 tff(c_6362, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subPropertyOf), true, ifeq(iext(P_47, uri_owl_someValuesFrom, uri_owl_someValuesFrom), true, true, true), true)=true))). % 34.07/21.03 tff(c_62193, plain, (![X_1119, Y_1120]: (ifeq(iext(uri_rdfs_seeAlso, X_1119, Y_1120), true, iext(uri_rdfs_seeAlso, X_1119, Y_1120), true)=true))). % 34.07/21.03 tff(c_10928, 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))). % 34.07/21.03 tff(c_61916, plain, (![C_1116]: (ifeq(iext(uri_rdfs_subClassOf, C_1116, uri_rdfs_Seq), true, iext(uri_rdfs_subClassOf, C_1116, uri_rdfs_Resource), true)=true))). % 34.07/21.03 tff(c_61769, plain, (![C_1114]: (ifeq(iext(uri_rdfs_subClassOf, C_1114, uri_rdfs_Datatype), true, iext(uri_rdfs_subClassOf, C_1114, uri_rdfs_Resource), true)=true))). % 34.07/21.03 tff(c_61699, plain, (![P_1112]: (ifeq(iext(uri_rdfs_subPropertyOf, P_1112, uri_rdf__3), true, iext(uri_rdfs_subPropertyOf, P_1112, uri_rdfs_member), true)=true))). % 34.07/21.03 tff(c_10549, 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))). % 34.07/21.03 tff(c_61546, plain, (![X_1107, Y_1108]: (ifeq(iext(uri_rdf_subject, X_1107, Y_1108), true, iext(uri_rdf_subject, X_1107, Y_1108), true)=true))). % 34.07/21.03 tff(c_4244, 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))). % 34.07/21.03 tff(c_61238, plain, (![X_1100, Y_1101]: (ifeq(iext(uri_rdf__2, X_1100, Y_1101), true, iext(uri_rdfs_member, X_1100, Y_1101), true)=true))). % 34.07/21.03 tff(c_11405, 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))). % 34.07/21.03 tff(c_4086, 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))). % 34.07/21.03 tff(c_9106, 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))). % 34.07/21.03 tff(c_11983, 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))). % 34.07/21.03 tff(c_4492, 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))). % 34.07/21.03 tff(c_11695, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, uri_owl_someValuesFrom, uri_rdf_Property), true, true, true), true)=true))). % 34.07/21.03 tff(c_60423, plain, (![C_1091]: (ifeq(iext(uri_rdfs_subClassOf, C_1091, uri_rdf_Alt), true, iext(uri_rdfs_subClassOf, C_1091, uri_rdfs_Resource), true)=true))). % 34.07/21.03 tff(c_8189, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subPropertyOf), true, ifeq(iext(P_47, uri_owl_equivalentClass, uri_owl_equivalentClass), true, true, true), true)=true))). % 34.07/21.03 tff(c_4440, 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))). % 34.07/21.03 tff(c_6157, 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))). % 34.07/21.03 tff(c_4914, 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))). % 34.09/21.03 tff(c_10135, 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))). % 34.09/21.03 tff(c_59732, plain, (![X_1081, Y_1082]: (ifeq(iext(uri_owl_someValuesFrom, X_1081, Y_1082), true, iext(uri_owl_someValuesFrom, X_1081, Y_1082), true)=true))). % 34.09/21.03 tff(c_5108, 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))). % 34.09/21.03 tff(c_4188, 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))). % 34.09/21.03 tff(c_58830, plain, (![X_1074, Y_1075]: (ifeq(iext(uri_rdfs_subClassOf, X_1074, Y_1075), true, iext(uri_rdfs_subClassOf, X_1074, Y_1075), true)=true))). % 34.09/21.03 tff(c_9490, 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))). % 34.09/21.03 tff(c_58636, plain, (![P_1071]: (ifeq(iext(uri_rdfs_subPropertyOf, P_1071, uri_rdf__2), true, iext(uri_rdfs_subPropertyOf, P_1071, uri_rdfs_member), true)=true))). % 34.09/21.03 tff(c_58482, plain, (![C_1069]: (ifeq(iext(uri_rdfs_subClassOf, C_1069, uri_rdfs_Class), true, iext(uri_rdfs_subClassOf, C_1069, uri_rdfs_Resource), true)=true))). % 34.09/21.03 tff(c_6097, 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))). % 34.09/21.03 tff(c_4145, 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))). % 34.09/21.03 tff(c_4142, 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))). % 34.09/21.03 tff(c_4437, 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))). % 34.09/21.03 tff(c_6976, 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))). % 34.09/21.03 tff(c_8902, 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))). % 34.09/21.03 tff(c_11548, 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))). % 34.09/21.03 tff(c_10235, 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))). % 34.09/21.03 tff(c_57282, plain, (![C_1056]: (ifeq(iext(uri_rdfs_subClassOf, C_1056, uri_rdfs_ContainerMembershipProperty), true, iext(uri_rdfs_subClassOf, C_1056, uri_rdfs_Resource), true)=true))). % 34.09/21.03 tff(c_9197, 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))). % 34.09/21.03 tff(c_4390, 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))). % 34.09/21.03 tff(c_5024, 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))). % 34.09/21.04 tff(c_56264, plain, (![X_1046, Y_1047]: (ifeq(iext(uri_rdfs_range, X_1046, Y_1047), true, iext(uri_rdfs_range, X_1046, Y_1047), true)=true))). % 34.09/21.04 tff(c_56107, plain, (![C_1044]: (ifeq(iext(uri_rdfs_subClassOf, C_1044, uri_rdfs_Literal), true, iext(uri_rdfs_subClassOf, C_1044, uri_rdfs_Resource), true)=true))). % 34.09/21.04 tff(c_55953, plain, (![C_1042]: (ifeq(iext(uri_rdfs_subClassOf, C_1042, uri_rdf_Property), true, iext(uri_rdfs_subClassOf, C_1042, uri_rdfs_Resource), true)=true))). % 34.09/21.04 tff(c_55926, plain, (![X_1038, Y_1039]: (ifeq(iext(uri_rdf_value, X_1038, Y_1039), true, iext(uri_rdf_value, X_1038, Y_1039), true)=true))). % 34.09/21.04 tff(c_55859, plain, (![P_1036]: (ifeq(iext(uri_rdfs_subPropertyOf, P_1036, uri_rdf__1), true, iext(uri_rdfs_subPropertyOf, P_1036, uri_rdfs_member), true)=true))). % 34.09/21.04 tff(c_10705, 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))). % 34.09/21.04 tff(c_4770, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, uri_owl_equivalentClass, uri_rdf_Property), true, true, true), true)=true))). % 34.09/21.04 tff(c_10771, 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))). % 34.09/21.04 tff(c_11639, 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))). % 34.09/21.04 tff(c_55325, plain, (![X_1028, Y_1029]: (ifeq(iext(uri_rdf__3, X_1028, Y_1029), true, iext(uri_rdfs_member, X_1028, Y_1029), true)=true))). % 34.09/21.04 tff(c_4290, 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))). % 34.09/21.04 tff(c_5970, 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))). % 34.09/21.04 tff(c_4339, 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))). % 34.09/21.04 tff(c_54897, plain, (![X_1019, Y_1020]: (ifeq(iext(uri_rdf__2, X_1019, Y_1020), true, iext(uri_rdf__2, X_1019, Y_1020), true)=true))). % 34.09/21.04 tff(c_8619, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, uri_owl_onProperty, uri_rdf_Property), true, true, true), true)=true))). % 34.09/21.04 tff(c_7894, 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))). % 34.09/21.04 tff(c_9425, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subPropertyOf), true, ifeq(iext(P_47, uri_owl_onProperty, uri_owl_onProperty), true, true, true), true)=true))). % 34.09/21.04 tff(c_54158, plain, (![C_1012]: (ifeq(iext(uri_rdfs_subClassOf, C_1012, uri_rdf_Bag), true, iext(uri_rdfs_subClassOf, C_1012, uri_rdfs_Resource), true)=true))). % 34.09/21.04 tff(c_5401, 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))). % 34.09/21.04 tff(c_9732, 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))). % 34.09/21.04 tff(c_53855, plain, (![X_1006, Y_1007]: (ifeq(iext(uri_owl_onProperty, X_1006, Y_1007), true, iext(uri_owl_onProperty, X_1006, Y_1007), true)=true))). % 34.09/21.04 tff(c_6633, 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))). % 34.09/21.04 tff(c_53703, plain, (![X_1001, Y_1002]: (ifeq(iext(uri_rdf__1, X_1001, Y_1002), true, iext(uri_rdfs_member, X_1001, Y_1002), true)=true))). % 34.09/21.04 tff(c_11075, 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))). % 34.09/21.04 tff(c_11271, 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))). % 34.09/21.04 tff(c_53397, plain, (![X_995, Y_996]: (ifeq(iext(uri_owl_equivalentClass, X_995, Y_996), true, iext(uri_owl_equivalentClass, X_995, Y_996), true)=true))). % 34.09/21.04 tff(c_6781, 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))). % 34.09/21.04 tff(c_8083, 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))). % 34.09/21.04 tff(c_5285, 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))). % 34.09/21.04 tff(c_52983, plain, (![X_988, Y_989]: (ifeq(iext(uri_rdfs_isDefinedBy, X_988, Y_989), true, iext(uri_rdfs_isDefinedBy, X_988, Y_989), true)=true))). % 34.09/21.04 tff(c_7826, 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))). % 34.09/21.04 tff(c_7564, 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))). % 34.09/21.04 tff(c_10395, 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))). % 34.09/21.04 tff(c_4083, 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))). % 34.09/21.04 tff(c_51511, plain, (![X_977, Y_978]: (ifeq(iext(uri_rdf_type, X_977, Y_978), true, iext(uri_rdf_type, X_977, Y_978), true)=true))). % 34.09/21.04 tff(c_5746, 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))). % 34.09/21.04 tff(c_6723, 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))). % 34.09/21.04 tff(c_5654, 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))). % 34.09/21.04 tff(c_10457, 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))). % 34.09/21.04 tff(c_4247, 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))). % 34.09/21.04 tff(c_4489, 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))). % 34.09/21.04 tff(c_49966, plain, (![X_963, Y_964]: (ifeq(iext(uri_rdfs_subPropertyOf, X_963, Y_964), true, iext(uri_rdfs_subPropertyOf, X_963, Y_964), true)=true))). % 34.09/21.04 tff(c_5477, 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))). % 34.09/21.04 tff(c_49694, plain, (![C_960]: (ifeq(iext(uri_rdfs_subClassOf, C_960, uri_rdf_XMLLiteral), true, iext(uri_rdfs_subClassOf, C_960, uri_rdfs_Resource), true)=true))). % 34.09/21.04 tff(c_10620, 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))). % 34.09/21.04 tff(c_4185, 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))). % 34.09/21.04 tff(c_49088, plain, (![X_951, Y_952]: (ifeq(iext(uri_rdf_rest, X_951, Y_952), true, iext(uri_rdf_rest, X_951, Y_952), true)=true))). % 34.09/21.04 tff(c_4336, 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))). % 34.09/21.04 tff(c_11921, 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))). % 34.09/21.04 tff(c_4293, 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))). % 34.09/21.04 tff(c_48125, plain, (![X_940, Y_941]: (ifeq(iext(uri_rdfs_domain, X_940, Y_941), true, iext(uri_rdfs_domain, X_940, Y_941), true)=true))). % 34.09/21.04 tff(c_48098, plain, (![X_936, Y_937]: (ifeq(iext(uri_rdf_object, X_936, Y_937), true, iext(uri_rdf_object, X_936, Y_937), true)=true))). % 34.09/21.04 tff(c_16235, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdfs_Class), true, ifeq(iext(P_18, uri_owl_Restriction, Y_21), true, true, true), true)=true))). % 34.09/21.04 tff(c_6442, 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))). % 34.09/21.04 tff(c_15310, 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))). % 34.09/21.04 tff(c_15307, 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))). % 34.09/21.04 tff(c_7702, 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))). % 34.09/21.04 tff(c_14804, 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))). % 34.09/21.04 tff(c_16232, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdfs_Class), true, ifeq(iext(P_28, X_30, uri_owl_Restriction), true, true, true), true)=true))). % 34.09/21.04 tff(c_8271, 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))). % 34.09/21.04 tff(c_12563, 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))). % 34.09/21.04 tff(c_4679, plain, (![P_47, X_138]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, X_138, uri_rdfs_Resource), true, true, true), true)=true))). % 34.09/21.04 tff(c_13404, 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))). % 34.09/21.04 tff(c_13671, 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))). % 34.09/21.04 tff(c_14801, 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))). % 34.09/21.04 tff(c_12560, 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))). % 34.09/21.04 tff(c_8268, 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))). % 34.09/21.04 tff(c_13668, 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))). % 34.09/21.04 tff(c_7705, 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))). % 34.09/21.04 tff(c_13407, 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))). % 34.09/21.04 tff(c_6445, 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))). % 34.09/21.04 tff(c_3423, 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))). % 34.09/21.04 tff(c_3952, 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))). % 34.09/21.05 tff(c_3949, 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))). % 34.09/21.05 tff(c_3521, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdf_Property), true, ifeq(iext(P_28, X_30, uri_rdf__1), true, true, true), true)=true))). % 34.09/21.05 tff(c_3759, 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))). % 34.09/21.05 tff(c_3715, 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))). % 34.09/21.05 tff(c_3635, 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))). % 34.09/21.05 tff(c_3995, 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))). % 34.09/21.05 tff(c_3475, 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))). % 34.09/21.05 tff(c_3550, 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))). % 34.09/21.05 tff(c_4035, 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))). % 34.09/21.05 tff(c_4038, 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))). % 34.09/21.05 tff(c_3665, 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))). % 34.09/21.05 tff(c_3426, 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))). % 34.09/21.05 tff(c_3638, 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))). % 34.09/21.05 tff(c_3789, 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))). % 34.09/21.05 tff(c_3588, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_owl_Restriction), true, ifeq(iext(P_28, X_30, sK1_testcase_premise_fullish_028_Inferred_Property_Characteristics_III_BNODE_z), true, true, true), true)=true))). % 34.09/21.05 tff(c_3712, 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))). % 34.09/21.05 tff(c_3668, 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))). % 34.09/21.05 tff(c_3591, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_owl_Restriction), true, ifeq(iext(P_18, sK1_testcase_premise_fullish_028_Inferred_Property_Characteristics_III_BNODE_z, Y_21), true, true, true), true)=true))). % 34.09/21.05 tff(c_3547, 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))). % 34.09/21.05 tff(c_3864, 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))). % 34.09/21.05 tff(c_3524, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdf_Property), true, ifeq(iext(P_18, uri_rdf__1, Y_21), true, true, true), true)=true))). % 34.09/21.05 tff(c_3823, 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))). % 34.09/21.05 tff(c_3826, 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))). % 34.09/21.05 tff(c_3762, 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))). % 34.09/21.05 tff(c_3786, 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))). % 34.09/21.05 tff(c_3914, 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))). % 34.09/21.05 tff(c_3911, 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))). % 34.09/21.05 tff(c_3867, 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))). % 34.09/21.05 tff(c_3998, 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))). % 34.09/21.05 tff(c_3472, 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))). % 34.09/21.05 tff(c_1949, plain, (![P_96, X_98, X_61]: (ifeq(iext(uri_rdfs_range, P_96, uri_rdfs_Resource), true, ifeq(iext(P_96, X_98, X_61), true, true, true), true)=true))). % 34.09/21.05 tff(c_1588, plain, (![P_92, X_61, Y_95]: (ifeq(iext(uri_rdfs_domain, P_92, uri_rdfs_Resource), true, ifeq(iext(P_92, X_61, Y_95), true, true, true), true)=true))). % 34.09/21.05 tff(c_2663, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdf_type), true, ifeq(iext(P_106, uri_rdf__3, uri_rdf_Property), true, true, true), true)=true))). % 34.09/21.05 tff(c_2528, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdf_type), true, ifeq(iext(P_106, uri_rdf__2, uri_rdf_Property), true, true, true), true)=true))). % 34.09/21.05 tff(c_2687, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_subClassOf), true, ifeq(iext(P_106, uri_rdf_Alt, uri_rdfs_Container), true, true, true), true)=true))). % 34.09/21.05 tff(c_38898, plain, (![C_823]: (ifeq(iext(uri_rdfs_subClassOf, C_823, uri_rdf_XMLLiteral), true, iext(uri_rdfs_subClassOf, C_823, uri_rdfs_Literal), true)=true))). % 34.09/21.05 tff(c_2564, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdf_type), true, ifeq(iext(P_106, sK1_testcase_premise_fullish_028_Inferred_Property_Characteristics_III_BNODE_z, uri_owl_Restriction), true, true, true), true)=true))). % 34.09/21.05 tff(c_38722, plain, (![P_820]: (ifeq(iext(uri_rdfs_subPropertyOf, P_820, uri_rdfs_isDefinedBy), true, iext(uri_rdfs_subPropertyOf, P_820, uri_rdfs_seeAlso), true)=true))). % 34.09/21.05 tff(c_2801, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdf_type), true, ifeq(iext(P_106, uri_rdf_nil, uri_rdf_List), true, true, true), true)=true))). % 34.09/21.05 tff(c_2711, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_domain), true, ifeq(iext(P_106, uri_rdf_value, uri_rdfs_Resource), true, true, true), true)=true))). % 34.09/21.05 tff(c_2582, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdf_type), true, ifeq(iext(P_106, uri_rdf_subject, uri_rdf_Property), true, true, true), true)=true))). % 34.09/21.05 tff(c_38270, plain, (![C_815]: (ifeq(iext(uri_rdfs_subClassOf, C_815, uri_rdf_Bag), true, iext(uri_rdfs_subClassOf, C_815, uri_rdfs_Container), true)=true))). % 34.09/21.05 tff(c_2639, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_domain), true, ifeq(iext(P_106, uri_rdfs_isDefinedBy, uri_rdfs_Resource), true, true, true), true)=true))). % 34.09/21.05 tff(c_2510, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdf_type), true, ifeq(iext(P_106, uri_rdf__3, uri_rdfs_ContainerMembershipProperty), true, true, true), true)=true))). % 34.09/21.05 tff(c_2504, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_subClassOf), true, ifeq(iext(P_106, uri_rdf_XMLLiteral, uri_rdfs_Literal), true, true, true), true)=true))). % 34.09/21.05 tff(c_2540, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_range), true, ifeq(iext(P_106, uri_rdf_value, uri_rdfs_Resource), true, true, true), true)=true))). % 34.09/21.05 tff(c_2675, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_range), true, ifeq(iext(P_106, uri_rdfs_domain, uri_rdfs_Class), true, true, true), true)=true))). % 34.09/21.05 tff(c_2735, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_domain), true, ifeq(iext(P_106, uri_rdf__2, uri_rdfs_Resource), true, true, true), true)=true))). % 34.09/21.05 tff(c_2486, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdf_type), true, ifeq(iext(P_106, uri_rdf__2, uri_rdfs_ContainerMembershipProperty), true, true, true), true)=true))). % 34.09/21.05 tff(c_2576, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_range), true, ifeq(iext(P_106, uri_rdf__2, uri_rdfs_Resource), true, true, true), true)=true))). % 34.09/21.05 tff(c_37167, plain, (![C_805]: (ifeq(iext(uri_rdfs_subClassOf, C_805, uri_rdf_Alt), true, iext(uri_rdfs_subClassOf, C_805, uri_rdfs_Container), true)=true))). % 34.09/21.05 tff(c_2603, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_subPropertyOf), true, ifeq(iext(P_106, uri_rdfs_isDefinedBy, uri_rdfs_seeAlso), true, true, true), true)=true))). % 34.09/21.05 tff(c_2681, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_domain), true, ifeq(iext(P_106, uri_rdf__3, uri_rdfs_Resource), true, true, true), true)=true))). % 34.09/21.05 tff(c_2669, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_range), true, ifeq(iext(P_106, uri_rdf__1, uri_rdfs_Resource), true, true, true), true)=true))). % 34.09/21.05 tff(c_2783, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_range), true, ifeq(iext(P_106, uri_rdf_rest, uri_rdf_List), true, true, true), true)=true))). % 34.09/21.05 tff(c_2813, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdf_type), true, ifeq(iext(P_106, uri_rdf_Property, uri_rdfs_Class), true, true, true), true)=true))). % 34.09/21.05 tff(c_2717, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_domain), true, ifeq(iext(P_106, uri_rdfs_member, uri_rdfs_Resource), true, true, true), true)=true))). % 34.09/21.05 tff(c_2777, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdf_type), true, ifeq(iext(P_106, uri_rdf_value, uri_rdf_Property), true, true, true), true)=true))). % 34.09/21.05 tff(c_36233, plain, (![X_794, Y_795]: (ifeq(iext(uri_rdfs_isDefinedBy, X_794, Y_795), true, iext(uri_rdfs_seeAlso, X_794, Y_795), true)=true))). % 34.09/21.05 tff(c_2795, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdf_type), true, ifeq(iext(P_106, uri_rdf_first, uri_rdf_Property), true, true, true), true)=true))). % 34.09/21.05 tff(c_2546, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_domain), true, ifeq(iext(P_106, uri_rdfs_seeAlso, uri_rdfs_Resource), true, true, true), true)=true))). % 34.09/21.05 tff(c_2522, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdf_type), true, ifeq(iext(P_106, uri_rdf__1, uri_rdfs_ContainerMembershipProperty), true, true, true), true)=true))). % 34.09/21.05 tff(c_2468, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_range), true, ifeq(iext(P_106, uri_rdfs_isDefinedBy, uri_rdfs_Resource), true, true, true), true)=true))). % 34.09/21.05 tff(c_2651, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_domain), true, ifeq(iext(P_106, uri_rdf__1, uri_rdfs_Resource), true, true, true), true)=true))). % 34.09/21.05 tff(c_2759, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_domain), true, ifeq(iext(P_106, uri_rdf_predicate, uri_rdfs_Statement), true, true, true), true)=true))). % 34.09/21.05 tff(c_2480, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_owl_equivalentClass), true, ifeq(iext(P_106, uri_ex_InversesOfFunctionalProperties, sK1_testcase_premise_fullish_028_Inferred_Property_Characteristics_III_BNODE_z), true, true, true), true)=true))). % 34.09/21.05 tff(c_2699, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_range), true, ifeq(iext(P_106, uri_rdfs_comment, uri_rdfs_Literal), true, true, true), true)=true))). % 34.09/21.05 tff(c_2771, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_domain), true, ifeq(iext(P_106, uri_rdf_first, uri_rdf_List), true, true, true), true)=true))). % 34.09/21.05 tff(c_2621, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_domain), true, ifeq(iext(P_106, uri_rdf_subject, uri_rdfs_Statement), true, true, true), true)=true))). % 34.09/21.05 tff(c_2807, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_range), true, ifeq(iext(P_106, uri_rdfs_range, uri_rdfs_Class), true, true, true), true)=true))). % 34.09/21.05 tff(c_2633, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdf_type), true, ifeq(iext(P_106, uri_rdf__1, uri_rdf_Property), true, true, true), true)=true))). % 34.09/21.05 tff(c_2657, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_range), true, ifeq(iext(P_106, uri_rdf_predicate, uri_rdfs_Resource), true, true, true), true)=true))). % 34.09/21.05 tff(c_2765, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_domain), true, ifeq(iext(P_106, uri_rdfs_comment, uri_rdfs_Resource), true, true, true), true)=true))). % 34.09/21.05 tff(c_34393, plain, (![C_778]: (ifeq(iext(uri_rdfs_subClassOf, C_778, uri_rdfs_Datatype), true, iext(uri_rdfs_subClassOf, C_778, uri_rdfs_Class), true)=true))). % 34.09/21.05 tff(c_2729, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_subClassOf), true, ifeq(iext(P_106, uri_rdfs_ContainerMembershipProperty, uri_rdf_Property), true, true, true), true)=true))). % 34.09/21.05 tff(c_2693, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_domain), true, ifeq(iext(P_106, uri_rdf_object, uri_rdfs_Statement), true, true, true), true)=true))). % 34.09/21.05 tff(c_2534, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_domain), true, ifeq(iext(P_106, uri_rdf_type, uri_rdfs_Resource), true, true, true), true)=true))). % 34.09/21.05 tff(c_2825, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_range), true, ifeq(iext(P_106, uri_rdf_type, uri_rdfs_Class), true, true, true), true)=true))). % 34.09/21.05 tff(c_33822, plain, (![D_772]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_772), true, icext(D_772, uri_rdfs_subPropertyOf), true)=true))). % 34.09/21.05 tff(c_33756, plain, (![D_770]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_770), true, icext(D_770, uri_rdfs_subClassOf), true)=true))). % 34.09/21.05 tff(c_2747, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_domain), true, ifeq(iext(P_106, uri_rdfs_range, uri_rdf_Property), true, true, true), true)=true))). % 34.09/21.06 tff(c_33560, plain, (![D_767]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_767), true, icext(D_767, uri_rdfs_range), true)=true))). % 34.09/21.06 tff(c_33494, plain, (![D_765]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_765), true, icext(D_765, uri_owl_onProperty), true)=true))). % 34.09/21.06 tff(c_33428, plain, (![D_763]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_763), true, icext(D_763, uri_rdfs_domain), true)=true))). % 34.09/21.06 tff(c_2627, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_domain), true, ifeq(iext(P_106, uri_rdf_rest, uri_rdf_List), true, true, true), true)=true))). % 34.09/21.06 tff(c_33233, plain, (![D_760]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_760), true, icext(D_760, uri_rdfs_isDefinedBy), true)=true))). % 34.09/21.06 tff(c_33167, plain, (![D_758]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_758), true, icext(D_758, uri_owl_equivalentClass), true)=true))). % 34.09/21.06 tff(c_33101, plain, (![D_756]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_756), true, icext(D_756, uri_owl_someValuesFrom), true)=true))). % 34.09/21.06 tff(c_33032, plain, (![D_754]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_754), true, icext(D_754, uri_rdfs_ContainerMembershipProperty), true)=true))). % 34.09/21.06 tff(c_32966, plain, (![D_752]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_752), true, icext(D_752, uri_rdf_Bag), true)=true))). % 34.09/21.06 tff(c_2474, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdf_type), true, ifeq(iext(P_106, uri_rdf_rest, uri_rdf_Property), true, true, true), true)=true))). % 34.09/21.06 tff(c_32775, plain, (![D_749]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_749), true, icext(D_749, uri_rdf_Alt), true)=true))). % 34.09/21.06 tff(c_32681, plain, (![D_747]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_747), true, icext(D_747, uri_rdfs_Class), true)=true))). % 34.09/21.06 tff(c_2723, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_subClassOf), true, ifeq(iext(P_106, uri_rdf_Bag, uri_rdfs_Container), true, true, true), true)=true))). % 34.09/21.06 tff(c_32486, plain, (![D_744]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_744), true, icext(D_744, uri_rdfs_Seq), true)=true))). % 34.09/21.06 tff(c_32411, plain, (![D_742]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_742), true, icext(D_742, uri_rdf_XMLLiteral), true)=true))). % 34.09/21.06 tff(c_2552, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_range), true, ifeq(iext(P_106, uri_rdf_subject, uri_rdfs_Resource), true, true, true), true)=true))). % 34.09/21.06 tff(c_32214, plain, (![D_739]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_739), true, icext(D_739, uri_rdfs_Container), true)=true))). % 34.09/21.06 tff(c_32148, plain, (![D_737]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_737), true, icext(D_737, uri_rdfs_Literal), true)=true))). % 34.09/21.06 tff(c_32082, plain, (![D_735]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_735), true, icext(D_735, uri_rdfs_Datatype), true)=true))). % 34.09/21.06 tff(c_2570, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_range), true, ifeq(iext(P_106, uri_rdf__3, uri_rdfs_Resource), true, true, true), true)=true))). % 34.09/21.06 tff(c_31881, plain, (![D_732]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_732), true, icext(D_732, uri_rdfs_seeAlso), true)=true))). % 34.09/21.06 tff(c_31815, plain, (![D_730]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_730), true, icext(D_730, uri_rdf_List), true)=true))). % 34.09/21.06 tff(c_31749, plain, (![D_728]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_728), true, icext(D_728, uri_rdf_predicate), true)=true))). % 34.09/21.06 tff(c_31682, plain, (![D_726]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_726), true, icext(D_726, uri_rdfs_Resource), true)=true))). % 34.09/21.06 tff(c_31616, plain, (![D_724]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_724), true, icext(D_724, uri_rdfs_label), true)=true))). % 34.09/21.06 tff(c_31419, plain, (![D_721]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_721), true, icext(D_721, uri_rdfs_Statement), true)=true))). % 34.09/21.06 tff(c_2789, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_range), true, ifeq(iext(P_106, uri_rdf_first, uri_rdfs_Resource), true, true, true), true)=true))). % 34.09/21.06 tff(c_31353, plain, (![D_719]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_719), true, icext(D_719, uri_rdfs_comment), true)=true))). % 34.09/21.06 tff(c_31286, plain, (![D_717]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_717), true, icext(D_717, uri_rdfs_member), true)=true))). % 34.09/21.06 tff(c_2492, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_range), true, ifeq(iext(P_106, uri_rdfs_subPropertyOf, uri_rdf_Property), true, true, true), true)=true))). % 34.09/21.06 tff(c_31087, plain, (![D_714]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_714), true, icext(D_714, uri_owl_Restriction), true)=true))). % 34.09/21.06 tff(c_14229, 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))). % 34.09/21.06 tff(c_15622, 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))). % 34.09/21.06 tff(c_15115, 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))). % 34.09/21.06 tff(c_2753, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_range), true, ifeq(iext(P_106, uri_rdfs_member, uri_rdfs_Resource), true, true, true), true)=true))). % 34.09/21.06 tff(c_13369, 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))). % 34.09/21.06 tff(c_30703, plain, (![D_702]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_702), true, icext(D_702, uri_rdf_value), true)=true))). % 34.09/21.06 tff(c_13060, 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))). % 34.09/21.06 tff(c_16613, plain, (![E_41]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Resource, E_41), true, iext(uri_rdfs_subClassOf, uri_owl_Restriction, E_41), true)=true))). % 34.09/21.06 tff(c_2516, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_subClassOf), true, ifeq(iext(P_106, uri_rdfs_Seq, uri_rdfs_Container), true, true, true), true)=true))). % 34.09/21.06 tff(c_13129, 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))). % 34.09/21.06 tff(c_14064, 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))). % 34.09/21.06 tff(c_13198, 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))). % 34.09/21.06 tff(c_13199, 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))). % 34.09/21.06 tff(c_16612, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_48), true, iext(Q_48, uri_owl_Restriction, uri_rdfs_Resource), true)=true))). % 34.09/21.06 tff(c_14063, 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))). % 34.09/21.06 tff(c_2741, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_range), true, ifeq(iext(P_106, uri_rdfs_label, uri_rdfs_Literal), true, true, true), true)=true))). % 34.09/21.06 tff(c_16546, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_48), true, iext(Q_48, uri_owl_Restriction, uri_owl_Restriction), true)=true))). % 34.09/21.06 tff(c_13972, 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))). % 34.09/21.06 tff(c_12315, 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))). % 34.09/21.06 tff(c_12876, 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))). % 34.09/21.06 tff(c_12415, 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))). % 34.09/21.06 tff(c_12462, 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))). % 34.09/21.06 tff(c_12924, 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))). % 34.09/21.06 tff(c_12362, 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))). % 34.09/21.06 tff(c_2615, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_range), true, ifeq(iext(P_106, uri_rdfs_subClassOf, uri_rdfs_Class), true, true, true), true)=true))). % 34.09/21.06 tff(c_12971, 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))). % 34.09/21.06 tff(c_12529, 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))). % 34.09/21.06 tff(c_12804, 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))). % 34.09/21.06 tff(c_29838, plain, (![D_675]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_675), true, icext(D_675, uri_rdf__1), true)=true))). % 34.09/21.06 tff(c_13576, 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))). % 34.09/21.06 tff(c_14983, 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))). % 34.09/21.06 tff(c_12724, 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))). % 34.09/21.06 tff(c_2594, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_domain), true, ifeq(iext(P_106, uri_rdfs_label, uri_rdfs_Resource), true, true, true), true)=true))). % 34.09/21.06 tff(c_15489, 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))). % 34.09/21.06 tff(c_16484, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, uri_owl_Restriction, uri_rdfs_Class), true)=true))). % 34.09/21.06 tff(c_12219, 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))). % 34.09/21.06 tff(c_29552, plain, (![D_666]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_666), true, icext(D_666, uri_rdf_first), true)=true))). % 34.09/21.06 tff(c_12267, 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))). % 34.09/21.06 tff(c_13910, 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))). % 34.09/21.06 tff(c_10426, 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))). % 34.09/21.06 tff(c_2462, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_domain), true, ifeq(iext(P_106, uri_rdfs_domain, uri_rdf_Property), true, true, true), true)=true))). % 34.09/21.06 tff(c_9140, 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))). % 34.09/21.06 tff(c_29235, plain, (![D_657]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, D_657), true, icext(D_657, uri_rdf_XMLLiteral), true)=true))). % 34.09/21.06 tff(c_4795, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, uri_owl_equivalentClass, uri_rdf_Property), true)=true))). % 34.09/21.06 tff(c_10491, 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))). % 34.09/21.06 tff(c_2456, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_subClassOf), true, ifeq(iext(P_106, uri_rdfs_Datatype, uri_rdfs_Class), true, true, true), true)=true))). % 34.09/21.06 tff(c_9231, 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))). % 34.09/21.06 tff(c_5684, 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))). % 34.09/21.06 tff(c_5431, 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))). % 34.09/21.06 tff(c_10172, 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))). % 34.09/21.06 tff(c_11306, 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))). % 34.09/21.06 tff(c_12017, 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))). % 34.09/21.06 tff(c_10427, 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))). % 34.09/21.06 tff(c_2558, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdf_type), true, ifeq(iext(P_106, uri_rdf_object, uri_rdf_Property), true, true, true), true)=true))). % 34.09/21.06 tff(c_5057, 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))). % 34.09/21.06 tff(c_12018, 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))). % 34.09/21.06 tff(c_28639, plain, (![D_639]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_639), true, icext(D_639, uri_rdf_subject), true)=true))). % 34.09/21.06 tff(c_10805, 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))). % 34.09/21.06 tff(c_10739, 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))). % 34.09/21.06 tff(c_5623, 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))). % 34.09/21.06 tff(c_8937, 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))). % 34.09/21.06 tff(c_6182, 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))). % 34.09/21.06 tff(c_10962, 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))). % 34.09/21.06 tff(c_10963, 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))). % 34.09/21.07 tff(c_5776, 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))). % 34.09/21.07 tff(c_6127, 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))). % 34.09/21.07 tff(c_9456, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_48), true, iext(Q_48, uri_owl_onProperty, uri_owl_onProperty), true)=true))). % 34.09/21.07 tff(c_2645, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_domain), true, ifeq(iext(P_106, uri_rdfs_subClassOf, uri_rdfs_Class), true, true, true), true)=true))). % 34.09/21.07 tff(c_7924, 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))). % 34.09/21.07 tff(c_11440, 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))). % 34.09/21.07 tff(c_7006, 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))). % 34.09/21.07 tff(c_5507, 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))). % 34.09/21.07 tff(c_7861, 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))). % 34.09/21.07 tff(c_2819, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_domain), true, ifeq(iext(P_106, uri_rdfs_subPropertyOf, uri_rdf_Property), true, true, true), true)=true))). % 34.09/21.07 tff(c_6753, 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))). % 34.09/21.07 tff(c_6664, 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))). % 34.09/21.07 tff(c_8117, 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))). % 34.09/21.07 tff(c_10270, 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))). % 34.09/21.07 tff(c_7245, 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))). % 34.09/21.07 tff(c_8537, 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))). % 34.09/21.07 tff(c_2609, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdf_type), true, ifeq(iext(P_106, uri_rdf_type, uri_rdf_Property), true, true, true), true)=true))). % 34.09/21.07 tff(c_6815, 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))). % 34.09/21.07 tff(c_9521, 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))). % 34.09/21.07 tff(c_6393, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_48), true, iext(Q_48, uri_owl_someValuesFrom, uri_owl_someValuesFrom), true)=true))). % 34.09/21.07 tff(c_8219, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_48), true, iext(Q_48, uri_owl_equivalentClass, uri_owl_equivalentClass), true)=true))). % 34.09/21.07 tff(c_2705, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_owl_someValuesFrom), true, ifeq(iext(P_106, sK1_testcase_premise_fullish_028_Inferred_Property_Characteristics_III_BNODE_z, uri_owl_FunctionalProperty), true, true, true), true)=true))). % 34.09/21.07 tff(c_10583, 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))). % 34.09/21.07 tff(c_11952, 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))). % 34.09/21.07 tff(c_5310, 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))). % 34.09/21.07 tff(c_27275, plain, (![D_595]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, D_595), true, icext(D_595, uri_rdf__1), true)=true))). % 34.09/21.07 tff(c_8118, 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))). % 34.09/21.07 tff(c_11720, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, uri_owl_someValuesFrom, uri_rdf_Property), true)=true))). % 34.09/21.07 tff(c_2498, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_range), true, ifeq(iext(P_106, uri_rdfs_seeAlso, uri_rdfs_Resource), true, true, true), true)=true))). % 34.09/21.07 tff(c_7925, 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))). % 34.09/21.07 tff(c_11439, 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))). % 34.09/21.07 tff(c_5933, 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))). % 34.09/21.07 tff(c_11100, 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))). % 34.09/21.07 tff(c_8936, 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))). % 34.09/21.07 tff(c_10651, 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))). % 34.09/21.07 tff(c_2831, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_owl_onProperty), true, ifeq(iext(P_106, sK1_testcase_premise_fullish_028_Inferred_Property_Characteristics_III_BNODE_z, uri_owl_inverseOf), true, true, true), true)=true))). % 34.09/21.07 tff(c_8644, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, uri_owl_onProperty, uri_rdf_Property), true)=true))). % 34.09/21.07 tff(c_4944, 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))). % 34.09/21.07 tff(c_11305, 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))). % 34.09/21.07 tff(c_10269, 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))). % 34.09/21.07 tff(c_9767, 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))). % 34.09/21.07 tff(c_26558, plain, (![C_574]: (ifeq(iext(uri_rdfs_subClassOf, C_574, uri_rdfs_Seq), true, iext(uri_rdfs_subClassOf, C_574, uri_rdfs_Container), true)=true))). % 34.09/21.07 tff(c_7589, 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))). % 34.09/21.07 tff(c_11582, 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))). % 34.09/21.07 tff(c_5139, 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))). % 34.09/21.07 tff(c_26372, plain, (![C_566]: (ifeq(iext(uri_rdfs_subClassOf, C_566, uri_rdfs_ContainerMembershipProperty), true, iext(uri_rdfs_subClassOf, C_566, uri_rdf_Property), true)=true))). % 34.09/21.07 tff(c_9766, 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))). % 34.09/21.07 tff(c_26240, plain, (![D_561]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_561), true, icext(D_561, uri_rdf_type), true)=true))). % 34.09/21.07 tff(c_5138, 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))). % 34.09/21.07 tff(c_2588, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdf_type), true, ifeq(iext(P_106, uri_rdf_XMLLiteral, uri_rdfs_Datatype), true, true, true), true)=true))). % 34.09/21.07 tff(c_6814, 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))). % 34.09/21.07 tff(c_11664, 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))). % 34.09/21.07 tff(c_10740, 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))). % 34.09/21.07 tff(c_6003, 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))). % 34.09/21.07 tff(c_4699, plain, (![Q_48, X_138]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, X_138, uri_rdfs_Resource), true)=true))). % 34.09/21.07 tff(c_2892, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_107), true, iext(Q_107, uri_rdf_first, uri_rdf_Property), true)=true))). % 34.09/21.07 tff(c_2882, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_107), true, iext(Q_107, uri_rdf__2, uri_rdfs_Resource), true)=true))). % 34.09/21.07 tff(c_2896, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_107), true, iext(Q_107, uri_rdfs_subPropertyOf, uri_rdf_Property), true)=true))). % 34.09/21.07 tff(c_2863, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_107), true, iext(Q_107, uri_rdf_subject, uri_rdfs_Statement), true)=true))). % 34.09/21.07 tff(c_2871, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_107), true, iext(Q_107, uri_rdf__1, uri_rdfs_Resource), true)=true))). % 34.09/21.07 tff(c_25578, plain, (![D_542]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_542), true, icext(D_542, uri_rdf_rest), true)=true))). % 34.09/21.07 tff(c_2836, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_107), true, iext(Q_107, uri_rdfs_Datatype, uri_rdfs_Class), true)=true))). % 34.09/21.07 tff(c_2369, plain, (![E_101]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, E_101), true, iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, E_101), true)=true))). % 34.09/21.07 tff(c_2852, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_107), true, iext(Q_107, uri_rdf_subject, uri_rdfs_Resource), true)=true))). % 34.09/21.07 tff(c_2842, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_107), true, iext(Q_107, uri_rdfs_subPropertyOf, uri_rdf_Property), true)=true))). % 34.09/21.07 tff(c_2874, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_107), true, iext(Q_107, uri_rdf_Alt, uri_rdfs_Container), true)=true))). % 34.09/21.07 tff(c_2862, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_107), true, iext(Q_107, uri_rdfs_subClassOf, uri_rdfs_Class), true)=true))). % 34.09/21.07 tff(c_2843, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_107), true, iext(Q_107, uri_rdfs_seeAlso, uri_rdfs_Resource), true)=true))). % 34.09/21.07 tff(c_25349, plain, (![D_533]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, D_533), true, icext(D_533, uri_rdf__2), true)=true))). % 34.09/21.07 tff(c_2876, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_107), true, iext(Q_107, uri_rdfs_comment, uri_rdfs_Literal), true)=true))). % 34.09/21.07 tff(c_2850, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_107), true, iext(Q_107, uri_rdf_value, uri_rdfs_Resource), true)=true))). % 34.09/21.07 tff(c_2888, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_107), true, iext(Q_107, uri_rdf_first, uri_rdf_List), true)=true))). % 34.09/21.07 tff(c_2848, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_107), true, iext(Q_107, uri_rdf__2, uri_rdf_Property), true)=true))). % 34.09/21.07 tff(c_2838, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_107), true, iext(Q_107, uri_rdfs_isDefinedBy, uri_rdfs_Resource), true)=true))). % 34.09/21.07 tff(c_2883, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_107), true, iext(Q_107, uri_rdfs_label, uri_rdfs_Literal), true)=true))). % 34.09/21.07 tff(c_2887, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_107), true, iext(Q_107, uri_rdfs_comment, uri_rdfs_Resource), true)=true))). % 34.09/21.07 tff(c_25155, plain, (![D_524]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_524), true, icext(D_524, uri_rdf_object), true)=true))). % 34.09/21.07 tff(c_2368, plain, (![E_101]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Container, E_101), true, iext(uri_rdfs_subClassOf, uri_rdf_Bag, E_101), true)=true))). % 34.09/21.07 tff(c_2840, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_owl_equivalentClass, Q_107), true, iext(Q_107, uri_ex_InversesOfFunctionalProperties, sK1_testcase_premise_fullish_028_Inferred_Property_Characteristics_III_BNODE_z), true)=true))). % 34.09/21.07 tff(c_2854, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_107), true, iext(Q_107, sK1_testcase_premise_fullish_028_Inferred_Property_Characteristics_III_BNODE_z, uri_owl_Restriction), true)=true))). % 34.09/21.07 tff(c_2894, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_107), true, iext(Q_107, uri_rdfs_range, uri_rdfs_Class), true)=true))). % 34.09/21.07 tff(c_2893, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_107), true, iext(Q_107, uri_rdf_nil, uri_rdf_List), true)=true))). % 34.09/21.07 tff(c_2847, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_107), true, iext(Q_107, uri_rdf__1, uri_rdfs_ContainerMembershipProperty), true)=true))). % 34.09/21.07 tff(c_2877, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_owl_someValuesFrom, Q_107), true, iext(Q_107, sK1_testcase_premise_fullish_028_Inferred_Property_Characteristics_III_BNODE_z, uri_owl_FunctionalProperty), true)=true))). % 34.09/21.07 tff(c_24954, plain, (![D_515]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_515), true, icext(D_515, uri_rdf__3), true)=true))). % 34.09/21.07 tff(c_2870, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_107), true, iext(Q_107, uri_rdf__3, uri_rdf_Property), true)=true))). % 34.09/21.07 tff(c_2890, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_107), true, iext(Q_107, uri_rdf_rest, uri_rdf_List), true)=true))). % 34.09/21.07 tff(c_2881, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_107), true, iext(Q_107, uri_rdfs_ContainerMembershipProperty, uri_rdf_Property), true)=true))). % 34.09/21.07 tff(c_2366, plain, (![E_101]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Container, E_101), true, iext(uri_rdfs_subClassOf, uri_rdfs_Seq, E_101), true)=true))). % 34.09/21.07 tff(c_2860, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_107), true, iext(Q_107, uri_rdfs_isDefinedBy, uri_rdfs_seeAlso), true)=true))). % 34.09/21.07 tff(c_2875, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_107), true, iext(Q_107, uri_rdf_object, uri_rdfs_Statement), true)=true))). % 34.09/21.07 tff(c_2865, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_107), true, iext(Q_107, uri_rdf__1, uri_rdf_Property), true)=true))). % 34.09/21.07 tff(c_24759, plain, (![D_506]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_506), true, icext(D_506, uri_rdf__2), true)=true))). % 34.09/21.07 tff(c_2868, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_107), true, iext(Q_107, uri_rdf__1, uri_rdfs_Resource), true)=true))). % 34.09/21.07 tff(c_2859, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_107), true, iext(Q_107, uri_rdfs_label, uri_rdfs_Resource), true)=true))). % 34.09/21.07 tff(c_2869, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_107), true, iext(Q_107, uri_rdf_predicate, uri_rdfs_Resource), true)=true))). % 34.09/21.07 tff(c_2864, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_107), true, iext(Q_107, uri_rdf_rest, uri_rdf_List), true)=true))). % 34.09/21.07 tff(c_2856, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_107), true, iext(Q_107, uri_rdf__2, uri_rdfs_Resource), true)=true))). % 34.09/21.07 tff(c_2878, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_107), true, iext(Q_107, uri_rdf_value, uri_rdfs_Resource), true)=true))). % 34.09/21.07 tff(c_2849, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_107), true, iext(Q_107, uri_rdf_type, uri_rdfs_Resource), true)=true))). % 34.09/21.08 tff(c_24542, plain, (![D_497]: (ifeq(iext(uri_rdfs_subClassOf, uri_owl_Restriction, D_497), true, icext(D_497, sK1_testcase_premise_fullish_028_Inferred_Property_Characteristics_III_BNODE_z), true)=true))). % 34.09/21.08 tff(c_2427, plain, (![R_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_seeAlso, R_104), true, iext(uri_rdfs_subPropertyOf, uri_rdfs_isDefinedBy, R_104), true)=true))). % 34.09/21.08 tff(c_2873, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_107), true, iext(Q_107, uri_rdf__3, uri_rdfs_Resource), true)=true))). % 34.09/21.08 tff(c_2851, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_107), true, iext(Q_107, uri_rdfs_seeAlso, uri_rdfs_Resource), true)=true))). % 34.09/21.08 tff(c_2858, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_107), true, iext(Q_107, uri_rdf_XMLLiteral, uri_rdfs_Datatype), true)=true))). % 34.09/21.08 tff(c_2884, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_107), true, iext(Q_107, uri_rdfs_range, uri_rdf_Property), true)=true))). % 34.09/21.08 tff(c_2855, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_107), true, iext(Q_107, uri_rdf__3, uri_rdfs_Resource), true)=true))). % 34.09/21.08 tff(c_2891, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_107), true, iext(Q_107, uri_rdf_first, uri_rdfs_Resource), true)=true))). % 34.09/21.08 tff(c_24331, plain, (![D_488]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_488), true, icext(D_488, uri_rdf_Property), true)=true))). % 34.09/21.08 tff(c_15625, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_predicate), true)=true))). % 34.09/21.08 tff(c_15626, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_predicate), true)=true))). % 34.09/21.08 tff(c_14233, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_label), true)=true))). % 34.09/21.08 tff(c_2889, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_107), true, iext(Q_107, uri_rdf_value, uri_rdf_Property), true)=true))). % 34.09/21.08 tff(c_14232, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_label), true)=true))). % 34.09/21.08 tff(c_15118, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_comment), true)=true))). % 34.09/21.08 tff(c_15119, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_comment), true)=true))). % 34.09/21.08 tff(c_13373, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_member), true)=true))). % 34.09/21.08 tff(c_13975, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdf_List), true)=true))). % 34.09/21.08 tff(c_2886, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_107), true, iext(Q_107, uri_rdf_predicate, uri_rdfs_Statement), true)=true))). % 34.09/21.08 tff(c_13133, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdfs_Resource), true)=true))). % 34.09/21.08 tff(c_16550, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_owl_Restriction), true)=true))). % 34.09/21.08 tff(c_16549, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_owl_Restriction), true)=true))). % 34.09/21.08 tff(c_13064, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdfs_Statement), true)=true))). % 34.09/21.08 tff(c_2885, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_107), true, iext(Q_107, uri_rdfs_member, uri_rdfs_Resource), true)=true))). % 34.09/21.08 tff(c_13063, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdfs_Statement), true)=true))). % 34.09/21.08 tff(c_14067, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdf_List), true)=true))). % 34.09/21.08 tff(c_2857, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_107), true, iext(Q_107, uri_rdf_subject, uri_rdf_Property), true)=true))). % 34.09/21.08 tff(c_2872, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_107), true, iext(Q_107, uri_rdfs_domain, uri_rdfs_Class), true)=true))). % 34.09/21.08 tff(c_23803, plain, (![D_467]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_List, D_467), true, icext(D_467, uri_rdf_nil), true)=true))). % 34.09/21.08 tff(c_2367, plain, (![E_101]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Container, E_101), true, iext(uri_rdfs_subClassOf, uri_rdf_Alt, E_101), true)=true))). % 34.09/21.08 tff(c_23688, plain, (![D_464]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, D_464), true, icext(D_464, uri_rdf__3), true)=true))). % 34.09/21.08 tff(c_2866, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_107), true, iext(Q_107, uri_rdfs_isDefinedBy, uri_rdfs_Resource), true)=true))). % 34.09/21.08 tff(c_23485, plain, (![C_89, X_61]: (ifeq(icext(C_89, X_61), true, true, true)=true))). % 34.09/21.08 tff(c_5778, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_isDefinedBy), true)=true))). % 34.09/21.08 tff(c_8222, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_owl_equivalentClass), true)=true))). % 34.09/21.08 tff(c_2846, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_107), true, iext(Q_107, uri_rdfs_Seq, uri_rdfs_Container), true)=true))). % 34.09/21.08 tff(c_5509, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_domain), true)=true))). % 34.09/21.08 tff(c_22984, plain, (![D_453, X_454]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Resource, D_453), true, icext(D_453, X_454), true)=true))). % 34.09/21.08 tff(c_8540, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_subject), true)=true))). % 34.09/21.08 tff(c_8221, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_owl_equivalentClass), true)=true))). % 34.09/21.08 tff(c_2844, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_107), true, iext(Q_107, uri_rdf_XMLLiteral, uri_rdfs_Literal), true)=true))). % 34.09/21.08 tff(c_22863, plain, (![X_446, Y_447]: (ifeq(iext(uri_rdf_rest, X_446, Y_447), true, icext(uri_rdf_List, X_446), true)=true))). % 34.09/21.08 tff(c_10654, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_subClassOf), true)=true))). % 34.09/21.08 tff(c_5686, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_value), true)=true))). % 34.09/21.08 tff(c_2861, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_107), true, iext(Q_107, uri_rdf_type, uri_rdf_Property), true)=true))). % 34.09/21.08 tff(c_5687, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_value), true)=true))). % 34.09/21.08 tff(c_22352, plain, (![X_438, Y_439]: (ifeq(iext(uri_rdfs_domain, X_438, Y_439), true, icext(uri_rdf_Property, X_438), true)=true))). % 34.09/21.08 tff(c_6005, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdf_XMLLiteral), true)=true))). % 34.09/21.08 tff(c_2880, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_107), true, iext(Q_107, uri_rdf_Bag, uri_rdfs_Container), true)=true))). % 34.09/21.08 tff(c_6666, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_object), true)=true))). % 34.09/21.08 tff(c_21943, plain, (![X_431, Y_432]: (ifeq(iext(uri_rdfs_range, X_431, Y_432), true, icext(uri_rdfs_Class, Y_432), true)=true))). % 34.09/21.08 tff(c_5141, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf__3), true)=true))). % 34.09/21.08 tff(c_5625, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_first), true)=true))). % 34.09/21.08 tff(c_2364, plain, (![E_101]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, E_101), true, iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, E_101), true)=true))). % 34.09/21.08 tff(c_9234, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdfs_Datatype), true)=true))). % 34.09/21.08 tff(c_21173, plain, (![X_422, Y_423]: (ifeq(iext(uri_rdfs_subClassOf, X_422, Y_423), true, icext(uri_rdfs_Class, X_422), true)=true))). % 34.09/21.08 tff(c_6756, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_rest), true)=true))). % 34.09/21.08 tff(c_4946, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_subPropertyOf), true)=true))). % 34.09/21.08 tff(c_10655, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_subClassOf), true)=true))). % 34.09/21.08 tff(c_2879, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_107), true, iext(Q_107, uri_rdfs_member, uri_rdfs_Resource), true)=true))). % 34.09/21.08 tff(c_9460, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_owl_onProperty), true)=true))). % 34.09/21.08 tff(c_20607, plain, (![X_413, Y_414]: (ifeq(iext(uri_rdfs_subPropertyOf, X_413, Y_414), true, icext(uri_rdf_Property, Y_414), true)=true))). % 34.09/21.08 tff(c_7008, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_range), true)=true))). % 34.09/21.08 tff(c_6395, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_owl_someValuesFrom), true)=true))). % 34.09/21.08 tff(c_2867, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_107), true, iext(Q_107, uri_rdfs_subClassOf, uri_rdfs_Class), true)=true))). % 34.09/21.08 tff(c_8539, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_subject), true)=true))). % 34.09/21.08 tff(c_20470, plain, (![X_405, Y_406]: (ifeq(iext(uri_rdf_first, X_405, Y_406), true, icext(uri_rdf_List, X_405), true)=true))). % 34.09/21.08 tff(c_5626, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_first), true)=true))). % 34.09/21.08 tff(c_2365, plain, (![E_101]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Literal, E_101), true, iext(uri_rdfs_subClassOf, uri_rdf_XMLLiteral, E_101), true)=true))). % 34.09/21.08 tff(c_5935, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf__3), true)=true))). % 34.09/21.08 tff(c_9525, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_seeAlso), true)=true))). % 34.09/21.08 tff(c_10494, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdfs_Seq), true)=true))). % 34.09/21.08 tff(c_20305, plain, (![X_396, Y_397]: (ifeq(iext(uri_rdf_predicate, X_396, Y_397), true, icext(uri_rdfs_Statement, X_396), true)=true))). % 34.09/21.08 tff(c_5433, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_type), true)=true))). % 34.09/21.08 tff(c_2841, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_107), true, iext(Q_107, uri_rdf__2, uri_rdfs_ContainerMembershipProperty), true)=true))). % 34.09/21.08 tff(c_20228, plain, (![X_390, Y_391]: (ifeq(iext(uri_rdfs_label, X_390, Y_391), true, icext(uri_rdfs_Literal, Y_391), true)=true))). % 34.09/21.08 tff(c_10429, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_member), true)=true))). % 34.09/21.08 tff(c_2895, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_107), true, iext(Q_107, uri_rdf_Property, uri_rdfs_Class), true)=true))). % 34.09/21.08 tff(c_10808, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdf_Bag), true)=true))). % 34.09/21.08 tff(c_19630, plain, (![X_382, Y_383]: (ifeq(iext(uri_rdfs_subClassOf, X_382, Y_383), true, icext(uri_rdfs_Class, Y_383), true)=true))). % 34.09/21.08 tff(c_6130, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf__2), true)=true))). % 34.09/21.08 tff(c_2853, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_107), true, iext(Q_107, uri_rdf_object, uri_rdf_Property), true)=true))). % 34.09/21.08 tff(c_9459, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_owl_onProperty), true)=true))). % 34.09/21.08 tff(c_9143, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdfs_ContainerMembershipProperty), true)=true))). % 34.09/21.08 tff(c_19033, plain, (![X_374, Y_375]: (ifeq(iext(uri_rdf_type, X_374, Y_375), true, icext(uri_rdfs_Class, Y_375), true)=true))). % 34.09/21.08 tff(c_6755, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_rest), true)=true))). % 34.09/21.08 tff(c_2837, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_107), true, iext(Q_107, uri_rdfs_domain, uri_rdf_Property), true)=true))). % 34.09/21.08 tff(c_10273, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdfs_Container), true)=true))). % 34.09/21.08 tff(c_10586, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdf_Alt), true)=true))). % 34.09/21.08 tff(c_18510, plain, (![X_366, Y_367]: (ifeq(iext(uri_rdfs_subPropertyOf, X_366, Y_367), true, icext(uri_rdf_Property, X_366), true)=true))). % 34.09/21.08 tff(c_5510, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_domain), true)=true))). % 34.09/21.08 tff(c_6396, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_owl_someValuesFrom), true)=true))). % 34.09/21.08 tff(c_2898, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_owl_onProperty, Q_107), true, iext(Q_107, sK1_testcase_premise_fullish_028_Inferred_Property_Characteristics_III_BNODE_z, uri_owl_inverseOf), true)=true))). % 34.09/21.08 tff(c_10176, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdfs_Literal), true)=true))). % 34.09/21.08 tff(c_7009, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_range), true)=true))). % 34.09/21.08 tff(c_12021, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdf_Property), true)=true))). % 34.09/21.08 tff(c_18337, plain, (![X_356, Y_357]: (ifeq(iext(uri_rdf_object, X_356, Y_357), true, icext(uri_rdfs_Statement, X_356), true)=true))). % 34.09/21.08 tff(c_5434, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_type), true)=true))). % 34.09/21.08 tff(c_6667, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_object), true)=true))). % 34.09/21.08 tff(c_2839, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_107), true, iext(Q_107, uri_rdf_rest, uri_rdf_Property), true)=true))). % 34.09/21.08 tff(c_11955, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf__1), true)=true))). % 34.09/21.08 tff(c_11956, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf__1), true)=true))). % 34.09/21.08 tff(c_18180, plain, (![X_347, Y_348]: (ifeq(iext(uri_rdf_subject, X_347, Y_348), true, icext(uri_rdfs_Statement, X_347), true)=true))). % 34.09/21.08 tff(c_6129, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf__2), true)=true))). % 34.09/21.08 tff(c_4947, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_subPropertyOf), true)=true))). % 34.09/21.08 tff(c_2845, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_107), true, iext(Q_107, uri_rdf__3, uri_rdfs_ContainerMembershipProperty), true)=true))). % 34.09/21.08 tff(c_5060, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdfs_Class), true)=true))). % 34.09/21.08 tff(c_17763, plain, (![X_339, Y_340]: (ifeq(iext(uri_rdfs_domain, X_339, Y_340), true, icext(uri_rdfs_Class, Y_340), true)=true))). % 34.09/21.08 tff(c_11308, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdfs_Resource), true)=true))). % 34.09/21.08 tff(c_4700, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_29), true, icext(C_29, uri_rdfs_Resource), true)=true))). % 34.09/21.08 tff(c_4701, plain, (![C_19, X_138]: (ifeq(iext(uri_rdfs_domain, uri_rdf_type, C_19), true, icext(C_19, X_138), true)=true))). % 34.09/21.08 tff(c_2897, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_107), true, iext(Q_107, uri_rdf_type, uri_rdfs_Class), true)=true))). % 34.09/21.08 tff(c_1867, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_93), true, icext(C_93, uri_rdf_subject), true)=true))). % 34.09/21.08 tff(c_1858, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_93), true, icext(C_93, uri_rdf__3), true)=true))). % 34.09/21.08 tff(c_1908, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_93), true, icext(C_93, uri_rdf_type), true)=true))). % 34.09/21.08 tff(c_2205, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_97), true, icext(C_97, uri_rdfs_Literal), true)=true))). % 34.09/21.08 tff(c_1859, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_93), true, icext(C_93, uri_rdf__2), true)=true))). % 34.09/21.08 tff(c_16912, plain, (![X_319, Y_320]: (ifeq(iext(uri_rdfs_range, X_319, Y_320), true, icext(uri_rdf_Property, X_319), true)=true))). % 34.09/21.09 tff(c_1874, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_93), true, icext(C_93, uri_rdf__1), true)=true))). % 34.09/21.09 tff(c_1855, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_93), true, icext(C_93, uri_rdf_subject), true)=true))). % 34.09/21.09 tff(c_1843, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_93), true, icext(C_93, uri_rdfs_subPropertyOf), true)=true))). % 34.09/21.09 tff(c_2200, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_owl_equivalentClass, C_97), true, icext(C_97, sK1_testcase_premise_fullish_028_Inferred_Property_Characteristics_III_BNODE_z), true)=true))). % 34.09/21.09 tff(c_1893, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_93), true, icext(C_93, uri_rdfs_label), true)=true))). % 34.09/21.09 tff(c_1895, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_93), true, icext(C_93, uri_rdfs_member), true)=true))). % 34.09/21.09 tff(c_16551, plain, (![X_33]: (ifeq(icext(uri_owl_Restriction, X_33), true, icext(uri_owl_Restriction, X_33), true)=true))). % 34.09/21.09 tff(c_1901, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_93), true, icext(C_93, uri_rdf_rest), true)=true))). % 34.09/21.09 tff(c_16561, plain, (iext(uri_rdfs_subClassOf, uri_owl_Restriction, uri_rdfs_Resource)=true)). % 34.09/21.09 tff(c_16495, plain, (iext(uri_rdfs_subClassOf, uri_owl_Restriction, uri_owl_Restriction)=true)). % 34.09/21.09 tff(c_16423, plain, (iext(uri_rdf_type, uri_owl_Restriction, uri_rdfs_Class)=true)). % 34.09/21.09 tff(c_1852, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_93), true, icext(C_93, uri_rdf_value), true)=true))). % 34.09/21.09 tff(c_16272, plain, (ic(uri_owl_Restriction)=true)). % 34.09/21.09 tff(c_16206, plain, (icext(uri_rdfs_Class, uri_owl_Restriction)=true)). % 34.09/21.09 tff(c_2217, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_97), true, icext(C_97, uri_owl_Restriction), true)=true))). % 34.09/21.09 tff(c_1839, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_93), true, icext(C_93, uri_rdfs_isDefinedBy), true)=true))). % 34.09/21.09 tff(c_1880, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_93), true, icext(C_93, uri_rdf__3), true)=true))). % 34.09/21.09 tff(c_2264, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_97), true, icext(C_97, uri_rdfs_Class), true)=true))). % 34.09/21.09 tff(c_1864, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_93), true, icext(C_93, uri_rdfs_isDefinedBy), true)=true))). % 34.09/21.09 tff(c_1890, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_93), true, icext(C_93, uri_rdfs_ContainerMembershipProperty), true)=true))). % 34.09/21.09 tff(c_15853, plain, (![X_296, Y_297]: (ifeq(iext(uri_rdf_rest, X_296, Y_297), true, icext(uri_rdf_List, Y_297), true)=true))). % 34.09/21.09 tff(c_1886, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_93), true, icext(C_93, uri_rdf_value), true)=true))). % 34.09/21.09 tff(c_1838, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_93), true, icext(C_93, uri_rdfs_domain), true)=true))). % 34.09/21.09 tff(c_2202, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdfs_range, C_97), true, icext(C_97, uri_rdf_Property), true)=true))). % 34.09/21.09 tff(c_2223, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_97), true, icext(C_97, uri_rdfs_Datatype), true)=true))). % 34.09/21.09 tff(c_2232, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdfs_domain, C_97), true, icext(C_97, uri_rdfs_Class), true)=true))). % 34.09/21.09 tff(c_1875, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_93), true, icext(C_93, uri_rdf_predicate), true)=true))). % 34.09/21.09 tff(c_1868, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_93), true, icext(C_93, uri_rdf_rest), true)=true))). % 34.09/21.09 tff(c_1872, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_93), true, icext(C_93, uri_rdfs_subClassOf), true)=true))). % 34.09/21.09 tff(c_1854, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_93), true, icext(C_93, uri_rdfs_seeAlso), true)=true))). % 34.09/21.09 tff(c_2256, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdfs_domain, C_97), true, icext(C_97, uri_rdf_List), true)=true))). % 34.09/21.09 tff(c_15571, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_predicate, uri_rdf_predicate)=true)). % 34.09/21.09 tff(c_15529, plain, (ip(uri_rdf_predicate)=true)). % 34.09/21.09 tff(c_2243, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdfs_range, C_97), true, icext(C_97, uri_rdfs_Literal), true)=true))). % 34.09/21.09 tff(c_15447, plain, (iext(uri_rdf_type, uri_rdf_predicate, uri_rdf_Property)=true)). % 34.09/21.09 tff(c_15281, plain, (icext(uri_rdf_Property, uri_rdf_predicate)=true)). % 34.09/21.09 tff(c_1896, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_93), true, icext(C_93, uri_rdf_predicate), true)=true))). % 34.09/21.09 tff(c_1845, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_93), true, icext(C_93, uri_rdf_XMLLiteral), true)=true))). % 34.09/21.09 tff(c_2248, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_97), true, icext(C_97, uri_rdf_Property), true)=true))). % 34.09/21.09 tff(c_1883, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_93), true, icext(C_93, uri_rdfs_comment), true)=true))). % 34.09/21.09 tff(c_2262, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_97), true, icext(C_97, uri_rdf_List), true)=true))). % 34.09/21.09 tff(c_1878, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_93), true, icext(C_93, uri_rdfs_domain), true)=true))). % 34.09/21.09 tff(c_15064, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_comment, uri_rdfs_comment)=true)). % 34.09/21.09 tff(c_1905, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_93), true, icext(C_93, uri_rdfs_range), true)=true))). % 34.09/21.09 tff(c_14994, plain, (ip(uri_rdfs_comment)=true)). % 34.09/21.09 tff(c_14941, plain, (iext(uri_rdf_type, uri_rdfs_comment, uri_rdf_Property)=true)). % 34.09/21.09 tff(c_14750, plain, (icext(uri_rdf_Property, uri_rdfs_comment)=true)). % 34.09/21.09 tff(c_2195, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_97), true, icext(C_97, uri_rdfs_Class), true)=true))). % 34.09/21.09 tff(c_1898, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_93), true, icext(C_93, uri_rdfs_comment), true)=true))). % 34.09/21.09 tff(c_1841, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_owl_equivalentClass, C_93), true, icext(C_93, uri_ex_InversesOfFunctionalProperties), true)=true))). % 34.09/21.09 tff(c_13065, plain, (![X_33]: (ifeq(icext(uri_rdfs_Statement, X_33), true, icext(uri_rdfs_Statement, X_33), true)=true))). % 34.09/21.09 tff(c_14280, plain, (![X_260, Y_261]: (ifeq(iext(uri_rdfs_comment, X_260, Y_261), true, icext(uri_rdfs_Literal, Y_261), true)=true))). % 34.09/21.09 tff(c_13977, plain, (![X_33]: (ifeq(icext(uri_rdf_List, X_33), true, icext(uri_rdf_List, X_33), true)=true))). % 34.09/21.09 tff(c_9145, plain, (![X_33]: (ifeq(icext(uri_rdfs_ContainerMembershipProperty, X_33), true, icext(uri_rdfs_ContainerMembershipProperty, X_33), true)=true))). % 34.09/21.09 tff(c_11587, plain, (![X_33]: (ifeq(icext(uri_rdf_Property, X_33), true, icext(uri_rdf_Property, X_33), true)=true))). % 34.09/21.09 tff(c_2196, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdfs_domain, C_97), true, icext(C_97, uri_rdf_Property), true)=true))). % 34.09/21.09 tff(c_10177, plain, (![X_33]: (ifeq(icext(uri_rdfs_Literal, X_33), true, icext(uri_rdfs_Literal, X_33), true)=true))). % 34.09/21.09 tff(c_7866, plain, (![X_33]: (ifeq(icext(uri_rdfs_Container, X_33), true, icext(uri_rdfs_Container, X_33), true)=true))). % 34.09/21.09 tff(c_5061, plain, (![X_33]: (ifeq(icext(uri_rdfs_Class, X_33), true, icext(uri_rdfs_Class, X_33), true)=true))). % 34.09/21.09 tff(c_6007, plain, (![X_33]: (ifeq(icext(uri_rdf_XMLLiteral, X_33), true, icext(uri_rdf_XMLLiteral, X_33), true)=true))). % 34.09/21.09 tff(c_10588, plain, (![X_33]: (ifeq(icext(uri_rdf_Alt, X_33), true, icext(uri_rdf_Alt, X_33), true)=true))). % 34.09/21.09 tff(c_10810, plain, (![X_33]: (ifeq(icext(uri_rdf_Bag, X_33), true, icext(uri_rdf_Bag, X_33), true)=true))). % 34.09/21.09 tff(c_9236, plain, (![X_33]: (ifeq(icext(uri_rdfs_Datatype, X_33), true, icext(uri_rdfs_Datatype, X_33), true)=true))). % 34.09/21.09 tff(c_10496, plain, (![X_33]: (ifeq(icext(uri_rdfs_Seq, X_33), true, icext(uri_rdfs_Seq, X_33), true)=true))). % 34.09/21.09 tff(c_14178, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_label, uri_rdfs_label)=true)). % 34.09/21.09 tff(c_14012, plain, (iext(uri_rdfs_subClassOf, uri_rdf_List, uri_rdfs_Resource)=true)). % 34.09/21.09 tff(c_1882, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_93), true, icext(C_93, uri_rdf_object), true)=true))). % 34.09/21.09 tff(c_13921, plain, (iext(uri_rdfs_subClassOf, uri_rdf_List, uri_rdf_List)=true)). % 34.09/21.09 tff(c_13874, plain, (iext(uri_rdf_type, uri_rdf_List, uri_rdfs_Class)=true)). % 34.09/21.09 tff(c_13706, plain, (ic(uri_rdf_List)=true)). % 34.09/21.09 tff(c_1894, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_93), true, icext(C_93, uri_rdfs_range), true)=true))). % 34.09/21.09 tff(c_13648, plain, (icext(uri_rdfs_Class, uri_rdf_List)=true)). % 34.09/21.09 tff(c_13607, plain, (ip(uri_rdfs_label)=true)). % 34.09/21.09 tff(c_2258, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdfs_range, C_97), true, icext(C_97, uri_rdf_List), true)=true))). % 34.09/21.09 tff(c_13534, plain, (iext(uri_rdf_type, uri_rdfs_label, uri_rdf_Property)=true)). % 34.09/21.09 tff(c_13384, plain, (icext(uri_rdf_Property, uri_rdfs_label)=true)). % 34.09/21.09 tff(c_13295, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_member, uri_rdfs_member)=true)). % 34.09/21.09 tff(c_1863, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_93), true, icext(C_93, uri_rdfs_label), true)=true))). % 34.09/21.09 tff(c_13147, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Statement, uri_rdfs_Resource)=true)). % 34.09/21.09 tff(c_13075, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Resource, uri_rdfs_Resource)=true)). % 34.09/21.09 tff(c_13009, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Statement, uri_rdfs_Statement)=true)). % 34.09/21.09 tff(c_1889, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_93), true, icext(C_93, uri_rdf_Bag), true)=true))). % 34.09/21.09 tff(c_12935, plain, (iext(uri_rdf_type, uri_rdfs_ContainerMembershipProperty, uri_rdfs_Class)=true)). % 34.09/21.09 tff(c_12888, plain, (iext(uri_rdf_type, uri_rdf_Bag, uri_rdfs_Class)=true)). % 34.09/21.09 tff(c_12840, plain, (iext(uri_rdf_type, uri_rdfs_Container, uri_rdfs_Class)=true)). % 34.09/21.09 tff(c_1851, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_93), true, icext(C_93, uri_rdf_type), true)=true))). % 34.09/21.09 tff(c_12768, plain, (iext(uri_rdf_type, uri_rdfs_Datatype, uri_rdfs_Class)=true)). % 34.09/21.09 tff(c_1866, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_93), true, icext(C_93, uri_rdfs_subClassOf), true)=true))). % 34.09/21.09 tff(c_12682, plain, (iext(uri_rdf_type, uri_rdfs_member, uri_rdf_Property)=true)). % 34.09/21.09 tff(c_12540, plain, (icext(uri_rdf_Property, uri_rdfs_member)=true)). % 34.09/21.09 tff(c_12473, plain, (iext(uri_rdf_type, uri_rdfs_Class, uri_rdfs_Class)=true)). % 34.09/21.09 tff(c_1888, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_93), true, icext(C_93, uri_rdfs_member), true)=true))). % 34.09/21.09 tff(c_12426, plain, (iext(uri_rdf_type, uri_rdf_Alt, uri_rdfs_Class)=true)). % 34.09/21.09 tff(c_12379, plain, (iext(uri_rdf_type, uri_rdfs_Literal, uri_rdfs_Class)=true)). % 34.09/21.09 tff(c_12326, plain, (iext(uri_rdf_type, uri_rdf_XMLLiteral, uri_rdfs_Class)=true)). % 34.09/21.09 tff(c_12279, plain, (iext(uri_rdf_type, uri_rdfs_Seq, uri_rdfs_Class)=true)). % 34.09/21.09 tff(c_12231, plain, (iext(uri_rdf_type, uri_rdfs_Resource, uri_rdfs_Class)=true)). % 34.09/21.09 tff(c_12183, plain, (iext(uri_rdf_type, uri_rdfs_Statement, uri_rdfs_Class)=true)). % 34.09/21.09 tff(c_11966, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Property, uri_rdfs_Resource)=true)). % 34.09/21.09 tff(c_11901, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf__1, uri_rdf__1)=true)). % 34.09/21.09 tff(c_1907, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_93), true, icext(C_93, uri_rdfs_subPropertyOf), true)=true))). % 34.09/21.09 tff(c_11735, plain, (icext(uri_rdf_Property, uri_owl_someValuesFrom)=true)). % 34.09/21.09 tff(c_11678, plain, (iext(uri_rdf_type, uri_owl_someValuesFrom, uri_rdf_Property)=true)). % 34.09/21.09 tff(c_11597, plain, (iext(uri_rdf_type, uri_rdfs_seeAlso, uri_rdf_Property)=true)). % 34.09/21.09 tff(c_1844, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_93), true, icext(C_93, uri_rdfs_seeAlso), true)=true))). % 34.09/21.09 tff(c_11531, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Property, uri_rdf_Property)=true)). % 34.09/21.09 tff(c_11388, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, uri_rdfs_Resource)=true)). % 34.09/21.09 tff(c_11254, plain, (iext(uri_rdfs_subClassOf, uri_rdf_XMLLiteral, uri_rdfs_Resource)=true)). % 34.09/21.09 tff(c_1899, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_93), true, icext(C_93, uri_rdf_first), true)=true))). % 34.09/21.09 tff(c_11115, plain, (icext(uri_rdf_Property, uri_rdfs_subPropertyOf)=true)). % 34.09/21.09 tff(c_11058, plain, (iext(uri_rdf_type, uri_rdfs_subPropertyOf, uri_rdf_Property)=true)). % 34.09/21.09 tff(c_2201, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_97), true, icext(C_97, uri_rdfs_ContainerMembershipProperty), true)=true))). % 34.09/21.09 tff(c_10911, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Bag, uri_rdfs_Resource)=true)). % 34.09/21.09 tff(c_10754, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Bag, uri_rdf_Bag)=true)). % 34.09/21.09 tff(c_10688, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Class, uri_rdfs_Resource)=true)). % 34.09/21.09 tff(c_1909, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_owl_onProperty, C_93), true, icext(C_93, sK1_testcase_premise_fullish_028_Inferred_Property_Characteristics_III_BNODE_z), true)=true))). % 34.09/21.09 tff(c_10600, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, uri_rdfs_subClassOf)=true)). % 34.09/21.09 tff(c_10507, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Alt, uri_rdf_Alt)=true)). % 34.09/21.09 tff(c_2230, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_97), true, icext(C_97, uri_rdf_Property), true)=true))). % 34.09/21.09 tff(c_10440, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Seq, uri_rdfs_Seq)=true)). % 34.09/21.09 tff(c_10375, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf__1, uri_rdfs_member)=true)). % 34.09/21.09 tff(c_3353, plain, (![S_5, O_6]: (ifeq(iext(uri_rdf_rest, S_5, O_6), true, true, true)=true))). % 34.09/21.09 tff(c_10218, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Container, uri_rdfs_Resource)=true)). % 34.09/21.09 tff(c_2221, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdfs_range, C_97), true, icext(C_97, uri_rdfs_Resource), true)=true))). % 34.09/21.09 tff(c_10118, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Literal, uri_rdfs_Literal)=true)). % 34.09/21.09 tff(c_3207, plain, (![S_5, O_6]: (ifeq(iext(uri_rdfs_subPropertyOf, S_5, O_6), true, true, true)=true))). % 34.09/21.09 tff(c_9715, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Literal, uri_rdfs_Resource)=true)). % 34.09/21.09 tff(c_870, plain, (![S_5, O_6]: (ifeq(iext(uri_rdfs_range, S_5, O_6), true, true, true)=true))). % 34.09/21.09 tff(c_2239, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdfs_range, C_97), true, icext(C_97, uri_rdfs_Class), true)=true))). % 34.09/21.09 tff(c_9470, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_seeAlso, uri_rdfs_seeAlso)=true)). % 34.09/21.09 tff(c_9405, plain, (iext(uri_rdfs_subPropertyOf, uri_owl_onProperty, uri_owl_onProperty)=true)). % 34.09/21.09 tff(c_9155, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, uri_rdfs_Datatype)=true)). % 34.09/21.09 tff(c_9089, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, uri_rdfs_ContainerMembershipProperty)=true)). % 34.09/21.09 tff(c_8861, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Seq, uri_rdfs_Resource)=true)). % 34.09/21.09 tff(c_1881, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_93), true, icext(C_93, uri_rdf_Alt), true)=true))). % 34.09/21.09 tff(c_8656, plain, (icext(uri_rdf_Property, uri_owl_onProperty)=true)). % 34.09/21.09 tff(c_8602, plain, (iext(uri_rdf_type, uri_owl_onProperty, uri_rdf_Property)=true)). % 34.09/21.09 tff(c_8486, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_subject, uri_rdf_subject)=true)). % 34.09/21.09 tff(c_1871, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_93), true, icext(C_93, uri_rdfs_isDefinedBy), true)=true))). % 34.09/21.09 tff(c_3169, plain, (![S_5, O_6]: (ifeq(iext(uri_rdf_object, S_5, O_6), true, true, true)=true))). % 34.09/21.09 tff(c_742, plain, (![S_5, O_6]: (ifeq(iext(uri_rdfs_subClassOf, S_5, O_6), true, true, true)=true))). % 34.09/21.09 tff(c_8250, plain, (icext(uri_rdf_Property, uri_rdfs_seeAlso)=true)). % 34.09/21.09 tff(c_2225, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_97), true, icext(C_97, uri_rdfs_seeAlso), true)=true))). % 34.09/21.09 tff(c_8171, plain, (iext(uri_rdfs_subPropertyOf, uri_owl_equivalentClass, uri_owl_equivalentClass)=true)). % 34.09/21.09 tff(c_8066, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Alt, uri_rdfs_Resource)=true)). % 34.09/21.09 tff(c_7876, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf__2, uri_rdfs_member)=true)). % 34.09/21.09 tff(c_7807, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Container, uri_rdfs_Container)=true)). % 34.09/21.09 tff(c_2244, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_owl_someValuesFrom, C_97), true, icext(C_97, uri_owl_FunctionalProperty), true)=true))). % 34.09/21.09 tff(c_7737, plain, (ic(uri_rdfs_Statement)=true)). % 34.09/21.09 tff(c_7684, plain, (icext(uri_rdfs_Class, uri_rdfs_Statement)=true)). % 34.09/21.09 tff(c_2254, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdfs_domain, C_97), true, icext(C_97, uri_rdfs_Statement), true)=true))). % 34.09/21.09 tff(c_7600, plain, (icext(uri_rdf_Property, uri_rdfs_isDefinedBy)=true)). % 34.09/21.09 tff(c_7547, plain, (iext(uri_rdf_type, uri_rdfs_isDefinedBy, uri_rdf_Property)=true)). % 34.09/21.09 tff(c_3045, plain, (![S_5, O_6]: (ifeq(iext(uri_owl_onProperty, S_5, O_6), true, true, true)=true))). % 34.09/21.09 tff(c_7280, plain, (icext(uri_rdf_Property, uri_rdfs_range)=true)). % 34.09/21.09 tff(c_1884, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_owl_someValuesFrom, C_93), true, icext(C_93, sK1_testcase_premise_fullish_028_Inferred_Property_Characteristics_III_BNODE_z), true)=true))). % 34.09/21.09 tff(c_7203, plain, (iext(uri_rdf_type, uri_rdfs_range, uri_rdf_Property)=true)). % 34.09/21.09 tff(c_2207, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_97), true, icext(C_97, uri_rdfs_Container), true)=true))). % 34.09/21.09 tff(c_6958, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_range, uri_rdfs_range)=true)). % 34.09/21.09 tff(c_1837, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_93), true, icext(C_93, uri_rdfs_Datatype), true)=true))). % 34.09/21.09 tff(c_6766, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, uri_rdfs_Resource)=true)). % 34.09/21.09 tff(c_6705, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_rest, uri_rdf_rest)=true)). % 34.09/21.09 tff(c_6613, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_object, uri_rdf_object)=true)). % 34.09/21.09 tff(c_1847, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_93), true, icext(C_93, uri_rdfs_Seq), true)=true))). % 34.09/21.09 tff(c_6473, plain, (ic(uri_rdfs_Resource)=true)). % 34.09/21.09 tff(c_6424, plain, (icext(uri_rdfs_Class, uri_rdfs_Resource)=true)). % 34.09/21.09 tff(c_2240, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdfs_domain, C_97), true, icext(C_97, uri_rdfs_Resource), true)=true))). % 34.09/21.09 tff(c_6342, plain, (iext(uri_rdfs_subPropertyOf, uri_owl_someValuesFrom, uri_owl_someValuesFrom)=true)). % 34.09/21.09 tff(c_6226, plain, (icext(uri_rdf_Property, uri_rdfs_domain)=true)). % 34.09/21.09 tff(c_6140, plain, (iext(uri_rdf_type, uri_rdfs_domain, uri_rdf_Property)=true)). % 34.09/21.09 tff(c_6079, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf__2, uri_rdf__2)=true)). % 34.09/21.09 tff(c_1892, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_93), true, icext(C_93, uri_rdf__2), true)=true))). % 34.09/21.10 tff(c_5955, plain, (iext(uri_rdfs_subClassOf, uri_rdf_XMLLiteral, uri_rdf_XMLLiteral)=true)). % 34.09/21.10 tff(c_5870, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf__3, uri_rdf__3)=true)). % 34.09/21.10 tff(c_2267, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_owl_onProperty, C_97), true, icext(C_97, uri_owl_inverseOf), true)=true))). % 34.09/21.10 tff(c_809, plain, (![S_5, O_6]: (ifeq(iext(uri_rdfs_domain, S_5, O_6), true, true, true)=true))). % 34.09/21.10 tff(c_3316, plain, (![S_5, O_6]: (ifeq(iext(uri_owl_someValuesFrom, S_5, O_6), true, true, true)=true))). % 34.09/21.10 tff(c_5728, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_isDefinedBy, uri_rdfs_isDefinedBy)=true)). % 34.09/21.10 tff(c_1877, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_93), true, icext(C_93, uri_rdf__1), true)=true))). % 34.09/21.10 tff(c_5636, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_value, uri_rdf_value)=true)). % 34.09/21.10 tff(c_5575, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_first, uri_rdf_first)=true)). % 34.09/21.10 tff(c_1902, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_93), true, icext(C_93, uri_rdf_first), true)=true))). % 34.09/21.10 tff(c_5459, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, uri_rdfs_domain)=true)). % 34.09/21.10 tff(c_5383, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_type, uri_rdf_type)=true)). % 34.09/21.10 tff(c_5329, plain, (icext(uri_rdf_Property, uri_rdfs_subClassOf)=true)). % 34.09/21.10 tff(c_1561, plain, (![X_90]: (ifeq(icext(uri_rdf_XMLLiteral, X_90), true, icext(uri_rdfs_Literal, X_90), true)=true))). % 34.09/21.10 tff(c_5268, plain, (iext(uri_rdf_type, uri_rdfs_subClassOf, uri_rdf_Property)=true)). % 34.09/21.10 tff(c_1562, plain, (![X_90]: (ifeq(icext(uri_rdfs_Seq, X_90), true, icext(uri_rdfs_Container, X_90), true)=true))). % 34.09/21.10 tff(c_5192, plain, (ip(uri_rdfs_member)=true)). % 34.09/21.10 tff(c_1560, plain, (![X_90]: (ifeq(icext(uri_rdfs_Datatype, X_90), true, icext(uri_rdfs_Class, X_90), true)=true))). % 34.09/21.10 tff(c_5090, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf__3, uri_rdfs_member)=true)). % 34.09/21.10 tff(c_5009, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Class, uri_rdfs_Class)=true)). % 34.09/21.10 tff(c_1563, plain, (![X_90]: (ifeq(icext(uri_rdf_Alt, X_90), true, icext(uri_rdfs_Container, X_90), true)=true))). % 34.09/21.10 tff(c_1524, plain, (![S_5, O_6]: (ifeq(iext(uri_owl_equivalentClass, S_5, O_6), true, true, true)=true))). % 34.09/21.10 tff(c_4844, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf)=true)). % 34.09/21.10 tff(c_1565, plain, (![X_90]: (ifeq(icext(uri_rdfs_ContainerMembershipProperty, X_90), true, icext(uri_rdf_Property, X_90), true)=true))). % 34.09/21.10 tff(c_4806, plain, (icext(uri_rdf_Property, uri_owl_equivalentClass)=true)). % 34.09/21.10 tff(c_4753, plain, (iext(uri_rdf_type, uri_owl_equivalentClass, uri_rdf_Property)=true)). % 34.09/21.10 tff(c_1564, plain, (![X_90]: (ifeq(icext(uri_rdf_Bag, X_90), true, icext(uri_rdfs_Container, X_90), true)=true))). % 34.09/21.10 tff(c_2234, plain, (![X_98, Y_99]: (ifeq(iext(uri_rdf_predicate, X_98, Y_99), true, true, true)=true))). % 34.09/21.10 tff(c_4659, plain, (![X_137]: (iext(uri_rdf_type, X_137, uri_rdfs_Resource)=true))). % 34.09/21.10 tff(c_1862, plain, (![X_94, Y_95]: (ifeq(iext(uri_rdfs_label, X_94, Y_95), true, true, true)=true))). % 34.09/21.10 tff(c_1897, plain, (![X_94, Y_95]: (ifeq(iext(uri_rdfs_comment, X_94, Y_95), true, true, true)=true))). % 34.09/21.10 tff(c_2214, plain, (![X_98, Y_99]: (ifeq(iext(uri_rdf_subject, X_98, Y_99), true, true, true)=true))). % 34.09/21.10 tff(c_1850, plain, (![X_94, Y_95]: (ifeq(iext(uri_rdf_type, X_94, Y_95), true, true, true)=true))). % 34.09/21.10 tff(c_1879, plain, (![X_94, Y_95]: (ifeq(iext(uri_rdf__3, X_94, Y_95), true, true, true)=true))). % 34.09/21.10 tff(c_1873, plain, (![X_94, Y_95]: (ifeq(iext(uri_rdf__1, X_94, Y_95), true, true, true)=true))). % 34.09/21.10 tff(c_2252, plain, (![X_98, Y_99]: (ifeq(iext(uri_rdfs_member, X_98, Y_99), true, true, true)=true))). % 34.09/21.10 tff(c_2203, plain, (![X_98, Y_99]: (ifeq(iext(uri_rdfs_seeAlso, X_98, Y_99), true, true, true)=true))). % 34.09/21.10 tff(c_2211, plain, (![X_98, Y_99]: (ifeq(iext(uri_rdf_value, X_98, Y_99), true, true, true)=true))). % 34.09/21.10 tff(c_4475, plain, (icext(uri_rdfs_Class, uri_rdf_XMLLiteral)=true)). % 34.09/21.10 tff(c_1870, plain, (![X_94, Y_95]: (ifeq(iext(uri_rdfs_isDefinedBy, X_94, Y_95), true, true, true)=true))). % 34.09/21.10 tff(c_4423, plain, (icext(uri_rdfs_Class, uri_rdf_Alt)=true)). % 34.09/21.10 tff(c_4378, plain, (icext(uri_rdfs_Class, uri_rdfs_Class)=true)). % 34.09/21.10 tff(c_2259, plain, (![X_98, Y_99]: (ifeq(iext(uri_rdf_first, X_98, Y_99), true, true, true)=true))). % 34.09/21.10 tff(c_4322, plain, (icext(uri_rdfs_Class, uri_rdfs_Container)=true)). % 34.09/21.10 tff(c_4276, plain, (icext(uri_rdfs_Class, uri_rdfs_Seq)=true)). % 34.09/21.10 tff(c_4220, plain, (icext(uri_rdfs_Class, uri_rdfs_Literal)=true)). % 34.09/21.10 tff(c_4173, plain, (icext(uri_rdfs_Class, uri_rdfs_Datatype)=true)). % 34.09/21.10 tff(c_4130, plain, (icext(uri_rdfs_Class, uri_rdf_Bag)=true)). % 34.09/21.10 tff(c_1891, plain, (![X_94, Y_95]: (ifeq(iext(uri_rdf__2, X_94, Y_95), true, true, true)=true))). % 34.09/21.10 tff(c_4071, plain, (icext(uri_rdfs_Class, uri_rdfs_ContainerMembershipProperty)=true)). % 34.09/21.10 tff(c_4023, plain, (icext(uri_rdf_Property, uri_rdf_rest)=true)). % 34.09/21.10 tff(c_3981, plain, (icext(uri_rdfs_ContainerMembershipProperty, uri_rdf__2)=true)). % 34.09/21.10 tff(c_3937, plain, (icext(uri_rdfs_ContainerMembershipProperty, uri_rdf__1)=true)). % 34.09/21.10 tff(c_3897, plain, (icext(uri_rdf_Property, uri_rdf__3)=true)). % 34.09/21.10 tff(c_3849, plain, (icext(uri_rdfs_Class, uri_rdf_Property)=true)). % 34.09/21.10 tff(c_3811, plain, (icext(uri_rdf_Property, uri_rdf__2)=true)). % 34.09/21.10 tff(c_3747, plain, (icext(uri_rdf_Property, uri_rdf_object)=true)). % 34.09/21.10 tff(c_3737, plain, (icext(uri_rdf_Property, uri_rdf_first)=true)). % 34.09/21.10 tff(c_3698, plain, (icext(uri_rdf_Property, uri_rdf_type)=true)). % 34.09/21.10 tff(c_3623, plain, (icext(uri_rdfs_Datatype, uri_rdf_XMLLiteral)=true)). % 34.09/21.10 tff(c_3613, plain, (icext(uri_rdfs_ContainerMembershipProperty, uri_rdf__3)=true)). % 34.09/21.10 tff(c_3574, plain, (icext(uri_owl_Restriction, sK1_testcase_premise_fullish_028_Inferred_Property_Characteristics_III_BNODE_z)=true)). % 34.09/21.10 tff(c_3511, plain, (icext(uri_rdf_Property, uri_rdf_subject)=true)). % 34.09/21.10 tff(c_3497, plain, (icext(uri_rdf_Property, uri_rdf__1)=true)). % 34.09/21.10 tff(c_3460, plain, (icext(uri_rdf_List, uri_rdf_nil)=true)). % 34.09/21.10 tff(c_3411, plain, (icext(uri_rdf_Property, uri_rdf_value)=true)). % 34.09/21.10 tff(c_3367, plain, (ic(uri_rdfs_ContainerMembershipProperty)=true)). % 34.09/21.10 tff(c_3324, plain, (ip(uri_rdf_rest)=true)). % 34.09/21.10 tff(c_3289, plain, (ip(uri_owl_someValuesFrom)=true)). % 34.09/21.10 tff(c_3252, plain, (ic(uri_rdfs_Literal)=true)). % 34.09/21.10 tff(c_3214, plain, (ic(uri_rdfs_Class)=true)). % 34.09/21.10 tff(c_3180, plain, (ip(uri_rdfs_subPropertyOf)=true)). % 34.09/21.10 tff(c_3140, plain, (ip(uri_rdf_object)=true)). % 34.09/21.10 tff(c_3098, plain, (ic(uri_rdf_Property)=true)). % 34.09/21.10 tff(c_3059, plain, (ip(uri_rdf_subject)=true)). % 34.09/21.10 tff(c_3018, plain, (ip(uri_owl_onProperty)=true)). % 34.09/21.10 tff(c_2975, plain, (ip(uri_rdf_value)=true)). % 34.09/21.10 tff(c_2929, plain, (ip(uri_rdfs_seeAlso)=true)). % 34.09/21.10 tff(c_2433, plain, (ip(uri_rdf__1)=true)). % 34.09/21.10 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))). % 34.09/21.10 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))). % 34.09/21.10 tff(c_2374, plain, (ip(uri_rdf__3)=true)). % 34.09/21.10 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))). % 34.09/21.10 tff(c_2272, plain, (ic(uri_rdfs_Container)=true)). % 34.09/21.10 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))). % 34.09/21.10 tff(c_1571, plain, (ic(uri_rdfs_Datatype)=true)). % 34.09/21.10 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))). % 34.09/21.10 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))). % 34.09/21.10 tff(c_1497, plain, (ip(uri_owl_equivalentClass)=true)). % 34.09/21.10 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))). % 34.09/21.10 tff(c_1398, plain, (ip(uri_rdf_first)=true)). % 34.09/21.10 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))). % 34.09/21.10 tff(c_1305, plain, (ip(uri_rdfs_isDefinedBy)=true)). % 34.09/21.10 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))). % 34.09/21.10 tff(c_1259, plain, (ip(uri_rdf__2)=true)). % 34.09/21.10 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))). % 34.09/21.10 tff(c_1209, plain, (ic(uri_rdfs_Seq)=true)). % 34.09/21.10 tff(c_30, plain, (![P_10]: (ifeq(iext(uri_rdf_type, P_10, uri_rdf_Property), true, ip(P_10), true)=true))). % 34.09/21.10 tff(c_1118, plain, (ic(uri_rdf_XMLLiteral)=true)). % 34.09/21.10 tff(c_58, plain, (![C_15]: (ifeq(ic(C_15), true, iext(uri_rdfs_subClassOf, C_15, uri_rdfs_Resource), true)=true))). % 34.09/21.10 tff(c_28, plain, (![P_9]: (ifeq(ip(P_9), true, iext(uri_rdf_type, P_9, uri_rdf_Property), true)=true))). % 34.09/21.10 tff(c_156, plain, (![C_39]: (ifeq(ic(C_39), true, iext(uri_rdfs_subClassOf, C_39, C_39), true)=true))). % 34.09/21.10 tff(c_955, plain, (ic(uri_rdf_Alt)=true)). % 34.09/21.10 tff(c_150, plain, (![C_35, D_36]: (ifeq(iext(uri_rdfs_subClassOf, C_35, D_36), true, ic(D_36), true)=true))). % 34.09/21.10 tff(c_170, plain, (![P_51]: (ifeq(ip(P_51), true, iext(uri_rdfs_subPropertyOf, P_51, P_51), true)=true))). % 34.09/21.10 tff(c_904, plain, (ic(uri_rdf_Bag)=true)). % 34.09/21.10 tff(c_152, plain, (![C_37, D_38]: (ifeq(iext(uri_rdfs_subClassOf, C_37, D_38), true, ic(C_37), true)=true))). % 34.09/21.10 tff(c_852, plain, (ip(uri_rdfs_range)=true)). % 34.09/21.10 tff(c_164, plain, (![P_45, Q_46]: (ifeq(iext(uri_rdfs_subPropertyOf, P_45, Q_46), true, ip(P_45), true)=true))). % 34.09/21.10 tff(c_794, plain, (ip(uri_rdfs_domain)=true)). % 34.09/21.10 tff(c_771, plain, (ip(uri_rdf_type)=true)). % 34.09/21.10 tff(c_162, plain, (![P_43, Q_44]: (ifeq(iext(uri_rdfs_subPropertyOf, P_43, Q_44), true, ip(Q_44), true)=true))). % 34.09/21.10 tff(c_730, plain, (ip(uri_rdfs_subClassOf)=true)). % 34.09/21.10 tff(c_4, plain, (![P_4, S_5, O_6]: (ifeq(iext(P_4, S_5, O_6), true, ip(P_4), true)=true))). % 34.09/21.10 tff(c_114, plain, (![X_22]: (ifeq(ic(X_22), true, icext(uri_rdfs_Class, X_22), true)=true))). % 34.09/21.10 tff(c_124, plain, (![X_27]: (ifeq(lv(X_27), true, icext(uri_rdfs_Literal, X_27), true)=true))). % 34.09/21.10 tff(c_116, plain, (![X_23]: (ifeq(icext(uri_rdfs_Class, X_23), true, ic(X_23), true)=true))). % 34.09/21.10 tff(c_483, plain, (![X_61]: (icext(uri_rdfs_Resource, X_61)=true))). % 34.09/21.10 tff(c_122, plain, (![X_26]: (ifeq(icext(uri_rdfs_Literal, X_26), true, lv(X_26), true)=true))). % 34.09/21.10 tff(c_195, plain, (![X_8]: (ifeq(lv(X_8), true, true, true)=true))). % 34.43/21.10 tff(c_2, plain, (![A_1, B_2, C_3]: (ifeq(A_1, A_1, B_2, C_3)=B_2))). % 34.43/21.10 tff(c_106, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, uri_rdfs_Class)=true)). % 34.43/21.10 tff(c_108, plain, (iext(uri_rdfs_domain, uri_rdfs_domain, uri_rdf_Property)=true)). % 34.43/21.10 tff(c_42, plain, (iext(uri_rdfs_range, uri_rdfs_isDefinedBy, uri_rdfs_Resource)=true)). % 34.43/21.10 tff(c_14, plain, (iext(uri_rdf_type, uri_rdf_rest, uri_rdf_Property)=true)). % 34.43/21.10 tff(c_186, plain, (iext(uri_owl_equivalentClass, uri_ex_InversesOfFunctionalProperties, sK1_testcase_premise_fullish_028_Inferred_Property_Characteristics_III_BNODE_z)=true)). % 34.43/21.10 tff(c_94, plain, (iext(uri_rdf_type, uri_rdf__2, uri_rdfs_ContainerMembershipProperty)=true)). % 34.43/21.10 tff(c_168, plain, (iext(uri_rdfs_range, uri_rdfs_subPropertyOf, uri_rdf_Property)=true)). % 34.43/21.10 tff(c_52, plain, (iext(uri_rdfs_range, uri_rdfs_seeAlso, uri_rdfs_Resource)=true)). % 34.43/21.10 tff(c_100, plain, (iext(uri_rdfs_subClassOf, uri_rdf_XMLLiteral, uri_rdfs_Literal)=true)). % 34.43/21.10 tff(c_96, plain, (iext(uri_rdf_type, uri_rdf__3, uri_rdfs_ContainerMembershipProperty)=true)). % 34.43/21.10 tff(c_98, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Seq, uri_rdfs_Container)=true)). % 34.43/21.10 tff(c_92, plain, (iext(uri_rdf_type, uri_rdf__1, uri_rdfs_ContainerMembershipProperty)=true)). % 34.43/21.10 tff(c_18, plain, (iext(uri_rdf_type, uri_rdf__2, uri_rdf_Property)=true)). % 34.43/21.10 tff(c_174, plain, (iext(uri_rdfs_domain, uri_rdf_type, uri_rdfs_Resource)=true)). % 34.43/21.10 tff(c_180, plain, (iext(uri_rdfs_range, uri_rdf_value, uri_rdfs_Resource)=true)). % 34.43/21.10 tff(c_50, plain, (iext(uri_rdfs_domain, uri_rdfs_seeAlso, uri_rdfs_Resource)=true)). % 34.43/21.10 tff(c_144, plain, (iext(uri_rdfs_range, uri_rdf_subject, uri_rdfs_Resource)=true)). % 34.43/21.10 tff(c_22, plain, (iext(uri_rdf_type, uri_rdf_object, uri_rdf_Property)=true)). % 34.43/21.10 tff(c_188, plain, (iext(uri_rdf_type, sK1_testcase_premise_fullish_028_Inferred_Property_Characteristics_III_BNODE_z, uri_owl_Restriction)=true)). % 34.43/21.10 tff(c_90, plain, (iext(uri_rdfs_range, uri_rdf__3, uri_rdfs_Resource)=true)). % 34.43/21.10 tff(c_88, plain, (iext(uri_rdfs_range, uri_rdf__2, uri_rdfs_Resource)=true)). % 34.43/21.10 tff(c_26, plain, (iext(uri_rdf_type, uri_rdf_subject, uri_rdf_Property)=true)). % 34.43/21.10 tff(c_102, plain, (iext(uri_rdf_type, uri_rdf_XMLLiteral, uri_rdfs_Datatype)=true)). % 34.43/21.10 tff(c_46, plain, (iext(uri_rdfs_domain, uri_rdfs_label, uri_rdfs_Resource)=true)). % 34.43/21.10 tff(c_44, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_isDefinedBy, uri_rdfs_seeAlso)=true)). % 34.43/21.10 tff(c_34, plain, (iext(uri_rdf_type, uri_rdf_type, uri_rdf_Property)=true)). % 34.43/21.10 tff(c_154, plain, (iext(uri_rdfs_range, uri_rdfs_subClassOf, uri_rdfs_Class)=true)). % 34.43/21.10 tff(c_142, plain, (iext(uri_rdfs_domain, uri_rdf_subject, uri_rdfs_Statement)=true)). % 34.43/21.10 tff(c_64, plain, (iext(uri_rdfs_domain, uri_rdf_rest, uri_rdf_List)=true)). % 34.43/21.10 tff(c_16, plain, (iext(uri_rdf_type, uri_rdf__1, uri_rdf_Property)=true)). % 34.43/21.10 tff(c_40, plain, (iext(uri_rdfs_domain, uri_rdfs_isDefinedBy, uri_rdfs_Resource)=true)). % 34.43/21.10 tff(c_146, plain, (iext(uri_rdfs_domain, uri_rdfs_subClassOf, uri_rdfs_Class)=true)). % 34.43/21.10 tff(c_80, plain, (iext(uri_rdfs_domain, uri_rdf__1, uri_rdfs_Resource)=true)). % 34.43/21.10 tff(c_140, plain, (iext(uri_rdfs_range, uri_rdf_predicate, uri_rdfs_Resource)=true)). % 34.43/21.10 tff(c_20, plain, (iext(uri_rdf_type, uri_rdf__3, uri_rdf_Property)=true)). % 34.43/21.10 tff(c_86, plain, (iext(uri_rdfs_range, uri_rdf__1, uri_rdfs_Resource)=true)). % 34.43/21.10 tff(c_112, plain, (iext(uri_rdfs_range, uri_rdfs_domain, uri_rdfs_Class)=true)). % 34.43/21.10 tff(c_84, plain, (iext(uri_rdfs_domain, uri_rdf__3, uri_rdfs_Resource)=true)). % 34.43/21.10 tff(c_68, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Alt, uri_rdfs_Container)=true)). % 34.43/21.10 tff(c_134, plain, (iext(uri_rdfs_domain, uri_rdf_object, uri_rdfs_Statement)=true)). % 34.43/21.10 tff(c_38, plain, (iext(uri_rdfs_range, uri_rdfs_comment, uri_rdfs_Literal)=true)). % 34.43/21.10 tff(c_182, plain, (iext(uri_owl_someValuesFrom, sK1_testcase_premise_fullish_028_Inferred_Property_Characteristics_III_BNODE_z, uri_owl_FunctionalProperty)=true)). % 34.43/21.10 tff(c_178, plain, (iext(uri_rdfs_domain, uri_rdf_value, uri_rdfs_Resource)=true)). % 34.43/21.10 tff(c_76, plain, (iext(uri_rdfs_domain, uri_rdfs_member, uri_rdfs_Resource)=true)). % 34.43/21.10 tff(c_70, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Bag, uri_rdfs_Container)=true)). % 34.43/21.10 tff(c_74, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, uri_rdf_Property)=true)). % 34.43/21.10 tff(c_82, plain, (iext(uri_rdfs_domain, uri_rdf__2, uri_rdfs_Resource)=true)). % 34.43/21.10 tff(c_48, plain, (iext(uri_rdfs_range, uri_rdfs_label, uri_rdfs_Literal)=true)). % 34.43/21.10 tff(c_128, plain, (iext(uri_rdfs_domain, uri_rdfs_range, uri_rdf_Property)=true)). % 34.43/21.10 tff(c_78, plain, (iext(uri_rdfs_range, uri_rdfs_member, uri_rdfs_Resource)=true)). % 34.43/21.10 tff(c_138, plain, (iext(uri_rdfs_domain, uri_rdf_predicate, uri_rdfs_Statement)=true)). % 34.43/21.10 tff(c_36, plain, (iext(uri_rdfs_domain, uri_rdfs_comment, uri_rdfs_Resource)=true)). % 34.43/21.10 tff(c_60, plain, (iext(uri_rdfs_domain, uri_rdf_first, uri_rdf_List)=true)). % 34.43/21.10 tff(c_24, plain, (iext(uri_rdf_type, uri_rdf_value, uri_rdf_Property)=true)). % 34.43/21.10 tff(c_66, plain, (iext(uri_rdfs_range, uri_rdf_rest, uri_rdf_List)=true)). % 34.43/21.10 tff(c_62, plain, (iext(uri_rdfs_range, uri_rdf_first, uri_rdfs_Resource)=true)). % 34.43/21.10 tff(c_10, plain, (iext(uri_rdf_type, uri_rdf_first, uri_rdf_Property)=true)). % 34.43/21.10 tff(c_12, plain, (iext(uri_rdf_type, uri_rdf_nil, uri_rdf_List)=true)). % 34.43/21.10 tff(c_132, plain, (iext(uri_rdfs_range, uri_rdfs_range, uri_rdfs_Class)=true)). % 34.43/21.10 tff(c_126, plain, (iext(uri_rdf_type, uri_rdf_Property, uri_rdfs_Class)=true)). % 34.43/21.10 tff(c_160, plain, (iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, uri_rdf_Property)=true)). % 34.43/21.10 tff(c_176, plain, (iext(uri_rdfs_range, uri_rdf_type, uri_rdfs_Class)=true)). % 34.43/21.10 tff(c_184, plain, (iext(uri_owl_onProperty, sK1_testcase_premise_fullish_028_Inferred_Property_Characteristics_III_BNODE_z, uri_owl_inverseOf)=true)). % 34.43/21.10 tff(c_190, plain, (iext(uri_rdfs_subClassOf, uri_ex_InversesOfFunctionalProperties, uri_owl_InverseFunctionalProperty)!=true)). % 34.43/21.10 tff(c_6, plain, (![X_7]: (ir(X_7)=true))). % 34.43/21.10 % SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 34.43/21.10 %------------------------------------------------------------------------------