%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : SWB008-10 : TPTP v9.0.0. Released v7.3.0. % Transfm : none % Format : tptp:raw % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % Computer : n023.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Wed Apr 9 09:15:47 PM UTC 2025 % Result : Satisfiable 29.70s 18.61s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : SWB008-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/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % 0.13/0.34 % Computer : n023.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 00:53:54 EDT 2025 % 0.13/0.34 % CPUTime : % 29.70/18.60 % 29.70/18.61 % SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 29.70/18.61 % 29.70/18.61 % SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 29.70/18.62 %$ ifeq > iext > icext > #nlpp > lv > literal_plain > ir > ip > ic > uri_rdfs_subPropertyOf > uri_rdfs_subClassOf > uri_rdfs_seeAlso > uri_rdfs_range > uri_rdfs_member > uri_rdfs_label > uri_rdfs_isDefinedBy > uri_rdfs_domain > uri_rdfs_comment > uri_rdfs_Statement > uri_rdfs_Seq > uri_rdfs_Resource > uri_rdfs_Literal > uri_rdfs_Datatype > uri_rdfs_ContainerMembershipProperty > uri_rdfs_Container > uri_rdfs_Class > uri_rdf_value > uri_rdf_type > uri_rdf_subject > uri_rdf_rest > uri_rdf_predicate > uri_rdf_object > uri_rdf_nil > uri_rdf_first > uri_rdf__3 > uri_rdf__2 > uri_rdf__1 > uri_rdf_XMLLiteral > uri_rdf_Property > uri_rdf_List > uri_rdf_Bag > uri_rdf_Alt > uri_owl_sameAs > uri_owl_InverseFunctionalProperty > uri_owl_DatatypeProperty > uri_foaf_mbox_sha1sum > uri_ex_robert > uri_ex_bob > true > dat_str_xyz % 29.70/18.62 % 29.70/18.62 %Foreground sorts: % 29.70/18.62 % 29.70/18.62 % 29.70/18.62 %Background operators: % 29.70/18.62 % 29.70/18.62 % 29.70/18.62 %Foreground operators: % 29.70/18.62 tff(uri_owl_InverseFunctionalProperty, type, uri_owl_InverseFunctionalProperty: $i). % 29.70/18.62 tff(uri_rdfs_Datatype, type, uri_rdfs_Datatype: $i). % 29.70/18.62 tff(uri_rdfs_ContainerMembershipProperty, type, uri_rdfs_ContainerMembershipProperty: $i). % 29.70/18.62 tff(uri_rdfs_Resource, type, uri_rdfs_Resource: $i). % 29.70/18.62 tff(uri_rdf_Property, type, uri_rdf_Property: $i). % 29.70/18.62 tff(uri_rdf_subject, type, uri_rdf_subject: $i). % 29.70/18.62 tff(uri_rdf_type, type, uri_rdf_type: $i). % 29.70/18.62 tff(uri_rdfs_subPropertyOf, type, uri_rdfs_subPropertyOf: $i). % 29.70/18.62 tff(uri_rdfs_seeAlso, type, uri_rdfs_seeAlso: $i). % 29.70/18.62 tff(icext, type, icext: ($i * $i) > $i). % 29.70/18.62 tff(uri_rdfs_range, type, uri_rdfs_range: $i). % 29.70/18.62 tff(uri_rdf_XMLLiteral, type, uri_rdf_XMLLiteral: $i). % 29.70/18.62 tff(uri_rdf_List, type, uri_rdf_List: $i). % 29.70/18.62 tff(uri_rdf_first, type, uri_rdf_first: $i). % 29.70/18.62 tff(uri_rdf_predicate, type, uri_rdf_predicate: $i). % 29.70/18.62 tff(ir, type, ir: $i > $i). % 29.70/18.62 tff(lv, type, lv: $i > $i). % 29.70/18.62 tff(dat_str_xyz, type, dat_str_xyz: $i). % 29.70/18.62 tff(uri_ex_bob, type, uri_ex_bob: $i). % 29.70/18.62 tff(uri_rdf__3, type, uri_rdf__3: $i). % 29.70/18.62 tff(uri_rdf_value, type, uri_rdf_value: $i). % 29.70/18.62 tff(ic, type, ic: $i > $i). % 29.70/18.62 tff(uri_rdfs_Statement, type, uri_rdfs_Statement: $i). % 29.70/18.62 tff(uri_rdf__1, type, uri_rdf__1: $i). % 29.70/18.62 tff(iext, type, iext: ($i * $i * $i) > $i). % 29.70/18.62 tff(uri_rdf_rest, type, uri_rdf_rest: $i). % 29.70/18.62 tff(uri_rdfs_label, type, uri_rdfs_label: $i). % 29.70/18.62 tff(uri_rdfs_Container, type, uri_rdfs_Container: $i). % 29.70/18.62 tff(uri_ex_robert, type, uri_ex_robert: $i). % 29.70/18.62 tff(uri_rdfs_subClassOf, type, uri_rdfs_subClassOf: $i). % 29.70/18.62 tff(uri_foaf_mbox_sha1sum, type, uri_foaf_mbox_sha1sum: $i). % 29.70/18.62 tff(uri_owl_sameAs, type, uri_owl_sameAs: $i). % 29.70/18.62 tff(uri_rdf_object, type, uri_rdf_object: $i). % 29.70/18.62 tff(ip, type, ip: $i > $i). % 29.70/18.62 tff(uri_rdfs_Class, type, uri_rdfs_Class: $i). % 29.70/18.62 tff(uri_rdfs_Seq, type, uri_rdfs_Seq: $i). % 29.70/18.62 tff(uri_owl_DatatypeProperty, type, uri_owl_DatatypeProperty: $i). % 29.70/18.62 tff(uri_rdfs_member, type, uri_rdfs_member: $i). % 29.70/18.62 tff(uri_rdf_Bag, type, uri_rdf_Bag: $i). % 29.70/18.62 tff(uri_rdf__2, type, uri_rdf__2: $i). % 29.70/18.62 tff(uri_rdfs_comment, type, uri_rdfs_comment: $i). % 29.70/18.62 tff(uri_rdfs_Literal, type, uri_rdfs_Literal: $i). % 29.70/18.62 tff(true, type, true: $i). % 29.70/18.62 tff(uri_rdf_Alt, type, uri_rdf_Alt: $i). % 29.70/18.62 tff(uri_rdf_nil, type, uri_rdf_nil: $i). % 29.70/18.62 tff(literal_plain, type, literal_plain: $i > $i). % 29.70/18.62 tff(uri_rdfs_isDefinedBy, type, uri_rdfs_isDefinedBy: $i). % 29.70/18.62 tff(uri_rdfs_domain, type, uri_rdfs_domain: $i). % 29.70/18.62 tff(ifeq, type, ifeq: ($i * $i * $i * $i) > $i). % 29.70/18.62 % 29.70/18.62 %Saturated clause set: % 29.70/18.63 tff(c_12491, 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))). % 29.70/18.63 tff(c_12034, 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))). % 29.70/18.63 tff(c_12037, 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))). % 29.70/18.63 tff(c_64856, plain, (![X_1178, Y_1179]: (ifeq(iext(uri_rdf_predicate, X_1178, Y_1179), true, iext(uri_rdf_predicate, X_1178, Y_1179), true)=true))). % 29.70/18.63 tff(c_12363, 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))). % 29.70/18.63 tff(c_64714, plain, (![X_1173, Y_1174]: (ifeq(iext(uri_rdfs_comment, X_1173, Y_1174), true, iext(uri_rdfs_comment, X_1173, Y_1174), true)=true))). % 29.70/18.63 tff(c_12429, 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))). % 29.70/18.63 tff(c_64569, plain, (![X_1168, Y_1169]: (ifeq(iext(uri_rdfs_member, X_1168, Y_1169), true, iext(uri_rdfs_member, X_1168, Y_1169), true)=true))). % 29.70/18.63 tff(c_4806, 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))). % 29.70/18.63 tff(c_12294, 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))). % 29.70/18.63 tff(c_64303, plain, (![X_1161, Y_1162]: (ifeq(iext(uri_rdfs_label, X_1161, Y_1162), true, iext(uri_rdfs_label, X_1161, Y_1162), true)=true))). % 29.70/18.63 tff(c_12189, 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))). % 29.70/18.63 tff(c_11980, 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))). % 29.70/18.63 tff(c_4809, 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))). % 29.70/18.63 tff(c_13617, 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))). % 29.70/18.63 tff(c_63527, plain, (![C_1154]: (ifeq(iext(uri_rdfs_subClassOf, C_1154, uri_owl_InverseFunctionalProperty), true, iext(uri_rdfs_subClassOf, C_1154, uri_rdfs_Resource), true)=true))). % 29.70/18.63 tff(c_11739, 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))). % 29.70/18.63 tff(c_11833, 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))). % 29.70/18.63 tff(c_11673, 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))). % 29.70/18.63 tff(c_15659, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subClassOf), true, ifeq(iext(P_47, uri_owl_DatatypeProperty, uri_owl_DatatypeProperty), true, true, true), true)=true))). % 29.70/18.63 tff(c_62906, plain, (![C_1148]: (ifeq(iext(uri_rdfs_subClassOf, C_1148, uri_rdf_List), true, iext(uri_rdfs_subClassOf, C_1148, uri_rdfs_Resource), true)=true))). % 29.70/18.63 tff(c_11534, 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))). % 29.70/18.63 tff(c_13548, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subClassOf), true, ifeq(iext(P_47, uri_owl_InverseFunctionalProperty, uri_owl_InverseFunctionalProperty), true, true, true), true)=true))). % 29.70/18.63 tff(c_62516, plain, (![C_1144]: (ifeq(iext(uri_rdfs_subClassOf, C_1144, uri_rdfs_Statement), true, iext(uri_rdfs_subClassOf, C_1144, uri_rdfs_Resource), true)=true))). % 29.70/18.63 tff(c_62360, plain, (![C_1142]: (ifeq(iext(uri_rdfs_subClassOf, C_1142, uri_owl_DatatypeProperty), true, iext(uri_rdfs_subClassOf, C_1142, uri_rdfs_Resource), true)=true))). % 29.70/18.63 tff(c_15510, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subClassOf), true, ifeq(iext(P_47, uri_owl_DatatypeProperty, uri_rdfs_Resource), true, true, true), true)=true))). % 29.70/18.63 tff(c_13407, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subClassOf), true, ifeq(iext(P_47, uri_owl_InverseFunctionalProperty, uri_rdfs_Resource), true, true, true), true)=true))). % 29.70/18.63 tff(c_11067, 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))). % 29.70/18.63 tff(c_9414, 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))). % 29.70/18.63 tff(c_11188, 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))). % 29.70/18.63 tff(c_8641, 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))). % 29.70/18.63 tff(c_11260, 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))). % 29.70/18.63 tff(c_11314, 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))). % 29.70/18.63 tff(c_9417, 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))). % 29.70/18.63 tff(c_7599, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdf_Property), true, ifeq(iext(P_28, X_30, uri_foaf_mbox_sha1sum), true, true, true), true)=true))). % 29.70/18.63 tff(c_9047, 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))). % 29.70/18.63 tff(c_4999, 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))). % 29.70/18.63 tff(c_11140, 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))). % 29.70/18.63 tff(c_11408, 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))). % 29.70/18.63 tff(c_9044, 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))). % 29.70/18.63 tff(c_5093, 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))). % 29.70/18.63 tff(c_11361, 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))). % 29.70/18.63 tff(c_8638, 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))). % 29.70/18.63 tff(c_10131, 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))). % 29.70/18.64 tff(c_5096, 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))). % 29.70/18.64 tff(c_7596, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdf_Property), true, ifeq(iext(P_18, uri_foaf_mbox_sha1sum, Y_21), true, true, true), true)=true))). % 29.70/18.64 tff(c_11484, 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))). % 29.70/18.64 tff(c_11020, 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))). % 29.70/18.64 tff(c_10134, 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))). % 29.70/18.64 tff(c_4996, 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))). % 29.70/18.64 tff(c_10971, 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))). % 29.70/18.64 tff(c_10848, 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))). % 29.70/18.64 tff(c_15345, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, uri_owl_DatatypeProperty, uri_rdfs_Class), true, true, true), true)=true))). % 29.70/18.64 tff(c_10776, 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))). % 29.70/18.64 tff(c_10677, 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))). % 29.70/18.64 tff(c_13360, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, uri_owl_InverseFunctionalProperty, uri_rdfs_Class), true, true, true), true)=true))). % 29.70/18.64 tff(c_7183, 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))). % 29.70/18.64 tff(c_4942, 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))). % 29.70/18.64 tff(c_9665, 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))). % 29.70/18.64 tff(c_7538, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, uri_foaf_mbox_sha1sum, uri_rdf_Property), true, true, true), true)=true))). % 29.70/18.64 tff(c_4155, 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))). % 29.70/18.64 tff(c_57670, plain, (![X_1087, Y_1088]: (ifeq(iext(uri_rdfs_range, X_1087, Y_1088), true, iext(uri_rdfs_range, X_1087, Y_1088), true)=true))). % 29.70/18.64 tff(c_57603, plain, (![P_1085]: (ifeq(iext(uri_rdfs_subPropertyOf, P_1085, uri_rdf__2), true, iext(uri_rdfs_subPropertyOf, P_1085, uri_rdfs_member), true)=true))). % 29.70/18.64 tff(c_4409, 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))). % 29.70/18.64 tff(c_57363, plain, (![X_1079, Y_1080]: (ifeq(iext(uri_rdf_subject, X_1079, Y_1080), true, iext(uri_rdf_subject, X_1079, Y_1080), true)=true))). % 29.70/18.64 tff(c_57335, plain, (![X_1075, Y_1076]: (ifeq(iext(uri_rdf_value, X_1075, Y_1076), true, iext(uri_rdf_value, X_1075, Y_1076), true)=true))). % 29.70/18.64 tff(c_4152, 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))). % 29.70/18.64 tff(c_57180, plain, (![X_1069, Y_1070]: (ifeq(iext(uri_rdf__2, X_1069, Y_1070), true, iext(uri_rdfs_member, X_1069, Y_1070), true)=true))). % 29.70/18.64 tff(c_57121, plain, (![X_1065, Y_1066]: (ifeq(iext(uri_foaf_mbox_sha1sum, X_1065, Y_1066), true, iext(uri_foaf_mbox_sha1sum, X_1065, Y_1066), true)=true))). % 29.70/18.64 tff(c_57093, plain, (![X_1061, Y_1062]: (ifeq(iext(uri_rdf__1, X_1061, Y_1062), true, iext(uri_rdfs_member, X_1061, Y_1062), true)=true))). % 29.70/18.64 tff(c_8355, 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))). % 29.70/18.64 tff(c_56951, plain, (![X_1056, Y_1057]: (ifeq(iext(uri_rdf_first, X_1056, Y_1057), true, iext(uri_rdf_first, X_1056, Y_1057), true)=true))). % 29.70/18.64 tff(c_7348, 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))). % 29.70/18.64 tff(c_5717, 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))). % 29.70/18.64 tff(c_8829, 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))). % 29.70/18.64 tff(c_4301, 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))). % 29.70/18.64 tff(c_4259, 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))). % 29.70/18.64 tff(c_9227, 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))). % 29.70/18.64 tff(c_7415, 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))). % 29.70/18.64 tff(c_55950, plain, (![C_1045]: (ifeq(iext(uri_rdfs_subClassOf, C_1045, uri_rdf_Bag), true, iext(uri_rdfs_subClassOf, C_1045, uri_rdfs_Resource), true)=true))). % 29.70/18.64 tff(c_8990, 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))). % 29.70/18.64 tff(c_5346, 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))). % 29.70/18.64 tff(c_5216, 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))). % 29.70/18.64 tff(c_10430, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subPropertyOf), true, ifeq(iext(P_47, uri_foaf_mbox_sha1sum, uri_foaf_mbox_sha1sum), true, true, true), true)=true))). % 29.70/18.64 tff(c_55327, plain, (![C_1039]: (ifeq(iext(uri_rdfs_subClassOf, C_1039, uri_rdfs_ContainerMembershipProperty), true, iext(uri_rdfs_subClassOf, C_1039, uri_rdfs_Resource), true)=true))). % 29.70/18.64 tff(c_55158, plain, (![C_1035]: (ifeq(iext(uri_rdfs_subClassOf, C_1035, uri_rdfs_Datatype), true, iext(uri_rdfs_subClassOf, C_1035, uri_rdfs_Resource), true)=true))). % 29.70/18.64 tff(c_55145, plain, (![X_1033, Y_1034]: (ifeq(iext(uri_rdf_object, X_1033, Y_1034), true, iext(uri_rdf_object, X_1033, Y_1034), true)=true))). % 29.70/18.64 tff(c_4304, 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))). % 29.70/18.64 tff(c_54863, plain, (![C_1029]: (ifeq(iext(uri_rdfs_subClassOf, C_1029, uri_rdf_XMLLiteral), true, iext(uri_rdfs_subClassOf, C_1029, uri_rdfs_Resource), true)=true))). % 29.70/18.64 tff(c_6496, 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))). % 29.70/18.64 tff(c_8424, 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))). % 29.70/18.64 tff(c_5505, 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))). % 29.70/18.64 tff(c_5590, 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))). % 29.70/18.64 tff(c_7089, 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))). % 29.70/18.64 tff(c_54211, plain, (![P_1022]: (ifeq(iext(uri_rdfs_subPropertyOf, P_1022, uri_rdf__1), true, iext(uri_rdfs_subPropertyOf, P_1022, uri_rdfs_member), true)=true))). % 29.70/18.64 tff(c_8052, 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))). % 29.70/18.64 tff(c_5903, 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))). % 29.70/18.64 tff(c_5821, 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))). % 29.70/18.64 tff(c_53698, plain, (![C_1017]: (ifeq(iext(uri_rdfs_subClassOf, C_1017, uri_rdfs_Literal), true, iext(uri_rdfs_subClassOf, C_1017, uri_rdfs_Resource), true)=true))). % 29.70/18.64 tff(c_4049, 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))). % 29.70/18.64 tff(c_5652, 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))). % 29.70/18.64 tff(c_7970, 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))). % 29.70/18.64 tff(c_4099, 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))). % 29.70/18.64 tff(c_8893, 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))). % 29.70/18.64 tff(c_4706, 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))). % 29.70/18.64 tff(c_52938, plain, (![X_1005, Y_1006]: (ifeq(iext(uri_rdf__3, X_1005, Y_1006), true, iext(uri_rdf__3, X_1005, Y_1006), true)=true))). % 29.70/18.64 tff(c_52759, plain, (![C_1003]: (ifeq(iext(uri_rdfs_subClassOf, C_1003, uri_rdfs_Container), true, iext(uri_rdfs_subClassOf, C_1003, uri_rdfs_Resource), true)=true))). % 29.70/18.64 tff(c_4096, 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))). % 29.70/18.64 tff(c_4256, 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))). % 29.70/18.64 tff(c_6043, 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))). % 29.70/18.65 tff(c_52227, plain, (![C_996]: (ifeq(iext(uri_rdfs_subClassOf, C_996, uri_rdfs_Seq), true, iext(uri_rdfs_subClassOf, C_996, uri_rdfs_Resource), true)=true))). % 29.70/18.65 tff(c_6223, 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))). % 29.70/18.65 tff(c_4406, 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))). % 29.70/18.65 tff(c_9163, 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))). % 29.70/18.65 tff(c_9771, 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))). % 29.70/18.65 tff(c_5968, 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))). % 29.70/18.65 tff(c_50915, plain, (![X_986, Y_987]: (ifeq(iext(uri_rdf_type, X_986, Y_987), true, iext(uri_rdf_type, X_986, Y_987), true)=true))). % 29.70/18.65 tff(c_50886, plain, (![X_982, Y_983]: (ifeq(iext(uri_rdf__1, X_982, Y_983), true, iext(uri_rdf__1, X_982, Y_983), true)=true))). % 29.70/18.65 tff(c_50819, plain, (![P_980]: (ifeq(iext(uri_rdfs_subPropertyOf, P_980, uri_rdf__3), true, iext(uri_rdfs_subPropertyOf, P_980, uri_rdfs_member), true)=true))). % 29.70/18.65 tff(c_4461, 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))). % 29.70/18.65 tff(c_6374, 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))). % 29.70/18.65 tff(c_9360, 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))). % 29.70/18.65 tff(c_5045, 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))). % 29.70/18.65 tff(c_10518, 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))). % 29.70/18.65 tff(c_49553, plain, (![X_970, Y_971]: (ifeq(iext(uri_rdfs_subClassOf, X_970, Y_971), true, iext(uri_rdfs_subClassOf, X_970, Y_971), true)=true))). % 29.70/18.65 tff(c_10590, 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))). % 29.70/18.65 tff(c_49410, plain, (![X_965, Y_966]: (ifeq(iext(uri_rdf__2, X_965, Y_966), true, iext(uri_rdf__2, X_965, Y_966), true)=true))). % 29.70/18.65 tff(c_9571, 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))). % 29.70/18.65 tff(c_49040, plain, (![X_958, Y_959]: (ifeq(iext(uri_rdf__3, X_958, Y_959), true, iext(uri_rdfs_member, X_958, Y_959), true)=true))). % 29.70/18.65 tff(c_10077, 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))). % 29.70/18.65 tff(c_4201, 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))). % 29.70/18.65 tff(c_6805, 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))). % 29.70/18.65 tff(c_4352, 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))). % 29.70/18.65 tff(c_48189, plain, (![X_948, Y_949]: (ifeq(iext(uri_rdfs_domain, X_948, Y_949), true, iext(uri_rdfs_domain, X_948, Y_949), true)=true))). % 29.70/18.65 tff(c_8584, 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))). % 29.70/18.65 tff(c_9909, 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))). % 29.70/18.65 tff(c_4458, 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))). % 29.70/18.65 tff(c_7703, 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))). % 29.70/18.65 tff(c_47547, plain, (![C_941]: (ifeq(iext(uri_rdfs_subClassOf, C_941, uri_rdf_Alt), true, iext(uri_rdfs_subClassOf, C_941, uri_rdfs_Resource), true)=true))). % 29.70/18.65 tff(c_13023, 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))). % 29.70/18.65 tff(c_46767, plain, (![X_935, Y_936]: (ifeq(iext(uri_rdfs_subPropertyOf, X_935, Y_936), true, iext(uri_rdfs_subPropertyOf, X_935, Y_936), true)=true))). % 29.70/18.65 tff(c_4198, 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))). % 29.70/18.65 tff(c_46518, plain, (![X_928, Y_929]: (ifeq(iext(uri_rdfs_isDefinedBy, X_928, Y_929), true, iext(uri_rdfs_isDefinedBy, X_928, Y_929), true)=true))). % 29.70/18.65 tff(c_10359, 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))). % 29.70/18.65 tff(c_6622, 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))). % 29.70/18.65 tff(c_4878, 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))). % 29.70/18.65 tff(c_45698, plain, (![C_921]: (ifeq(iext(uri_rdfs_subClassOf, C_921, uri_rdfs_Class), true, iext(uri_rdfs_subClassOf, C_921, uri_rdfs_Resource), true)=true))). % 29.70/18.65 tff(c_5144, 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))). % 29.70/18.65 tff(c_45555, plain, (![X_916, Y_917]: (ifeq(iext(uri_rdfs_seeAlso, X_916, Y_917), true, iext(uri_rdfs_seeAlso, X_916, Y_917), true)=true))). % 29.70/18.65 tff(c_45529, plain, (![X_912, Y_913]: (ifeq(iext(uri_rdf_rest, X_912, Y_913), true, iext(uri_rdf_rest, X_912, Y_913), true)=true))). % 29.70/18.65 tff(c_4355, 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))). % 29.70/18.65 tff(c_45239, plain, (![C_908]: (ifeq(iext(uri_rdfs_subClassOf, C_908, uri_rdf_Property), true, iext(uri_rdfs_subClassOf, C_908, uri_rdfs_Resource), true)=true))). % 29.70/18.65 tff(c_4052, 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))). % 29.70/18.65 tff(c_6122, 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))). % 29.70/18.65 tff(c_7002, 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))). % 29.70/18.65 tff(c_6125, 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))). % 29.70/18.65 tff(c_13151, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdfs_Class), true, ifeq(iext(P_18, uri_owl_InverseFunctionalProperty, Y_21), true, true, true), true)=true))). % 29.70/18.65 tff(c_6999, 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))). % 29.70/18.65 tff(c_6706, 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))). % 29.70/18.65 tff(c_13154, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdfs_Class), true, ifeq(iext(P_28, X_30, uri_owl_InverseFunctionalProperty), true, true, true), true)=true))). % 29.70/18.65 tff(c_6889, 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))). % 29.70/18.65 tff(c_6709, 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))). % 29.70/18.65 tff(c_6892, 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))). % 29.70/18.65 tff(c_4567, plain, (![P_47, X_131]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, X_131, uri_rdfs_Resource), true, true, true), true)=true))). % 29.70/18.65 tff(c_15222, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdfs_Class), true, ifeq(iext(P_18, uri_owl_DatatypeProperty, Y_21), true, true, true), true)=true))). % 29.70/18.65 tff(c_15225, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdfs_Class), true, ifeq(iext(P_28, X_30, uri_owl_DatatypeProperty), true, true, true), true)=true))). % 29.70/18.65 tff(c_3678, 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))). % 29.70/18.65 tff(c_12869, 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))). % 29.70/18.65 tff(c_3636, 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))). % 29.70/18.65 tff(c_3348, 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))). % 29.70/18.65 tff(c_3557, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_owl_InverseFunctionalProperty), true, ifeq(iext(P_18, uri_foaf_mbox_sha1sum, Y_21), true, true, true), true)=true))). % 29.70/18.65 tff(c_3608, 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))). % 29.70/18.65 tff(c_3393, 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))). % 29.70/18.65 tff(c_3713, 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))). % 29.70/18.65 tff(c_3471, 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))). % 29.70/18.65 tff(c_3970, 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))). % 29.70/18.65 tff(c_4009, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_owl_DatatypeProperty), true, ifeq(iext(P_28, X_30, uri_foaf_mbox_sha1sum), true, true, true), true)=true))). % 29.70/18.65 tff(c_3847, 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))). % 29.70/18.65 tff(c_3794, 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))). % 29.70/18.65 tff(c_3633, 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))). % 29.70/18.65 tff(c_3797, 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))). % 29.70/18.65 tff(c_3520, 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))). % 29.70/18.65 tff(c_3887, 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))). % 29.70/18.65 tff(c_3716, 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))). % 29.70/18.65 tff(c_3850, 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))). % 29.70/18.65 tff(c_3427, 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))). % 29.70/18.65 tff(c_3430, 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))). % 29.70/18.65 tff(c_3757, 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))). % 29.70/18.65 tff(c_3474, 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))). % 29.70/18.65 tff(c_3890, 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))). % 29.70/18.65 tff(c_3760, 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))). % 29.70/18.65 tff(c_3390, 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))). % 29.70/18.65 tff(c_2522, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_foaf_mbox_sha1sum), true, ifeq(iext(P_106, uri_ex_robert, literal_plain(dat_str_xyz)), true, true, true), true)=true))). % 29.70/18.66 tff(c_3930, 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))). % 29.70/18.66 tff(c_3967, 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))). % 29.70/18.66 tff(c_3605, 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))). % 29.70/18.66 tff(c_3927, 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))). % 29.70/18.66 tff(c_3560, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_owl_InverseFunctionalProperty), true, ifeq(iext(P_28, X_30, uri_foaf_mbox_sha1sum), true, true, true), true)=true))). % 29.70/18.66 tff(c_3675, 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))). % 29.70/18.66 tff(c_3345, 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))). % 29.70/18.66 tff(c_3517, 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))). % 29.70/18.66 tff(c_12872, 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))). % 29.70/18.66 tff(c_2528, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_foaf_mbox_sha1sum), true, ifeq(iext(P_106, uri_ex_bob, literal_plain(dat_str_xyz)), true, true, true), true)=true))). % 29.70/18.66 tff(c_4006, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_owl_DatatypeProperty), true, ifeq(iext(P_18, uri_foaf_mbox_sha1sum, Y_21), true, true, true), true)=true))). % 29.70/18.66 tff(c_1646, plain, (![P_92, X_94, X_61]: (ifeq(iext(uri_rdfs_range, P_92, uri_rdfs_Resource), true, ifeq(iext(P_92, X_94, X_61), true, true, true), true)=true))). % 29.70/18.66 tff(c_2021, plain, (![P_96, X_61, Y_99]: (ifeq(iext(uri_rdfs_domain, P_96, uri_rdfs_Resource), true, ifeq(iext(P_96, X_61, Y_99), true, true, true), true)=true))). % 29.70/18.66 tff(c_2825, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_domain), true, ifeq(iext(P_106, uri_rdf_object, uri_rdfs_Statement), true, true, true), true)=true))). % 29.70/18.66 tff(c_36648, plain, (![P_795]: (ifeq(iext(uri_rdfs_subPropertyOf, P_795, uri_rdfs_isDefinedBy), true, iext(uri_rdfs_subPropertyOf, P_795, uri_rdfs_seeAlso), true)=true))). % 29.70/18.66 tff(c_2534, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_range), true, ifeq(iext(P_106, uri_rdf_rest, uri_rdf_List), true, true, true), true)=true))). % 29.70/18.66 tff(c_2693, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_domain), true, ifeq(iext(P_106, uri_rdfs_isDefinedBy, uri_rdfs_Resource), true, true, true), true)=true))). % 29.70/18.66 tff(c_36354, plain, (![C_791]: (ifeq(iext(uri_rdfs_subClassOf, C_791, uri_rdf_XMLLiteral), true, iext(uri_rdfs_subClassOf, C_791, uri_rdfs_Literal), true)=true))). % 29.70/18.66 tff(c_2552, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdf_type), true, ifeq(iext(P_106, uri_rdf__2, uri_rdfs_ContainerMembershipProperty), true, true, true), true)=true))). % 29.70/18.66 tff(c_2861, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdf_type), true, ifeq(iext(P_106, uri_rdf_first, uri_rdf_Property), true, true, true), true)=true))). % 29.70/18.66 tff(c_2807, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_domain), true, ifeq(iext(P_106, uri_rdf_type, uri_rdfs_Resource), true, true, true), true)=true))). % 29.70/18.66 tff(c_2570, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdf_type), true, ifeq(iext(P_106, uri_rdf__3, uri_rdfs_ContainerMembershipProperty), true, true, true), true)=true))). % 29.70/18.66 tff(c_2624, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_range), true, ifeq(iext(P_106, uri_rdf__2, uri_rdfs_Resource), true, true, true), true)=true))). % 29.70/18.66 tff(c_2717, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_subClassOf), true, ifeq(iext(P_106, uri_rdfs_ContainerMembershipProperty, uri_rdf_Property), true, true, true), true)=true))). % 29.70/18.66 tff(c_35581, plain, (![C_783]: (ifeq(iext(uri_rdfs_subClassOf, C_783, uri_rdfs_Seq), true, iext(uri_rdfs_subClassOf, C_783, uri_rdfs_Container), true)=true))). % 29.70/18.66 tff(c_2636, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdf_type), true, ifeq(iext(P_106, uri_rdf__2, uri_rdf_Property), true, true, true), true)=true))). % 29.70/18.66 tff(c_2630, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_range), true, ifeq(iext(P_106, uri_rdfs_isDefinedBy, uri_rdfs_Resource), true, true, true), true)=true))). % 29.70/18.66 tff(c_2666, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_domain), true, ifeq(iext(P_106, uri_rdfs_domain, uri_rdf_Property), true, true, true), true)=true))). % 29.70/18.66 tff(c_35171, plain, (![C_778]: (ifeq(iext(uri_rdfs_subClassOf, C_778, uri_rdfs_Datatype), true, iext(uri_rdfs_subClassOf, C_778, uri_rdfs_Class), true)=true))). % 29.70/18.66 tff(c_35104, plain, (![C_776]: (ifeq(iext(uri_rdfs_subClassOf, C_776, uri_rdf_Alt), true, iext(uri_rdfs_subClassOf, C_776, uri_rdfs_Container), true)=true))). % 29.70/18.66 tff(c_35053, plain, (![C_774]: (ifeq(iext(uri_rdfs_subClassOf, C_774, uri_rdfs_ContainerMembershipProperty), true, iext(uri_rdfs_subClassOf, C_774, uri_rdf_Property), true)=true))). % 29.70/18.66 tff(c_2600, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_domain), true, ifeq(iext(P_106, uri_rdfs_label, uri_rdfs_Resource), true, true, true), true)=true))). % 29.70/18.66 tff(c_2801, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_domain), true, ifeq(iext(P_106, uri_rdfs_member, uri_rdfs_Resource), true, true, true), true)=true))). % 29.70/18.66 tff(c_2654, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_domain), true, ifeq(iext(P_106, uri_rdf__3, uri_rdfs_Resource), true, true, true), true)=true))). % 29.70/18.66 tff(c_2885, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdf_type), true, ifeq(iext(P_106, uri_rdf_Property, uri_rdfs_Class), true, true, true), true)=true))). % 29.70/18.66 tff(c_2831, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_range), true, ifeq(iext(P_106, uri_rdfs_comment, uri_rdfs_Literal), true, true, true), true)=true))). % 29.70/18.66 tff(c_2855, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_domain), true, ifeq(iext(P_106, uri_rdf_first, uri_rdf_List), true, true, true), true)=true))). % 29.70/18.66 tff(c_2813, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_domain), true, ifeq(iext(P_106, uri_rdf_rest, uri_rdf_List), true, true, true), true)=true))). % 29.70/18.66 tff(c_2705, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdf_type), true, ifeq(iext(P_106, uri_rdf_type, uri_rdf_Property), true, true, true), true)=true))). % 29.70/18.66 tff(c_2789, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdf_type), true, ifeq(iext(P_106, uri_rdf__3, uri_rdf_Property), true, true, true), true)=true))). % 29.70/18.66 tff(c_33807, plain, (![C_762]: (ifeq(iext(uri_rdfs_subClassOf, C_762, uri_rdf_Bag), true, iext(uri_rdfs_subClassOf, C_762, uri_rdfs_Container), true)=true))). % 29.70/18.66 tff(c_2849, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdf_type), true, ifeq(iext(P_106, uri_rdf__1, uri_rdf_Property), true, true, true), true)=true))). % 29.70/18.66 tff(c_2897, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_range), true, ifeq(iext(P_106, uri_rdf_type, uri_rdfs_Class), true, true, true), true)=true))). % 29.70/18.66 tff(c_2723, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_domain), true, ifeq(iext(P_106, uri_rdfs_subClassOf, uri_rdfs_Class), true, true, true), true)=true))). % 29.70/18.66 tff(c_33546, plain, (![X_756, Y_757]: (ifeq(iext(uri_rdfs_isDefinedBy, X_756, Y_757), true, iext(uri_rdfs_seeAlso, X_756, Y_757), true)=true))). % 29.70/18.66 tff(c_2588, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdf_type), true, ifeq(iext(P_106, uri_rdf__1, uri_rdfs_ContainerMembershipProperty), true, true, true), true)=true))). % 29.70/18.66 tff(c_2783, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdf_type), true, ifeq(iext(P_106, uri_rdf_XMLLiteral, uri_rdfs_Datatype), true, true, true), true)=true))). % 29.70/18.66 tff(c_2681, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_subPropertyOf), true, ifeq(iext(P_106, uri_rdfs_isDefinedBy, uri_rdfs_seeAlso), true, true, true), true)=true))). % 29.70/18.66 tff(c_2729, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdf_type), true, ifeq(iext(P_106, uri_rdf_subject, uri_rdf_Property), true, true, true), true)=true))). % 29.70/18.66 tff(c_2648, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_subClassOf), true, ifeq(iext(P_106, uri_rdfs_Seq, uri_rdfs_Container), true, true, true), true)=true))). % 29.70/18.66 tff(c_2558, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_domain), true, ifeq(iext(P_106, uri_rdf_subject, uri_rdfs_Statement), true, true, true), true)=true))). % 29.70/18.66 tff(c_2540, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdf_type), true, ifeq(iext(P_106, uri_rdf_rest, uri_rdf_Property), true, true, true), true)=true))). % 29.70/18.66 tff(c_2612, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_range), true, ifeq(iext(P_106, uri_rdf_predicate, uri_rdfs_Resource), true, true, true), true)=true))). % 29.70/18.66 tff(c_2837, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_range), true, ifeq(iext(P_106, uri_rdfs_seeAlso, uri_rdfs_Resource), true, true, true), true)=true))). % 29.70/18.66 tff(c_2711, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_domain), true, ifeq(iext(P_106, uri_rdf__2, uri_rdfs_Resource), true, true, true), true)=true))). % 29.70/18.66 tff(c_2564, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_domain), true, ifeq(iext(P_106, uri_rdfs_seeAlso, uri_rdfs_Resource), true, true, true), true)=true))). % 29.70/18.66 tff(c_2735, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_range), true, ifeq(iext(P_106, uri_rdf__1, uri_rdfs_Resource), true, true, true), true)=true))). % 29.70/18.66 tff(c_2576, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_range), true, ifeq(iext(P_106, uri_rdf_value, uri_rdfs_Resource), true, true, true), true)=true))). % 29.70/18.66 tff(c_31935, plain, (![D_741]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_741), true, icext(D_741, uri_rdfs_member), true)=true))). % 29.70/18.66 tff(c_31868, plain, (![D_739]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_739), true, icext(D_739, uri_rdfs_Resource), true)=true))). % 29.70/18.66 tff(c_31686, plain, (![D_736]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_736), true, icext(D_736, uri_rdfs_seeAlso), true)=true))). % 29.70/18.66 tff(c_2759, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_range), true, ifeq(iext(P_106, uri_rdfs_range, uri_rdfs_Class), true, true, true), true)=true))). % 29.70/18.66 tff(c_31619, plain, (![D_734]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_734), true, icext(D_734, uri_rdfs_isDefinedBy), true)=true))). % 29.70/18.66 tff(c_31553, plain, (![D_732]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_732), true, icext(D_732, uri_rdfs_range), true)=true))). % 29.70/18.66 tff(c_2672, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_range), true, ifeq(iext(P_106, uri_rdfs_label, uri_rdfs_Literal), true, true, true), true)=true))). % 29.70/18.66 tff(c_31372, plain, (![D_729]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_729), true, icext(D_729, uri_rdfs_subClassOf), true)=true))). % 29.70/18.66 tff(c_31306, plain, (![D_727]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_727), true, icext(D_727, uri_rdfs_domain), true)=true))). % 29.70/18.66 tff(c_31224, plain, (![D_725]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_725), true, icext(D_725, uri_foaf_mbox_sha1sum), true)=true))). % 29.70/18.66 tff(c_2606, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_range), true, ifeq(iext(P_106, uri_rdf_subject, uri_rdfs_Resource), true, true, true), true)=true))). % 29.70/18.66 tff(c_31038, plain, (![D_722]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_722), true, icext(D_722, uri_rdfs_subPropertyOf), true)=true))). % 29.70/18.66 tff(c_30972, plain, (![D_720]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_720), true, icext(D_720, uri_rdfs_ContainerMembershipProperty), true)=true))). % 29.70/18.66 tff(c_30878, plain, (![D_718]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_718), true, icext(D_718, uri_rdfs_Class), true)=true))). % 29.70/18.66 tff(c_2594, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_range), true, ifeq(iext(P_106, uri_rdf__3, uri_rdfs_Resource), true, true, true), true)=true))). % 29.70/18.66 tff(c_30686, plain, (![D_715]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_715), true, icext(D_715, uri_rdfs_Datatype), true)=true))). % 29.70/18.66 tff(c_30620, plain, (![D_713]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_713), true, icext(D_713, uri_rdfs_Literal), true)=true))). % 29.70/18.66 tff(c_30544, plain, (![D_711]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_711), true, icext(D_711, uri_rdf_XMLLiteral), true)=true))). % 29.70/18.66 tff(c_30477, plain, (![D_709]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_709), true, icext(D_709, uri_rdf_Alt), true)=true))). % 29.70/18.66 tff(c_30411, plain, (![D_707]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_707), true, icext(D_707, uri_rdfs_Container), true)=true))). % 29.70/18.66 tff(c_2843, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_subClassOf), true, ifeq(iext(P_106, uri_rdfs_Datatype, uri_rdfs_Class), true, true, true), true)=true))). % 29.70/18.66 tff(c_30226, plain, (![D_704]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_704), true, icext(D_704, uri_rdfs_Seq), true)=true))). % 29.70/18.66 tff(c_30160, plain, (![D_702]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_702), true, icext(D_702, uri_rdf_Bag), true)=true))). % 29.70/18.66 tff(c_2765, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_range), true, ifeq(iext(P_106, uri_rdfs_domain, uri_rdfs_Class), true, true, true), true)=true))). % 29.70/18.66 tff(c_29974, plain, (![D_699]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_699), true, icext(D_699, uri_rdf_List), true)=true))). % 29.70/18.66 tff(c_29908, plain, (![D_697]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_697), true, icext(D_697, uri_rdfs_comment), true)=true))). % 29.70/18.66 tff(c_29840, plain, (![D_695]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_695), true, icext(D_695, uri_owl_InverseFunctionalProperty), true)=true))). % 29.70/18.66 tff(c_29772, plain, (![D_693]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_693), true, icext(D_693, uri_owl_DatatypeProperty), true)=true))). % 29.70/18.66 tff(c_2546, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_range), true, ifeq(iext(P_106, uri_rdfs_subPropertyOf, uri_rdf_Property), true, true, true), true)=true))). % 29.70/18.66 tff(c_29583, plain, (![D_690]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_690), true, icext(D_690, uri_rdfs_Statement), true)=true))). % 29.70/18.66 tff(c_29517, plain, (![D_688]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_688), true, icext(D_688, uri_rdf_predicate), true)=true))). % 29.70/18.66 tff(c_2687, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_domain), true, ifeq(iext(P_106, uri_rdfs_comment, uri_rdfs_Resource), true, true, true), true)=true))). % 29.70/18.66 tff(c_29312, plain, (![D_685]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, D_685), true, icext(D_685, uri_rdf_XMLLiteral), true)=true))). % 29.70/18.66 tff(c_12510, 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))). % 29.70/18.66 tff(c_12460, 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))). % 29.70/18.66 tff(c_12394, 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))). % 29.70/18.66 tff(c_2879, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_range), true, ifeq(iext(P_106, uri_rdf_first, uri_rdfs_Resource), true, true, true), true)=true))). % 29.70/18.66 tff(c_12005, 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))). % 29.70/18.66 tff(c_12226, 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))). % 29.70/18.66 tff(c_28945, plain, (![D_673]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_673), true, icext(D_673, uri_rdf__2), true)=true))). % 29.70/18.66 tff(c_12328, 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))). % 29.70/18.66 tff(c_13648, 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))). % 29.70/18.66 tff(c_2777, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_range), true, ifeq(iext(P_106, uri_rdfs_member, uri_rdfs_Resource), true, true, true), true)=true))). % 29.70/18.67 tff(c_11569, 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))). % 29.70/18.67 tff(c_13582, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_48), true, iext(Q_48, uri_owl_InverseFunctionalProperty, uri_owl_InverseFunctionalProperty), true)=true))). % 29.99/18.67 tff(c_11707, 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))). % 29.99/18.67 tff(c_28637, plain, (![D_664]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, D_664), true, icext(D_664, uri_rdf__3), true)=true))). % 29.99/18.67 tff(c_13441, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_48), true, iext(Q_48, uri_owl_InverseFunctionalProperty, uri_rdfs_Resource), true)=true))). % 29.99/18.67 tff(c_11773, 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))). % 29.99/18.67 tff(c_11867, 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))). % 29.99/18.67 tff(c_2867, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdf_type), true, ifeq(iext(P_106, uri_rdf_nil, uri_rdf_List), true, true, true), true)=true))). % 29.99/18.67 tff(c_11868, 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))). % 29.99/18.67 tff(c_11568, 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))). % 29.99/18.67 tff(c_28331, plain, (![D_655]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_655), true, icext(D_655, uri_rdf_type), true)=true))). % 29.99/18.67 tff(c_15693, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_48), true, iext(Q_48, uri_owl_DatatypeProperty, uri_owl_DatatypeProperty), true)=true))). % 29.99/18.67 tff(c_13442, plain, (![E_41]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Resource, E_41), true, iext(uri_rdfs_subClassOf, uri_owl_InverseFunctionalProperty, E_41), true)=true))). % 29.99/18.67 tff(c_2747, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_domain), true, ifeq(iext(P_106, uri_rdf_predicate, uri_rdfs_Statement), true, true, true), true)=true))). % 29.99/18.67 tff(c_15545, plain, (![E_41]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Resource, E_41), true, iext(uri_rdfs_subClassOf, uri_owl_DatatypeProperty, E_41), true)=true))). % 29.99/18.67 tff(c_15544, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_48), true, iext(Q_48, uri_owl_DatatypeProperty, uri_rdfs_Resource), true)=true))). % 29.99/18.67 tff(c_11279, 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))). % 29.99/18.67 tff(c_11207, 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))). % 29.99/18.67 tff(c_11039, 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))). % 29.99/18.67 tff(c_11427, 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))). % 29.99/18.67 tff(c_2582, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdf_type), true, ifeq(iext(P_106, uri_foaf_mbox_sha1sum, uri_owl_DatatypeProperty), true, true, true), true)=true))). % 29.99/18.67 tff(c_11503, 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))). % 29.99/18.67 tff(c_11159, 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))). % 29.99/18.67 tff(c_11086, 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))). % 29.99/18.67 tff(c_11380, 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))). % 29.99/18.67 tff(c_11333, 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))). % 29.99/18.67 tff(c_10873, 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))). % 29.99/18.67 tff(c_10990, 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))). % 29.99/18.67 tff(c_10702, 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))). % 29.99/18.67 tff(c_2618, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_subClassOf), true, ifeq(iext(P_106, uri_rdf_XMLLiteral, uri_rdfs_Literal), true, true, true), true)=true))). % 29.99/18.67 tff(c_13379, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, uri_owl_InverseFunctionalProperty, uri_rdfs_Class), true)=true))). % 29.99/18.67 tff(c_15364, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, uri_owl_DatatypeProperty, uri_rdfs_Class), true)=true))). % 29.99/18.67 tff(c_10795, 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))). % 29.99/18.67 tff(c_27503, plain, (![D_628]: (ifeq(iext(uri_rdfs_subClassOf, uri_owl_DatatypeProperty, D_628), true, icext(D_628, uri_foaf_mbox_sha1sum), true)=true))). % 29.99/18.67 tff(c_5174, 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))). % 29.99/18.67 tff(c_2753, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_range), true, ifeq(iext(P_106, uri_rdfs_subClassOf, uri_rdfs_Class), true, true, true), true)=true))). % 29.99/18.67 tff(c_5747, 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))). % 29.99/18.67 tff(c_8004, 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))). % 29.99/18.67 tff(c_6254, 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))). % 29.99/18.67 tff(c_27187, plain, (![D_619]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_619), true, icext(D_619, uri_rdf_object), true)=true))). % 29.99/18.67 tff(c_8927, 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))). % 29.99/18.67 tff(c_6073, 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))). % 29.99/18.67 tff(c_2795, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_subClassOf), true, ifeq(iext(P_106, uri_rdf_Alt, uri_rdfs_Container), true, true, true), true)=true))). % 29.99/18.67 tff(c_6839, 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))). % 29.99/18.67 tff(c_8086, 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))). % 29.99/18.67 tff(c_7381, 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))). % 29.99/18.67 tff(c_5249, 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))). % 29.99/18.67 tff(c_5854, 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))). % 29.99/18.67 tff(c_9602, 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))). % 29.99/18.67 tff(c_2660, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdf_type), true, ifeq(iext(P_106, uri_rdf_object, uri_rdf_Property), true, true, true), true)=true))). % 29.99/18.67 tff(c_8386, 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))). % 29.99/18.67 tff(c_26582, plain, (![D_601]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_List, D_601), true, icext(D_601, uri_rdf_nil), true)=true))). % 29.99/18.67 tff(c_5376, 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))). % 29.99/18.67 tff(c_7119, 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))). % 29.99/18.67 tff(c_6005, 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))). % 29.99/18.67 tff(c_2873, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_subClassOf), true, ifeq(iext(P_106, uri_rdf_Bag, uri_rdfs_Container), true, true, true), true)=true))). % 29.99/18.67 tff(c_9194, 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))). % 29.99/18.67 tff(c_8005, 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))). % 29.99/18.67 tff(c_10461, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_48), true, iext(Q_48, uri_foaf_mbox_sha1sum, uri_foaf_mbox_sha1sum), true)=true))). % 29.99/18.67 tff(c_6838, 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))). % 29.99/18.67 tff(c_9806, 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))). % 29.99/18.67 tff(c_6655, 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))). % 29.99/18.67 tff(c_2771, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_domain), true, ifeq(iext(P_106, uri_rdf_value, uri_rdfs_Resource), true, true, true), true)=true))). % 29.99/18.67 tff(c_6253, 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))). % 29.99/18.67 tff(c_6530, 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))). % 29.99/18.67 tff(c_9699, 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))). % 29.99/18.67 tff(c_4739, 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))). % 29.99/18.67 tff(c_4967, 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))). % 29.99/18.67 tff(c_4740, 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))). % 29.99/18.67 tff(c_5685, 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))). % 29.99/18.67 tff(c_2741, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdf_type), true, ifeq(iext(P_106, uri_foaf_mbox_sha1sum, uri_owl_InverseFunctionalProperty), true, true, true), true)=true))). % 29.99/18.67 tff(c_9603, 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))). % 29.99/18.67 tff(c_25705, plain, (![D_574]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_574), true, icext(D_574, uri_rdf_rest), true)=true))). % 29.99/18.67 tff(c_9943, 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))). % 29.99/18.67 tff(c_9261, 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))). % 29.99/18.67 tff(c_2819, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_domain), true, ifeq(iext(P_106, uri_rdfs_range, uri_rdf_Property), true, true, true), true)=true))). % 29.99/18.67 tff(c_9385, 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))). % 29.99/18.67 tff(c_8860, 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))). % 29.99/18.67 tff(c_9015, 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))). % 29.99/18.67 tff(c_7734, 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))). % 29.99/18.67 tff(c_5934, 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))). % 29.99/18.67 tff(c_4911, 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))). % 29.99/18.67 tff(c_13048, 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))). % 29.99/18.67 tff(c_2699, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_domain), true, ifeq(iext(P_106, uri_rdf__1, uri_rdfs_Resource), true, true, true), true)=true))). % 29.99/18.67 tff(c_8455, 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))). % 29.99/18.67 tff(c_7214, 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))). % 29.99/18.67 tff(c_25126, plain, (![D_556]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_556), true, icext(D_556, uri_rdf_first), true)=true))). % 29.99/18.67 tff(c_6531, 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))). % 29.99/18.67 tff(c_7563, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, uri_foaf_mbox_sha1sum, uri_rdf_Property), true)=true))). % 29.99/18.67 tff(c_6407, 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))). % 29.99/18.67 tff(c_2891, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_domain), true, ifeq(iext(P_106, uri_rdfs_subPropertyOf, uri_rdf_Property), true, true, true), true)=true))). % 29.99/18.67 tff(c_9944, 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))). % 29.99/18.67 tff(c_24807, plain, (![D_547]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_547), true, icext(D_547, uri_rdf_value), true)=true))). % 29.99/18.67 tff(c_9805, 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))). % 29.99/18.67 tff(c_10102, 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))). % 29.99/18.67 tff(c_2642, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdf_type), true, ifeq(iext(P_106, uri_rdf_value, uri_rdf_Property), true, true, true), true)=true))). % 29.99/18.67 tff(c_10621, 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))). % 29.99/18.67 tff(c_5620, 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))). % 29.99/18.67 tff(c_5535, 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))). % 29.99/18.67 tff(c_9700, 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))). % 29.99/18.67 tff(c_7446, 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))). % 29.99/18.67 tff(c_8609, 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))). % 29.99/18.67 tff(c_2902, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_foaf_mbox_sha1sum, Q_107), true, iext(Q_107, uri_ex_robert, literal_plain(dat_str_xyz)), true)=true))). % 29.99/18.67 tff(c_10393, 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))). % 29.99/18.67 tff(c_24315, plain, (![D_529]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_529), true, icext(D_529, uri_rdf_subject), true)=true))). % 29.99/18.67 tff(c_6656, 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))). % 29.99/18.67 tff(c_2903, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_foaf_mbox_sha1sum, Q_107), true, iext(Q_107, uri_ex_bob, literal_plain(dat_str_xyz)), true)=true))). % 29.99/18.67 tff(c_5250, 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))). % 29.99/18.67 tff(c_10552, 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))). % 29.99/18.67 tff(c_8087, 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))). % 29.99/18.67 tff(c_5070, 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))). % 29.99/18.67 tff(c_8861, 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))). % 29.99/18.67 tff(c_4586, plain, (![Q_48, X_131]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, X_131, uri_rdfs_Resource), true)=true))). % 29.99/18.67 tff(c_2914, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_107), true, iext(Q_107, uri_rdf__3, uri_rdfs_Resource), true)=true))). % 29.99/18.67 tff(c_2953, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_107), true, iext(Q_107, uri_rdfs_comment, uri_rdfs_Literal), true)=true))). % 29.99/18.67 tff(c_2493, plain, (![E_104]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Container, E_104), true, iext(uri_rdfs_subClassOf, uri_rdf_Bag, E_104), true)=true))). % 29.99/18.67 tff(c_2950, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_107), true, iext(Q_107, uri_rdf_rest, uri_rdf_List), true)=true))). % 29.99/18.67 tff(c_23741, plain, (![D_510]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_510), true, icext(D_510, uri_rdf__1), true)=true))). % 29.99/18.67 tff(c_2489, plain, (![E_104]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Container, E_104), true, iext(uri_rdfs_subClassOf, uri_rdfs_Seq, E_104), true)=true))). % 29.99/18.67 tff(c_2943, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_107), true, iext(Q_107, uri_rdf_value, uri_rdfs_Resource), true)=true))). % 29.99/18.67 tff(c_2949, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_107), true, iext(Q_107, uri_rdf_type, uri_rdfs_Resource), true)=true))). % 29.99/18.68 tff(c_2959, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_107), true, iext(Q_107, uri_rdf_nil, uri_rdf_List), true)=true))). % 29.99/18.68 tff(c_2396, plain, (![R_101]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_seeAlso, R_101), true, iext(uri_rdfs_subPropertyOf, uri_rdfs_isDefinedBy, R_101), true)=true))). % 29.99/18.68 tff(c_2963, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_107), true, iext(Q_107, uri_rdfs_subPropertyOf, uri_rdf_Property), true)=true))). % 29.99/18.68 tff(c_2904, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_107), true, iext(Q_107, uri_rdf_rest, uri_rdf_List), true)=true))). % 29.99/18.68 tff(c_23528, plain, (![D_501]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_501), true, icext(D_501, uri_rdf_Property), true)=true))). % 29.99/18.68 tff(c_2916, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_107), true, iext(Q_107, uri_rdf_subject, uri_rdfs_Resource), true)=true))). % 29.99/18.68 tff(c_2927, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_107), true, iext(Q_107, uri_rdfs_label, uri_rdfs_Literal), true)=true))). % 29.99/18.68 tff(c_2955, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_107), true, iext(Q_107, uri_rdfs_Datatype, uri_rdfs_Class), true)=true))). % 29.99/18.68 tff(c_2909, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_107), true, iext(Q_107, uri_rdfs_seeAlso, uri_rdfs_Resource), true)=true))). % 29.99/18.68 tff(c_2944, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_107), true, iext(Q_107, uri_rdfs_member, uri_rdfs_Resource), true)=true))). % 29.99/18.68 tff(c_2946, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_107), true, iext(Q_107, uri_rdf__3, uri_rdf_Property), true)=true))). % 29.99/18.68 tff(c_2962, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_107), true, iext(Q_107, uri_rdf_Property, uri_rdfs_Class), true)=true))). % 29.99/18.68 tff(c_23314, plain, (![D_492]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, D_492), true, icext(D_492, uri_rdf__1), true)=true))). % 29.99/18.68 tff(c_2922, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_107), true, iext(Q_107, uri_rdf_value, uri_rdf_Property), true)=true))). % 29.99/18.68 tff(c_2960, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_107), true, iext(Q_107, uri_rdf_Bag, uri_rdfs_Container), true)=true))). % 29.99/18.68 tff(c_2910, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_107), true, iext(Q_107, uri_rdf__3, uri_rdfs_ContainerMembershipProperty), true)=true))). % 29.99/18.68 tff(c_2924, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_107), true, iext(Q_107, uri_rdf__3, uri_rdfs_Resource), true)=true))). % 29.99/18.68 tff(c_2931, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_107), true, iext(Q_107, uri_rdf__1, uri_rdfs_Resource), true)=true))). % 29.99/18.68 tff(c_2492, plain, (![E_104]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, E_104), true, iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, E_104), true)=true))). % 29.99/18.68 tff(c_2908, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_107), true, iext(Q_107, uri_rdf_subject, uri_rdfs_Statement), true)=true))). % 29.99/18.68 tff(c_23113, plain, (![D_483]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_483), true, icext(D_483, uri_rdfs_label), true)=true))). % 29.99/18.68 tff(c_2923, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_107), true, iext(Q_107, uri_rdfs_Seq, uri_rdfs_Container), true)=true))). % 29.99/18.68 tff(c_2941, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_107), true, iext(Q_107, uri_rdfs_range, uri_rdfs_Class), true)=true))). % 29.99/18.68 tff(c_2488, plain, (![E_104]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Literal, E_104), true, iext(uri_rdfs_subClassOf, uri_rdf_XMLLiteral, E_104), true)=true))). % 29.99/18.68 tff(c_2490, plain, (![E_104]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, E_104), true, iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, E_104), true)=true))). % 29.99/18.68 tff(c_2954, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_107), true, iext(Q_107, uri_rdfs_seeAlso, uri_rdfs_Resource), true)=true))). % 29.99/18.68 tff(c_2928, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_107), true, iext(Q_107, uri_rdfs_isDefinedBy, uri_rdfs_seeAlso), true)=true))). % 29.99/18.68 tff(c_2491, plain, (![E_104]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Container, E_104), true, iext(uri_rdfs_subClassOf, uri_rdf_Alt, E_104), true)=true))). % 29.99/18.68 tff(c_2957, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_107), true, iext(Q_107, uri_rdf_first, uri_rdf_List), true)=true))). % 29.99/18.68 tff(c_2940, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_107), true, iext(Q_107, uri_rdfs_subClassOf, uri_rdfs_Class), true)=true))). % 29.99/18.68 tff(c_2939, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_107), true, iext(Q_107, uri_rdf_predicate, uri_rdfs_Statement), true)=true))). % 29.99/18.68 tff(c_2945, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_107), true, iext(Q_107, uri_rdf_XMLLiteral, uri_rdfs_Datatype), true)=true))). % 29.99/18.68 tff(c_2956, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_107), true, iext(Q_107, uri_rdf__1, uri_rdf_Property), true)=true))). % 29.99/18.68 tff(c_2926, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_107), true, iext(Q_107, uri_rdfs_domain, uri_rdf_Property), true)=true))). % 29.99/18.68 tff(c_2932, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_107), true, iext(Q_107, uri_rdf_type, uri_rdf_Property), true)=true))). % 29.99/18.68 tff(c_2918, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_107), true, iext(Q_107, uri_rdf_XMLLiteral, uri_rdfs_Literal), true)=true))). % 29.99/18.68 tff(c_2920, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_107), true, iext(Q_107, uri_rdfs_isDefinedBy, uri_rdfs_Resource), true)=true))). % 29.99/18.68 tff(c_22706, plain, (![D_465]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_465), true, icext(D_465, uri_rdf__3), true)=true))). % 29.99/18.68 tff(c_2919, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_107), true, iext(Q_107, uri_rdf__2, uri_rdfs_Resource), true)=true))). % 29.99/18.68 tff(c_2958, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_107), true, iext(Q_107, uri_rdf_first, uri_rdf_Property), true)=true))). % 29.99/18.68 tff(c_2929, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_107), true, iext(Q_107, uri_rdfs_comment, uri_rdfs_Resource), true)=true))). % 29.99/18.68 tff(c_2917, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_107), true, iext(Q_107, uri_rdf_predicate, uri_rdfs_Resource), true)=true))). % 29.99/18.68 tff(c_2942, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_107), true, iext(Q_107, uri_rdfs_domain, uri_rdfs_Class), true)=true))). % 29.99/18.68 tff(c_2913, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_107), true, iext(Q_107, uri_rdf__1, uri_rdfs_ContainerMembershipProperty), true)=true))). % 29.99/18.68 tff(c_12397, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_comment), true)=true))). % 29.99/18.68 tff(c_12398, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_comment), true)=true))). % 29.99/18.68 tff(c_12463, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_predicate), true)=true))). % 29.99/18.68 tff(c_2907, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_107), true, iext(Q_107, uri_rdf__2, uri_rdfs_ContainerMembershipProperty), true)=true))). % 29.99/18.68 tff(c_12464, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_predicate), true)=true))). % 29.99/18.68 tff(c_12331, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_member), true)=true))). % 29.99/18.68 tff(c_12229, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdfs_Resource), true)=true))). % 29.99/18.68 tff(c_13651, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_label), true)=true))). % 29.99/18.68 tff(c_13652, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_label), true)=true))). % 29.99/18.68 tff(c_2936, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_107), true, iext(Q_107, uri_rdf_subject, uri_rdf_Property), true)=true))). % 29.99/18.68 tff(c_11711, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdf_List), true)=true))). % 29.99/18.68 tff(c_11776, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdfs_Statement), true)=true))). % 29.99/18.68 tff(c_11777, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdfs_Statement), true)=true))). % 29.99/18.68 tff(c_2912, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_107), true, iext(Q_107, uri_foaf_mbox_sha1sum, uri_owl_DatatypeProperty), true)=true))). % 29.99/18.68 tff(c_11870, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdf_List), true)=true))). % 29.99/18.68 tff(c_22154, plain, (![D_442]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, D_442), true, icext(D_442, uri_rdf__2), true)=true))). % 29.99/18.68 tff(c_15697, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_owl_DatatypeProperty), true)=true))). % 29.99/18.68 tff(c_13585, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_owl_InverseFunctionalProperty), true)=true))). % 29.99/18.68 tff(c_2925, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_107), true, iext(Q_107, uri_rdf_object, uri_rdf_Property), true)=true))). % 29.99/18.68 tff(c_15696, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_owl_DatatypeProperty), true)=true))). % 29.99/18.68 tff(c_13586, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_owl_InverseFunctionalProperty), true)=true))). % 29.99/18.68 tff(c_21955, plain, (![D_435]: (ifeq(iext(uri_rdfs_subClassOf, uri_owl_InverseFunctionalProperty, D_435), true, icext(D_435, uri_foaf_mbox_sha1sum), true)=true))). % 29.99/18.68 tff(c_2906, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_107), true, iext(Q_107, uri_rdfs_subPropertyOf, uri_rdf_Property), true)=true))). % 29.99/18.68 tff(c_2938, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_107), true, iext(Q_107, uri_foaf_mbox_sha1sum, uri_owl_InverseFunctionalProperty), true)=true))). % 29.99/18.68 tff(c_2948, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_107), true, iext(Q_107, uri_rdfs_member, uri_rdfs_Resource), true)=true))). % 29.99/18.68 tff(c_21456, plain, (![D_428, X_429]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Resource, D_428), true, icext(D_428, X_429), true)=true))). % 29.99/18.68 tff(c_2951, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_107), true, iext(Q_107, uri_rdfs_range, uri_rdf_Property), true)=true))). % 29.99/18.68 tff(c_21262, plain, (![C_89, X_61]: (ifeq(icext(C_89, X_61), true, true, true)=true))). % 29.99/18.68 tff(c_2911, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_107), true, iext(Q_107, uri_rdf_value, uri_rdfs_Resource), true)=true))). % 29.99/18.68 tff(c_5936, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_range), true)=true))). % 29.99/18.68 tff(c_8459, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_subPropertyOf), true)=true))). % 29.99/18.68 tff(c_10556, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdf_XMLLiteral), true)=true))). % 29.99/18.68 tff(c_21117, plain, (![X_417, Y_418]: (ifeq(iext(uri_rdf_object, X_417, Y_418), true, icext(uri_rdfs_Statement, X_417), true)=true))). % 29.99/18.68 tff(c_7217, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_domain), true)=true))). % 29.99/18.68 tff(c_2933, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_107), true, iext(Q_107, uri_rdf__2, uri_rdfs_Resource), true)=true))). % 29.99/18.68 tff(c_21031, plain, (![X_411, Y_412]: (ifeq(iext(uri_rdf_subject, X_411, Y_412), true, icext(uri_rdfs_Statement, X_411), true)=true))). % 29.99/18.68 tff(c_10464, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_foaf_mbox_sha1sum), true)=true))). % 29.99/18.68 tff(c_2915, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_107), true, iext(Q_107, uri_rdfs_label, uri_rdfs_Resource), true)=true))). % 29.99/18.68 tff(c_20645, plain, (![X_405, Y_406]: (ifeq(iext(uri_rdfs_domain, X_405, Y_406), true, icext(uri_rdfs_Class, Y_406), true)=true))). % 29.99/18.68 tff(c_7383, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdf_Property), true)=true))). % 29.99/18.68 tff(c_2961, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_107), true, iext(Q_107, uri_rdf_first, uri_rdfs_Resource), true)=true))). % 29.99/18.68 tff(c_7122, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_object), true)=true))). % 29.99/18.68 tff(c_7738, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_isDefinedBy), true)=true))). % 29.99/18.68 tff(c_20155, plain, (![X_397, Y_398]: (ifeq(iext(uri_rdfs_domain, X_397, Y_398), true, icext(uri_rdf_Property, X_397), true)=true))). % 29.99/18.68 tff(c_9265, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdfs_Seq), true)=true))). % 29.99/18.68 tff(c_2937, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_107), true, iext(Q_107, uri_rdf__1, uri_rdfs_Resource), true)=true))). % 29.99/18.68 tff(c_9198, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_rest), true)=true))). % 29.99/18.68 tff(c_19681, plain, (![X_390, Y_391]: (ifeq(iext(uri_rdfs_subPropertyOf, X_390, Y_391), true, icext(uri_rdf_Property, Y_391), true)=true))). % 29.99/18.68 tff(c_6255, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf__1), true)=true))). % 29.99/18.68 tff(c_9197, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_rest), true)=true))). % 29.99/18.68 tff(c_5379, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_value), true)=true))). % 29.99/18.68 tff(c_2930, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_107), true, iext(Q_107, uri_rdfs_isDefinedBy, uri_rdfs_Resource), true)=true))). % 29.99/18.68 tff(c_18922, plain, (![X_381, Y_382]: (ifeq(iext(uri_rdfs_subClassOf, X_381, Y_382), true, icext(uri_rdfs_Class, X_381), true)=true))). % 29.99/18.68 tff(c_8864, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_member), true)=true))). % 29.99/18.68 tff(c_2964, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_107), true, iext(Q_107, uri_rdf_type, uri_rdfs_Class), true)=true))). % 29.99/18.68 tff(c_9702, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdfs_Container), true)=true))). % 29.99/18.68 tff(c_6410, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdfs_Datatype), true)=true))). % 29.99/18.68 tff(c_18797, plain, (![X_373, Y_374]: (ifeq(iext(uri_rdf_predicate, X_373, Y_374), true, icext(uri_rdfs_Statement, X_373), true)=true))). % 29.99/18.68 tff(c_6076, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf__2), true)=true))). % 29.99/18.68 tff(c_5378, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_value), true)=true))). % 29.99/18.68 tff(c_2934, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_107), true, iext(Q_107, uri_rdfs_ContainerMembershipProperty, uri_rdf_Property), true)=true))). % 29.99/18.68 tff(c_8458, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_subPropertyOf), true)=true))). % 29.99/18.68 tff(c_10465, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_foaf_mbox_sha1sum), true)=true))). % 29.99/18.68 tff(c_18612, plain, (![X_364, Y_365]: (ifeq(iext(uri_rdf_rest, X_364, Y_365), true, icext(uri_rdf_List, Y_365), true)=true))). % 29.99/18.68 tff(c_5750, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_first), true)=true))). % 29.99/18.68 tff(c_8388, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_type), true)=true))). % 29.99/18.68 tff(c_8931, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdfs_ContainerMembershipProperty), true)=true))). % 29.99/18.68 tff(c_2921, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_107), true, iext(Q_107, uri_rdf__2, uri_rdf_Property), true)=true))). % 29.99/18.68 tff(c_5857, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdf_Bag), true)=true))). % 29.99/18.68 tff(c_18111, plain, (![X_355, Y_356]: (ifeq(iext(uri_rdfs_subPropertyOf, X_355, Y_356), true, icext(uri_rdf_Property, X_355), true)=true))). % 29.99/18.68 tff(c_5688, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdf_Alt), true)=true))). % 29.99/18.68 tff(c_5176, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_subClassOf), true)=true))). % 29.99/18.68 tff(c_7121, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_object), true)=true))). % 29.99/18.68 tff(c_2952, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_107), true, iext(Q_107, uri_rdf_object, uri_rdfs_Statement), true)=true))). % 29.99/18.68 tff(c_6075, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf__2), true)=true))). % 29.99/18.68 tff(c_17646, plain, (![X_346, Y_347]: (ifeq(iext(uri_rdfs_range, X_346, Y_347), true, icext(uri_rdfs_Class, Y_347), true)=true))). % 29.99/18.68 tff(c_7449, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf__3), true)=true))). % 29.99/18.68 tff(c_2905, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_107), true, iext(Q_107, uri_rdf_rest, uri_rdf_Property), true)=true))). % 29.99/18.68 tff(c_6008, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdfs_Literal), true)=true))). % 29.99/18.68 tff(c_5622, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_seeAlso), true)=true))). % 29.99/18.68 tff(c_5937, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_range), true)=true))). % 29.99/18.68 tff(c_17485, plain, (![X_337, Y_338]: (ifeq(iext(uri_rdf_first, X_337, Y_338), true, icext(uri_rdf_List, X_337), true)=true))). % 29.99/18.68 tff(c_10625, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf__1), true)=true))). % 29.99/18.68 tff(c_2947, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_107), true, iext(Q_107, uri_rdf_Alt, uri_rdfs_Container), true)=true))). % 29.99/18.68 tff(c_8389, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_type), true)=true))). % 29.99/18.68 tff(c_5538, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_subject), true)=true))). % 29.99/18.68 tff(c_7216, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_domain), true)=true))). % 29.99/18.68 tff(c_17332, plain, (![X_328, Y_329]: (ifeq(iext(uri_rdfs_comment, X_328, Y_329), true, icext(uri_rdfs_Literal, Y_329), true)=true))). % 29.99/18.68 tff(c_5537, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_subject), true)=true))). % 29.99/18.68 tff(c_2935, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_107), true, iext(Q_107, uri_rdfs_subClassOf, uri_rdfs_Class), true)=true))). % 29.99/18.68 tff(c_5749, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_first), true)=true))). % 29.99/18.68 tff(c_7448, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf__3), true)=true))). % 29.99/18.69 tff(c_16723, plain, (![X_320, Y_321]: (ifeq(iext(uri_rdf_type, X_320, Y_321), true, icext(uri_rdfs_Class, Y_321), true)=true))). % 29.99/18.69 tff(c_10396, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdfs_Class), true)=true))). % 29.99/18.69 tff(c_5177, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_subClassOf), true)=true))). % 29.99/18.69 tff(c_1893, plain, (![C_93]: (ifeq(iext(uri_rdfs_range, uri_foaf_mbox_sha1sum, C_93), true, icext(C_93, literal_plain(dat_str_xyz)), true)=true))). % 29.99/18.69 tff(c_4742, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdfs_Resource), true)=true))). % 29.99/18.69 tff(c_4587, plain, (![C_19, X_131]: (ifeq(iext(uri_rdfs_domain, uri_rdf_type, C_19), true, icext(C_19, X_131), true)=true))). % 29.99/18.69 tff(c_4588, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_29), true, icext(C_29, uri_rdfs_Resource), true)=true))). % 29.99/18.69 tff(c_15917, plain, (![X_306, Y_307]: (ifeq(iext(uri_rdfs_subClassOf, X_306, Y_307), true, icext(uri_rdfs_Class, Y_307), true)=true))). % 29.99/18.69 tff(c_2309, plain, (![C_97]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_97), true, icext(C_97, uri_rdfs_ContainerMembershipProperty), true)=true))). % 29.99/18.69 tff(c_2298, plain, (![C_97]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_97), true, icext(C_97, uri_rdfs_label), true)=true))). % 29.99/18.69 tff(c_2310, plain, (![C_97]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_97), true, icext(C_97, uri_rdfs_subClassOf), true)=true))). % 29.99/18.69 tff(c_15698, plain, (![X_33]: (ifeq(icext(uri_owl_DatatypeProperty, X_33), true, icext(uri_owl_DatatypeProperty, X_33), true)=true))). % 29.99/18.69 tff(c_15642, plain, (iext(uri_rdfs_subClassOf, uri_owl_DatatypeProperty, uri_owl_DatatypeProperty)=true)). % 29.99/18.69 tff(c_15493, plain, (iext(uri_rdfs_subClassOf, uri_owl_DatatypeProperty, uri_rdfs_Resource)=true)). % 29.99/18.69 tff(c_15328, plain, (iext(uri_rdf_type, uri_owl_DatatypeProperty, uri_rdfs_Class)=true)). % 29.99/18.69 tff(c_15287, plain, (ic(uri_owl_DatatypeProperty)=true)). % 29.99/18.69 tff(c_2319, plain, (![C_97]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_97), true, icext(C_97, uri_rdf_value), true)=true))). % 29.99/18.69 tff(c_15196, plain, (icext(uri_rdfs_Class, uri_owl_DatatypeProperty)=true)). % 29.99/18.69 tff(c_1903, plain, (![C_93]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_93), true, icext(C_93, uri_owl_DatatypeProperty), true)=true))). % 29.99/18.69 tff(c_2287, plain, (![C_97]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_97), true, icext(C_97, uri_rdf_predicate), true)=true))). % 29.99/18.69 tff(c_2316, plain, (![C_97]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_97), true, icext(C_97, uri_rdfs_range), true)=true))). % 29.99/18.69 tff(c_2339, plain, (![C_97]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_97), true, icext(C_97, uri_rdf_first), true)=true))). % 29.99/18.69 tff(c_2342, plain, (![C_97]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_97), true, icext(C_97, uri_rdf_type), true)=true))). % 29.99/18.69 tff(c_2278, plain, (![C_97]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_97), true, icext(C_97, uri_rdfs_seeAlso), true)=true))). % 29.99/18.69 tff(c_14820, plain, (![X_283, Y_284]: (ifeq(iext(uri_rdf_rest, X_283, Y_284), true, icext(uri_rdf_List, X_283), true)=true))). % 29.99/18.69 tff(c_1962, plain, (![C_93]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_93), true, icext(C_93, uri_rdfs_Class), true)=true))). % 29.99/18.69 tff(c_2325, plain, (![C_97]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_97), true, icext(C_97, uri_rdfs_member), true)=true))). % 29.99/18.69 tff(c_2286, plain, (![C_97]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_97), true, icext(C_97, uri_rdf_subject), true)=true))). % 29.99/18.69 tff(c_1897, plain, (![C_93]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_93), true, icext(C_93, uri_rdfs_ContainerMembershipProperty), true)=true))). % 29.99/18.69 tff(c_2327, plain, (![C_97]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_97), true, icext(C_97, uri_rdf_type), true)=true))). % 29.99/18.69 tff(c_2341, plain, (![C_97]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_97), true, icext(C_97, uri_rdfs_subPropertyOf), true)=true))). % 29.99/18.69 tff(c_2289, plain, (![C_97]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_97), true, icext(C_97, uri_rdf__2), true)=true))). % 29.99/18.69 tff(c_2333, plain, (![C_97]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_97), true, icext(C_97, uri_rdfs_Datatype), true)=true))). % 29.99/18.69 tff(c_2330, plain, (![C_97]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_97), true, icext(C_97, uri_rdf_object), true)=true))). % 29.99/18.69 tff(c_2283, plain, (![C_97]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_97), true, icext(C_97, uri_rdf__3), true)=true))). % 29.99/18.69 tff(c_2328, plain, (![C_97]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_97), true, icext(C_97, uri_rdf_rest), true)=true))). % 29.99/18.69 tff(c_1894, plain, (![C_93]: (ifeq(iext(uri_rdfs_range, uri_rdfs_range, C_93), true, icext(C_93, uri_rdf_List), true)=true))). % 29.99/18.69 tff(c_2270, plain, (![C_97]: (ifeq(iext(uri_rdfs_domain, uri_foaf_mbox_sha1sum, C_97), true, icext(C_97, uri_ex_robert), true)=true))). % 29.99/18.69 tff(c_1963, plain, (![C_93]: (ifeq(iext(uri_rdfs_range, uri_rdfs_domain, C_93), true, icext(C_93, uri_rdf_Property), true)=true))). % 29.99/18.69 tff(c_14377, plain, (![X_263, Y_264]: (ifeq(iext(uri_rdfs_label, X_263, Y_264), true, icext(uri_rdfs_Literal, Y_264), true)=true))). % 29.99/18.69 tff(c_1954, plain, (![C_93]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_93), true, icext(C_93, uri_rdfs_Class), true)=true))). % 29.99/18.69 tff(c_1912, plain, (![C_93]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_93), true, icext(C_93, uri_rdfs_Literal), true)=true))). % 29.99/18.69 tff(c_2317, plain, (![C_97]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_97), true, icext(C_97, uri_rdfs_domain), true)=true))). % 29.99/18.69 tff(c_2329, plain, (![C_97]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_97), true, icext(C_97, uri_rdfs_range), true)=true))). % 29.99/18.69 tff(c_1956, plain, (![C_93]: (ifeq(iext(uri_rdfs_range, uri_rdfs_domain, C_93), true, icext(C_93, uri_rdf_List), true)=true))). % 29.99/18.69 tff(c_2320, plain, (![C_97]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_97), true, icext(C_97, uri_rdfs_member), true)=true))). % 29.99/18.69 tff(c_2288, plain, (![C_97]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_97), true, icext(C_97, uri_rdf_XMLLiteral), true)=true))). % 29.99/18.69 tff(c_2285, plain, (![C_97]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_97), true, icext(C_97, uri_rdfs_label), true)=true))). % 29.99/18.69 tff(c_2308, plain, (![C_97]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_97), true, icext(C_97, uri_rdf__2), true)=true))). % 29.99/18.69 tff(c_1896, plain, (![C_93]: (ifeq(iext(uri_rdfs_range, uri_rdfs_range, C_93), true, icext(C_93, uri_rdf_Property), true)=true))). % 29.99/18.69 tff(c_2290, plain, (![C_97]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_97), true, icext(C_97, uri_rdfs_isDefinedBy), true)=true))). % 29.99/18.69 tff(c_2274, plain, (![C_97]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_97), true, icext(C_97, uri_rdfs_subPropertyOf), true)=true))). % 29.99/18.69 tff(c_1924, plain, (![C_93]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_93), true, icext(C_93, uri_rdfs_seeAlso), true)=true))). % 29.99/18.69 tff(c_1943, plain, (![C_93]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_93), true, icext(C_93, uri_rdfs_Datatype), true)=true))). % 29.99/18.69 tff(c_11778, plain, (![X_33]: (ifeq(icext(uri_rdfs_Statement, X_33), true, icext(uri_rdfs_Statement, X_33), true)=true))). % 29.99/18.69 tff(c_13587, plain, (![X_33]: (ifeq(icext(uri_owl_InverseFunctionalProperty, X_33), true, icext(uri_owl_InverseFunctionalProperty, X_33), true)=true))). % 29.99/18.69 tff(c_12764, plain, (![X_236, Y_237]: (ifeq(iext(uri_rdfs_range, X_236, Y_237), true, icext(uri_rdf_Property, X_236), true)=true))). % 29.99/18.69 tff(c_11712, plain, (![X_33]: (ifeq(icext(uri_rdf_List, X_33), true, icext(uri_rdf_List, X_33), true)=true))). % 29.99/18.69 tff(c_7385, plain, (![X_33]: (ifeq(icext(uri_rdf_Property, X_33), true, icext(uri_rdf_Property, X_33), true)=true))). % 29.99/18.69 tff(c_5689, plain, (![X_33]: (ifeq(icext(uri_rdf_Alt, X_33), true, icext(uri_rdf_Alt, X_33), true)=true))). % 29.99/18.69 tff(c_2299, plain, (![C_97]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_97), true, icext(C_97, uri_rdfs_isDefinedBy), true)=true))). % 29.99/18.69 tff(c_9266, plain, (![X_33]: (ifeq(icext(uri_rdfs_Seq, X_33), true, icext(uri_rdfs_Seq, X_33), true)=true))). % 29.99/18.69 tff(c_10557, plain, (![X_33]: (ifeq(icext(uri_rdf_XMLLiteral, X_33), true, icext(uri_rdf_XMLLiteral, X_33), true)=true))). % 29.99/18.69 tff(c_13597, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_label, uri_rdfs_label)=true)). % 29.99/18.69 tff(c_13531, plain, (iext(uri_rdfs_subClassOf, uri_owl_InverseFunctionalProperty, uri_owl_InverseFunctionalProperty)=true)). % 29.99/18.69 tff(c_13390, plain, (iext(uri_rdfs_subClassOf, uri_owl_InverseFunctionalProperty, uri_rdfs_Resource)=true)). % 29.99/18.69 tff(c_13343, plain, (iext(uri_rdf_type, uri_owl_InverseFunctionalProperty, uri_rdfs_Class)=true)). % 29.99/18.69 tff(c_13191, plain, (ic(uri_owl_InverseFunctionalProperty)=true)). % 29.99/18.69 tff(c_13125, plain, (icext(uri_rdfs_Class, uri_owl_InverseFunctionalProperty)=true)). % 29.99/18.69 tff(c_13083, plain, (ip(uri_rdfs_label)=true)). % 29.99/18.69 tff(c_1935, plain, (![C_93]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_93), true, icext(C_93, uri_owl_InverseFunctionalProperty), true)=true))). % 29.99/18.69 tff(c_13006, plain, (iext(uri_rdf_type, uri_rdfs_label, uri_rdf_Property)=true)). % 29.99/18.69 tff(c_12848, plain, (icext(uri_rdf_Property, uri_rdfs_label)=true)). % 29.99/18.69 tff(c_4915, plain, (![X_33]: (ifeq(icext(uri_rdfs_Container, X_33), true, icext(uri_rdfs_Container, X_33), true)=true))). % 29.99/18.69 tff(c_5858, plain, (![X_33]: (ifeq(icext(uri_rdf_Bag, X_33), true, icext(uri_rdf_Bag, X_33), true)=true))). % 29.99/18.69 tff(c_10398, plain, (![X_33]: (ifeq(icext(uri_rdfs_Class, X_33), true, icext(uri_rdfs_Class, X_33), true)=true))). % 29.99/18.69 tff(c_6411, plain, (![X_33]: (ifeq(icext(uri_rdfs_Datatype, X_33), true, icext(uri_rdfs_Datatype, X_33), true)=true))). % 29.99/18.69 tff(c_8932, plain, (![X_33]: (ifeq(icext(uri_rdfs_ContainerMembershipProperty, X_33), true, icext(uri_rdfs_ContainerMembershipProperty, X_33), true)=true))). % 29.99/18.69 tff(c_6010, plain, (![X_33]: (ifeq(icext(uri_rdfs_Literal, X_33), true, icext(uri_rdfs_Literal, X_33), true)=true))). % 29.99/18.69 tff(c_12474, plain, (iext(uri_rdf_type, uri_rdfs_Resource, uri_rdfs_Class)=true)). % 29.99/18.69 tff(c_12409, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_predicate, uri_rdf_predicate)=true)). % 29.99/18.69 tff(c_12343, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_comment, uri_rdfs_comment)=true)). % 29.99/18.69 tff(c_12274, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_member, uri_rdfs_member)=true)). % 29.99/18.69 tff(c_2297, plain, (![C_97]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_97), true, icext(C_97, uri_rdfs_domain), true)=true))). % 29.99/18.69 tff(c_12172, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Resource, uri_rdfs_Resource)=true)). % 29.99/18.69 tff(c_12017, plain, (icext(uri_rdf_Property, uri_rdfs_member)=true)). % 29.99/18.69 tff(c_11934, plain, (iext(uri_rdf_type, uri_rdfs_member, uri_rdf_Property)=true)). % 29.99/18.69 tff(c_2305, plain, (![C_97]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_97), true, icext(C_97, uri_rdf__1), true)=true))). % 29.99/18.69 tff(c_11816, plain, (iext(uri_rdfs_subClassOf, uri_rdf_List, uri_rdfs_Resource)=true)). % 29.99/18.69 tff(c_1959, plain, (![C_93]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_93), true, icext(C_93, uri_rdfs_Container), true)=true))). % 29.99/18.69 tff(c_11722, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Statement, uri_rdfs_Statement)=true)). % 29.99/18.69 tff(c_11656, plain, (iext(uri_rdfs_subClassOf, uri_rdf_List, uri_rdf_List)=true)). % 29.99/18.69 tff(c_2331, plain, (![C_97]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_97), true, icext(C_97, uri_rdfs_comment), true)=true))). % 29.99/18.69 tff(c_11517, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Statement, uri_rdfs_Resource)=true)). % 29.99/18.69 tff(c_11467, plain, (iext(uri_rdf_type, uri_rdf_Bag, uri_rdfs_Class)=true)). % 29.99/18.69 tff(c_2295, plain, (![C_97]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_97), true, icext(C_97, uri_rdf__3), true)=true))). % 29.99/18.69 tff(c_11391, plain, (iext(uri_rdf_type, uri_rdf_XMLLiteral, uri_rdfs_Class)=true)). % 29.99/18.69 tff(c_11344, plain, (iext(uri_rdf_type, uri_rdfs_Datatype, uri_rdfs_Class)=true)). % 29.99/18.69 tff(c_11297, plain, (iext(uri_rdf_type, uri_rdfs_Container, uri_rdfs_Class)=true)). % 29.99/18.69 tff(c_11243, plain, (iext(uri_rdf_type, uri_rdfs_Seq, uri_rdfs_Class)=true)). % 29.99/18.69 tff(c_11171, plain, (iext(uri_rdf_type, uri_rdfs_Class, uri_rdfs_Class)=true)). % 29.99/18.69 tff(c_11123, plain, (iext(uri_rdf_type, uri_rdfs_Literal, uri_rdfs_Class)=true)). % 29.99/18.69 tff(c_2280, plain, (![C_97]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_97), true, icext(C_97, uri_rdf_value), true)=true))). % 29.99/18.69 tff(c_11050, plain, (iext(uri_rdf_type, uri_rdfs_ContainerMembershipProperty, uri_rdfs_Class)=true)). % 29.99/18.69 tff(c_11003, plain, (iext(uri_rdf_type, uri_rdf_Alt, uri_rdfs_Class)=true)). % 29.99/18.69 tff(c_10925, plain, (iext(uri_rdf_type, uri_rdf_List, uri_rdfs_Class)=true)). % 29.99/18.69 tff(c_10884, plain, (ip(uri_rdf_predicate)=true)). % 29.99/18.69 tff(c_10831, plain, (iext(uri_rdf_type, uri_rdf_predicate, uri_rdf_Property)=true)). % 29.99/18.69 tff(c_2332, plain, (![C_97]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_97), true, icext(C_97, uri_rdfs_seeAlso), true)=true))). % 29.99/18.69 tff(c_10759, plain, (iext(uri_rdf_type, uri_rdfs_Statement, uri_rdfs_Class)=true)). % 29.99/18.69 tff(c_10717, plain, (ip(uri_rdfs_comment)=true)). % 29.99/18.69 tff(c_10660, plain, (iext(uri_rdf_type, uri_rdfs_comment, uri_rdf_Property)=true)). % 29.99/18.69 tff(c_10570, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf__1, uri_rdf__1)=true)). % 29.99/18.69 tff(c_10501, plain, (iext(uri_rdfs_subClassOf, uri_rdf_XMLLiteral, uri_rdf_XMLLiteral)=true)). % 29.99/18.69 tff(c_1931, plain, (![C_93]: (ifeq(iext(uri_rdfs_range, uri_rdfs_domain, C_93), true, icext(C_93, uri_rdfs_Class), true)=true))). % 29.99/18.69 tff(c_10410, plain, (iext(uri_rdfs_subPropertyOf, uri_foaf_mbox_sha1sum, uri_foaf_mbox_sha1sum)=true)). % 29.99/18.69 tff(c_10342, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Class, uri_rdfs_Class)=true)). % 29.99/18.69 tff(c_1029, plain, (![S_5, O_6]: (ifeq(iext(uri_rdfs_range, S_5, O_6), true, true, true)=true))). % 29.99/18.69 tff(c_10114, plain, (icext(uri_rdf_Property, uri_rdfs_subPropertyOf)=true)). % 29.99/18.69 tff(c_10036, plain, (iext(uri_rdf_type, uri_rdfs_subPropertyOf, uri_rdf_Property)=true)). % 29.99/18.69 tff(c_2293, plain, (![C_97]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_97), true, icext(C_97, uri_rdfs_Seq), true)=true))). % 29.99/18.69 tff(c_9892, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Class, uri_rdfs_Resource)=true)). % 29.99/18.69 tff(c_9754, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Bag, uri_rdfs_Resource)=true)). % 29.99/18.69 tff(c_9648, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Container, uri_rdfs_Resource)=true)). % 29.99/18.69 tff(c_2323, plain, (![C_97]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_97), true, icext(C_97, uri_rdf_Alt), true)=true))). % 29.99/18.69 tff(c_9551, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf__3, uri_rdfs_member)=true)). % 29.99/18.69 tff(c_9397, plain, (icext(uri_rdf_Property, uri_rdfs_range)=true)). % 29.99/18.69 tff(c_9343, plain, (iext(uri_rdf_type, uri_rdfs_range, uri_rdf_Property)=true)). % 29.99/18.69 tff(c_1902, plain, (![C_93]: (ifeq(iext(uri_rdfs_range, uri_rdfs_range, C_93), true, icext(C_93, uri_rdfs_Resource), true)=true))). % 29.99/18.69 tff(c_2363, plain, (![S_5, O_6]: (ifeq(iext(uri_rdf_rest, S_5, O_6), true, true, true)=true))). % 29.99/18.69 tff(c_2315, plain, (![C_97]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_97), true, icext(C_97, uri_rdfs_subClassOf), true)=true))). % 29.99/18.69 tff(c_9210, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Seq, uri_rdfs_Seq)=true)). % 29.99/18.69 tff(c_9143, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_rest, uri_rdf_rest)=true)). % 29.99/18.69 tff(c_9027, plain, (icext(uri_rdf_Property, uri_rdfs_seeAlso)=true)). % 29.99/18.69 tff(c_8973, plain, (iext(uri_rdf_type, uri_rdfs_seeAlso, uri_rdf_Property)=true)). % 29.99/18.69 tff(c_1930, plain, (![C_93]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_93), true, icext(C_93, uri_rdf_Property), true)=true))). % 29.99/18.69 tff(c_8876, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, uri_rdfs_ContainerMembershipProperty)=true)). % 29.99/18.69 tff(c_8809, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf__2, uri_rdfs_member)=true)). % 29.99/18.69 tff(c_3317, plain, (![S_5, O_6]: (ifeq(iext(uri_rdfs_subPropertyOf, S_5, O_6), true, true, true)=true))). % 30.14/18.69 tff(c_8621, plain, (icext(uri_rdf_Property, uri_rdfs_subClassOf)=true)). % 30.14/18.69 tff(c_8543, plain, (iext(uri_rdf_type, uri_rdfs_subClassOf, uri_rdf_Property)=true)). % 30.14/18.69 tff(c_2303, plain, (![C_97]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_97), true, icext(C_97, uri_rdfs_isDefinedBy), true)=true))). % 30.14/18.69 tff(c_8404, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf)=true)). % 30.14/18.69 tff(c_8307, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_type, uri_rdf_type)=true)). % 30.14/18.69 tff(c_2312, plain, (![C_97]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_97), true, icext(C_97, uri_rdf__1), true)=true))). % 30.14/18.69 tff(c_786, plain, (![S_5, O_6]: (ifeq(iext(uri_rdfs_domain, S_5, O_6), true, true, true)=true))). % 30.14/18.69 tff(c_2338, plain, (![C_97]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_97), true, icext(C_97, uri_rdf_Bag), true)=true))). % 30.14/18.69 tff(c_8035, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Property, uri_rdfs_Resource)=true)). % 30.14/18.69 tff(c_7953, plain, (iext(uri_rdfs_subClassOf, uri_rdf_XMLLiteral, uri_rdfs_Resource)=true)). % 30.14/18.69 tff(c_1946, plain, (![C_93]: (ifeq(iext(uri_rdfs_range, uri_rdfs_domain, C_93), true, icext(C_93, uri_rdfs_Resource), true)=true))). % 30.14/18.69 tff(c_2335, plain, (![C_97]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_97), true, icext(C_97, uri_rdf_first), true)=true))). % 30.14/18.69 tff(c_7683, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_isDefinedBy, uri_rdfs_isDefinedBy)=true)). % 30.14/18.69 tff(c_7579, plain, (icext(uri_rdf_Property, uri_foaf_mbox_sha1sum)=true)). % 30.14/18.69 tff(c_7521, plain, (iext(uri_rdf_type, uri_foaf_mbox_sha1sum, uri_rdf_Property)=true)). % 30.14/18.69 tff(c_1107, plain, (![S_5, O_6]: (ifeq(iext(uri_rdfs_subClassOf, S_5, O_6), true, true, true)=true))). % 30.14/18.69 tff(c_7395, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf__3, uri_rdf__3)=true)). % 30.14/18.69 tff(c_7308, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Property, uri_rdf_Property)=true)). % 30.14/18.69 tff(c_7163, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, uri_rdfs_domain)=true)). % 30.14/18.69 tff(c_2272, plain, (![C_97]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_97), true, icext(C_97, uri_rdf_rest), true)=true))). % 30.14/18.69 tff(c_7071, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_object, uri_rdf_object)=true)). % 30.14/18.69 tff(c_6981, plain, (icext(uri_rdf_Property, uri_rdfs_comment)=true)). % 30.14/18.69 tff(c_2301, plain, (![C_97]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_97), true, icext(C_97, uri_rdfs_comment), true)=true))). % 30.14/18.69 tff(c_6920, plain, (ic(uri_rdf_List)=true)). % 30.14/18.69 tff(c_6871, plain, (icext(uri_rdfs_Class, uri_rdf_List)=true)). % 30.14/18.69 tff(c_1958, plain, (![C_93]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_93), true, icext(C_93, uri_rdf_List), true)=true))). % 30.14/18.69 tff(c_6790, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, uri_rdfs_Resource)=true)). % 30.14/18.69 tff(c_742, plain, (![S_5, O_6]: (ifeq(iext(uri_foaf_mbox_sha1sum, S_5, O_6), true, true, true)=true))). % 30.14/18.69 tff(c_6688, plain, (icext(uri_rdf_Property, uri_rdf_predicate)=true)). % 30.14/18.69 tff(c_2314, plain, (![C_97]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_97), true, icext(C_97, uri_rdf_predicate), true)=true))). % 30.14/18.69 tff(c_6607, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Seq, uri_rdfs_Resource)=true)). % 30.14/18.69 tff(c_6454, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Literal, uri_rdfs_Resource)=true)). % 30.14/18.69 tff(c_1964, plain, (![C_93]: (ifeq(iext(uri_rdfs_range, uri_rdfs_range, C_93), true, icext(C_93, uri_rdfs_Class), true)=true))). % 30.14/18.69 tff(c_3221, plain, (![S_5, O_6]: (ifeq(iext(uri_rdf_object, S_5, O_6), true, true, true)=true))). % 30.14/18.69 tff(c_6359, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, uri_rdfs_Datatype)=true)). % 30.14/18.69 tff(c_1951, plain, (![C_93]: (ifeq(iext(uri_rdfs_range, uri_rdfs_range, C_93), true, icext(C_93, uri_rdfs_Literal), true)=true))). % 30.14/18.69 tff(c_6265, plain, (ip(uri_rdfs_member)=true)). % 30.14/18.69 tff(c_6205, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf__1, uri_rdfs_member)=true)). % 30.14/18.70 tff(c_6153, plain, (ic(uri_rdfs_Statement)=true)). % 30.14/18.70 tff(c_6104, plain, (icext(uri_rdfs_Class, uri_rdfs_Statement)=true)). % 30.14/18.70 tff(c_1950, plain, (![C_93]: (ifeq(iext(uri_rdfs_range, uri_rdfs_domain, C_93), true, icext(C_93, uri_rdfs_Statement), true)=true))). % 30.14/18.70 tff(c_6025, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf__2, uri_rdf__2)=true)). % 30.14/18.70 tff(c_5951, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Literal, uri_rdfs_Literal)=true)). % 30.14/18.70 tff(c_5868, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_range, uri_rdfs_range)=true)). % 30.14/18.70 tff(c_2271, plain, (![C_97]: (ifeq(iext(uri_rdfs_domain, uri_foaf_mbox_sha1sum, C_97), true, icext(C_97, uri_ex_bob), true)=true))). % 30.14/18.70 tff(c_5806, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Bag, uri_rdf_Bag)=true)). % 30.14/18.70 tff(c_2276, plain, (![C_97]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_97), true, icext(C_97, uri_rdf_subject), true)=true))). % 30.14/18.70 tff(c_5699, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_first, uri_rdf_first)=true)). % 30.14/18.70 tff(c_5637, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Alt, uri_rdf_Alt)=true)). % 30.14/18.70 tff(c_5548, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_seeAlso, uri_rdfs_seeAlso)=true)). % 30.14/18.70 tff(c_1918, plain, (![C_93]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_93), true, icext(C_93, uri_rdf_Property), true)=true))). % 30.14/18.70 tff(c_5487, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_subject, uri_rdf_subject)=true)). % 30.14/18.70 tff(c_1628, plain, (![X_90]: (ifeq(icext(uri_rdfs_ContainerMembershipProperty, X_90), true, icext(uri_rdf_Property, X_90), true)=true))). % 30.14/18.70 tff(c_5328, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_value, uri_rdf_value)=true)). % 30.14/18.70 tff(c_1630, plain, (![X_90]: (ifeq(icext(uri_rdfs_Datatype, X_90), true, icext(uri_rdfs_Class, X_90), true)=true))). % 30.14/18.70 tff(c_5201, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Alt, uri_rdfs_Resource)=true)). % 30.14/18.70 tff(c_5119, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, uri_rdfs_subClassOf)=true)). % 30.14/18.70 tff(c_1631, plain, (![X_90]: (ifeq(icext(uri_rdf_Bag, X_90), true, icext(uri_rdfs_Container, X_90), true)=true))). % 30.14/18.70 tff(c_5081, plain, (icext(uri_rdf_Property, uri_rdfs_domain)=true)). % 30.14/18.70 tff(c_5028, plain, (iext(uri_rdf_type, uri_rdfs_domain, uri_rdf_Property)=true)). % 30.14/18.70 tff(c_1627, plain, (![X_90]: (ifeq(icext(uri_rdfs_Seq, X_90), true, icext(uri_rdfs_Container, X_90), true)=true))). % 30.14/18.70 tff(c_4982, plain, (icext(uri_rdf_Property, uri_rdfs_isDefinedBy)=true)). % 30.14/18.70 tff(c_4925, plain, (iext(uri_rdf_type, uri_rdfs_isDefinedBy, uri_rdf_Property)=true)). % 30.14/18.70 tff(c_4863, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Container, uri_rdfs_Container)=true)). % 30.14/18.70 tff(c_1626, plain, (![X_90]: (ifeq(icext(uri_rdf_XMLLiteral, X_90), true, icext(uri_rdfs_Literal, X_90), true)=true))). % 30.14/18.70 tff(c_4794, plain, (icext(uri_rdfs_Class, uri_rdfs_Resource)=true)). % 30.14/18.70 tff(c_4759, plain, (ic(uri_rdfs_Resource)=true)). % 30.14/18.70 tff(c_1629, plain, (![X_90]: (ifeq(icext(uri_rdf_Alt, X_90), true, icext(uri_rdfs_Container, X_90), true)=true))). % 30.14/18.70 tff(c_4691, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, uri_rdfs_Resource)=true)). % 30.14/18.70 tff(c_1910, plain, (![X_94, Y_95]: (ifeq(iext(uri_rdf_predicate, X_94, Y_95), true, true, true)=true))). % 30.14/18.70 tff(c_2326, plain, (![X_98, Y_99]: (ifeq(iext(uri_rdf_type, X_98, Y_99), true, true, true)=true))). % 30.14/18.70 tff(c_2300, plain, (![X_98, Y_99]: (ifeq(iext(uri_rdfs_comment, X_98, Y_99), true, true, true)=true))). % 30.14/18.70 tff(c_1960, plain, (![X_94, Y_95]: (ifeq(iext(uri_rdf_first, X_94, Y_95), true, true, true)=true))). % 30.14/18.70 tff(c_4549, plain, (![X_130]: (iext(uri_rdf_type, X_130, uri_rdfs_Resource)=true))). % 30.14/18.70 tff(c_2277, plain, (![X_98, Y_99]: (ifeq(iext(uri_rdfs_seeAlso, X_98, Y_99), true, true, true)=true))). % 30.14/18.70 tff(c_1908, plain, (![X_94, Y_95]: (ifeq(iext(uri_rdf_subject, X_94, Y_95), true, true, true)=true))). % 30.14/18.70 tff(c_1913, plain, (![X_94, Y_95]: (ifeq(iext(uri_rdf__2, X_94, Y_95), true, true, true)=true))). % 30.14/18.70 tff(c_1933, plain, (![X_94, Y_95]: (ifeq(iext(uri_rdf__1, X_94, Y_95), true, true, true)=true))). % 30.14/18.70 tff(c_1941, plain, (![X_94, Y_95]: (ifeq(iext(uri_rdfs_member, X_94, Y_95), true, true, true)=true))). % 30.14/18.70 tff(c_4444, plain, (icext(uri_rdfs_Class, uri_rdfs_Datatype)=true)). % 30.14/18.70 tff(c_2284, plain, (![X_98, Y_99]: (ifeq(iext(uri_rdfs_label, X_98, Y_99), true, true, true)=true))). % 30.14/18.70 tff(c_4392, plain, (icext(uri_rdfs_Class, uri_rdfs_Class)=true)). % 30.14/18.70 tff(c_4340, plain, (icext(uri_rdfs_Class, uri_rdf_XMLLiteral)=true)). % 30.14/18.70 tff(c_1901, plain, (![X_94, Y_95]: (ifeq(iext(uri_rdf_value, X_94, Y_95), true, true, true)=true))). % 30.14/18.70 tff(c_4287, plain, (icext(uri_rdfs_Class, uri_rdf_Bag)=true)). % 30.14/18.70 tff(c_4242, plain, (icext(uri_rdfs_Class, uri_rdfs_Container)=true)). % 30.14/18.70 tff(c_2302, plain, (![X_98, Y_99]: (ifeq(iext(uri_rdfs_isDefinedBy, X_98, Y_99), true, true, true)=true))). % 30.14/18.70 tff(c_4184, plain, (icext(uri_rdfs_Class, uri_rdfs_ContainerMembershipProperty)=true)). % 30.14/18.70 tff(c_4138, plain, (icext(uri_rdfs_Class, uri_rdfs_Literal)=true)). % 30.14/18.70 tff(c_1905, plain, (![X_94, Y_95]: (ifeq(iext(uri_rdf__3, X_94, Y_95), true, true, true)=true))). % 30.14/18.70 tff(c_4084, plain, (icext(uri_rdfs_Class, uri_rdfs_Seq)=true)). % 30.14/18.70 tff(c_4037, plain, (icext(uri_rdfs_Class, uri_rdf_Alt)=true)). % 30.14/18.70 tff(c_3992, plain, (icext(uri_owl_DatatypeProperty, uri_foaf_mbox_sha1sum)=true)). % 30.14/18.70 tff(c_3953, plain, (icext(uri_rdf_Property, uri_rdf__1)=true)). % 30.14/18.70 tff(c_3915, plain, (icext(uri_rdf_Property, uri_rdf__3)=true)). % 30.14/18.70 tff(c_3873, plain, (icext(uri_rdfs_ContainerMembershipProperty, uri_rdf__2)=true)). % 30.14/18.70 tff(c_3833, plain, (icext(uri_rdf_Property, uri_rdf__2)=true)). % 30.14/18.70 tff(c_3782, plain, (icext(uri_rdfs_Class, uri_rdf_Property)=true)). % 30.14/18.70 tff(c_3743, plain, (icext(uri_rdf_Property, uri_rdf_subject)=true)). % 30.14/18.70 tff(c_3700, plain, (icext(uri_rdfs_Datatype, uri_rdf_XMLLiteral)=true)). % 30.14/18.70 tff(c_3663, plain, (icext(uri_rdf_Property, uri_rdf_first)=true)). % 30.14/18.70 tff(c_3597, plain, (icext(uri_rdf_Property, uri_rdf_rest)=true)). % 30.14/18.70 tff(c_3583, plain, (icext(uri_rdf_Property, uri_rdf_object)=true)). % 30.14/18.70 tff(c_3543, plain, (icext(uri_owl_InverseFunctionalProperty, uri_foaf_mbox_sha1sum)=true)). % 30.14/18.70 tff(c_3503, plain, (icext(uri_rdf_Property, uri_rdf_type)=true)). % 30.14/18.70 tff(c_3459, plain, (icext(uri_rdfs_ContainerMembershipProperty, uri_rdf__3)=true)). % 30.14/18.70 tff(c_3415, plain, (icext(uri_rdfs_ContainerMembershipProperty, uri_rdf__1)=true)). % 30.14/18.70 tff(c_3374, plain, (icext(uri_rdf_List, uri_rdf_nil)=true)). % 30.14/18.70 tff(c_3333, plain, (icext(uri_rdf_Property, uri_rdf_value)=true)). % 30.14/18.70 tff(c_3289, plain, (ip(uri_rdfs_subPropertyOf)=true)). % 30.14/18.70 tff(c_3235, plain, (ic(uri_rdf_XMLLiteral)=true)). % 30.14/18.70 tff(c_3194, plain, (ip(uri_rdf_object)=true)). % 30.14/18.70 tff(c_3153, plain, (ip(uri_rdf_subject)=true)). % 30.14/18.70 tff(c_3115, plain, (ic(uri_rdfs_Literal)=true)). % 30.14/18.70 tff(c_3078, plain, (ic(uri_rdf_Property)=true)). % 30.14/18.70 tff(c_3039, plain, (ic(uri_rdfs_Datatype)=true)). % 30.14/18.70 tff(c_2998, plain, (ip(uri_rdfs_seeAlso)=true)). % 30.14/18.70 tff(c_2499, plain, (ip(uri_rdf__3)=true)). % 30.14/18.70 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))). % 30.14/18.70 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))). % 30.14/18.70 tff(c_2377, plain, (ip(uri_rdf_value)=true)). % 30.14/18.70 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))). % 30.14/18.70 tff(c_2004, plain, (ip(uri_rdf_rest)=true)). % 30.14/18.70 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))). % 30.14/18.70 tff(c_1968, plain, (ic(uri_rdfs_Container)=true)). % 30.14/18.70 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))). % 30.14/18.70 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))). % 30.14/18.70 tff(c_1562, plain, (ic(uri_rdfs_Class)=true)). % 30.14/18.70 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))). % 30.14/18.70 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))). % 30.14/18.70 tff(c_1452, plain, (ip(uri_rdfs_isDefinedBy)=true)). % 30.14/18.70 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))). % 30.14/18.70 tff(c_1352, plain, (ip(uri_rdf__2)=true)). % 30.14/18.70 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))). % 30.14/18.70 tff(c_1244, plain, (ic(uri_rdf_Alt)=true)). % 30.14/18.70 tff(c_28, plain, (![P_9]: (ifeq(ip(P_9), true, iext(uri_rdf_type, P_9, uri_rdf_Property), true)=true))). % 30.14/18.70 tff(c_150, plain, (![C_35, D_36]: (ifeq(iext(uri_rdfs_subClassOf, C_35, D_36), true, ic(D_36), true)=true))). % 30.14/18.70 tff(c_1165, plain, (ic(uri_rdfs_ContainerMembershipProperty)=true)). % 30.14/18.70 tff(c_1133, plain, (ic(uri_rdfs_Seq)=true)). % 30.14/18.70 tff(c_156, plain, (![C_39]: (ifeq(ic(C_39), true, iext(uri_rdfs_subClassOf, C_39, C_39), true)=true))). % 30.14/18.70 tff(c_1083, plain, (ip(uri_rdfs_subClassOf)=true)). % 30.14/18.70 tff(c_162, plain, (![P_43, Q_44]: (ifeq(iext(uri_rdfs_subPropertyOf, P_43, Q_44), true, ip(Q_44), true)=true))). % 30.14/18.70 tff(c_1008, plain, (ip(uri_rdfs_range)=true)). % 30.14/18.70 tff(c_58, plain, (![C_15]: (ifeq(ic(C_15), true, iext(uri_rdfs_subClassOf, C_15, uri_rdfs_Resource), true)=true))). % 30.14/18.70 tff(c_948, plain, (ip(uri_rdf__1)=true)). % 30.14/18.70 tff(c_170, plain, (![P_51]: (ifeq(ip(P_51), true, iext(uri_rdfs_subPropertyOf, P_51, P_51), true)=true))). % 30.14/18.70 tff(c_922, plain, (ic(uri_rdf_Bag)=true)). % 30.14/18.70 tff(c_152, plain, (![C_37, D_38]: (ifeq(iext(uri_rdfs_subClassOf, C_37, D_38), true, ic(C_37), true)=true))). % 30.14/18.70 tff(c_870, plain, (ip(uri_rdf_first)=true)). % 30.14/18.70 tff(c_30, plain, (![P_10]: (ifeq(iext(uri_rdf_type, P_10, uri_rdf_Property), true, ip(P_10), true)=true))). % 30.14/18.70 tff(c_794, plain, (ip(uri_rdf_type)=true)). % 30.14/18.70 tff(c_771, plain, (ip(uri_rdfs_domain)=true)). % 30.14/18.70 tff(c_164, plain, (![P_45, Q_46]: (ifeq(iext(uri_rdfs_subPropertyOf, P_45, Q_46), true, ip(P_45), true)=true))). % 30.14/18.70 tff(c_730, plain, (ip(uri_foaf_mbox_sha1sum)=true)). % 30.14/18.70 tff(c_4, plain, (![P_4, S_5, O_6]: (ifeq(iext(P_4, S_5, O_6), true, ip(P_4), true)=true))). % 30.14/18.70 tff(c_114, plain, (![X_22]: (ifeq(ic(X_22), true, icext(uri_rdfs_Class, X_22), true)=true))). % 30.14/18.70 tff(c_124, plain, (![X_27]: (ifeq(lv(X_27), true, icext(uri_rdfs_Literal, X_27), true)=true))). % 30.14/18.70 tff(c_116, plain, (![X_23]: (ifeq(icext(uri_rdfs_Class, X_23), true, ic(X_23), true)=true))). % 30.14/18.70 tff(c_483, plain, (![X_61]: (icext(uri_rdfs_Resource, X_61)=true))). % 30.14/18.70 tff(c_122, plain, (![X_26]: (ifeq(icext(uri_rdfs_Literal, X_26), true, lv(X_26), true)=true))). % 30.14/18.70 tff(c_195, plain, (![X_8]: (ifeq(lv(X_8), true, true, true)=true))). % 30.14/18.70 tff(c_2, plain, (![A_1, B_2, C_3]: (ifeq(A_1, A_1, B_2, C_3)=B_2))). % 30.14/18.70 tff(c_182, plain, (iext(uri_foaf_mbox_sha1sum, uri_ex_robert, literal_plain(dat_str_xyz))=true)). % 30.14/18.70 tff(c_184, plain, (iext(uri_foaf_mbox_sha1sum, uri_ex_bob, literal_plain(dat_str_xyz))=true)). % 30.14/18.70 tff(c_66, plain, (iext(uri_rdfs_range, uri_rdf_rest, uri_rdf_List)=true)). % 30.14/18.70 tff(c_14, plain, (iext(uri_rdf_type, uri_rdf_rest, uri_rdf_Property)=true)). % 30.14/18.70 tff(c_168, plain, (iext(uri_rdfs_range, uri_rdfs_subPropertyOf, uri_rdf_Property)=true)). % 30.14/18.70 tff(c_94, plain, (iext(uri_rdf_type, uri_rdf__2, uri_rdfs_ContainerMembershipProperty)=true)). % 30.14/18.70 tff(c_142, plain, (iext(uri_rdfs_domain, uri_rdf_subject, uri_rdfs_Statement)=true)). % 30.14/18.70 tff(c_50, plain, (iext(uri_rdfs_domain, uri_rdfs_seeAlso, uri_rdfs_Resource)=true)). % 30.14/18.70 tff(c_96, plain, (iext(uri_rdf_type, uri_rdf__3, uri_rdfs_ContainerMembershipProperty)=true)). % 30.14/18.70 tff(c_180, plain, (iext(uri_rdfs_range, uri_rdf_value, uri_rdfs_Resource)=true)). % 30.14/18.70 tff(c_186, plain, (iext(uri_rdf_type, uri_foaf_mbox_sha1sum, uri_owl_DatatypeProperty)=true)). % 30.14/18.70 tff(c_92, plain, (iext(uri_rdf_type, uri_rdf__1, uri_rdfs_ContainerMembershipProperty)=true)). % 30.14/18.70 tff(c_90, plain, (iext(uri_rdfs_range, uri_rdf__3, uri_rdfs_Resource)=true)). % 30.14/18.70 tff(c_46, plain, (iext(uri_rdfs_domain, uri_rdfs_label, uri_rdfs_Resource)=true)). % 30.14/18.70 tff(c_144, plain, (iext(uri_rdfs_range, uri_rdf_subject, uri_rdfs_Resource)=true)). % 30.14/18.70 tff(c_140, plain, (iext(uri_rdfs_range, uri_rdf_predicate, uri_rdfs_Resource)=true)). % 30.14/18.70 tff(c_100, plain, (iext(uri_rdfs_subClassOf, uri_rdf_XMLLiteral, uri_rdfs_Literal)=true)). % 30.14/18.70 tff(c_88, plain, (iext(uri_rdfs_range, uri_rdf__2, uri_rdfs_Resource)=true)). % 30.14/18.70 tff(c_42, plain, (iext(uri_rdfs_range, uri_rdfs_isDefinedBy, uri_rdfs_Resource)=true)). % 30.14/18.70 tff(c_18, plain, (iext(uri_rdf_type, uri_rdf__2, uri_rdf_Property)=true)). % 30.14/18.70 tff(c_24, plain, (iext(uri_rdf_type, uri_rdf_value, uri_rdf_Property)=true)). % 30.14/18.70 tff(c_98, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Seq, uri_rdfs_Container)=true)). % 30.14/18.70 tff(c_84, plain, (iext(uri_rdfs_domain, uri_rdf__3, uri_rdfs_Resource)=true)). % 30.14/18.70 tff(c_22, plain, (iext(uri_rdf_type, uri_rdf_object, uri_rdf_Property)=true)). % 30.14/18.70 tff(c_108, plain, (iext(uri_rdfs_domain, uri_rdfs_domain, uri_rdf_Property)=true)). % 30.14/18.70 tff(c_48, plain, (iext(uri_rdfs_range, uri_rdfs_label, uri_rdfs_Literal)=true)). % 30.14/18.70 tff(c_44, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_isDefinedBy, uri_rdfs_seeAlso)=true)). % 30.14/18.70 tff(c_36, plain, (iext(uri_rdfs_domain, uri_rdfs_comment, uri_rdfs_Resource)=true)). % 30.14/18.70 tff(c_40, plain, (iext(uri_rdfs_domain, uri_rdfs_isDefinedBy, uri_rdfs_Resource)=true)). % 30.14/18.70 tff(c_80, plain, (iext(uri_rdfs_domain, uri_rdf__1, uri_rdfs_Resource)=true)). % 30.14/18.70 tff(c_34, plain, (iext(uri_rdf_type, uri_rdf_type, uri_rdf_Property)=true)). % 30.14/18.70 tff(c_82, plain, (iext(uri_rdfs_domain, uri_rdf__2, uri_rdfs_Resource)=true)). % 30.14/18.70 tff(c_74, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, uri_rdf_Property)=true)). % 30.14/18.70 tff(c_146, plain, (iext(uri_rdfs_domain, uri_rdfs_subClassOf, uri_rdfs_Class)=true)). % 30.14/18.70 tff(c_26, plain, (iext(uri_rdf_type, uri_rdf_subject, uri_rdf_Property)=true)). % 30.14/18.70 tff(c_86, plain, (iext(uri_rdfs_range, uri_rdf__1, uri_rdfs_Resource)=true)). % 30.14/18.70 tff(c_188, plain, (iext(uri_rdf_type, uri_foaf_mbox_sha1sum, uri_owl_InverseFunctionalProperty)=true)). % 30.14/18.70 tff(c_138, plain, (iext(uri_rdfs_domain, uri_rdf_predicate, uri_rdfs_Statement)=true)). % 30.14/18.70 tff(c_154, plain, (iext(uri_rdfs_range, uri_rdfs_subClassOf, uri_rdfs_Class)=true)). % 30.14/18.70 tff(c_132, plain, (iext(uri_rdfs_range, uri_rdfs_range, uri_rdfs_Class)=true)). % 30.14/18.70 tff(c_112, plain, (iext(uri_rdfs_range, uri_rdfs_domain, uri_rdfs_Class)=true)). % 30.14/18.70 tff(c_178, plain, (iext(uri_rdfs_domain, uri_rdf_value, uri_rdfs_Resource)=true)). % 30.14/18.70 tff(c_78, plain, (iext(uri_rdfs_range, uri_rdfs_member, uri_rdfs_Resource)=true)). % 30.14/18.70 tff(c_102, plain, (iext(uri_rdf_type, uri_rdf_XMLLiteral, uri_rdfs_Datatype)=true)). % 30.14/18.70 tff(c_20, plain, (iext(uri_rdf_type, uri_rdf__3, uri_rdf_Property)=true)). % 30.14/18.70 tff(c_68, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Alt, uri_rdfs_Container)=true)). % 30.14/18.70 tff(c_76, plain, (iext(uri_rdfs_domain, uri_rdfs_member, uri_rdfs_Resource)=true)). % 30.14/18.70 tff(c_174, plain, (iext(uri_rdfs_domain, uri_rdf_type, uri_rdfs_Resource)=true)). % 30.14/18.70 tff(c_64, plain, (iext(uri_rdfs_domain, uri_rdf_rest, uri_rdf_List)=true)). % 30.14/18.70 tff(c_128, plain, (iext(uri_rdfs_domain, uri_rdfs_range, uri_rdf_Property)=true)). % 30.14/18.70 tff(c_134, plain, (iext(uri_rdfs_domain, uri_rdf_object, uri_rdfs_Statement)=true)). % 30.14/18.70 tff(c_38, plain, (iext(uri_rdfs_range, uri_rdfs_comment, uri_rdfs_Literal)=true)). % 30.14/18.70 tff(c_52, plain, (iext(uri_rdfs_range, uri_rdfs_seeAlso, uri_rdfs_Resource)=true)). % 30.14/18.70 tff(c_106, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, uri_rdfs_Class)=true)). % 30.14/18.70 tff(c_16, plain, (iext(uri_rdf_type, uri_rdf__1, uri_rdf_Property)=true)). % 30.14/18.70 tff(c_60, plain, (iext(uri_rdfs_domain, uri_rdf_first, uri_rdf_List)=true)). % 30.14/18.70 tff(c_10, plain, (iext(uri_rdf_type, uri_rdf_first, uri_rdf_Property)=true)). % 30.14/18.70 tff(c_12, plain, (iext(uri_rdf_type, uri_rdf_nil, uri_rdf_List)=true)). % 30.14/18.70 tff(c_70, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Bag, uri_rdfs_Container)=true)). % 30.14/18.70 tff(c_62, plain, (iext(uri_rdfs_range, uri_rdf_first, uri_rdfs_Resource)=true)). % 30.14/18.70 tff(c_126, plain, (iext(uri_rdf_type, uri_rdf_Property, uri_rdfs_Class)=true)). % 30.14/18.70 tff(c_160, plain, (iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, uri_rdf_Property)=true)). % 30.14/18.70 tff(c_176, plain, (iext(uri_rdfs_range, uri_rdf_type, uri_rdfs_Class)=true)). % 30.14/18.70 tff(c_190, plain, (iext(uri_owl_sameAs, uri_ex_bob, uri_ex_robert)!=true)). % 30.14/18.70 tff(c_6, plain, (![X_7]: (ir(X_7)=true))). % 30.14/18.70 % SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 30.14/18.70 %------------------------------------------------------------------------------