%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : SWB032-10 : TPTP v9.0.0. Released v7.3.0. % Transfm : none % Format : tptp:raw % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % Computer : n017.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:59 PM UTC 2025 % Result : Satisfiable 26.88s 17.17s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : SWB032-10 : TPTP v9.0.0. Released v7.3.0. % 0.07/0.13 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % 0.13/0.34 % Computer : n017.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 300 % 0.13/0.34 % DateTime : Wed Apr 9 01:05:10 EDT 2025 % 0.13/0.34 % CPUTime : % 26.88/17.17 % 26.88/17.17 % SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 26.88/17.17 % 26.88/17.17 % SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 26.88/17.19 %$ ifeq > iext > tuple > icext > #nlpp > lv > ir > ip > ic > uri_xsd_string > uri_xsd_integer > uri_xsd_decimal > 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_disjointWith > true % 26.88/17.19 % 26.88/17.19 %Foreground sorts: % 26.88/17.19 % 26.88/17.19 % 26.88/17.19 %Background operators: % 26.88/17.19 % 26.88/17.19 % 26.88/17.19 %Foreground operators: % 26.88/17.19 tff(uri_rdfs_Datatype, type, uri_rdfs_Datatype: $i). % 26.88/17.19 tff(uri_rdfs_ContainerMembershipProperty, type, uri_rdfs_ContainerMembershipProperty: $i). % 26.88/17.19 tff(uri_rdfs_Resource, type, uri_rdfs_Resource: $i). % 26.88/17.19 tff(uri_rdf_Property, type, uri_rdf_Property: $i). % 26.88/17.19 tff(uri_rdf_subject, type, uri_rdf_subject: $i). % 26.88/17.19 tff(uri_xsd_integer, type, uri_xsd_integer: $i). % 26.88/17.19 tff(uri_rdf_type, type, uri_rdf_type: $i). % 26.88/17.19 tff(uri_xsd_decimal, type, uri_xsd_decimal: $i). % 26.88/17.19 tff(uri_rdfs_subPropertyOf, type, uri_rdfs_subPropertyOf: $i). % 26.88/17.19 tff(uri_rdfs_seeAlso, type, uri_rdfs_seeAlso: $i). % 26.88/17.19 tff(icext, type, icext: ($i * $i) > $i). % 26.88/17.19 tff(uri_rdfs_range, type, uri_rdfs_range: $i). % 26.88/17.19 tff(uri_rdf_XMLLiteral, type, uri_rdf_XMLLiteral: $i). % 26.88/17.19 tff(uri_rdf_List, type, uri_rdf_List: $i). % 26.88/17.19 tff(uri_rdf_first, type, uri_rdf_first: $i). % 26.88/17.19 tff(uri_rdf_predicate, type, uri_rdf_predicate: $i). % 26.88/17.19 tff(tuple, type, tuple: ($i * $i) > $i). % 26.88/17.19 tff(ir, type, ir: $i > $i). % 26.88/17.19 tff(lv, type, lv: $i > $i). % 26.88/17.19 tff(uri_rdf__3, type, uri_rdf__3: $i). % 26.88/17.19 tff(uri_rdf_value, type, uri_rdf_value: $i). % 26.88/17.19 tff(ic, type, ic: $i > $i). % 26.88/17.19 tff(uri_rdfs_Statement, type, uri_rdfs_Statement: $i). % 26.88/17.19 tff(uri_owl_disjointWith, type, uri_owl_disjointWith: $i). % 26.88/17.19 tff(uri_xsd_string, type, uri_xsd_string: $i). % 26.88/17.19 tff(uri_rdf__1, type, uri_rdf__1: $i). % 26.88/17.19 tff(iext, type, iext: ($i * $i * $i) > $i). % 26.88/17.19 tff(uri_rdf_rest, type, uri_rdf_rest: $i). % 26.88/17.19 tff(uri_rdfs_label, type, uri_rdfs_label: $i). % 26.88/17.19 tff(uri_rdfs_Container, type, uri_rdfs_Container: $i). % 26.88/17.19 tff(uri_rdfs_subClassOf, type, uri_rdfs_subClassOf: $i). % 26.88/17.19 tff(uri_rdf_object, type, uri_rdf_object: $i). % 26.88/17.19 tff(ip, type, ip: $i > $i). % 26.88/17.19 tff(uri_rdfs_Class, type, uri_rdfs_Class: $i). % 26.88/17.19 tff(uri_rdfs_Seq, type, uri_rdfs_Seq: $i). % 26.88/17.19 tff(uri_rdfs_member, type, uri_rdfs_member: $i). % 26.88/17.19 tff(uri_rdf_Bag, type, uri_rdf_Bag: $i). % 26.88/17.19 tff(uri_rdf__2, type, uri_rdf__2: $i). % 26.88/17.19 tff(uri_rdfs_comment, type, uri_rdfs_comment: $i). % 26.88/17.19 tff(uri_rdfs_Literal, type, uri_rdfs_Literal: $i). % 26.88/17.19 tff(true, type, true: $i). % 26.88/17.19 tff(uri_rdf_Alt, type, uri_rdf_Alt: $i). % 26.88/17.19 tff(uri_rdf_nil, type, uri_rdf_nil: $i). % 26.88/17.19 tff(uri_rdfs_isDefinedBy, type, uri_rdfs_isDefinedBy: $i). % 26.88/17.19 tff(uri_rdfs_domain, type, uri_rdfs_domain: $i). % 26.88/17.19 tff(ifeq, type, ifeq: ($i * $i * $i * $i) > $i). % 26.88/17.19 % 26.88/17.19 %Saturated clause set: % 26.88/17.19 tff(c_14120, 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))). % 26.88/17.19 tff(c_13993, 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))). % 26.88/17.19 tff(c_15359, 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))). % 26.88/17.19 tff(c_61714, plain, (![X_1133, Y_1134]: (ifeq(iext(uri_rdfs_label, X_1133, Y_1134), true, iext(uri_rdfs_label, X_1133, Y_1134), true)=true))). % 26.88/17.19 tff(c_61687, plain, (![X_1129, Y_1130]: (ifeq(iext(uri_rdfs_comment, X_1129, Y_1130), true, iext(uri_rdfs_comment, X_1129, Y_1130), true)=true))). % 26.88/17.19 tff(c_14058, 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))). % 26.88/17.19 tff(c_61549, plain, (![X_1124, Y_1125]: (ifeq(iext(uri_rdf_predicate, X_1124, Y_1125), true, iext(uri_rdf_predicate, X_1124, Y_1125), true)=true))). % 26.88/17.19 tff(c_13816, 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))). % 26.88/17.19 tff(c_61407, plain, (![X_1119, Y_1120]: (ifeq(iext(uri_rdfs_member, X_1119, Y_1120), true, iext(uri_rdfs_member, X_1119, Y_1120), true)=true))). % 26.88/17.19 tff(c_5548, 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))). % 26.88/17.19 tff(c_5551, 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))). % 26.88/17.19 tff(c_13895, 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))). % 26.88/17.19 tff(c_13379, 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))). % 26.88/17.19 tff(c_13677, 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))). % 26.88/17.19 tff(c_13446, 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))). % 26.88/17.19 tff(c_60443, plain, (![C_1109]: (ifeq(iext(uri_rdfs_subClassOf, C_1109, uri_rdfs_Statement), true, iext(uri_rdfs_subClassOf, C_1109, uri_rdfs_Resource), true)=true))). % 26.88/17.19 tff(c_13586, 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))). % 26.88/17.19 tff(c_60192, plain, (![C_1106]: (ifeq(iext(uri_rdfs_subClassOf, C_1106, uri_rdf_List), true, iext(uri_rdfs_subClassOf, C_1106, uri_rdfs_Resource), true)=true))). % 26.88/17.19 tff(c_5816, 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))). % 26.88/17.19 tff(c_13010, 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))). % 26.88/17.19 tff(c_10566, 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))). % 26.88/17.20 tff(c_13057, 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))). % 26.88/17.20 tff(c_10569, 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))). % 26.88/17.20 tff(c_12594, 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))). % 26.88/17.20 tff(c_13257, 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))). % 26.88/17.20 tff(c_12642, 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))). % 26.88/17.20 tff(c_13182, 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))). % 26.88/17.20 tff(c_5819, 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))). % 26.88/17.20 tff(c_12717, 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))). % 26.88/17.20 tff(c_9654, 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))). % 26.88/17.20 tff(c_9657, 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))). % 26.88/17.20 tff(c_13305, 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))). % 26.88/17.20 tff(c_13105, 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))). % 26.88/17.20 tff(c_12427, 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))). % 27.03/17.20 tff(c_12234, 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))). % 27.03/17.20 tff(c_12834, 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))). % 27.03/17.20 tff(c_12547, 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))). % 27.03/17.20 tff(c_15146, 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))). % 27.03/17.20 tff(c_12354, 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))). % 27.03/17.20 tff(c_11559, 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))). % 27.03/17.20 tff(c_9333, 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))). % 27.03/17.20 tff(c_57544, plain, (![X_1073, Y_1074]: (ifeq(iext(uri_rdfs_seeAlso, X_1073, Y_1074), true, iext(uri_rdfs_seeAlso, X_1073, Y_1074), true)=true))). % 27.03/17.20 tff(c_57405, plain, (![C_1071]: (ifeq(iext(uri_rdfs_subClassOf, C_1071, uri_rdf_Bag), true, iext(uri_rdfs_subClassOf, C_1071, uri_rdfs_Resource), true)=true))). % 27.03/17.20 tff(c_57144, plain, (![C_1067]: (ifeq(iext(uri_rdfs_subClassOf, C_1067, uri_rdfs_Seq), true, iext(uri_rdfs_subClassOf, C_1067, uri_rdfs_Resource), true)=true))). % 27.03/17.20 tff(c_4044, 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))). % 27.03/17.20 tff(c_57005, plain, (![C_1065]: (ifeq(iext(uri_rdfs_subClassOf, C_1065, uri_rdfs_Datatype), true, iext(uri_rdfs_subClassOf, C_1065, uri_rdfs_Resource), true)=true))). % 27.03/17.20 tff(c_4001, 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))). % 27.03/17.20 tff(c_56849, plain, (![X_1059, Y_1060]: (ifeq(iext(uri_rdf_first, X_1059, Y_1060), true, iext(uri_rdf_first, X_1059, Y_1060), true)=true))). % 27.03/17.20 tff(c_56822, plain, (![X_1055, Y_1056]: (ifeq(iext(uri_rdfs_isDefinedBy, X_1055, Y_1056), true, iext(uri_rdfs_isDefinedBy, X_1055, Y_1056), true)=true))). % 27.03/17.20 tff(c_4251, 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))). % 27.03/17.20 tff(c_8838, 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))). % 27.03/17.20 tff(c_7477, 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))). % 27.03/17.20 tff(c_56441, plain, (![X_1047, Y_1048]: (ifeq(iext(uri_rdf_object, X_1047, Y_1048), true, iext(uri_rdf_object, X_1047, Y_1048), true)=true))). % 27.03/17.20 tff(c_56374, plain, (![P_1045]: (ifeq(iext(uri_rdfs_subPropertyOf, P_1045, uri_rdf__2), true, iext(uri_rdfs_subPropertyOf, P_1045, uri_rdfs_member), true)=true))). % 27.03/17.20 tff(c_6101, 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))). % 27.03/17.20 tff(c_56237, plain, (![X_1040, Y_1041]: (ifeq(iext(uri_rdf_value, X_1040, Y_1041), true, iext(uri_rdf_value, X_1040, Y_1041), true)=true))). % 27.03/17.20 tff(c_9519, 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))). % 27.03/17.20 tff(c_3852, 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))). % 27.03/17.20 tff(c_8329, 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))). % 27.03/17.20 tff(c_7333, 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))). % 27.03/17.20 tff(c_4147, 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))). % 27.03/17.20 tff(c_55578, plain, (![P_1031]: (ifeq(iext(uri_rdfs_subPropertyOf, P_1031, uri_rdf__3), true, iext(uri_rdfs_subPropertyOf, P_1031, uri_rdfs_member), true)=true))). % 27.03/17.20 tff(c_55550, plain, (![X_1027, Y_1028]: (ifeq(iext(uri_rdf__2, X_1027, Y_1028), true, iext(uri_rdfs_member, X_1027, Y_1028), true)=true))). % 27.03/17.20 tff(c_4507, 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))). % 27.03/17.20 tff(c_4248, 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))). % 27.03/17.20 tff(c_5661, 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))). % 27.03/17.20 tff(c_55057, plain, (![C_1021]: (ifeq(iext(uri_rdfs_subClassOf, C_1021, uri_rdfs_Class), true, iext(uri_rdfs_subClassOf, C_1021, uri_rdfs_Resource), true)=true))). % 27.03/17.20 tff(c_55029, plain, (![X_1017, Y_1018]: (ifeq(iext(uri_rdf__3, X_1017, Y_1018), true, iext(uri_rdfs_member, X_1017, Y_1018), true)=true))). % 27.03/17.20 tff(c_54866, plain, (![C_1015]: (ifeq(iext(uri_rdfs_subClassOf, C_1015, uri_rdfs_Container), true, iext(uri_rdfs_subClassOf, C_1015, uri_rdfs_Resource), true)=true))). % 27.03/17.20 tff(c_3954, 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))). % 27.03/17.20 tff(c_54713, plain, (![X_1009, Y_1010]: (ifeq(iext(uri_rdf_subject, X_1009, Y_1010), true, iext(uri_rdf_subject, X_1009, Y_1010), true)=true))). % 27.03/17.20 tff(c_4104, 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))). % 27.03/17.20 tff(c_10512, 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))). % 27.03/17.20 tff(c_54403, plain, (![P_1004]: (ifeq(iext(uri_rdfs_subPropertyOf, P_1004, uri_rdf__1), true, iext(uri_rdfs_subPropertyOf, P_1004, uri_rdfs_member), true)=true))). % 27.03/17.20 tff(c_10033, 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))). % 27.03/17.20 tff(c_11843, 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))). % 27.03/17.20 tff(c_7588, 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))). % 27.03/17.20 tff(c_3951, 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))). % 27.03/17.21 tff(c_53333, plain, (![X_995, Y_996]: (ifeq(iext(uri_rdfs_subPropertyOf, X_995, Y_996), true, iext(uri_rdfs_subPropertyOf, X_995, Y_996), true)=true))). % 27.03/17.21 tff(c_7112, 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))). % 27.03/17.21 tff(c_11301, 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))). % 27.03/17.21 tff(c_52961, plain, (![C_991]: (ifeq(iext(uri_rdfs_subClassOf, C_991, uri_rdfs_Literal), true, iext(uri_rdfs_subClassOf, C_991, uri_rdfs_Resource), true)=true))). % 27.03/17.21 tff(c_9262, 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))). % 27.03/17.21 tff(c_5975, 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))). % 27.03/17.21 tff(c_52712, plain, (![X_985, Y_986]: (ifeq(iext(uri_rdf_rest, X_985, Y_986), true, iext(uri_rdf_rest, X_985, Y_986), true)=true))). % 27.03/17.21 tff(c_3896, 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))). % 27.03/17.21 tff(c_4150, 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))). % 27.03/17.21 tff(c_6587, 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))). % 27.03/17.21 tff(c_9784, 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))). % 27.03/17.21 tff(c_5020, 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))). % 27.03/17.21 tff(c_4570, 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))). % 27.03/17.21 tff(c_10166, 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))). % 27.03/17.21 tff(c_4047, 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))). % 27.03/17.21 tff(c_8157, 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))). % 27.03/17.21 tff(c_6880, 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))). % 27.03/17.21 tff(c_50908, plain, (![X_968, Y_969]: (ifeq(iext(uri_rdf_type, X_968, Y_969), true, iext(uri_rdf_type, X_968, Y_969), true)=true))). % 27.03/17.21 tff(c_8481, 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))). % 27.03/17.21 tff(c_50211, plain, (![X_963, Y_964]: (ifeq(iext(uri_rdfs_subClassOf, X_963, Y_964), true, iext(uri_rdfs_subClassOf, X_963, Y_964), true)=true))). % 27.03/17.21 tff(c_49880, plain, (![X_959, Y_960]: (ifeq(iext(uri_rdfs_domain, X_959, Y_960), true, iext(uri_rdfs_domain, X_959, Y_960), true)=true))). % 27.03/17.21 tff(c_5394, 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))). % 27.03/17.21 tff(c_5284, 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))). % 27.03/17.21 tff(c_3899, 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))). % 27.03/17.21 tff(c_4955, 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))). % 27.03/17.21 tff(c_10456, 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))). % 27.03/17.21 tff(c_48898, plain, (![C_949]: (ifeq(iext(uri_rdfs_subClassOf, C_949, uri_rdfs_ContainerMembershipProperty), true, iext(uri_rdfs_subClassOf, C_949, uri_rdfs_Resource), true)=true))). % 27.03/17.21 tff(c_3849, 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))). % 27.03/17.21 tff(c_4101, 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))). % 27.03/17.21 tff(c_4206, 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))). % 27.03/17.21 tff(c_48100, plain, (![C_939]: (ifeq(iext(uri_rdfs_subClassOf, C_939, uri_rdf_Alt), true, iext(uri_rdfs_subClassOf, C_939, uri_rdfs_Resource), true)=true))). % 27.03/17.21 tff(c_9848, 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))). % 27.03/17.21 tff(c_5913, 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))). % 27.03/17.21 tff(c_10877, 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))). % 27.03/17.21 tff(c_47185, plain, (![X_928, Y_929]: (ifeq(iext(uri_rdfs_range, X_928, Y_929), true, iext(uri_rdfs_range, X_928, Y_929), true)=true))). % 27.03/17.21 tff(c_47172, plain, (![X_926, Y_927]: (ifeq(iext(uri_rdf__1, X_926, Y_927), true, iext(uri_rdf__1, X_926, Y_927), true)=true))). % 27.03/17.21 tff(c_9600, 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))). % 27.03/17.21 tff(c_4639, 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))). % 27.03/17.21 tff(c_5170, 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))). % 27.03/17.21 tff(c_45488, plain, (![C_911]: (ifeq(iext(uri_rdfs_subClassOf, C_911, uri_rdf_Property), true, iext(uri_rdfs_subClassOf, C_911, uri_rdfs_Resource), true)=true))). % 27.03/17.21 tff(c_4203, 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))). % 27.03/17.21 tff(c_45461, plain, (![X_907, Y_908]: (ifeq(iext(uri_rdf__3, X_907, Y_908), true, iext(uri_rdf__3, X_907, Y_908), true)=true))). % 27.03/17.21 tff(c_45322, plain, (![C_905]: (ifeq(iext(uri_rdfs_subClassOf, C_905, uri_rdf_XMLLiteral), true, iext(uri_rdfs_subClassOf, C_905, uri_rdfs_Resource), true)=true))). % 27.03/17.21 tff(c_11720, 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))). % 27.03/17.21 tff(c_45178, plain, (![X_900, Y_901]: (ifeq(iext(uri_rdf__2, X_900, Y_901), true, iext(uri_rdf__2, X_900, Y_901), true)=true))). % 27.03/17.21 tff(c_11114, 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))). % 27.03/17.21 tff(c_4750, 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))). % 27.03/17.21 tff(c_6770, 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))). % 27.03/17.21 tff(c_7709, 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))). % 27.03/17.21 tff(c_3998, 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))). % 27.03/17.21 tff(c_10675, 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))). % 27.03/17.21 tff(c_11180, 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))). % 27.03/17.21 tff(c_43813, plain, (![X_884, Y_885]: (ifeq(iext(uri_rdf__1, X_884, Y_885), true, iext(uri_rdfs_member, X_884, Y_885), true)=true))). % 27.03/17.21 tff(c_5762, 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))). % 27.03/17.21 tff(c_9933, 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))). % 27.03/17.21 tff(c_12003, 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))). % 27.03/17.21 tff(c_10961, 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))). % 27.03/17.21 tff(c_8928, 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))). % 27.03/17.21 tff(c_6288, 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))). % 27.03/17.21 tff(c_6291, 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))). % 27.03/17.21 tff(c_6462, 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))). % 27.03/17.21 tff(c_12000, 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))). % 27.03/17.21 tff(c_12792, 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))). % 27.03/17.21 tff(c_9422, 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))). % 27.03/17.21 tff(c_15102, 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))). % 27.03/17.21 tff(c_12789, 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))). % 27.03/17.21 tff(c_8925, 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))). % 27.03/17.21 tff(c_9419, 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))). % 27.03/17.21 tff(c_6459, 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))). % 27.03/17.21 tff(c_15099, 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))). % 27.03/17.21 tff(c_10964, 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))). % 27.03/17.22 tff(c_4433, 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))). % 27.03/17.22 tff(c_9936, 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))). % 27.03/17.22 tff(c_3375, 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))). % 27.03/17.22 tff(c_3583, 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))). % 27.03/17.22 tff(c_3548, 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))). % 27.03/17.22 tff(c_3797, 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))). % 27.03/17.22 tff(c_3345, 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))). % 27.03/17.22 tff(c_3208, 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))). % 27.03/17.22 tff(c_3504, 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))). % 27.03/17.22 tff(c_3624, 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))). % 27.03/17.22 tff(c_3372, 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))). % 27.03/17.22 tff(c_3660, 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))). % 27.03/17.22 tff(c_3211, 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))). % 27.03/17.22 tff(c_3621, 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))). % 27.03/17.22 tff(c_3348, 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))). % 27.03/17.22 tff(c_3252, 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))). % 27.03/17.22 tff(c_3255, 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))). % 27.03/17.22 tff(c_3551, 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))). % 27.03/17.22 tff(c_3457, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdf_Property), true, ifeq(iext(P_28, X_30, uri_rdf_object), true, true, true), true)=true))). % 27.03/17.22 tff(c_3417, 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))). % 27.03/17.22 tff(c_3580, 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))). % 27.03/17.22 tff(c_3414, 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))). % 27.03/17.22 tff(c_3800, 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))). % 27.03/17.22 tff(c_3663, 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))). % 27.03/17.22 tff(c_3708, 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))). % 27.03/17.22 tff(c_3711, 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))). % 27.03/17.22 tff(c_3755, 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))). % 27.03/17.22 tff(c_3758, 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))). % 27.03/17.22 tff(c_3460, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdf_Property), true, ifeq(iext(P_18, uri_rdf_object, Y_21), true, true, true), true)=true))). % 27.03/17.22 tff(c_3289, 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))). % 27.03/17.22 tff(c_3501, 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))). % 27.03/17.22 tff(c_3292, 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))). % 27.03/17.22 tff(c_1923, plain, (![P_95, X_97, X_60]: (ifeq(iext(uri_rdfs_range, P_95, uri_rdfs_Resource), true, ifeq(iext(P_95, X_97, X_60), true, true, true), true)=true))). % 27.03/17.22 tff(c_1594, plain, (![P_91, X_60, Y_94]: (ifeq(iext(uri_rdfs_domain, P_91, uri_rdfs_Resource), true, ifeq(iext(P_91, X_60, Y_94), true, true, true), true)=true))). % 27.03/17.22 tff(c_2752, plain, (![P_105]: (ifeq(iext(uri_rdfs_subPropertyOf, P_105, uri_rdfs_range), true, ifeq(iext(P_105, uri_rdf_value, uri_rdfs_Resource), true, true, true), true)=true))). % 27.03/17.22 tff(c_2590, plain, (![P_105]: (ifeq(iext(uri_rdfs_subPropertyOf, P_105, uri_rdfs_range), true, ifeq(iext(P_105, uri_rdfs_subClassOf, uri_rdfs_Class), true, true, true), true)=true))). % 27.03/17.22 tff(c_2668, plain, (![P_105]: (ifeq(iext(uri_rdfs_subPropertyOf, P_105, uri_rdfs_subClassOf), true, ifeq(iext(P_105, uri_rdf_Bag, uri_rdfs_Container), true, true, true), true)=true))). % 27.03/17.22 tff(c_2584, plain, (![P_105]: (ifeq(iext(uri_rdfs_subPropertyOf, P_105, uri_rdfs_range), true, ifeq(iext(P_105, uri_rdf_subject, uri_rdfs_Resource), true, true, true), true)=true))). % 27.03/17.22 tff(c_35136, plain, (![P_769]: (ifeq(iext(uri_rdfs_subPropertyOf, P_769, uri_rdfs_isDefinedBy), true, iext(uri_rdfs_subPropertyOf, P_769, uri_rdfs_seeAlso), true)=true))). % 27.03/17.22 tff(c_2431, plain, (![P_105]: (ifeq(iext(uri_rdfs_subPropertyOf, P_105, uri_rdfs_range), true, ifeq(iext(P_105, uri_rdf__3, uri_rdfs_Resource), true, true, true), true)=true))). % 27.03/17.22 tff(c_34855, plain, (![C_765]: (ifeq(iext(uri_rdfs_subClassOf, C_765, uri_rdfs_ContainerMembershipProperty), true, iext(uri_rdfs_subClassOf, C_765, uri_rdf_Property), true)=true))). % 27.03/17.22 tff(c_2710, plain, (![P_105]: (ifeq(iext(uri_rdfs_subPropertyOf, P_105, uri_rdf_type), true, ifeq(iext(P_105, uri_rdf_first, uri_rdf_Property), true, true, true), true)=true))). % 27.03/17.22 tff(c_2479, plain, (![P_105]: (ifeq(iext(uri_rdfs_subPropertyOf, P_105, uri_rdfs_range), true, ifeq(iext(P_105, uri_rdfs_range, uri_rdfs_Class), true, true, true), true)=true))). % 27.03/17.22 tff(c_2662, plain, (![P_105]: (ifeq(iext(uri_rdfs_subPropertyOf, P_105, uri_rdfs_range), true, ifeq(iext(P_105, uri_rdf_first, uri_rdfs_Resource), true, true, true), true)=true))). % 27.03/17.22 tff(c_34535, plain, (![C_760]: (ifeq(iext(uri_rdfs_subClassOf, C_760, uri_rdf_Alt), true, iext(uri_rdfs_subClassOf, C_760, uri_rdfs_Container), true)=true))). % 27.03/17.22 tff(c_34510, plain, (![C_759]: (ifeq(iext(uri_rdfs_subClassOf, C_759, uri_rdfs_Datatype), true, iext(uri_rdfs_subClassOf, C_759, uri_rdfs_Class), true)=true))). % 27.03/17.22 tff(c_2518, plain, (![P_105]: (ifeq(iext(uri_rdfs_subPropertyOf, P_105, uri_rdfs_range), true, ifeq(iext(P_105, uri_rdfs_label, uri_rdfs_Literal), true, true, true), true)=true))). % 27.03/17.22 tff(c_2632, plain, (![P_105]: (ifeq(iext(uri_rdfs_subPropertyOf, P_105, uri_rdf_type), true, ifeq(iext(P_105, uri_rdf_type, uri_rdf_Property), true, true, true), true)=true))). % 27.03/17.22 tff(c_2524, plain, (![P_105]: (ifeq(iext(uri_rdfs_subPropertyOf, P_105, uri_rdf_type), true, ifeq(iext(P_105, uri_rdf_object, uri_rdf_Property), true, true, true), true)=true))). % 27.03/17.22 tff(c_2461, plain, (![P_105]: (ifeq(iext(uri_rdfs_subPropertyOf, P_105, uri_rdfs_domain), true, ifeq(iext(P_105, uri_rdf__2, uri_rdfs_Resource), true, true, true), true)=true))). % 27.03/17.22 tff(c_2506, plain, (![P_105]: (ifeq(iext(uri_rdfs_subPropertyOf, P_105, uri_rdfs_subPropertyOf), true, ifeq(iext(P_105, uri_rdfs_isDefinedBy, uri_rdfs_seeAlso), true, true, true), true)=true))). % 27.03/17.22 tff(c_33924, plain, (![X_750, Y_751]: (ifeq(iext(uri_rdfs_isDefinedBy, X_750, Y_751), true, iext(uri_rdfs_seeAlso, X_750, Y_751), true)=true))). % 27.03/17.22 tff(c_2650, plain, (![P_105]: (ifeq(iext(uri_rdfs_subPropertyOf, P_105, uri_rdfs_domain), true, ifeq(iext(P_105, uri_rdfs_domain, uri_rdf_Property), true, true, true), true)=true))). % 27.03/17.22 tff(c_2425, plain, (![P_105]: (ifeq(iext(uri_rdfs_subPropertyOf, P_105, uri_rdfs_domain), true, ifeq(iext(P_105, uri_rdf_predicate, uri_rdfs_Statement), true, true, true), true)=true))). % 27.03/17.22 tff(c_2686, plain, (![P_105]: (ifeq(iext(uri_rdfs_subPropertyOf, P_105, uri_rdf_type), true, ifeq(iext(P_105, uri_rdf__1, uri_rdf_Property), true, true, true), true)=true))). % 27.03/17.22 tff(c_2497, plain, (![P_105]: (ifeq(iext(uri_rdfs_subPropertyOf, P_105, uri_rdf_type), true, ifeq(iext(P_105, uri_rdf_rest, uri_rdf_Property), true, true, true), true)=true))). % 27.03/17.22 tff(c_2698, plain, (![P_105]: (ifeq(iext(uri_rdfs_subPropertyOf, P_105, uri_rdfs_domain), true, ifeq(iext(P_105, uri_rdf_first, uri_rdf_List), true, true, true), true)=true))). % 27.03/17.22 tff(c_2572, plain, (![P_105]: (ifeq(iext(uri_rdfs_subPropertyOf, P_105, uri_rdfs_domain), true, ifeq(iext(P_105, uri_rdf_subject, uri_rdfs_Statement), true, true, true), true)=true))). % 27.03/17.22 tff(c_2614, plain, (![P_105]: (ifeq(iext(uri_rdfs_subPropertyOf, P_105, uri_rdfs_range), true, ifeq(iext(P_105, uri_rdfs_isDefinedBy, uri_rdfs_Resource), true, true, true), true)=true))). % 27.03/17.22 tff(c_2734, plain, (![P_105]: (ifeq(iext(uri_rdfs_subPropertyOf, P_105, uri_rdfs_range), true, ifeq(iext(P_105, uri_rdfs_seeAlso, uri_rdfs_Resource), true, true, true), true)=true))). % 27.03/17.22 tff(c_2413, plain, (![P_105]: (ifeq(iext(uri_rdfs_subPropertyOf, P_105, uri_rdfs_range), true, ifeq(iext(P_105, uri_rdf__2, uri_rdfs_Resource), true, true, true), true)=true))). % 27.03/17.22 tff(c_2548, plain, (![P_105]: (ifeq(iext(uri_rdfs_subPropertyOf, P_105, uri_rdfs_range), true, ifeq(iext(P_105, uri_rdf_predicate, uri_rdfs_Resource), true, true, true), true)=true))). % 27.03/17.22 tff(c_2437, plain, (![P_105]: (ifeq(iext(uri_rdfs_subPropertyOf, P_105, uri_rdfs_domain), true, ifeq(iext(P_105, uri_rdf__3, uri_rdfs_Resource), true, true, true), true)=true))). % 27.03/17.22 tff(c_2692, plain, (![P_105]: (ifeq(iext(uri_rdfs_subPropertyOf, P_105, uri_rdfs_subClassOf), true, ifeq(iext(P_105, uri_rdfs_Datatype, uri_rdfs_Class), true, true, true), true)=true))). % 27.03/17.22 tff(c_2449, plain, (![P_105]: (ifeq(iext(uri_rdfs_subPropertyOf, P_105, uri_rdf_type), true, ifeq(iext(P_105, uri_rdf_nil, uri_rdf_List), true, true, true), true)=true))). % 27.03/17.22 tff(c_2608, plain, (![P_105]: (ifeq(iext(uri_rdfs_subPropertyOf, P_105, uri_rdfs_domain), true, ifeq(iext(P_105, uri_rdf_rest, uri_rdf_List), true, true, true), true)=true))). % 27.03/17.22 tff(c_2722, plain, (![P_105]: (ifeq(iext(uri_rdfs_subPropertyOf, P_105, uri_rdfs_range), true, ifeq(iext(P_105, uri_rdf_rest, uri_rdf_List), true, true, true), true)=true))). % 27.03/17.22 tff(c_2674, plain, (![P_105]: (ifeq(iext(uri_rdfs_subPropertyOf, P_105, uri_rdfs_subClassOf), true, ifeq(iext(P_105, uri_rdfs_ContainerMembershipProperty, uri_rdf_Property), true, true, true), true)=true))). % 27.03/17.22 tff(c_2455, plain, (![P_105]: (ifeq(iext(uri_rdfs_subPropertyOf, P_105, uri_rdfs_domain), true, ifeq(iext(P_105, uri_rdfs_subPropertyOf, uri_rdf_Property), true, true, true), true)=true))). % 27.03/17.22 tff(c_2554, plain, (![P_105]: (ifeq(iext(uri_rdfs_subPropertyOf, P_105, uri_rdfs_domain), true, ifeq(iext(P_105, uri_rdfs_label, uri_rdfs_Resource), true, true, true), true)=true))). % 27.03/17.22 tff(c_2485, plain, (![P_105]: (ifeq(iext(uri_rdfs_subPropertyOf, P_105, uri_rdf_type), true, ifeq(iext(P_105, uri_rdf__1, uri_rdfs_ContainerMembershipProperty), true, true, true), true)=true))). % 27.03/17.22 tff(c_2512, plain, (![P_105]: (ifeq(iext(uri_rdfs_subPropertyOf, P_105, uri_rdf_type), true, ifeq(iext(P_105, uri_rdf__2, uri_rdfs_ContainerMembershipProperty), true, true, true), true)=true))). % 27.03/17.22 tff(c_2716, plain, (![P_105]: (ifeq(iext(uri_rdfs_subPropertyOf, P_105, uri_rdf_type), true, ifeq(iext(P_105, uri_rdf__3, uri_rdfs_ContainerMembershipProperty), true, true, true), true)=true))). % 27.03/17.22 tff(c_2467, plain, (![P_105]: (ifeq(iext(uri_rdfs_subPropertyOf, P_105, uri_rdfs_range), true, ifeq(iext(P_105, uri_rdf__1, uri_rdfs_Resource), true, true, true), true)=true))). % 27.03/17.22 tff(c_2419, plain, (![P_105]: (ifeq(iext(uri_rdfs_subPropertyOf, P_105, uri_rdfs_domain), true, ifeq(iext(P_105, uri_rdf_object, uri_rdfs_Statement), true, true, true), true)=true))). % 27.03/17.22 tff(c_2740, plain, (![P_105]: (ifeq(iext(uri_rdfs_subPropertyOf, P_105, uri_rdfs_range), true, ifeq(iext(P_105, uri_rdfs_domain, uri_rdfs_Class), true, true, true), true)=true))). % 27.03/17.22 tff(c_2602, plain, (![P_105]: (ifeq(iext(uri_rdfs_subPropertyOf, P_105, uri_rdfs_domain), true, ifeq(iext(P_105, uri_rdf_type, uri_rdfs_Resource), true, true, true), true)=true))). % 27.03/17.22 tff(c_31002, plain, (![C_722]: (ifeq(iext(uri_rdfs_subClassOf, C_722, uri_rdf_XMLLiteral), true, iext(uri_rdfs_subClassOf, C_722, uri_rdfs_Literal), true)=true))). % 27.03/17.22 tff(c_30972, plain, (![D_721]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_721), true, icext(D_721, uri_rdfs_Resource), true)=true))). % 27.03/17.22 tff(c_30905, plain, (![D_719]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_719), true, icext(D_719, uri_rdfs_subPropertyOf), true)=true))). % 27.03/17.22 tff(c_30839, plain, (![D_717]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_717), true, icext(D_717, uri_rdfs_subClassOf), true)=true))). % 27.03/17.22 tff(c_2620, plain, (![P_105]: (ifeq(iext(uri_rdfs_subPropertyOf, P_105, uri_rdfs_domain), true, ifeq(iext(P_105, uri_rdfs_subClassOf, uri_rdfs_Class), true, true, true), true)=true))). % 27.03/17.22 tff(c_30658, plain, (![D_714]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_714), true, icext(D_714, uri_rdfs_range), true)=true))). % 27.03/17.22 tff(c_30592, plain, (![D_712]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_712), true, icext(D_712, uri_rdfs_ContainerMembershipProperty), true)=true))). % 27.03/17.22 tff(c_30524, plain, (![C_710]: (ifeq(iext(uri_rdfs_subClassOf, C_710, uri_rdfs_Seq), true, iext(uri_rdfs_subClassOf, C_710, uri_rdfs_Container), true)=true))). % 27.03/17.22 tff(c_30431, plain, (![D_708]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_708), true, icext(D_708, uri_rdfs_Class), true)=true))). % 27.03/17.22 tff(c_30364, plain, (![D_706]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_706), true, icext(D_706, uri_rdfs_Container), true)=true))). % 27.03/17.22 tff(c_30296, plain, (![C_704]: (ifeq(iext(uri_rdfs_subClassOf, C_704, uri_rdf_Bag), true, iext(uri_rdfs_subClassOf, C_704, uri_rdfs_Container), true)=true))). % 27.03/17.22 tff(c_30230, plain, (![D_702]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_702), true, icext(D_702, uri_rdfs_Seq), true)=true))). % 27.03/17.22 tff(c_30162, plain, (![D_700]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_700), true, icext(D_700, uri_rdfs_Datatype), true)=true))). % 27.03/17.22 tff(c_30087, plain, (![D_698]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_698), true, icext(D_698, uri_rdf_XMLLiteral), true)=true))). % 27.03/17.22 tff(c_30020, plain, (![D_696]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_696), true, icext(D_696, uri_rdf_Bag), true)=true))). % 27.03/17.22 tff(c_2560, plain, (![P_105]: (ifeq(iext(uri_rdfs_subPropertyOf, P_105, uri_rdfs_range), true, ifeq(iext(P_105, uri_rdfs_comment, uri_rdfs_Literal), true, true, true), true)=true))). % 27.03/17.22 tff(c_29842, plain, (![D_693]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_693), true, icext(D_693, uri_rdf_Alt), true)=true))). % 27.03/17.22 tff(c_29774, plain, (![D_691]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_691), true, icext(D_691, uri_rdfs_Literal), true)=true))). % 27.03/17.23 tff(c_29589, plain, (![D_688]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_688), true, icext(D_688, uri_rdfs_member), true)=true))). % 27.03/17.23 tff(c_2473, plain, (![P_105]: (ifeq(iext(uri_rdfs_subPropertyOf, P_105, uri_rdfs_domain), true, ifeq(iext(P_105, uri_rdf__1, uri_rdfs_Resource), true, true, true), true)=true))). % 27.03/17.23 tff(c_29523, plain, (![D_686]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_686), true, icext(D_686, uri_rdfs_Statement), true)=true))). % 27.03/17.23 tff(c_29457, plain, (![D_684]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_684), true, icext(D_684, uri_rdfs_isDefinedBy), true)=true))). % 27.03/17.23 tff(c_2596, plain, (![P_105]: (ifeq(iext(uri_rdfs_subPropertyOf, P_105, uri_rdfs_subClassOf), true, ifeq(iext(P_105, uri_rdf_XMLLiteral, uri_rdfs_Literal), true, true, true), true)=true))). % 27.03/17.23 tff(c_29280, plain, (![D_681]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_681), true, icext(D_681, uri_rdfs_comment), true)=true))). % 27.03/17.23 tff(c_29214, plain, (![D_679]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_679), true, icext(D_679, uri_rdfs_seeAlso), true)=true))). % 27.03/17.23 tff(c_29148, plain, (![D_677]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_677), true, icext(D_677, uri_rdf_predicate), true)=true))). % 27.03/17.23 tff(c_2491, plain, (![P_105]: (ifeq(iext(uri_rdfs_subPropertyOf, P_105, uri_rdfs_domain), true, ifeq(iext(P_105, uri_rdfs_member, uri_rdfs_Resource), true, true, true), true)=true))). % 27.03/17.23 tff(c_28963, plain, (![D_674]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_674), true, icext(D_674, uri_rdfs_label), true)=true))). % 27.03/17.23 tff(c_28896, plain, (![D_672]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_672), true, icext(D_672, uri_rdf_List), true)=true))). % 27.03/17.23 tff(c_28830, plain, (![D_670]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_670), true, icext(D_670, uri_rdfs_domain), true)=true))). % 27.03/17.23 tff(c_2656, plain, (![P_105]: (ifeq(iext(uri_rdfs_subPropertyOf, P_105, uri_rdf_type), true, ifeq(iext(P_105, uri_rdf_Property, uri_rdfs_Class), true, true, true), true)=true))). % 27.03/17.23 tff(c_28637, plain, (![D_667]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, D_667), true, icext(D_667, uri_rdf__2), true)=true))). % 27.03/17.23 tff(c_28571, plain, (![D_665]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_665), true, icext(D_665, uri_rdf_rest), true)=true))). % 27.03/17.23 tff(c_14139, 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))). % 27.03/17.23 tff(c_14024, 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))). % 27.03/17.23 tff(c_2704, plain, (![P_105]: (ifeq(iext(uri_rdfs_subPropertyOf, P_105, uri_rdf_type), true, ifeq(iext(P_105, uri_rdf_value, uri_rdf_Property), true, true, true), true)=true))). % 27.03/17.23 tff(c_15390, 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))). % 27.03/17.23 tff(c_14089, 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))). % 27.03/17.23 tff(c_13853, 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))). % 27.03/17.23 tff(c_2626, plain, (![P_105]: (ifeq(iext(uri_rdfs_subPropertyOf, P_105, uri_rdfs_range), true, ifeq(iext(P_105, uri_rdfs_member, uri_rdfs_Resource), true, true, true), true)=true))). % 27.03/17.23 tff(c_13929, 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))). % 27.03/17.23 tff(c_13413, 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))). % 27.03/17.23 tff(c_13480, 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))). % 27.03/17.23 tff(c_28030, plain, (![D_648]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_648), true, icext(D_648, uri_rdf_subject), true)=true))). % 27.03/17.23 tff(c_13711, 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))). % 27.03/17.23 tff(c_13481, 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))). % 27.03/17.23 tff(c_2644, plain, (![P_105]: (ifeq(iext(uri_rdfs_subPropertyOf, P_105, uri_rdfs_subClassOf), true, ifeq(iext(P_105, uri_rdfs_Seq, uri_rdfs_Container), true, true, true), true)=true))). % 27.03/17.23 tff(c_13712, 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))). % 27.03/17.23 tff(c_13620, 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))). % 27.03/17.23 tff(c_27719, plain, (![D_639]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_639), true, icext(D_639, uri_rdf_first), true)=true))). % 27.03/17.23 tff(c_13124, 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))). % 27.03/17.23 tff(c_13276, 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))). % 27.03/17.23 tff(c_12661, 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))). % 27.03/17.23 tff(c_13029, 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))). % 27.03/17.23 tff(c_13076, 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))). % 27.03/17.23 tff(c_13324, 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))). % 27.03/17.23 tff(c_13201, 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))). % 27.03/17.23 tff(c_12613, 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))). % 27.03/17.23 tff(c_12736, 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))). % 27.03/17.23 tff(c_12373, 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))). % 27.03/17.23 tff(c_12259, 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))). % 27.03/17.23 tff(c_2407, plain, (![P_105]: (ifeq(iext(uri_rdfs_subPropertyOf, P_105, uri_rdfs_domain), true, ifeq(iext(P_105, uri_rdfs_isDefinedBy, uri_rdfs_Resource), true, true, true), true)=true))). % 27.03/17.23 tff(c_12452, 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))). % 27.03/17.23 tff(c_12566, 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))). % 27.03/17.23 tff(c_12859, 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))). % 27.03/17.23 tff(c_15171, 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))). % 27.03/17.23 tff(c_9365, 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))). % 27.03/17.23 tff(c_11755, 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))). % 27.03/17.23 tff(c_7622, 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))). % 27.03/17.23 tff(c_4985, 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))). % 27.03/17.23 tff(c_2566, plain, (![P_105]: (ifeq(iext(uri_rdfs_subPropertyOf, P_105, uri_rdfs_domain), true, ifeq(iext(P_105, uri_rdfs_range, uri_rdf_Property), true, true, true), true)=true))). % 27.03/17.23 tff(c_9625, 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))). % 27.03/17.23 tff(c_27014, plain, (![D_613]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_613), true, icext(D_613, uri_rdf__1), true)=true))). % 27.03/17.23 tff(c_5051, 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))). % 27.03/17.23 tff(c_5427, 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))). % 27.03/17.23 tff(c_10067, 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))). % 27.03/17.23 tff(c_2536, plain, (![P_105]: (ifeq(iext(uri_rdfs_subPropertyOf, P_105, uri_rdfs_subClassOf), true, ifeq(iext(P_105, uri_rdf_Alt, uri_rdfs_Container), true, true, true), true)=true))). % 27.03/17.23 tff(c_9815, 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))). % 27.03/17.23 tff(c_7147, 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))). % 27.03/17.23 tff(c_26710, plain, (![D_604]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_604), true, icext(D_604, uri_rdf_type), true)=true))). % 27.03/17.23 tff(c_11878, 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))). % 27.03/17.23 tff(c_10909, 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))). % 27.03/17.23 tff(c_4537, 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))). % 27.03/17.23 tff(c_2746, plain, (![P_105]: (ifeq(iext(uri_rdfs_subPropertyOf, P_105, uri_rdfs_range), true, ifeq(iext(P_105, uri_rdfs_subPropertyOf, uri_rdf_Property), true, true, true), true)=true))). % 27.03/17.23 tff(c_4783, 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))). % 27.03/17.23 tff(c_8360, 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))). % 27.03/17.23 tff(c_6131, 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))). % 27.03/17.23 tff(c_8361, 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))). % 27.03/17.23 tff(c_11754, 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))). % 27.03/17.23 tff(c_9879, 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))). % 27.03/17.23 tff(c_2530, plain, (![P_105]: (ifeq(iext(uri_rdfs_subPropertyOf, P_105, uri_rdfs_domain), true, ifeq(iext(P_105, uri_rdfs_comment, uri_rdfs_Resource), true, true, true), true)=true))). % 27.03/17.23 tff(c_11214, 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))). % 27.03/17.23 tff(c_8873, 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))). % 27.03/17.23 tff(c_26134, plain, (![D_586]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_586), true, icext(D_586, uri_rdf__3), true)=true))). % 27.03/17.23 tff(c_4601, 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))). % 27.03/17.23 tff(c_7741, 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))). % 27.03/17.23 tff(c_2680, plain, (![P_105]: (ifeq(iext(uri_rdfs_subPropertyOf, P_105, uri_rdf_type), true, ifeq(iext(P_105, uri_rdf__2, uri_rdf_Property), true, true, true), true)=true))). % 27.03/17.23 tff(c_8193, 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))). % 27.03/17.23 tff(c_7502, 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))). % 27.03/17.23 tff(c_10537, 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))). % 27.03/17.23 tff(c_25848, plain, (![D_577]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_List, D_577), true, icext(D_577, uri_rdf_nil), true)=true))). % 27.03/17.23 tff(c_11335, 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))). % 27.03/17.23 tff(c_11877, 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))). % 27.03/17.23 tff(c_2401, plain, (![P_105]: (ifeq(iext(uri_rdfs_subPropertyOf, P_105, uri_rdf_type), true, ifeq(iext(P_105, uri_rdf__3, uri_rdf_Property), true, true, true), true)=true))). % 27.03/17.23 tff(c_5318, 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))). % 27.03/17.23 tff(c_11215, 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))). % 27.03/17.23 tff(c_10068, 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))). % 27.03/17.23 tff(c_6802, 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))). % 27.03/17.23 tff(c_9296, 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))). % 27.03/17.23 tff(c_7623, 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))). % 27.03/17.23 tff(c_5695, 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))). % 27.03/17.23 tff(c_10709, 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))). % 27.03/17.23 tff(c_6005, 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))). % 27.03/17.23 tff(c_2542, plain, (![P_105]: (ifeq(iext(uri_rdfs_subPropertyOf, P_105, uri_rdf_type), true, ifeq(iext(P_105, uri_rdf_subject, uri_rdf_Property), true, true, true), true)=true))). % 27.03/17.23 tff(c_5787, 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))). % 27.03/17.23 tff(c_6913, 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))). % 27.03/17.23 tff(c_25043, plain, (![D_551]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, D_551), true, icext(D_551, uri_rdf__1), true)=true))). % 27.03/17.23 tff(c_11594, 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))). % 27.03/17.23 tff(c_10197, 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))). % 27.03/17.23 tff(c_2443, plain, (![P_105]: (ifeq(iext(uri_rdfs_subPropertyOf, P_105, uri_rdfs_domain), true, ifeq(iext(P_105, uri_rdf_value, uri_rdfs_Resource), true, true, true), true)=true))). % 27.03/17.23 tff(c_7146, 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))). % 27.03/17.23 tff(c_8515, 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))). % 27.03/17.24 tff(c_5428, 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))). % 27.03/17.24 tff(c_7364, 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))). % 27.03/17.24 tff(c_6914, 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))). % 27.03/17.24 tff(c_2578, plain, (![P_105]: (ifeq(iext(uri_rdfs_subPropertyOf, P_105, uri_rdfs_range), true, ifeq(iext(P_105, uri_rdf_type, uri_rdfs_Class), true, true, true), true)=true))). % 27.03/17.24 tff(c_5944, 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))). % 27.03/17.24 tff(c_4669, 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))). % 27.03/17.24 tff(c_6801, 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))). % 27.03/17.24 tff(c_24458, plain, (![D_533]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_533), true, icext(D_533, uri_rdf_Property), true)=true))). % 27.03/17.24 tff(c_6620, 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))). % 27.03/17.24 tff(c_2638, plain, (![P_105]: (ifeq(iext(uri_rdfs_subPropertyOf, P_105, uri_rdf_type), true, ifeq(iext(P_105, uri_rdf_XMLLiteral, uri_rdfs_Datatype), true, true, true), true)=true))). % 27.03/17.24 tff(c_8872, 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))). % 27.03/17.24 tff(c_5200, 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))). % 27.03/17.24 tff(c_10481, 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))). % 27.03/17.24 tff(c_11148, 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))). % 27.03/17.24 tff(c_9544, 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))). % 27.03/17.24 tff(c_2728, plain, (![P_105]: (ifeq(iext(uri_rdfs_subPropertyOf, P_105, uri_rdfs_domain), true, ifeq(iext(P_105, uri_rdfs_seeAlso, uri_rdfs_Resource), true, true, true), true)=true))). % 27.03/17.24 tff(c_5050, 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))). % 27.03/17.24 tff(c_11593, 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))). % 27.03/17.24 tff(c_4453, 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))). % 27.03/17.24 tff(c_23692, plain, (![D_514]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, D_514), true, icext(D_514, uri_rdf_XMLLiteral), true)=true))). % 27.03/17.24 tff(c_2782, plain, (![Q_106]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_106), true, iext(Q_106, uri_rdfs_label, uri_rdfs_Resource), true)=true))). % 27.03/17.24 tff(c_2803, plain, (![Q_106]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_106), true, iext(Q_106, uri_rdf__2, uri_rdf_Property), true)=true))). % 27.03/17.24 tff(c_2796, plain, (![Q_106]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_106), true, iext(Q_106, uri_rdf_XMLLiteral, uri_rdfs_Datatype), true)=true))). % 27.03/17.24 tff(c_2776, plain, (![Q_106]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_106), true, iext(Q_106, uri_rdfs_label, uri_rdfs_Literal), true)=true))). % 27.03/17.24 tff(c_2774, plain, (![Q_106]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_106), true, iext(Q_106, uri_rdfs_isDefinedBy, uri_rdfs_seeAlso), true)=true))). % 27.03/17.24 tff(c_2809, plain, (![Q_106]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_106), true, iext(Q_106, uri_rdf__3, uri_rdfs_ContainerMembershipProperty), true)=true))). % 27.03/17.24 tff(c_2814, plain, (![Q_106]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_106), true, iext(Q_106, uri_rdfs_subPropertyOf, uri_rdf_Property), true)=true))). % 27.03/17.24 tff(c_23508, plain, (![D_505]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_505), true, icext(D_505, uri_rdf_object), true)=true))). % 27.03/17.24 tff(c_2810, plain, (![Q_106]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_106), true, iext(Q_106, uri_rdf_rest, uri_rdf_List), true)=true))). % 27.03/17.24 tff(c_2773, plain, (![Q_106]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_106), true, iext(Q_106, uri_rdf_rest, uri_rdf_Property), true)=true))). % 27.03/17.24 tff(c_2779, plain, (![Q_106]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_106), true, iext(Q_106, uri_rdf_Alt, uri_rdfs_Container), true)=true))). % 27.03/17.24 tff(c_2356, plain, (![E_100]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Container, E_100), true, iext(uri_rdfs_subClassOf, uri_rdfs_Seq, E_100), true)=true))). % 27.03/17.24 tff(c_2358, plain, (![E_100]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, E_100), true, iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, E_100), true)=true))). % 27.03/17.24 tff(c_2761, plain, (![Q_106]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_106), true, iext(Q_106, uri_rdf_predicate, uri_rdfs_Statement), true)=true))). % 27.03/17.24 tff(c_2808, plain, (![Q_106]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_106), true, iext(Q_106, uri_rdf_first, uri_rdf_Property), true)=true))). % 27.03/17.24 tff(c_23293, plain, (![D_496]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, D_496), true, icext(D_496, uri_rdf__3), true)=true))). % 27.03/17.24 tff(c_2813, plain, (![Q_106]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_106), true, iext(Q_106, uri_rdfs_domain, uri_rdfs_Class), true)=true))). % 27.03/17.24 tff(c_2784, plain, (![Q_106]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_106), true, iext(Q_106, uri_rdfs_range, uri_rdf_Property), true)=true))). % 27.03/17.24 tff(c_2794, plain, (![Q_106]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_106), true, iext(Q_106, uri_rdfs_member, uri_rdfs_Resource), true)=true))). % 27.03/17.24 tff(c_2771, plain, (![Q_106]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_106), true, iext(Q_106, uri_rdf__1, uri_rdfs_ContainerMembershipProperty), true)=true))). % 27.03/17.24 tff(c_2770, plain, (![Q_106]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_106), true, iext(Q_106, uri_rdfs_range, uri_rdfs_Class), true)=true))). % 27.03/17.24 tff(c_2354, plain, (![E_100]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Container, E_100), true, iext(uri_rdfs_subClassOf, uri_rdf_Alt, E_100), true)=true))). % 27.03/17.24 tff(c_2768, plain, (![Q_106]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_106), true, iext(Q_106, uri_rdf__1, uri_rdfs_Resource), true)=true))). % 27.03/17.24 tff(c_2760, plain, (![Q_106]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_106), true, iext(Q_106, uri_rdf_object, uri_rdfs_Statement), true)=true))). % 27.03/17.24 tff(c_2772, plain, (![Q_106]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_106), true, iext(Q_106, uri_rdfs_member, uri_rdfs_Resource), true)=true))). % 27.03/17.24 tff(c_2811, plain, (![Q_106]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_106), true, iext(Q_106, uri_rdfs_seeAlso, uri_rdfs_Resource), true)=true))). % 27.03/17.24 tff(c_2799, plain, (![Q_106]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_106), true, iext(Q_106, uri_rdf_Property, uri_rdfs_Class), true)=true))). % 27.03/17.24 tff(c_2759, plain, (![Q_106]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_106), true, iext(Q_106, uri_rdf__2, uri_rdfs_Resource), true)=true))). % 27.03/17.24 tff(c_2355, plain, (![E_100]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Literal, E_100), true, iext(uri_rdfs_subClassOf, uri_rdf_XMLLiteral, E_100), true)=true))). % 27.03/17.24 tff(c_2379, plain, (![R_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_seeAlso, R_103), true, iext(uri_rdfs_subPropertyOf, uri_rdfs_isDefinedBy, R_103), true)=true))). % 27.03/17.24 tff(c_2778, plain, (![Q_106]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_106), true, iext(Q_106, uri_rdfs_comment, uri_rdfs_Resource), true)=true))). % 27.03/17.24 tff(c_2815, plain, (![Q_106]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_106), true, iext(Q_106, uri_rdf_value, uri_rdfs_Resource), true)=true))). % 27.03/17.24 tff(c_2798, plain, (![Q_106]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_106), true, iext(Q_106, uri_rdfs_domain, uri_rdf_Property), true)=true))). % 27.03/17.24 tff(c_2786, plain, (![Q_106]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_106), true, iext(Q_106, uri_rdf_type, uri_rdfs_Class), true)=true))). % 27.03/17.24 tff(c_2763, plain, (![Q_106]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_106), true, iext(Q_106, uri_rdf__3, uri_rdfs_Resource), true)=true))). % 27.03/17.24 tff(c_2795, plain, (![Q_106]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_106), true, iext(Q_106, uri_rdf_type, uri_rdf_Property), true)=true))). % 27.03/17.24 tff(c_2757, plain, (![Q_106]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_106), true, iext(Q_106, uri_rdf__3, uri_rdf_Property), true)=true))). % 27.03/17.24 tff(c_2767, plain, (![Q_106]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_106), true, iext(Q_106, uri_rdf__2, uri_rdfs_Resource), true)=true))). % 27.03/17.24 tff(c_2802, plain, (![Q_106]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_106), true, iext(Q_106, uri_rdfs_ContainerMembershipProperty, uri_rdf_Property), true)=true))). % 27.03/17.24 tff(c_2788, plain, (![Q_106]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_106), true, iext(Q_106, uri_rdfs_subClassOf, uri_rdfs_Class), true)=true))). % 27.03/17.24 tff(c_2806, plain, (![Q_106]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_106), true, iext(Q_106, uri_rdf_first, uri_rdf_List), true)=true))). % 27.03/17.24 tff(c_22703, plain, (![D_469]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_469), true, icext(D_469, uri_rdf_value), true)=true))). % 27.03/17.24 tff(c_2777, plain, (![Q_106]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_106), true, iext(Q_106, uri_rdf_object, uri_rdf_Property), true)=true))). % 27.03/17.24 tff(c_2769, plain, (![Q_106]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_106), true, iext(Q_106, uri_rdf__1, uri_rdfs_Resource), true)=true))). % 27.03/17.24 tff(c_2804, plain, (![Q_106]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_106), true, iext(Q_106, uri_rdf__1, uri_rdf_Property), true)=true))). % 27.03/17.24 tff(c_2775, plain, (![Q_106]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_106), true, iext(Q_106, uri_rdf__2, uri_rdfs_ContainerMembershipProperty), true)=true))). % 27.03/17.24 tff(c_2797, plain, (![Q_106]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_106), true, iext(Q_106, uri_rdfs_Seq, uri_rdfs_Container), true)=true))). % 27.03/17.24 tff(c_2357, plain, (![E_100]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Container, E_100), true, iext(uri_rdfs_subClassOf, uri_rdf_Bag, E_100), true)=true))). % 27.03/17.24 tff(c_2789, plain, (![Q_106]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_106), true, iext(Q_106, uri_rdf_XMLLiteral, uri_rdfs_Literal), true)=true))). % 27.03/17.24 tff(c_15393, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_predicate), true)=true))). % 27.03/17.24 tff(c_15394, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_predicate), true)=true))). % 27.03/17.24 tff(c_14093, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_label), true)=true))). % 27.03/17.24 tff(c_2791, plain, (![Q_106]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_106), true, iext(Q_106, uri_rdf_rest, uri_rdf_List), true)=true))). % 27.03/17.24 tff(c_14092, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_label), true)=true))). % 27.03/17.24 tff(c_14027, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_comment), true)=true))). % 27.03/17.24 tff(c_14028, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_comment), true)=true))). % 27.03/17.24 tff(c_13857, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdfs_Resource), true)=true))). % 27.03/17.24 tff(c_13933, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_member), true)=true))). % 27.03/17.24 tff(c_2792, plain, (![Q_106]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_106), true, iext(Q_106, uri_rdfs_isDefinedBy, uri_rdfs_Resource), true)=true))). % 27.03/17.24 tff(c_13416, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdf_List), true)=true))). % 27.03/17.24 tff(c_13417, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdf_List), true)=true))). % 27.03/17.24 tff(c_13623, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdfs_Statement), true)=true))). % 27.03/17.24 tff(c_13624, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdfs_Statement), true)=true))). % 27.03/17.24 tff(c_2812, plain, (![Q_106]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_106), true, iext(Q_106, uri_rdfs_seeAlso, uri_rdfs_Resource), true)=true))). % 27.03/17.24 tff(c_2785, plain, (![Q_106]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_106), true, iext(Q_106, uri_rdf_subject, uri_rdfs_Statement), true)=true))). % 27.03/17.24 tff(c_22097, plain, (![D_444]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_444), true, icext(D_444, uri_rdf__2), true)=true))). % 27.03/17.24 tff(c_2762, plain, (![Q_106]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_106), true, iext(Q_106, uri_rdf__3, uri_rdfs_Resource), true)=true))). % 27.03/17.24 tff(c_21694, plain, (![D_439, X_440]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Resource, D_439), true, icext(D_439, X_440), true)=true))). % 27.03/17.24 tff(c_2359, plain, (![E_100]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, E_100), true, iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, E_100), true)=true))). % 27.03/17.24 tff(c_21509, plain, (![C_88, X_60]: (ifeq(icext(C_88, X_60), true, true, true)=true))). % 27.03/17.24 tff(c_4672, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_subPropertyOf), true)=true))). % 27.03/17.24 tff(c_2790, plain, (![Q_106]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_106), true, iext(Q_106, uri_rdf_type, uri_rdfs_Resource), true)=true))). % 27.03/17.24 tff(c_6134, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_range), true)=true))). % 27.03/17.24 tff(c_21396, plain, (![X_429, Y_430]: (ifeq(iext(uri_rdf_subject, X_429, Y_430), true, icext(uri_rdfs_Statement, X_429), true)=true))). % 27.03/17.24 tff(c_4603, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf__3), true)=true))). % 27.03/17.24 tff(c_2758, plain, (![Q_106]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_106), true, iext(Q_106, uri_rdfs_isDefinedBy, uri_rdfs_Resource), true)=true))). % 27.03/17.24 tff(c_10712, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdfs_Seq), true)=true))). % 27.03/17.24 tff(c_20862, plain, (![X_422, Y_423]: (ifeq(iext(uri_rdf_type, X_422, Y_423), true, icext(uri_rdfs_Class, Y_423), true)=true))). % 27.03/17.24 tff(c_9818, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_domain), true)=true))). % 27.03/17.24 tff(c_7366, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_object), true)=true))). % 27.03/17.24 tff(c_2801, plain, (![Q_106]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_106), true, iext(Q_106, uri_rdf_Bag, uri_rdfs_Container), true)=true))). % 27.03/17.24 tff(c_7744, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_value), true)=true))). % 27.03/17.24 tff(c_10912, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_first), true)=true))). % 27.03/17.24 tff(c_20693, plain, (![X_413, Y_414]: (ifeq(iext(uri_rdf_rest, X_413, Y_414), true, icext(uri_rdf_List, Y_414), true)=true))). % 27.03/17.24 tff(c_11151, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdfs_ContainerMembershipProperty), true)=true))). % 27.03/17.24 tff(c_4785, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdf_Alt), true)=true))). % 27.03/17.24 tff(c_4540, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_subject), true)=true))). % 27.03/17.24 tff(c_2781, plain, (![Q_106]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_106), true, iext(Q_106, uri_rdf_predicate, uri_rdfs_Resource), true)=true))). % 27.03/17.24 tff(c_10200, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_rest), true)=true))). % 27.03/17.24 tff(c_20054, plain, (![X_403, Y_404]: (ifeq(iext(uri_rdfs_subClassOf, X_403, Y_404), true, icext(uri_rdfs_Class, Y_404), true)=true))). % 27.03/17.24 tff(c_2800, plain, (![Q_106]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_106), true, iext(Q_106, uri_rdf_first, uri_rdfs_Resource), true)=true))). % 27.03/17.24 tff(c_10913, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_first), true)=true))). % 27.03/17.24 tff(c_9299, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdfs_Datatype), true)=true))). % 27.03/17.24 tff(c_19948, plain, (![X_396, Y_397]: (ifeq(iext(uri_rdf_predicate, X_396, Y_397), true, icext(uri_rdfs_Statement, X_396), true)=true))). % 27.03/17.24 tff(c_2765, plain, (![Q_106]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_106), true, iext(Q_106, uri_rdf_nil, uri_rdf_List), true)=true))). % 27.03/17.24 tff(c_7367, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_object), true)=true))). % 27.03/17.24 tff(c_19531, plain, (![X_390, Y_391]: (ifeq(iext(uri_rdfs_domain, X_390, Y_391), true, icext(uri_rdf_Property, X_390), true)=true))). % 27.03/17.24 tff(c_9817, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_domain), true)=true))). % 27.03/17.24 tff(c_2805, plain, (![Q_106]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_106), true, iext(Q_106, uri_rdfs_Datatype, uri_rdfs_Class), true)=true))). % 27.03/17.24 tff(c_7745, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_value), true)=true))). % 27.03/17.24 tff(c_10199, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_rest), true)=true))). % 27.03/17.24 tff(c_19054, plain, (![X_382, Y_383]: (ifeq(iext(uri_rdfs_subPropertyOf, X_382, Y_383), true, icext(uri_rdf_Property, X_382), true)=true))). % 27.03/17.25 tff(c_6133, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_range), true)=true))). % 27.03/17.25 tff(c_8517, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdf_Bag), true)=true))). % 27.03/17.25 tff(c_2807, plain, (![Q_106]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_106), true, iext(Q_106, uri_rdf_value, uri_rdf_Property), true)=true))). % 27.03/17.25 tff(c_9369, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_type), true)=true))). % 27.03/17.25 tff(c_18929, plain, (![X_374, Y_375]: (ifeq(iext(uri_rdfs_label, X_374, Y_375), true, icext(uri_rdfs_Literal, Y_375), true)=true))). % 27.03/17.25 tff(c_11339, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdfs_Container), true)=true))). % 27.03/17.25 tff(c_8196, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdfs_Literal), true)=true))). % 27.03/17.25 tff(c_2764, plain, (![Q_106]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_106), true, iext(Q_106, uri_rdf_value, uri_rdfs_Resource), true)=true))). % 27.03/17.25 tff(c_6007, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_isDefinedBy), true)=true))). % 27.03/17.25 tff(c_18487, plain, (![X_366, Y_367]: (ifeq(iext(uri_rdfs_range, X_366, Y_367), true, icext(uri_rdf_Property, X_366), true)=true))). % 27.03/17.25 tff(c_5699, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdfs_Class), true)=true))). % 27.03/17.25 tff(c_2766, plain, (![Q_106]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_106), true, iext(Q_106, uri_rdfs_subPropertyOf, uri_rdf_Property), true)=true))). % 27.03/17.25 tff(c_4671, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_subPropertyOf), true)=true))). % 27.03/17.25 tff(c_5947, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf__1), true)=true))). % 27.03/17.25 tff(c_18330, plain, (![X_358, Y_359]: (ifeq(iext(uri_rdf_first, X_358, Y_359), true, icext(uri_rdf_List, X_358), true)=true))). % 27.03/17.25 tff(c_2793, plain, (![Q_106]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_106), true, iext(Q_106, uri_rdfs_subClassOf, uri_rdfs_Class), true)=true))). % 27.03/17.25 tff(c_9882, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_subClassOf), true)=true))). % 27.03/17.25 tff(c_9881, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_subClassOf), true)=true))). % 27.03/17.25 tff(c_17889, plain, (![X_351, Y_352]: (ifeq(iext(uri_rdfs_subPropertyOf, X_351, Y_352), true, icext(uri_rdf_Property, Y_352), true)=true))). % 27.03/17.25 tff(c_4604, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf__3), true)=true))). % 27.03/17.25 tff(c_4987, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf__2), true)=true))). % 27.03/17.25 tff(c_2787, plain, (![Q_106]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_106), true, iext(Q_106, uri_rdf_subject, uri_rdfs_Resource), true)=true))). % 27.03/17.25 tff(c_5321, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdf_XMLLiteral), true)=true))). % 27.03/17.25 tff(c_6623, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdf_Property), true)=true))). % 27.03/17.25 tff(c_17723, plain, (![X_342, Y_343]: (ifeq(iext(uri_rdf_object, X_342, Y_343), true, icext(uri_rdfs_Statement, X_342), true)=true))). % 27.03/17.25 tff(c_9368, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_type), true)=true))). % 27.03/17.25 tff(c_2783, plain, (![Q_106]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_106), true, iext(Q_106, uri_rdfs_comment, uri_rdfs_Literal), true)=true))). % 27.03/17.25 tff(c_6804, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_member), true)=true))). % 27.03/17.25 tff(c_11880, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdfs_Resource), true)=true))). % 27.03/17.25 tff(c_17590, plain, (![X_334, Y_335]: (ifeq(iext(uri_rdf_rest, X_334, Y_335), true, icext(uri_rdf_List, X_334), true)=true))). % 27.03/17.25 tff(c_5053, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf__2), true)=true))). % 27.03/17.25 tff(c_4539, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_subject), true)=true))). % 27.03/17.25 tff(c_5946, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf__1), true)=true))). % 27.03/17.25 tff(c_2780, plain, (![Q_106]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_106), true, iext(Q_106, uri_rdf_subject, uri_rdf_Property), true)=true))). % 27.03/17.25 tff(c_5203, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_seeAlso), true)=true))). % 27.03/17.25 tff(c_4455, plain, (![C_19, X_138]: (ifeq(iext(uri_rdfs_domain, uri_rdf_type, C_19), true, icext(C_19, X_138), true)=true))). % 27.03/17.25 tff(c_16704, plain, (![X_322, Y_323]: (ifeq(iext(uri_rdfs_subClassOf, X_322, Y_323), true, icext(uri_rdfs_Class, X_322), true)=true))). % 27.03/17.25 tff(c_4454, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_29), true, icext(C_29, uri_rdfs_Resource), true)=true))). % 27.03/17.25 tff(c_2177, plain, (![C_96]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_96), true, icext(C_96, uri_rdfs_seeAlso), true)=true))). % 27.03/17.25 tff(c_1854, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_92), true, icext(C_92, uri_rdfs_isDefinedBy), true)=true))). % 27.03/17.25 tff(c_1893, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_92), true, icext(C_92, uri_rdf_rest), true)=true))). % 27.03/17.25 tff(c_1877, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_92), true, icext(C_92, uri_rdfs_member), true)=true))). % 27.03/17.25 tff(c_1839, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_92), true, icext(C_92, uri_rdf__3), true)=true))). % 27.03/17.25 tff(c_1871, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_92), true, icext(C_92, uri_rdf_XMLLiteral), true)=true))). % 27.03/17.25 tff(c_1862, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_92), true, icext(C_92, uri_rdf_predicate), true)=true))). % 27.03/17.25 tff(c_1876, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_92), true, icext(C_92, uri_rdfs_subClassOf), true)=true))). % 27.03/17.25 tff(c_1856, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_92), true, icext(C_92, uri_rdfs_label), true)=true))). % 27.03/17.25 tff(c_16290, plain, (![X_304, Y_305]: (ifeq(iext(uri_rdfs_comment, X_304, Y_305), true, icext(uri_rdfs_Literal, Y_305), true)=true))). % 27.03/17.25 tff(c_2206, plain, (![C_96]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_96), true, icext(C_96, uri_rdfs_Class), true)=true))). % 27.03/17.25 tff(c_1833, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_92), true, icext(C_92, uri_rdfs_isDefinedBy), true)=true))). % 27.03/17.25 tff(c_2213, plain, (![C_96]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_96), true, icext(C_96, uri_rdfs_Class), true)=true))). % 27.03/17.25 tff(c_1899, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_92), true, icext(C_92, uri_rdf_value), true)=true))). % 27.03/17.25 tff(c_1843, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_92), true, icext(C_92, uri_rdfs_subPropertyOf), true)=true))). % 27.03/17.25 tff(c_1873, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_92), true, icext(C_92, uri_rdf_type), true)=true))). % 27.03/17.25 tff(c_1884, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_92), true, icext(C_92, uri_rdf_Bag), true)=true))). % 27.03/17.25 tff(c_1897, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_92), true, icext(C_92, uri_rdfs_domain), true)=true))). % 27.03/17.25 tff(c_1870, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_92), true, icext(C_92, uri_rdfs_subClassOf), true)=true))). % 27.03/17.25 tff(c_1860, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_92), true, icext(C_92, uri_rdf_Alt), true)=true))). % 27.03/17.25 tff(c_1848, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_92), true, icext(C_92, uri_rdf__1), true)=true))). % 27.03/17.25 tff(c_15585, plain, (![X_283, Y_284]: (ifeq(iext(uri_rdfs_range, X_283, Y_284), true, icext(uri_rdfs_Class, Y_284), true)=true))). % 27.03/17.25 tff(c_2194, plain, (![C_96]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_96), true, icext(C_96, uri_rdfs_Literal), true)=true))). % 27.03/17.25 tff(c_1880, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_92), true, icext(C_92, uri_rdfs_Seq), true)=true))). % 27.03/17.25 tff(c_2199, plain, (![C_96]: (ifeq(iext(uri_rdfs_range, uri_rdfs_domain, C_96), true, icext(C_96, uri_rdfs_Class), true)=true))). % 27.03/17.25 tff(c_1868, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_92), true, icext(C_92, uri_rdf_type), true)=true))). % 27.03/17.25 tff(c_1841, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_92), true, icext(C_92, uri_rdf_value), true)=true))). % 27.03/17.25 tff(c_1885, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_92), true, icext(C_92, uri_rdfs_ContainerMembershipProperty), true)=true))). % 27.03/17.25 tff(c_1889, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_92), true, icext(C_92, uri_rdf_first), true)=true))). % 27.03/17.25 tff(c_1898, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_92), true, icext(C_92, uri_rdfs_subPropertyOf), true)=true))). % 27.03/17.25 tff(c_1867, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_92), true, icext(C_92, uri_rdf_subject), true)=true))). % 27.03/17.25 tff(c_1888, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_92), true, icext(C_92, uri_rdfs_Datatype), true)=true))). % 27.03/17.25 tff(c_1845, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_92), true, icext(C_92, uri_rdf__2), true)=true))). % 27.03/17.25 tff(c_15339, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_predicate, uri_rdf_predicate)=true)). % 27.03/17.25 tff(c_15186, plain, (ip(uri_rdf_predicate)=true)). % 27.03/17.25 tff(c_15129, plain, (iext(uri_rdf_type, uri_rdf_predicate, uri_rdf_Property)=true)). % 27.03/17.25 tff(c_15073, plain, (icext(uri_rdf_Property, uri_rdf_predicate)=true)). % 27.03/17.25 tff(c_1836, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_92), true, icext(C_92, uri_rdf_predicate), true)=true))). % 27.03/17.25 tff(c_2223, plain, (![C_96]: (ifeq(iext(uri_rdfs_range, uri_rdfs_range, C_96), true, icext(C_96, uri_rdf_Property), true)=true))). % 27.03/17.25 tff(c_1883, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_92), true, icext(C_92, uri_rdf_first), true)=true))). % 27.03/17.25 tff(c_2168, plain, (![C_96]: (ifeq(iext(uri_rdfs_range, uri_rdfs_domain, C_96), true, icext(C_96, uri_rdf_Property), true)=true))). % 27.03/17.25 tff(c_1846, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_92), true, icext(C_92, uri_rdf__1), true)=true))). % 27.03/17.25 tff(c_1849, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_92), true, icext(C_92, uri_rdfs_range), true)=true))). % 27.03/17.25 tff(c_13418, plain, (![X_33]: (ifeq(icext(uri_rdf_List, X_33), true, icext(uri_rdf_List, X_33), true)=true))). % 27.03/17.25 tff(c_14386, plain, (![X_255, Y_256]: (ifeq(iext(uri_rdfs_domain, X_255, Y_256), true, icext(uri_rdfs_Class, Y_256), true)=true))). % 27.03/17.25 tff(c_13625, plain, (![X_33]: (ifeq(icext(uri_rdfs_Statement, X_33), true, icext(uri_rdfs_Statement, X_33), true)=true))). % 27.03/17.25 tff(c_10714, plain, (![X_33]: (ifeq(icext(uri_rdfs_Seq, X_33), true, icext(uri_rdfs_Seq, X_33), true)=true))). % 27.03/17.25 tff(c_8519, plain, (![X_33]: (ifeq(icext(uri_rdf_Bag, X_33), true, icext(uri_rdf_Bag, X_33), true)=true))). % 27.03/17.25 tff(c_5700, plain, (![X_33]: (ifeq(icext(uri_rdfs_Class, X_33), true, icext(uri_rdfs_Class, X_33), true)=true))). % 27.03/17.25 tff(c_11153, plain, (![X_33]: (ifeq(icext(uri_rdfs_ContainerMembershipProperty, X_33), true, icext(uri_rdfs_ContainerMembershipProperty, X_33), true)=true))). % 27.03/17.25 tff(c_4787, plain, (![X_33]: (ifeq(icext(uri_rdf_Alt, X_33), true, icext(uri_rdf_Alt, X_33), true)=true))). % 27.03/17.25 tff(c_9301, plain, (![X_33]: (ifeq(icext(uri_rdfs_Datatype, X_33), true, icext(uri_rdfs_Datatype, X_33), true)=true))). % 27.03/17.25 tff(c_8197, plain, (![X_33]: (ifeq(icext(uri_rdfs_Literal, X_33), true, icext(uri_rdfs_Literal, X_33), true)=true))). % 27.03/17.25 tff(c_11340, plain, (![X_33]: (ifeq(icext(uri_rdfs_Container, X_33), true, icext(uri_rdfs_Container, X_33), true)=true))). % 27.03/17.25 tff(c_6624, plain, (![X_33]: (ifeq(icext(uri_rdf_Property, X_33), true, icext(uri_rdf_Property, X_33), true)=true))). % 27.03/17.25 tff(c_5323, plain, (![X_33]: (ifeq(icext(uri_rdf_XMLLiteral, X_33), true, icext(uri_rdf_XMLLiteral, X_33), true)=true))). % 27.03/17.25 tff(c_1866, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_92), true, icext(C_92, uri_rdfs_range), true)=true))). % 27.03/17.25 tff(c_14103, plain, (iext(uri_rdf_type, uri_rdfs_Resource, uri_rdfs_Class)=true)). % 27.03/17.25 tff(c_14038, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_label, uri_rdfs_label)=true)). % 27.03/17.25 tff(c_13973, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_comment, uri_rdfs_comment)=true)). % 27.03/17.25 tff(c_13875, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_member, uri_rdfs_member)=true)). % 27.03/17.25 tff(c_13799, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Resource, uri_rdfs_Resource)=true)). % 27.03/17.25 tff(c_13660, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Statement, uri_rdfs_Resource)=true)). % 27.03/17.25 tff(c_1835, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_92), true, icext(C_92, uri_rdf_object), true)=true))). % 27.03/17.25 tff(c_13569, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Statement, uri_rdfs_Statement)=true)). % 27.03/17.25 tff(c_13429, plain, (iext(uri_rdfs_subClassOf, uri_rdf_List, uri_rdfs_Resource)=true)). % 27.03/17.25 tff(c_13337, plain, (iext(uri_rdfs_subClassOf, uri_rdf_List, uri_rdf_List)=true)). % 27.03/17.25 tff(c_2210, plain, (![C_96]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_96), true, icext(C_96, uri_rdf_Property), true)=true))). % 27.03/17.25 tff(c_13288, plain, (iext(uri_rdf_type, uri_rdfs_Datatype, uri_rdfs_Class)=true)). % 27.03/17.25 tff(c_13215, plain, (iext(uri_rdf_type, uri_rdfs_Container, uri_rdfs_Class)=true)). % 27.03/17.25 tff(c_2178, plain, (![C_96]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_96), true, icext(C_96, uri_rdfs_ContainerMembershipProperty), true)=true))). % 27.03/17.25 tff(c_13165, plain, (iext(uri_rdf_type, uri_rdf_XMLLiteral, uri_rdfs_Class)=true)). % 27.03/17.25 tff(c_1834, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_92), true, icext(C_92, uri_rdf__2), true)=true))). % 27.03/17.25 tff(c_13088, plain, (iext(uri_rdf_type, uri_rdfs_Literal, uri_rdfs_Class)=true)). % 27.03/17.25 tff(c_13040, plain, (iext(uri_rdf_type, uri_rdf_Bag, uri_rdfs_Class)=true)). % 27.03/17.25 tff(c_12993, plain, (iext(uri_rdf_type, uri_rdf_Alt, uri_rdfs_Class)=true)). % 27.03/17.25 tff(c_12817, plain, (iext(uri_rdf_type, uri_rdfs_member, uri_rdf_Property)=true)). % 27.03/17.25 tff(c_12769, plain, (icext(uri_rdf_Property, uri_rdfs_member)=true)). % 27.03/17.25 tff(c_1852, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_92), true, icext(C_92, uri_rdfs_member), true)=true))). % 27.03/17.25 tff(c_12700, plain, (iext(uri_rdf_type, uri_rdfs_Seq, uri_rdfs_Class)=true)). % 27.03/17.25 tff(c_1869, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_92), true, icext(C_92, uri_rdf_subject), true)=true))). % 27.03/17.25 tff(c_12625, plain, (iext(uri_rdf_type, uri_rdfs_ContainerMembershipProperty, uri_rdfs_Class)=true)). % 27.03/17.25 tff(c_12577, plain, (iext(uri_rdf_type, uri_rdfs_Class, uri_rdfs_Class)=true)). % 27.03/17.25 tff(c_12530, plain, (iext(uri_rdf_type, uri_rdfs_Statement, uri_rdfs_Class)=true)). % 27.03/17.25 tff(c_1896, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_92), true, icext(C_92, uri_rdfs_seeAlso), true)=true))). % 27.03/17.25 tff(c_12463, plain, (ip(uri_rdfs_label)=true)). % 27.03/17.25 tff(c_12410, plain, (iext(uri_rdf_type, uri_rdfs_label, uri_rdf_Property)=true)). % 27.03/17.25 tff(c_1859, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_92), true, icext(C_92, uri_rdfs_comment), true)=true))). % 27.03/17.25 tff(c_12337, plain, (iext(uri_rdf_type, uri_rdf_List, uri_rdfs_Class)=true)). % 27.03/17.25 tff(c_12295, plain, (ip(uri_rdfs_comment)=true)). % 27.03/17.25 tff(c_2179, plain, (![C_96]: (ifeq(iext(uri_rdfs_range, uri_rdfs_range, C_96), true, icext(C_96, uri_rdfs_Literal), true)=true))). % 27.03/17.25 tff(c_12217, plain, (iext(uri_rdf_type, uri_rdfs_comment, uri_rdf_Property)=true)). % 27.03/17.25 tff(c_1500, plain, (![S_5, O_6]: (ifeq(iext(uri_rdfs_subPropertyOf, S_5, O_6), true, true, true)=true))). % 27.03/17.25 tff(c_11980, plain, (icext(uri_rdf_Property, uri_rdfs_comment)=true)). % 27.03/17.25 tff(c_1865, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_92), true, icext(C_92, uri_rdfs_comment), true)=true))). % 27.03/17.25 tff(c_11826, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, uri_rdfs_Resource)=true)). % 27.03/17.25 tff(c_11702, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Literal, uri_rdfs_Resource)=true)). % 27.03/17.25 tff(c_11542, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Class, uri_rdfs_Resource)=true)). % 27.03/17.25 tff(c_944, plain, (![S_5, O_6]: (ifeq(iext(uri_rdfs_domain, S_5, O_6), true, true, true)=true))). % 27.03/17.25 tff(c_11284, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Container, uri_rdfs_Container)=true)). % 27.03/17.25 tff(c_11163, plain, (iext(uri_rdfs_subClassOf, uri_rdf_XMLLiteral, uri_rdfs_Resource)=true)). % 27.03/17.25 tff(c_11097, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, uri_rdfs_ContainerMembershipProperty)=true)). % 27.03/17.25 tff(c_10993, plain, (ic(uri_rdfs_Statement)=true)). % 27.03/17.25 tff(c_10943, plain, (icext(uri_rdfs_Class, uri_rdfs_Statement)=true)). % 27.03/17.25 tff(c_2189, plain, (![C_96]: (ifeq(iext(uri_rdfs_range, uri_rdfs_domain, C_96), true, icext(C_96, uri_rdfs_Statement), true)=true))). % 27.03/17.25 tff(c_10855, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_first, uri_rdf_first)=true)). % 27.03/17.25 tff(c_3181, plain, (![S_5, O_6]: (ifeq(iext(uri_rdf_object, S_5, O_6), true, true, true)=true))). % 27.03/17.25 tff(c_10657, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Seq, uri_rdfs_Seq)=true)). % 27.03/17.25 tff(c_10549, plain, (icext(uri_rdf_Property, uri_rdfs_range)=true)). % 27.03/17.25 tff(c_10495, plain, (iext(uri_rdf_type, uri_rdfs_range, uri_rdf_Property)=true)). % 27.03/17.25 tff(c_10439, plain, (iext(uri_rdf_type, uri_rdfs_isDefinedBy, uri_rdf_Property)=true)). % 27.03/17.25 tff(c_10146, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_rest, uri_rdf_rest)=true)). % 27.03/17.25 tff(c_2190, plain, (![C_96]: (ifeq(iext(uri_rdfs_range, uri_rdfs_range, C_96), true, icext(C_96, uri_rdfs_Class), true)=true))). % 27.03/17.25 tff(c_10016, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Seq, uri_rdfs_Resource)=true)). % 27.03/17.26 tff(c_9913, plain, (icext(uri_rdf_Property, uri_rdfs_label)=true)). % 27.03/17.26 tff(c_1864, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_92), true, icext(C_92, uri_rdfs_label), true)=true))). % 27.03/17.26 tff(c_9828, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, uri_rdfs_subClassOf)=true)). % 27.03/17.26 tff(c_9764, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, uri_rdfs_domain)=true)). % 27.03/17.26 tff(c_2218, plain, (![C_96]: (ifeq(iext(uri_rdfs_range, uri_rdfs_range, C_96), true, icext(C_96, uri_rdf_List), true)=true))). % 27.03/17.26 tff(c_9637, plain, (icext(uri_rdf_Property, uri_rdfs_subPropertyOf)=true)). % 27.03/17.26 tff(c_9583, plain, (iext(uri_rdf_type, uri_rdfs_subPropertyOf, uri_rdf_Property)=true)). % 27.03/17.26 tff(c_2196, plain, (![C_96]: (ifeq(iext(uri_rdfs_range, uri_rdfs_domain, C_96), true, icext(C_96, uri_rdf_List), true)=true))). % 27.03/17.26 tff(c_9502, plain, (iext(uri_rdf_type, uri_rdfs_domain, uri_rdf_Property)=true)). % 27.03/17.26 tff(c_9399, plain, (icext(uri_rdf_Property, uri_rdfs_isDefinedBy)=true)). % 27.03/17.26 tff(c_1875, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_92), true, icext(C_92, uri_rdfs_isDefinedBy), true)=true))). % 27.03/17.26 tff(c_9311, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_type, uri_rdf_type)=true)). % 27.03/17.26 tff(c_9245, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, uri_rdfs_Datatype)=true)). % 27.03/17.26 tff(c_1465, plain, (![S_5, O_6]: (ifeq(iext(uri_rdfs_subClassOf, S_5, O_6), true, true, true)=true))). % 27.03/17.26 tff(c_8961, plain, (ic(uri_rdf_List)=true)). % 27.03/17.26 tff(c_8907, plain, (icext(uri_rdfs_Class, uri_rdf_List)=true)). % 27.03/17.26 tff(c_2167, plain, (![C_96]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_96), true, icext(C_96, uri_rdf_List), true)=true))). % 27.03/17.26 tff(c_8821, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Container, uri_rdfs_Resource)=true)). % 27.03/17.26 tff(c_8464, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Bag, uri_rdf_Bag)=true)). % 27.03/17.26 tff(c_8309, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf__1, uri_rdfs_member)=true)). % 27.03/17.26 tff(c_8142, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Literal, uri_rdfs_Literal)=true)). % 27.03/17.26 tff(c_7687, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_value, uri_rdf_value)=true)). % 27.03/17.26 tff(c_2171, plain, (![C_96]: (ifeq(iext(uri_rdfs_range, uri_rdfs_range, C_96), true, icext(C_96, uri_rdfs_Resource), true)=true))). % 27.03/17.26 tff(c_7571, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, uri_rdfs_Resource)=true)). % 27.03/17.26 tff(c_7460, plain, (iext(uri_rdf_type, uri_rdfs_seeAlso, uri_rdf_Property)=true)). % 27.03/17.26 tff(c_1874, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_92), true, icext(C_92, uri_rdf_rest), true)=true))). % 27.03/17.26 tff(c_7313, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_object, uri_rdf_object)=true)). % 27.03/17.26 tff(c_801, plain, (![S_5, O_6]: (ifeq(iext(uri_rdfs_range, S_5, O_6), true, true, true)=true))). % 27.03/17.26 tff(c_2203, plain, (![C_96]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_96), true, icext(C_96, uri_rdfs_Datatype), true)=true))). % 27.03/17.26 tff(c_7095, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Alt, uri_rdfs_Resource)=true)). % 27.03/17.26 tff(c_2166, plain, (![C_96]: (ifeq(iext(uri_rdfs_range, uri_rdfs_domain, C_96), true, icext(C_96, uri_rdfs_Resource), true)=true))). % 27.03/17.26 tff(c_6865, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Bag, uri_rdfs_Resource)=true)). % 27.03/17.26 tff(c_6750, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf__3, uri_rdfs_member)=true)). % 27.03/17.26 tff(c_1837, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_92), true, icext(C_92, uri_rdf__3), true)=true))). % 27.03/17.26 tff(c_6572, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Property, uri_rdf_Property)=true)). % 27.03/17.26 tff(c_6439, plain, (icext(uri_rdf_Property, uri_rdfs_seeAlso)=true)). % 27.03/17.26 tff(c_1895, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_92), true, icext(C_92, uri_rdfs_seeAlso), true)=true))). % 27.03/17.26 tff(c_6268, plain, (icext(uri_rdf_Property, uri_rdfs_domain)=true)). % 27.03/17.26 tff(c_1881, plain, (![C_92]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_92), true, icext(C_92, uri_rdfs_domain), true)=true))). % 27.03/17.26 tff(c_6083, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_range, uri_rdfs_range)=true)). % 27.03/17.26 tff(c_5957, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_isDefinedBy, uri_rdfs_isDefinedBy)=true)). % 27.03/17.26 tff(c_5893, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf__1, uri_rdf__1)=true)). % 27.03/17.26 tff(c_5799, plain, (icext(uri_rdf_Property, uri_rdfs_subClassOf)=true)). % 27.03/17.26 tff(c_5745, plain, (iext(uri_rdf_type, uri_rdfs_subClassOf, uri_rdf_Property)=true)). % 27.03/17.26 tff(c_5620, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Class, uri_rdfs_Class)=true)). % 27.03/17.26 tff(c_5533, plain, (icext(uri_rdfs_Class, uri_rdfs_Resource)=true)). % 27.03/17.26 tff(c_2180, plain, (![C_96]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_96), true, icext(C_96, uri_rdf_Property), true)=true))). % 27.03/17.26 tff(c_5440, plain, (ic(uri_rdfs_Resource)=true)). % 27.03/17.26 tff(c_5379, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Property, uri_rdfs_Resource)=true)). % 27.03/17.26 tff(c_2209, plain, (![C_96]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_96), true, icext(C_96, uri_rdfs_Container), true)=true))). % 27.03/17.26 tff(c_5267, plain, (iext(uri_rdfs_subClassOf, uri_rdf_XMLLiteral, uri_rdf_XMLLiteral)=true)). % 27.03/17.26 tff(c_5152, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_seeAlso, uri_rdfs_seeAlso)=true)). % 27.03/17.26 tff(c_1541, plain, (![X_89]: (ifeq(icext(uri_rdf_Bag, X_89), true, icext(uri_rdfs_Container, X_89), true)=true))). % 27.03/17.26 tff(c_1538, plain, (![X_89]: (ifeq(icext(uri_rdf_Alt, X_89), true, icext(uri_rdfs_Container, X_89), true)=true))). % 27.03/17.26 tff(c_5062, plain, (ip(uri_rdfs_member)=true)). % 27.03/17.26 tff(c_5002, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf__2, uri_rdfs_member)=true)). % 27.03/17.26 tff(c_4895, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf__2, uri_rdf__2)=true)). % 27.03/17.26 tff(c_1543, plain, (![X_89]: (ifeq(icext(uri_rdfs_Datatype, X_89), true, icext(uri_rdfs_Class, X_89), true)=true))). % 27.03/17.26 tff(c_3016, plain, (![S_5, O_6]: (ifeq(iext(uri_rdf_rest, S_5, O_6), true, true, true)=true))). % 27.03/17.26 tff(c_1542, plain, (![X_89]: (ifeq(icext(uri_rdfs_ContainerMembershipProperty, X_89), true, icext(uri_rdf_Property, X_89), true)=true))). % 27.03/17.26 tff(c_4735, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Alt, uri_rdf_Alt)=true)). % 27.03/17.26 tff(c_4621, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf)=true)). % 27.03/17.26 tff(c_1539, plain, (![X_89]: (ifeq(icext(uri_rdf_XMLLiteral, X_89), true, icext(uri_rdfs_Literal, X_89), true)=true))). % 27.03/17.26 tff(c_4550, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf__3, uri_rdf__3)=true)). % 27.03/17.26 tff(c_4489, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_subject, uri_rdf_subject)=true)). % 27.03/17.26 tff(c_1540, plain, (![X_89]: (ifeq(icext(uri_rdfs_Seq, X_89), true, icext(uri_rdfs_Container, X_89), true)=true))). % 27.03/17.26 tff(c_4413, plain, (![X_137]: (iext(uri_rdf_type, X_137, uri_rdfs_Resource)=true))). % 27.03/17.26 tff(c_2197, plain, (![X_97, Y_98]: (ifeq(iext(uri_rdfs_isDefinedBy, X_97, Y_98), true, true, true)=true))). % 27.03/17.26 tff(c_2200, plain, (![X_97, Y_98]: (ifeq(iext(uri_rdfs_member, X_97, Y_98), true, true, true)=true))). % 27.03/17.26 tff(c_1863, plain, (![X_93, Y_94]: (ifeq(iext(uri_rdfs_label, X_93, Y_94), true, true, true)=true))). % 27.03/17.26 tff(c_1858, plain, (![X_93, Y_94]: (ifeq(iext(uri_rdfs_comment, X_93, Y_94), true, true, true)=true))). % 27.03/17.26 tff(c_1894, plain, (![X_93, Y_94]: (ifeq(iext(uri_rdfs_seeAlso, X_93, Y_94), true, true, true)=true))). % 27.03/17.26 tff(c_1872, plain, (![X_93, Y_94]: (ifeq(iext(uri_rdf_type, X_93, Y_94), true, true, true)=true))). % 27.03/17.26 tff(c_2170, plain, (![X_97, Y_98]: (ifeq(iext(uri_rdf__1, X_97, Y_98), true, true, true)=true))). % 27.03/17.26 tff(c_2163, plain, (![X_97, Y_98]: (ifeq(iext(uri_rdf__3, X_97, Y_98), true, true, true)=true))). % 27.03/17.26 tff(c_1840, plain, (![X_93, Y_94]: (ifeq(iext(uri_rdf_value, X_93, Y_94), true, true, true)=true))). % 27.03/17.26 tff(c_4234, plain, (icext(uri_rdfs_Class, uri_rdfs_Seq)=true)). % 27.03/17.26 tff(c_4189, plain, (icext(uri_rdfs_Class, uri_rdfs_Datatype)=true)). % 27.03/17.26 tff(c_1844, plain, (![X_93, Y_94]: (ifeq(iext(uri_rdf__2, X_93, Y_94), true, true, true)=true))). % 27.03/17.26 tff(c_4133, plain, (icext(uri_rdfs_Class, uri_rdfs_ContainerMembershipProperty)=true)). % 27.03/17.26 tff(c_4087, plain, (icext(uri_rdfs_Class, uri_rdf_Bag)=true)). % 27.03/17.26 tff(c_2184, plain, (![X_97, Y_98]: (ifeq(iext(uri_rdf_predicate, X_97, Y_98), true, true, true)=true))). % 27.03/17.26 tff(c_4030, plain, (icext(uri_rdfs_Class, uri_rdf_XMLLiteral)=true)). % 27.03/17.26 tff(c_3986, plain, (icext(uri_rdfs_Class, uri_rdf_Alt)=true)). % 27.03/17.26 tff(c_3932, plain, (icext(uri_rdfs_Class, uri_rdfs_Class)=true)). % 27.03/17.26 tff(c_2207, plain, (![X_97, Y_98]: (ifeq(iext(uri_rdf_first, X_97, Y_98), true, true, true)=true))). % 27.03/17.26 tff(c_3884, plain, (icext(uri_rdfs_Class, uri_rdfs_Literal)=true)). % 27.03/17.26 tff(c_3828, plain, (icext(uri_rdfs_Class, uri_rdfs_Container)=true)). % 27.03/17.26 tff(c_2191, plain, (![X_97, Y_98]: (ifeq(iext(uri_rdf_subject, X_97, Y_98), true, true, true)=true))). % 27.03/17.26 tff(c_3783, plain, (icext(uri_rdf_Property, uri_rdf_type)=true)). % 27.03/17.26 tff(c_3741, plain, (icext(uri_rdfs_ContainerMembershipProperty, uri_rdf__1)=true)). % 27.03/17.26 tff(c_3694, plain, (icext(uri_rdfs_Class, uri_rdf_Property)=true)). % 27.03/17.26 tff(c_3646, plain, (icext(uri_rdf_Property, uri_rdf__2)=true)). % 27.03/17.26 tff(c_3609, plain, (icext(uri_rdf_Property, uri_rdf__3)=true)). % 27.03/17.26 tff(c_3536, plain, (icext(uri_rdfs_Datatype, uri_rdf_XMLLiteral)=true)). % 27.03/17.26 tff(c_3526, plain, (icext(uri_rdfs_ContainerMembershipProperty, uri_rdf__2)=true)). % 27.03/17.26 tff(c_3487, plain, (icext(uri_rdf_Property, uri_rdf_value)=true)). % 27.03/17.26 tff(c_3443, plain, (icext(uri_rdf_Property, uri_rdf_object)=true)). % 27.03/17.26 tff(c_3402, plain, (icext(uri_rdf_Property, uri_rdf_rest)=true)). % 27.03/17.26 tff(c_3333, plain, (icext(uri_rdf_Property, uri_rdf__1)=true)). % 27.03/17.26 tff(c_3323, plain, (icext(uri_rdf_Property, uri_rdf_first)=true)). % 27.03/17.26 tff(c_3277, plain, (icext(uri_rdf_Property, uri_rdf_subject)=true)). % 27.03/17.26 tff(c_3236, plain, (icext(uri_rdf_List, uri_rdf_nil)=true)). % 27.03/17.26 tff(c_3196, plain, (icext(uri_rdfs_ContainerMembershipProperty, uri_rdf__3)=true)). % 27.03/17.26 tff(c_3154, plain, (ip(uri_rdf_object)=true)). % 27.03/17.26 tff(c_3116, plain, (ip(uri_rdf__3)=true)). % 27.03/17.26 tff(c_3073, plain, (ip(uri_rdf_subject)=true)). % 27.03/17.26 tff(c_2992, plain, (ic(uri_rdfs_Seq)=true)). % 27.03/17.26 tff(c_2982, plain, (ip(uri_rdf_rest)=true)). % 27.03/17.26 tff(c_2940, plain, (ip(uri_rdf_first)=true)). % 27.03/17.26 tff(c_2901, plain, (ic(uri_rdf_XMLLiteral)=true)). % 27.03/17.26 tff(c_2866, plain, (ic(uri_rdf_Property)=true)). % 27.03/17.26 tff(c_2819, plain, (ic(uri_rdf_Alt)=true)). % 27.03/17.26 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))). % 27.03/17.26 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))). % 27.03/17.26 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))). % 27.03/17.26 tff(c_2262, plain, (ic(uri_rdfs_Literal)=true)). % 27.03/17.26 tff(c_1905, plain, (ip(uri_rdf_value)=true)). % 27.03/17.26 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))). % 27.03/17.26 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))). % 27.03/17.26 tff(c_1553, plain, (ip(uri_rdfs_seeAlso)=true)). % 27.03/17.26 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))). % 27.03/17.26 tff(c_1476, plain, (ip(uri_rdfs_subPropertyOf)=true)). % 27.03/17.26 tff(c_182, plain, (tuple(iext(uri_rdfs_subClassOf, uri_xsd_integer, uri_xsd_decimal), iext(uri_owl_disjointWith, uri_xsd_decimal, uri_xsd_string))!=tuple(true, true))). % 27.03/17.26 tff(c_1441, plain, (ip(uri_rdfs_subClassOf)=true)). % 27.03/17.26 tff(c_1402, plain, (ip(uri_rdf__2)=true)). % 27.03/17.26 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))). % 27.03/17.26 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))). % 27.03/17.26 tff(c_1295, plain, (ip(uri_rdf__1)=true)). % 27.03/17.26 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))). % 27.03/17.26 tff(c_1195, plain, (ic(uri_rdfs_ContainerMembershipProperty)=true)). % 27.03/17.26 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))). % 27.03/17.26 tff(c_1160, plain, (ic(uri_rdf_Bag)=true)). % 27.03/17.26 tff(c_170, plain, (![P_51]: (ifeq(ip(P_51), true, iext(uri_rdfs_subPropertyOf, P_51, P_51), true)=true))). % 27.03/17.26 tff(c_1105, plain, (ic(uri_rdfs_Class)=true)). % 27.03/17.26 tff(c_156, plain, (![C_39]: (ifeq(ic(C_39), true, iext(uri_rdfs_subClassOf, C_39, C_39), true)=true))). % 27.03/17.26 tff(c_28, plain, (![P_9]: (ifeq(ip(P_9), true, iext(uri_rdf_type, P_9, uri_rdf_Property), true)=true))). % 27.03/17.26 tff(c_991, plain, (ic(uri_rdfs_Datatype)=true)). % 27.03/17.26 tff(c_152, plain, (![C_37, D_38]: (ifeq(iext(uri_rdfs_subClassOf, C_37, D_38), true, ic(C_37), true)=true))). % 27.03/17.26 tff(c_926, plain, (ip(uri_rdfs_domain)=true)). % 27.03/17.26 tff(c_162, plain, (![P_43, Q_44]: (ifeq(iext(uri_rdfs_subPropertyOf, P_43, Q_44), true, ip(Q_44), true)=true))). % 27.03/17.26 tff(c_861, plain, (ip(uri_rdf_type)=true)). % 27.03/17.26 tff(c_30, plain, (![P_10]: (ifeq(iext(uri_rdf_type, P_10, uri_rdf_Property), true, ip(P_10), true)=true))). % 27.03/17.26 tff(c_789, plain, (ip(uri_rdfs_range)=true)). % 27.03/17.26 tff(c_4, plain, (![P_4, S_5, O_6]: (ifeq(iext(P_4, S_5, O_6), true, ip(P_4), true)=true))). % 27.03/17.26 tff(c_564, plain, (ic(uri_rdfs_Container)=true)). % 27.03/17.26 tff(c_150, plain, (![C_35, D_36]: (ifeq(iext(uri_rdfs_subClassOf, C_35, D_36), true, ic(D_36), true)=true))). % 27.03/17.26 tff(c_519, plain, (ip(uri_rdfs_isDefinedBy)=true)). % 27.03/17.26 tff(c_164, plain, (![P_45, Q_46]: (ifeq(iext(uri_rdfs_subPropertyOf, P_45, Q_46), true, ip(P_45), true)=true))). % 27.03/17.26 tff(c_58, plain, (![C_15]: (ifeq(ic(C_15), true, iext(uri_rdfs_subClassOf, C_15, uri_rdfs_Resource), true)=true))). % 27.03/17.26 tff(c_122, plain, (![X_26]: (ifeq(icext(uri_rdfs_Literal, X_26), true, lv(X_26), true)=true))). % 27.03/17.26 tff(c_124, plain, (![X_27]: (ifeq(lv(X_27), true, icext(uri_rdfs_Literal, X_27), true)=true))). % 27.03/17.26 tff(c_116, plain, (![X_23]: (ifeq(icext(uri_rdfs_Class, X_23), true, ic(X_23), true)=true))). % 27.03/17.26 tff(c_114, plain, (![X_22]: (ifeq(ic(X_22), true, icext(uri_rdfs_Class, X_22), true)=true))). % 27.03/17.26 tff(c_452, plain, (![X_60]: (icext(uri_rdfs_Resource, X_60)=true))). % 27.03/17.26 tff(c_187, plain, (![X_8]: (ifeq(lv(X_8), true, true, true)=true))). % 27.03/17.26 tff(c_2, plain, (![A_1, B_2, C_3]: (ifeq(A_1, A_1, B_2, C_3)=B_2))). % 27.03/17.26 tff(c_20, plain, (iext(uri_rdf_type, uri_rdf__3, uri_rdf_Property)=true)). % 27.03/17.26 tff(c_40, plain, (iext(uri_rdfs_domain, uri_rdfs_isDefinedBy, uri_rdfs_Resource)=true)). % 27.03/17.26 tff(c_88, plain, (iext(uri_rdfs_range, uri_rdf__2, uri_rdfs_Resource)=true)). % 27.03/17.26 tff(c_134, plain, (iext(uri_rdfs_domain, uri_rdf_object, uri_rdfs_Statement)=true)). % 27.03/17.26 tff(c_138, plain, (iext(uri_rdfs_domain, uri_rdf_predicate, uri_rdfs_Statement)=true)). % 27.03/17.26 tff(c_90, plain, (iext(uri_rdfs_range, uri_rdf__3, uri_rdfs_Resource)=true)). % 27.03/17.26 tff(c_84, plain, (iext(uri_rdfs_domain, uri_rdf__3, uri_rdfs_Resource)=true)). % 27.03/17.26 tff(c_178, plain, (iext(uri_rdfs_domain, uri_rdf_value, uri_rdfs_Resource)=true)). % 27.03/17.26 tff(c_12, plain, (iext(uri_rdf_type, uri_rdf_nil, uri_rdf_List)=true)). % 27.03/17.26 tff(c_160, plain, (iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, uri_rdf_Property)=true)). % 27.03/17.26 tff(c_82, plain, (iext(uri_rdfs_domain, uri_rdf__2, uri_rdfs_Resource)=true)). % 27.03/17.26 tff(c_86, plain, (iext(uri_rdfs_range, uri_rdf__1, uri_rdfs_Resource)=true)). % 27.03/17.26 tff(c_80, plain, (iext(uri_rdfs_domain, uri_rdf__1, uri_rdfs_Resource)=true)). % 27.03/17.26 tff(c_132, plain, (iext(uri_rdfs_range, uri_rdfs_range, uri_rdfs_Class)=true)). % 27.03/17.26 tff(c_92, plain, (iext(uri_rdf_type, uri_rdf__1, uri_rdfs_ContainerMembershipProperty)=true)). % 27.03/17.26 tff(c_76, plain, (iext(uri_rdfs_domain, uri_rdfs_member, uri_rdfs_Resource)=true)). % 27.03/17.26 tff(c_14, plain, (iext(uri_rdf_type, uri_rdf_rest, uri_rdf_Property)=true)). % 27.03/17.26 tff(c_44, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_isDefinedBy, uri_rdfs_seeAlso)=true)). % 27.03/17.26 tff(c_94, plain, (iext(uri_rdf_type, uri_rdf__2, uri_rdfs_ContainerMembershipProperty)=true)). % 27.03/17.26 tff(c_48, plain, (iext(uri_rdfs_range, uri_rdfs_label, uri_rdfs_Literal)=true)). % 27.03/17.26 tff(c_22, plain, (iext(uri_rdf_type, uri_rdf_object, uri_rdf_Property)=true)). % 27.03/17.26 tff(c_36, plain, (iext(uri_rdfs_domain, uri_rdfs_comment, uri_rdfs_Resource)=true)). % 27.03/17.26 tff(c_68, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Alt, uri_rdfs_Container)=true)). % 27.03/17.26 tff(c_26, plain, (iext(uri_rdf_type, uri_rdf_subject, uri_rdf_Property)=true)). % 27.03/17.26 tff(c_140, plain, (iext(uri_rdfs_range, uri_rdf_predicate, uri_rdfs_Resource)=true)). % 27.03/17.26 tff(c_46, plain, (iext(uri_rdfs_domain, uri_rdfs_label, uri_rdfs_Resource)=true)). % 27.03/17.26 tff(c_38, plain, (iext(uri_rdfs_range, uri_rdfs_comment, uri_rdfs_Literal)=true)). % 27.03/17.26 tff(c_128, plain, (iext(uri_rdfs_domain, uri_rdfs_range, uri_rdf_Property)=true)). % 27.03/17.26 tff(c_142, plain, (iext(uri_rdfs_domain, uri_rdf_subject, uri_rdfs_Statement)=true)). % 27.03/17.26 tff(c_176, plain, (iext(uri_rdfs_range, uri_rdf_type, uri_rdfs_Class)=true)). % 27.03/17.26 tff(c_144, plain, (iext(uri_rdfs_range, uri_rdf_subject, uri_rdfs_Resource)=true)). % 27.03/17.26 tff(c_154, plain, (iext(uri_rdfs_range, uri_rdfs_subClassOf, uri_rdfs_Class)=true)). % 27.03/17.26 tff(c_100, plain, (iext(uri_rdfs_subClassOf, uri_rdf_XMLLiteral, uri_rdfs_Literal)=true)). % 27.03/17.26 tff(c_174, plain, (iext(uri_rdfs_domain, uri_rdf_type, uri_rdfs_Resource)=true)). % 27.03/17.26 tff(c_64, plain, (iext(uri_rdfs_domain, uri_rdf_rest, uri_rdf_List)=true)). % 27.03/17.26 tff(c_42, plain, (iext(uri_rdfs_range, uri_rdfs_isDefinedBy, uri_rdfs_Resource)=true)). % 27.03/17.26 tff(c_146, plain, (iext(uri_rdfs_domain, uri_rdfs_subClassOf, uri_rdfs_Class)=true)). % 27.03/17.26 tff(c_78, plain, (iext(uri_rdfs_range, uri_rdfs_member, uri_rdfs_Resource)=true)). % 27.03/17.26 tff(c_34, plain, (iext(uri_rdf_type, uri_rdf_type, uri_rdf_Property)=true)). % 27.03/17.26 tff(c_102, plain, (iext(uri_rdf_type, uri_rdf_XMLLiteral, uri_rdfs_Datatype)=true)). % 27.03/17.27 tff(c_98, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Seq, uri_rdfs_Container)=true)). % 27.03/17.27 tff(c_108, plain, (iext(uri_rdfs_domain, uri_rdfs_domain, uri_rdf_Property)=true)). % 27.03/17.27 tff(c_126, plain, (iext(uri_rdf_type, uri_rdf_Property, uri_rdfs_Class)=true)). % 27.03/17.27 tff(c_62, plain, (iext(uri_rdfs_range, uri_rdf_first, uri_rdfs_Resource)=true)). % 27.03/17.27 tff(c_70, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Bag, uri_rdfs_Container)=true)). % 27.03/17.27 tff(c_74, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, uri_rdf_Property)=true)). % 27.03/17.27 tff(c_18, plain, (iext(uri_rdf_type, uri_rdf__2, uri_rdf_Property)=true)). % 27.03/17.27 tff(c_16, plain, (iext(uri_rdf_type, uri_rdf__1, uri_rdf_Property)=true)). % 27.03/17.27 tff(c_106, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, uri_rdfs_Class)=true)). % 27.03/17.27 tff(c_60, plain, (iext(uri_rdfs_domain, uri_rdf_first, uri_rdf_List)=true)). % 27.03/17.27 tff(c_24, plain, (iext(uri_rdf_type, uri_rdf_value, uri_rdf_Property)=true)). % 27.03/17.27 tff(c_10, plain, (iext(uri_rdf_type, uri_rdf_first, uri_rdf_Property)=true)). % 27.03/17.27 tff(c_96, plain, (iext(uri_rdf_type, uri_rdf__3, uri_rdfs_ContainerMembershipProperty)=true)). % 27.03/17.27 tff(c_66, plain, (iext(uri_rdfs_range, uri_rdf_rest, uri_rdf_List)=true)). % 27.03/17.27 tff(c_50, plain, (iext(uri_rdfs_domain, uri_rdfs_seeAlso, uri_rdfs_Resource)=true)). % 27.03/17.27 tff(c_52, plain, (iext(uri_rdfs_range, uri_rdfs_seeAlso, uri_rdfs_Resource)=true)). % 27.03/17.27 tff(c_112, plain, (iext(uri_rdfs_range, uri_rdfs_domain, uri_rdfs_Class)=true)). % 27.03/17.27 tff(c_168, plain, (iext(uri_rdfs_range, uri_rdfs_subPropertyOf, uri_rdf_Property)=true)). % 27.03/17.27 tff(c_180, plain, (iext(uri_rdfs_range, uri_rdf_value, uri_rdfs_Resource)=true)). % 27.03/17.27 tff(c_6, plain, (![X_7]: (ir(X_7)=true))). % 27.03/17.27 % SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 27.03/17.27 %------------------------------------------------------------------------------