%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : SWB006-10 : TPTP v9.0.0. Released v7.3.0. % Transfm : none % Format : tptp:raw % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % Computer : n021.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:46 PM UTC 2025 % Result : Satisfiable 31.03s 18.34s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.08/0.12 % Problem : SWB006-10 : TPTP v9.0.0. Released v7.3.0. % 0.08/0.13 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % 0.13/0.34 % Computer : n021.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:14 EDT 2025 % 0.13/0.34 % CPUTime : % 31.03/18.34 % 31.03/18.34 % SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 31.03/18.34 % 31.03/18.34 % SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 31.03/18.36 %$ 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_ex_w > uri_ex_u > true > sK1_testcase_premise_fullish_006_Literal_Values_represented_by_URIs_and_Blank_Nodes_BNODE_x > dat_str_abc % 31.03/18.36 % 31.03/18.36 %Foreground sorts: % 31.03/18.36 % 31.03/18.36 % 31.03/18.36 %Background operators: % 31.03/18.36 % 31.03/18.36 % 31.03/18.36 %Foreground operators: % 31.03/18.36 tff(uri_rdfs_Datatype, type, uri_rdfs_Datatype: $i). % 31.03/18.36 tff(uri_rdfs_ContainerMembershipProperty, type, uri_rdfs_ContainerMembershipProperty: $i). % 31.03/18.36 tff(uri_rdfs_Resource, type, uri_rdfs_Resource: $i). % 31.03/18.36 tff(uri_rdf_Property, type, uri_rdf_Property: $i). % 31.03/18.36 tff(uri_rdf_subject, type, uri_rdf_subject: $i). % 31.03/18.36 tff(uri_rdf_type, type, uri_rdf_type: $i). % 31.03/18.36 tff(uri_rdfs_subPropertyOf, type, uri_rdfs_subPropertyOf: $i). % 31.03/18.36 tff(uri_ex_u, type, uri_ex_u: $i). % 31.03/18.36 tff(uri_rdfs_seeAlso, type, uri_rdfs_seeAlso: $i). % 31.03/18.36 tff(icext, type, icext: ($i * $i) > $i). % 31.03/18.36 tff(uri_rdfs_range, type, uri_rdfs_range: $i). % 31.03/18.36 tff(uri_rdf_XMLLiteral, type, uri_rdf_XMLLiteral: $i). % 31.03/18.36 tff(uri_rdf_List, type, uri_rdf_List: $i). % 31.03/18.36 tff(uri_rdf_first, type, uri_rdf_first: $i). % 31.03/18.36 tff(uri_rdf_predicate, type, uri_rdf_predicate: $i). % 31.03/18.36 tff(ir, type, ir: $i > $i). % 31.03/18.36 tff(lv, type, lv: $i > $i). % 31.03/18.36 tff(uri_rdf__3, type, uri_rdf__3: $i). % 31.03/18.36 tff(uri_rdf_value, type, uri_rdf_value: $i). % 31.03/18.36 tff(ic, type, ic: $i > $i). % 31.03/18.36 tff(dat_str_abc, type, dat_str_abc: $i). % 31.03/18.36 tff(uri_rdfs_Statement, type, uri_rdfs_Statement: $i). % 31.03/18.36 tff(uri_rdf__1, type, uri_rdf__1: $i). % 31.03/18.36 tff(iext, type, iext: ($i * $i * $i) > $i). % 31.03/18.36 tff(uri_ex_w, type, uri_ex_w: $i). % 31.03/18.36 tff(sK1_testcase_premise_fullish_006_Literal_Values_represented_by_URIs_and_Blank_Nodes_BNODE_x, type, sK1_testcase_premise_fullish_006_Literal_Values_represented_by_URIs_and_Blank_Nodes_BNODE_x: $i). % 31.03/18.36 tff(uri_rdf_rest, type, uri_rdf_rest: $i). % 31.03/18.36 tff(uri_rdfs_label, type, uri_rdfs_label: $i). % 31.03/18.36 tff(uri_rdfs_Container, type, uri_rdfs_Container: $i). % 31.03/18.36 tff(uri_rdfs_subClassOf, type, uri_rdfs_subClassOf: $i). % 31.03/18.36 tff(uri_owl_sameAs, type, uri_owl_sameAs: $i). % 31.03/18.36 tff(uri_rdf_object, type, uri_rdf_object: $i). % 31.03/18.36 tff(ip, type, ip: $i > $i). % 31.03/18.36 tff(uri_rdfs_Class, type, uri_rdfs_Class: $i). % 31.03/18.36 tff(uri_rdfs_Seq, type, uri_rdfs_Seq: $i). % 31.03/18.36 tff(uri_rdfs_member, type, uri_rdfs_member: $i). % 31.03/18.36 tff(uri_rdf_Bag, type, uri_rdf_Bag: $i). % 31.03/18.36 tff(uri_rdf__2, type, uri_rdf__2: $i). % 31.03/18.36 tff(uri_rdfs_comment, type, uri_rdfs_comment: $i). % 31.03/18.36 tff(uri_rdfs_Literal, type, uri_rdfs_Literal: $i). % 31.03/18.36 tff(true, type, true: $i). % 31.03/18.36 tff(uri_rdf_Alt, type, uri_rdf_Alt: $i). % 31.03/18.36 tff(uri_rdf_nil, type, uri_rdf_nil: $i). % 31.03/18.36 tff(literal_plain, type, literal_plain: $i > $i). % 31.03/18.36 tff(uri_rdfs_isDefinedBy, type, uri_rdfs_isDefinedBy: $i). % 31.03/18.36 tff(uri_rdfs_domain, type, uri_rdfs_domain: $i). % 31.03/18.36 tff(ifeq, type, ifeq: ($i * $i * $i * $i) > $i). % 31.03/18.36 % 31.03/18.36 %Saturated clause set: % 31.03/18.36 tff(c_14146, 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))). % 31.03/18.36 tff(c_13672, 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))). % 31.03/18.36 tff(c_13669, 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))). % 31.03/18.36 tff(c_14003, 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))). % 31.03/18.36 tff(c_65034, plain, (![X_1165, Y_1166]: (ifeq(iext(uri_rdfs_label, X_1165, Y_1166), true, iext(uri_rdfs_label, X_1165, Y_1166), true)=true))). % 31.03/18.36 tff(c_65026, plain, (![X_1163, Y_1164]: (ifeq(iext(uri_rdf_predicate, X_1163, Y_1164), true, iext(uri_rdf_predicate, X_1163, Y_1164), true)=true))). % 31.03/18.36 tff(c_14093, 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))). % 31.03/18.36 tff(c_13934, 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))). % 31.03/18.36 tff(c_14809, 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))). % 31.03/18.36 tff(c_5016, 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))). % 31.03/18.36 tff(c_5013, 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))). % 31.03/18.36 tff(c_13834, 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))). % 31.03/18.37 tff(c_13615, 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))). % 31.03/18.37 tff(c_64028, plain, (![X_1150, Y_1151]: (ifeq(iext(uri_rdfs_member, X_1150, Y_1151), true, iext(uri_rdfs_member, X_1150, Y_1151), true)=true))). % 31.03/18.37 tff(c_64001, plain, (![X_1146, Y_1147]: (ifeq(iext(uri_rdfs_comment, X_1146, Y_1147), true, iext(uri_rdfs_comment, X_1146, Y_1147), true)=true))). % 31.03/18.37 tff(c_63862, plain, (![C_1144]: (ifeq(iext(uri_rdfs_subClassOf, C_1144, uri_rdf_List), true, iext(uri_rdfs_subClassOf, C_1144, uri_rdfs_Resource), true)=true))). % 31.03/18.37 tff(c_63721, plain, (![C_1142]: (ifeq(iext(uri_rdfs_subClassOf, C_1142, uri_rdfs_Statement), true, iext(uri_rdfs_subClassOf, C_1142, uri_rdfs_Resource), true)=true))). % 31.03/18.37 tff(c_13410, 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))). % 31.03/18.37 tff(c_13476, 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))). % 31.03/18.37 tff(c_13185, 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))). % 31.03/18.37 tff(c_13253, 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))). % 31.03/18.37 tff(c_7828, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdf_Property), true, ifeq(iext(P_18, uri_owl_sameAs, Y_21), true, true, true), true)=true))). % 31.03/18.37 tff(c_11829, 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))). % 31.03/18.37 tff(c_5671, 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))). % 31.03/18.37 tff(c_12478, 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))). % 31.03/18.37 tff(c_5668, 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))). % 31.03/18.37 tff(c_13027, 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))). % 31.03/18.37 tff(c_13103, 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))). % 31.03/18.37 tff(c_12858, 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))). % 31.03/18.37 tff(c_6341, 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))). % 31.03/18.37 tff(c_12525, 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))). % 31.03/18.37 tff(c_8394, 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))). % 31.03/18.37 tff(c_7328, 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))). % 31.03/18.37 tff(c_12380, 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))). % 31.03/18.37 tff(c_12978, 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))). % 31.03/18.37 tff(c_7325, 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))). % 31.03/18.37 tff(c_12428, 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))). % 31.03/18.37 tff(c_6344, 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))). % 31.03/18.37 tff(c_11832, 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))). % 31.03/18.37 tff(c_8391, 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))). % 31.03/18.37 tff(c_7831, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdf_Property), true, ifeq(iext(P_28, X_30, uri_owl_sameAs), true, true, true), true)=true))). % 31.03/18.37 tff(c_12906, 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))). % 31.03/18.37 tff(c_12191, 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))). % 31.03/18.37 tff(c_12333, 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))). % 31.03/18.37 tff(c_12640, 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))). % 31.03/18.37 tff(c_12285, 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))). % 31.03/18.37 tff(c_60077, plain, (![X_1096, Y_1097]: (ifeq(iext(uri_rdf__3, X_1096, Y_1097), true, iext(uri_rdf__3, X_1096, Y_1097), true)=true))). % 31.03/18.37 tff(c_8871, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subPropertyOf), true, ifeq(iext(P_47, uri_owl_sameAs, uri_owl_sameAs), true, true, true), true)=true))). % 31.03/18.37 tff(c_59929, plain, (![C_1094]: (ifeq(iext(uri_rdfs_subClassOf, C_1094, uri_rdfs_Literal), true, iext(uri_rdfs_subClassOf, C_1094, uri_rdfs_Resource), true)=true))). % 31.03/18.37 tff(c_10306, 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))). % 31.03/18.37 tff(c_59667, plain, (![C_1091]: (ifeq(iext(uri_rdfs_subClassOf, C_1091, uri_rdfs_Class), true, iext(uri_rdfs_subClassOf, C_1091, uri_rdfs_Resource), true)=true))). % 31.03/18.37 tff(c_8959, 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))). % 31.03/18.37 tff(c_6481, 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))). % 31.03/18.37 tff(c_4007, 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))). % 31.03/18.37 tff(c_58684, plain, (![X_1083, Y_1084]: (ifeq(iext(uri_rdfs_subClassOf, X_1083, Y_1084), true, iext(uri_rdfs_subClassOf, X_1083, Y_1084), true)=true))). % 31.03/18.37 tff(c_4010, 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))). % 31.03/18.37 tff(c_58108, plain, (![X_1073, Y_1074]: (ifeq(iext(uri_rdfs_seeAlso, X_1073, Y_1074), true, iext(uri_rdfs_seeAlso, X_1073, Y_1074), true)=true))). % 31.03/18.37 tff(c_7162, 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))). % 31.03/18.37 tff(c_57723, plain, (![P_1068]: (ifeq(iext(uri_rdfs_subPropertyOf, P_1068, uri_rdf__3), true, iext(uri_rdfs_subPropertyOf, P_1068, uri_rdfs_member), true)=true))). % 31.03/18.37 tff(c_57648, plain, (![X_1064, Y_1065]: (ifeq(iext(uri_owl_sameAs, X_1064, Y_1065), true, iext(uri_owl_sameAs, X_1064, Y_1065), true)=true))). % 31.03/18.37 tff(c_4100, 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))). % 31.03/18.37 tff(c_4360, 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))). % 31.03/18.37 tff(c_57233, plain, (![C_1058]: (ifeq(iext(uri_rdfs_subClassOf, C_1058, uri_rdf_XMLLiteral), true, iext(uri_rdfs_subClassOf, C_1058, uri_rdfs_Resource), true)=true))). % 31.03/18.37 tff(c_4318, 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))). % 31.03/18.37 tff(c_9430, 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))). % 31.03/18.37 tff(c_56852, plain, (![C_1053]: (ifeq(iext(uri_rdfs_subClassOf, C_1053, uri_rdfs_Seq), true, iext(uri_rdfs_subClassOf, C_1053, uri_rdfs_Resource), true)=true))). % 31.03/18.37 tff(c_11016, 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))). % 31.03/18.37 tff(c_56710, plain, (![X_1048, Y_1049]: (ifeq(iext(uri_rdf__3, X_1048, Y_1049), true, iext(uri_rdfs_member, X_1048, Y_1049), true)=true))). % 31.03/18.37 tff(c_5897, 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))). % 31.03/18.37 tff(c_56568, plain, (![X_1043, Y_1044]: (ifeq(iext(uri_rdf_rest, X_1043, Y_1044), true, iext(uri_rdf_rest, X_1043, Y_1044), true)=true))). % 31.03/18.38 tff(c_11310, 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))). % 31.03/18.38 tff(c_4315, 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))). % 31.03/18.38 tff(c_8077, 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))). % 31.03/18.38 tff(c_7244, 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))). % 31.03/18.38 tff(c_56060, plain, (![X_1034, Y_1035]: (ifeq(iext(uri_rdf_object, X_1034, Y_1035), true, iext(uri_rdf_object, X_1034, Y_1035), true)=true))). % 31.03/18.38 tff(c_55993, plain, (![P_1032]: (ifeq(iext(uri_rdfs_subPropertyOf, P_1032, uri_rdf__1), true, iext(uri_rdfs_subPropertyOf, P_1032, uri_rdfs_member), true)=true))). % 31.03/18.38 tff(c_4172, 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))). % 31.03/18.38 tff(c_9263, 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))). % 31.03/18.38 tff(c_4097, 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))). % 31.03/18.38 tff(c_55446, plain, (![C_1025]: (ifeq(iext(uri_rdfs_subClassOf, C_1025, uri_rdfs_Container), true, iext(uri_rdfs_subClassOf, C_1025, uri_rdfs_Resource), true)=true))). % 31.03/18.38 tff(c_4656, 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))). % 31.03/18.38 tff(c_55101, plain, (![X_1018, Y_1019]: (ifeq(iext(uri_rdf__2, X_1018, Y_1019), true, iext(uri_rdf__2, X_1018, Y_1019), true)=true))). % 31.03/18.38 tff(c_55074, plain, (![X_1014, Y_1015]: (ifeq(iext(uri_rdf_first, X_1014, Y_1015), true, iext(uri_rdf_first, X_1014, Y_1015), true)=true))). % 31.03/18.38 tff(c_54743, plain, (![X_1010, Y_1011]: (ifeq(iext(uri_rdfs_domain, X_1010, Y_1011), true, iext(uri_rdfs_domain, X_1010, Y_1011), true)=true))). % 31.03/18.38 tff(c_4218, 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))). % 31.03/18.38 tff(c_54093, plain, (![X_1002, Y_1003]: (ifeq(iext(uri_rdfs_range, X_1002, Y_1003), true, iext(uri_rdfs_range, X_1002, Y_1003), true)=true))). % 31.03/18.38 tff(c_6774, 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))). % 31.03/18.38 tff(c_53946, plain, (![X_997, Y_998]: (ifeq(iext(uri_rdf_value, X_997, Y_998), true, iext(uri_rdf_value, X_997, Y_998), true)=true))). % 31.03/18.38 tff(c_8337, 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))). % 31.03/18.38 tff(c_53282, plain, (![X_990, Y_991]: (ifeq(iext(uri_rdfs_subPropertyOf, X_990, Y_991), true, iext(uri_rdfs_subPropertyOf, X_990, Y_991), true)=true))). % 31.03/18.38 tff(c_53269, plain, (![X_988, Y_989]: (ifeq(iext(uri_rdf__2, X_988, Y_989), true, iext(uri_rdfs_member, X_988, Y_989), true)=true))). % 31.03/18.38 tff(c_52880, plain, (![P_983]: (ifeq(iext(uri_rdfs_subPropertyOf, P_983, uri_rdf__2), true, iext(uri_rdfs_subPropertyOf, P_983, uri_rdfs_member), true)=true))). % 31.03/18.38 tff(c_52811, plain, (![C_982]: (ifeq(iext(uri_rdfs_subClassOf, C_982, uri_rdf_Alt), true, iext(uri_rdfs_subClassOf, C_982, uri_rdfs_Resource), true)=true))). % 31.03/18.38 tff(c_9364, 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))). % 31.03/18.38 tff(c_10126, 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))). % 31.03/18.38 tff(c_4221, 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))). % 31.03/18.38 tff(c_4764, 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))). % 31.03/18.38 tff(c_52195, plain, (![C_975]: (ifeq(iext(uri_rdfs_subClassOf, C_975, uri_rdf_Bag), true, iext(uri_rdfs_subClassOf, C_975, uri_rdfs_Resource), true)=true))). % 31.03/18.38 tff(c_4263, 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))). % 31.03/18.38 tff(c_9094, 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))). % 31.03/18.38 tff(c_4266, 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))). % 31.03/18.38 tff(c_11562, 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))). % 31.03/18.38 tff(c_51665, plain, (![X_965, Y_966]: (ifeq(iext(uri_rdf__1, X_965, Y_966), true, iext(uri_rdf__1, X_965, Y_966), true)=true))). % 31.03/18.38 tff(c_51525, plain, (![C_963]: (ifeq(iext(uri_rdfs_subClassOf, C_963, uri_rdfs_ContainerMembershipProperty), true, iext(uri_rdfs_subClassOf, C_963, uri_rdfs_Resource), true)=true))). % 31.03/18.38 tff(c_51296, plain, (![X_957, Y_958]: (ifeq(iext(uri_rdf_subject, X_957, Y_958), true, iext(uri_rdf_subject, X_957, Y_958), true)=true))). % 31.03/18.38 tff(c_4912, 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))). % 31.03/18.38 tff(c_6399, 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))). % 31.03/18.38 tff(c_7523, 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))). % 31.03/18.38 tff(c_5322, 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))). % 31.03/18.38 tff(c_14686, 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))). % 31.03/18.38 tff(c_50564, plain, (![C_950]: (ifeq(iext(uri_rdfs_subClassOf, C_950, uri_rdfs_Datatype), true, iext(uri_rdfs_subClassOf, C_950, uri_rdfs_Resource), true)=true))). % 31.03/18.38 tff(c_9025, 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))). % 31.03/18.38 tff(c_7774, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, uri_owl_sameAs, uri_rdf_Property), true, true, true), true)=true))). % 31.03/18.38 tff(c_6290, 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))). % 31.03/18.38 tff(c_5963, 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))). % 31.03/18.38 tff(c_5783, 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))). % 31.03/18.38 tff(c_48152, plain, (![X_933, Y_934]: (ifeq(iext(uri_rdf_type, X_933, Y_934), true, iext(uri_rdf_type, X_933, Y_934), true)=true))). % 31.03/18.38 tff(c_4053, 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))). % 31.03/18.38 tff(c_3953, 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))). % 31.03/18.38 tff(c_47323, plain, (![C_924]: (ifeq(iext(uri_rdfs_subClassOf, C_924, uri_rdf_Property), true, iext(uri_rdfs_subClassOf, C_924, uri_rdfs_Resource), true)=true))). % 31.03/18.38 tff(c_9715, 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))). % 31.03/18.38 tff(c_8768, 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))). % 31.03/18.38 tff(c_5617, 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))). % 31.03/18.38 tff(c_46861, plain, (![X_916, Y_917]: (ifeq(iext(uri_rdf__1, X_916, Y_917), true, iext(uri_rdfs_member, X_916, Y_917), true)=true))). % 31.03/18.38 tff(c_9200, 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))). % 31.03/18.38 tff(c_4175, 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))). % 31.03/18.38 tff(c_6577, 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))). % 31.03/18.38 tff(c_4363, 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))). % 31.03/18.38 tff(c_4050, 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))). % 31.03/18.38 tff(c_11961, 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))). % 31.03/18.38 tff(c_12050, 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))). % 31.03/18.38 tff(c_8682, 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))). % 31.03/18.38 tff(c_9519, 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))). % 31.03/18.38 tff(c_5073, 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))). % 31.03/18.38 tff(c_3956, 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))). % 31.03/18.39 tff(c_5219, 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))). % 31.03/18.39 tff(c_11465, 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))). % 31.03/18.39 tff(c_44894, plain, (![X_893, Y_894]: (ifeq(iext(uri_rdfs_isDefinedBy, X_893, Y_894), true, iext(uri_rdfs_isDefinedBy, X_893, Y_894), true)=true))). % 31.03/18.39 tff(c_6028, 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))). % 31.03/18.39 tff(c_11696, 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))). % 31.03/18.39 tff(c_4847, 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))). % 31.03/18.39 tff(c_11750, 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))). % 31.03/18.39 tff(c_6974, 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))). % 31.03/18.39 tff(c_12595, 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))). % 31.03/18.39 tff(c_11093, 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))). % 31.03/18.39 tff(c_4556, plain, (![P_47, X_140]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, X_140, uri_rdfs_Resource), true, true, true), true)=true))). % 31.03/18.39 tff(c_10753, 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))). % 31.03/18.39 tff(c_5488, 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))). % 31.03/18.39 tff(c_11096, 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))). % 31.03/18.39 tff(c_12598, 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))). % 31.03/18.39 tff(c_10750, 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))). % 31.03/18.39 tff(c_6101, 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))). % 31.03/18.39 tff(c_5491, 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))). % 31.03/18.39 tff(c_6098, 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))). % 31.03/18.39 tff(c_3576, 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))). % 31.03/18.39 tff(c_3402, 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))). % 31.03/18.39 tff(c_3537, 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))). % 31.03/18.39 tff(c_3664, 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))). % 31.03/18.39 tff(c_3912, 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))). % 31.03/18.39 tff(c_3451, 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))). % 31.03/18.39 tff(c_3454, 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))). % 31.03/18.39 tff(c_3830, 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))). % 31.03/18.39 tff(c_3866, 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))). % 31.03/18.39 tff(c_3909, 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))). % 31.03/18.39 tff(c_3540, 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))). % 31.03/18.39 tff(c_3372, 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))). % 31.03/18.39 tff(c_3405, 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))). % 31.03/18.39 tff(c_3827, 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))). % 31.03/18.39 tff(c_3375, 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))). % 31.03/18.39 tff(c_3710, 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))). % 31.03/18.39 tff(c_3869, 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))). % 31.03/18.39 tff(c_3667, 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))). % 31.03/18.39 tff(c_3495, 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))). % 31.03/18.39 tff(c_3625, 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))). % 31.03/18.39 tff(c_3622, 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))). % 31.03/18.39 tff(c_3498, 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))). % 31.03/18.39 tff(c_2295, plain, (![P_100]: (ifeq(iext(uri_rdfs_subPropertyOf, P_100, uri_owl_sameAs), true, ifeq(iext(P_100, sK1_testcase_premise_fullish_006_Literal_Values_represented_by_URIs_and_Blank_Nodes_BNODE_x, literal_plain(dat_str_abc)), true, true, true), true)=true))). % 31.03/18.39 tff(c_3791, 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))). % 31.03/18.39 tff(c_3749, 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))). % 31.03/18.39 tff(c_3788, 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))). % 31.03/18.39 tff(c_3746, 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))). % 31.03/18.39 tff(c_14532, 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))). % 31.03/18.39 tff(c_3579, 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))). % 31.03/18.39 tff(c_14535, 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))). % 31.03/18.39 tff(c_3707, 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))). % 31.03/18.39 tff(c_3318, 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))). % 31.03/18.39 tff(c_2289, plain, (![P_100]: (ifeq(iext(uri_rdfs_subPropertyOf, P_100, uri_owl_sameAs), true, ifeq(iext(P_100, uri_ex_u, literal_plain(dat_str_abc)), true, true, true), true)=true))). % 31.03/18.39 tff(c_3315, 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))). % 31.03/18.39 tff(c_1587, 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))). % 31.03/18.39 tff(c_1915, 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))). % 31.03/18.39 tff(c_36294, plain, (![C_786]: (ifeq(iext(uri_rdfs_subClassOf, C_786, uri_rdfs_ContainerMembershipProperty), true, iext(uri_rdfs_subClassOf, C_786, uri_rdf_Property), true)=true))). % 31.03/18.39 tff(c_2481, plain, (![P_100]: (ifeq(iext(uri_rdfs_subPropertyOf, P_100, uri_rdfs_domain), true, ifeq(iext(P_100, uri_rdf_object, uri_rdfs_Statement), true, true, true), true)=true))). % 31.03/18.39 tff(c_2511, plain, (![P_100]: (ifeq(iext(uri_rdfs_subPropertyOf, P_100, uri_rdfs_domain), true, ifeq(iext(P_100, uri_rdfs_comment, uri_rdfs_Resource), true, true, true), true)=true))). % 31.03/18.39 tff(c_2592, plain, (![P_100]: (ifeq(iext(uri_rdfs_subPropertyOf, P_100, uri_rdfs_range), true, ifeq(iext(P_100, uri_rdfs_range, uri_rdfs_Class), true, true, true), true)=true))). % 31.03/18.39 tff(c_2367, plain, (![P_100]: (ifeq(iext(uri_rdfs_subPropertyOf, P_100, uri_rdfs_range), true, ifeq(iext(P_100, uri_rdf_predicate, uri_rdfs_Resource), true, true, true), true)=true))). % 31.03/18.39 tff(c_2331, plain, (![P_100]: (ifeq(iext(uri_rdfs_subPropertyOf, P_100, uri_rdf_type), true, ifeq(iext(P_100, uri_rdf__2, uri_rdfs_ContainerMembershipProperty), true, true, true), true)=true))). % 31.03/18.39 tff(c_2301, plain, (![P_100]: (ifeq(iext(uri_rdfs_subPropertyOf, P_100, uri_rdf_type), true, ifeq(iext(P_100, uri_rdf_Property, uri_rdfs_Class), true, true, true), true)=true))). % 31.03/18.39 tff(c_2409, plain, (![P_100]: (ifeq(iext(uri_rdfs_subPropertyOf, P_100, uri_rdf_type), true, ifeq(iext(P_100, uri_rdf__2, uri_rdf_Property), true, true, true), true)=true))). % 31.03/18.39 tff(c_2439, plain, (![P_100]: (ifeq(iext(uri_rdfs_subPropertyOf, P_100, uri_rdf_type), true, ifeq(iext(P_100, uri_rdf__3, uri_rdf_Property), true, true, true), true)=true))). % 31.03/18.39 tff(c_2535, plain, (![P_100]: (ifeq(iext(uri_rdfs_subPropertyOf, P_100, uri_rdfs_range), true, ifeq(iext(P_100, uri_rdf_type, uri_rdfs_Class), true, true, true), true)=true))). % 31.03/18.39 tff(c_2559, plain, (![P_100]: (ifeq(iext(uri_rdfs_subPropertyOf, P_100, uri_rdfs_range), true, ifeq(iext(P_100, uri_rdf_rest, uri_rdf_List), true, true, true), true)=true))). % 31.03/18.39 tff(c_2529, plain, (![P_100]: (ifeq(iext(uri_rdfs_subPropertyOf, P_100, uri_rdfs_range), true, ifeq(iext(P_100, uri_rdfs_subPropertyOf, uri_rdf_Property), true, true, true), true)=true))). % 31.03/18.39 tff(c_2565, plain, (![P_100]: (ifeq(iext(uri_rdfs_subPropertyOf, P_100, uri_rdfs_subClassOf), true, ifeq(iext(P_100, uri_rdfs_ContainerMembershipProperty, uri_rdf_Property), true, true, true), true)=true))). % 31.03/18.39 tff(c_2604, plain, (![P_100]: (ifeq(iext(uri_rdfs_subPropertyOf, P_100, uri_rdfs_range), true, ifeq(iext(P_100, uri_rdfs_label, uri_rdfs_Literal), true, true, true), true)=true))). % 31.03/18.39 tff(c_2499, plain, (![P_100]: (ifeq(iext(uri_rdfs_subPropertyOf, P_100, uri_rdfs_subClassOf), true, ifeq(iext(P_100, uri_rdf_Alt, uri_rdfs_Container), true, true, true), true)=true))). % 31.03/18.39 tff(c_2391, plain, (![P_100]: (ifeq(iext(uri_rdfs_subPropertyOf, P_100, uri_rdf_type), true, ifeq(iext(P_100, uri_rdf_type, uri_rdf_Property), true, true, true), true)=true))). % 31.03/18.40 tff(c_2313, plain, (![P_100]: (ifeq(iext(uri_rdfs_subPropertyOf, P_100, uri_rdf_type), true, ifeq(iext(P_100, uri_rdf__1, uri_rdfs_ContainerMembershipProperty), true, true, true), true)=true))). % 31.03/18.40 tff(c_2553, plain, (![P_100]: (ifeq(iext(uri_rdfs_subPropertyOf, P_100, uri_rdfs_domain), true, ifeq(iext(P_100, uri_rdfs_domain, uri_rdf_Property), true, true, true), true)=true))). % 31.03/18.40 tff(c_2646, plain, (![P_100]: (ifeq(iext(uri_rdfs_subPropertyOf, P_100, uri_rdfs_range), true, ifeq(iext(P_100, uri_rdfs_seeAlso, uri_rdfs_Resource), true, true, true), true)=true))). % 31.03/18.40 tff(c_2337, plain, (![P_100]: (ifeq(iext(uri_rdfs_subPropertyOf, P_100, uri_rdfs_domain), true, ifeq(iext(P_100, uri_rdf_subject, uri_rdfs_Statement), true, true, true), true)=true))). % 31.03/18.40 tff(c_2598, plain, (![P_100]: (ifeq(iext(uri_rdfs_subPropertyOf, P_100, uri_rdf_type), true, ifeq(iext(P_100, uri_rdf_value, uri_rdf_Property), true, true, true), true)=true))). % 31.03/18.40 tff(c_2652, plain, (![P_100]: (ifeq(iext(uri_rdfs_subPropertyOf, P_100, uri_rdfs_domain), true, ifeq(iext(P_100, uri_rdf_first, uri_rdf_List), true, true, true), true)=true))). % 31.03/18.40 tff(c_2523, plain, (![P_100]: (ifeq(iext(uri_rdfs_subPropertyOf, P_100, uri_rdfs_subClassOf), true, ifeq(iext(P_100, uri_rdf_Bag, uri_rdfs_Container), true, true, true), true)=true))). % 31.03/18.40 tff(c_2622, plain, (![P_100]: (ifeq(iext(uri_rdfs_subPropertyOf, P_100, uri_rdfs_domain), true, ifeq(iext(P_100, uri_rdfs_label, uri_rdfs_Resource), true, true, true), true)=true))). % 31.03/18.40 tff(c_2610, plain, (![P_100]: (ifeq(iext(uri_rdfs_subPropertyOf, P_100, uri_rdfs_domain), true, ifeq(iext(P_100, uri_rdf_rest, uri_rdf_List), true, true, true), true)=true))). % 31.03/18.40 tff(c_2487, plain, (![P_100]: (ifeq(iext(uri_rdfs_subPropertyOf, P_100, uri_rdf_type), true, ifeq(iext(P_100, uri_rdf_object, uri_rdf_Property), true, true, true), true)=true))). % 31.28/18.40 tff(c_2379, plain, (![P_100]: (ifeq(iext(uri_rdfs_subPropertyOf, P_100, uri_rdfs_domain), true, ifeq(iext(P_100, uri_rdf_predicate, uri_rdfs_Statement), true, true, true), true)=true))). % 31.28/18.40 tff(c_2469, plain, (![P_100]: (ifeq(iext(uri_rdfs_subPropertyOf, P_100, uri_rdfs_range), true, ifeq(iext(P_100, uri_rdf_value, uri_rdfs_Resource), true, true, true), true)=true))). % 31.28/18.40 tff(c_2343, plain, (![P_100]: (ifeq(iext(uri_rdfs_subPropertyOf, P_100, uri_rdfs_domain), true, ifeq(iext(P_100, uri_rdf_value, uri_rdfs_Resource), true, true, true), true)=true))). % 31.28/18.40 tff(c_2325, plain, (![P_100]: (ifeq(iext(uri_rdfs_subPropertyOf, P_100, uri_rdfs_range), true, ifeq(iext(P_100, uri_rdfs_subClassOf, uri_rdfs_Class), true, true, true), true)=true))). % 31.28/18.40 tff(c_2505, plain, (![P_100]: (ifeq(iext(uri_rdfs_subPropertyOf, P_100, uri_rdfs_subClassOf), true, ifeq(iext(P_100, uri_rdfs_Datatype, uri_rdfs_Class), true, true, true), true)=true))). % 31.28/18.40 tff(c_2541, plain, (![P_100]: (ifeq(iext(uri_rdfs_subPropertyOf, P_100, uri_rdfs_subClassOf), true, ifeq(iext(P_100, uri_rdf_XMLLiteral, uri_rdfs_Literal), true, true, true), true)=true))). % 31.28/18.40 tff(c_2349, plain, (![P_100]: (ifeq(iext(uri_rdfs_subPropertyOf, P_100, uri_owl_sameAs), true, ifeq(iext(P_100, sK1_testcase_premise_fullish_006_Literal_Values_represented_by_URIs_and_Blank_Nodes_BNODE_x, uri_ex_w), true, true, true), true)=true))). % 31.28/18.40 tff(c_2451, plain, (![P_100]: (ifeq(iext(uri_rdfs_subPropertyOf, P_100, uri_rdfs_domain), true, ifeq(iext(P_100, uri_rdfs_isDefinedBy, uri_rdfs_Resource), true, true, true), true)=true))). % 31.28/18.40 tff(c_2634, plain, (![P_100]: (ifeq(iext(uri_rdfs_subPropertyOf, P_100, uri_rdfs_domain), true, ifeq(iext(P_100, uri_rdfs_range, uri_rdf_Property), true, true, true), true)=true))). % 31.28/18.40 tff(c_2658, plain, (![P_100]: (ifeq(iext(uri_rdfs_subPropertyOf, P_100, uri_rdfs_domain), true, ifeq(iext(P_100, uri_rdf_type, uri_rdfs_Resource), true, true, true), true)=true))). % 31.28/18.40 tff(c_32110, plain, (![C_749]: (ifeq(iext(uri_rdfs_subClassOf, C_749, uri_rdfs_Seq), true, iext(uri_rdfs_subClassOf, C_749, uri_rdfs_Container), true)=true))). % 31.28/18.40 tff(c_2475, plain, (![P_100]: (ifeq(iext(uri_rdfs_subPropertyOf, P_100, uri_rdf_type), true, ifeq(iext(P_100, uri_rdf_first, uri_rdf_Property), true, true, true), true)=true))). % 31.28/18.40 tff(c_2547, plain, (![P_100]: (ifeq(iext(uri_rdfs_subPropertyOf, P_100, uri_rdfs_domain), true, ifeq(iext(P_100, uri_rdfs_subClassOf, uri_rdfs_Class), true, true, true), true)=true))). % 31.28/18.40 tff(c_2403, plain, (![P_100]: (ifeq(iext(uri_rdfs_subPropertyOf, P_100, uri_rdf_type), true, ifeq(iext(P_100, uri_rdf__1, uri_rdf_Property), true, true, true), true)=true))). % 31.28/18.40 tff(c_2319, plain, (![P_100]: (ifeq(iext(uri_rdfs_subPropertyOf, P_100, uri_rdf_type), true, ifeq(iext(P_100, uri_rdf__3, uri_rdfs_ContainerMembershipProperty), true, true, true), true)=true))). % 31.28/18.40 tff(c_2571, plain, (![P_100]: (ifeq(iext(uri_rdfs_subPropertyOf, P_100, uri_rdfs_range), true, ifeq(iext(P_100, uri_rdf_first, uri_rdfs_Resource), true, true, true), true)=true))). % 31.28/18.40 tff(c_31475, plain, (![C_742]: (ifeq(iext(uri_rdfs_subClassOf, C_742, uri_rdf_XMLLiteral), true, iext(uri_rdfs_subClassOf, C_742, uri_rdfs_Literal), true)=true))). % 31.28/18.40 tff(c_31424, plain, (![P_740]: (ifeq(iext(uri_rdfs_subPropertyOf, P_740, uri_rdfs_isDefinedBy), true, iext(uri_rdfs_subPropertyOf, P_740, uri_rdfs_seeAlso), true)=true))). % 31.28/18.40 tff(c_2445, plain, (![P_100]: (ifeq(iext(uri_rdfs_subPropertyOf, P_100, uri_rdfs_range), true, ifeq(iext(P_100, uri_rdfs_domain, uri_rdfs_Class), true, true, true), true)=true))). % 31.28/18.40 tff(c_2415, plain, (![P_100]: (ifeq(iext(uri_rdfs_subPropertyOf, P_100, uri_rdfs_range), true, ifeq(iext(P_100, uri_rdf_subject, uri_rdfs_Resource), true, true, true), true)=true))). % 31.28/18.40 tff(c_31123, plain, (![D_736]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_736), true, icext(D_736, uri_rdfs_member), true)=true))). % 31.28/18.40 tff(c_31056, plain, (![D_734]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_734), true, icext(D_734, uri_rdfs_Resource), true)=true))). % 31.28/18.40 tff(c_2421, plain, (![P_100]: (ifeq(iext(uri_rdfs_subPropertyOf, P_100, uri_rdfs_domain), true, ifeq(iext(P_100, uri_rdf__2, uri_rdfs_Resource), true, true, true), true)=true))). % 31.28/18.40 tff(c_30866, plain, (![D_731]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_731), true, icext(D_731, uri_rdfs_isDefinedBy), true)=true))). % 31.28/18.40 tff(c_30800, plain, (![D_729]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_729), true, icext(D_729, uri_rdfs_domain), true)=true))). % 31.28/18.40 tff(c_30734, plain, (![D_727]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_727), true, icext(D_727, uri_rdfs_range), true)=true))). % 31.28/18.40 tff(c_2385, plain, (![P_100]: (ifeq(iext(uri_rdfs_subPropertyOf, P_100, uri_rdfs_subClassOf), true, ifeq(iext(P_100, uri_rdfs_Seq, uri_rdfs_Container), true, true, true), true)=true))). % 31.28/18.40 tff(c_30553, plain, (![D_724]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_724), true, icext(D_724, uri_rdfs_subPropertyOf), true)=true))). % 31.28/18.40 tff(c_30487, plain, (![D_722]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_722), true, icext(D_722, uri_owl_sameAs), true)=true))). % 31.28/18.40 tff(c_30418, plain, (![D_720]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_720), true, icext(D_720, uri_rdfs_subClassOf), true)=true))). % 31.28/18.40 tff(c_30352, plain, (![D_718]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_718), true, icext(D_718, uri_rdfs_ContainerMembershipProperty), true)=true))). % 31.28/18.40 tff(c_30258, plain, (![D_716]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_716), true, icext(D_716, uri_rdfs_Class), true)=true))). % 31.28/18.40 tff(c_2307, plain, (![P_100]: (ifeq(iext(uri_rdfs_subPropertyOf, P_100, uri_rdf_type), true, ifeq(iext(P_100, uri_rdf_nil, uri_rdf_List), true, true, true), true)=true))). % 31.28/18.40 tff(c_30068, plain, (![D_713]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_713), true, icext(D_713, uri_rdf_XMLLiteral), true)=true))). % 31.28/18.40 tff(c_30001, plain, (![D_711]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_711), true, icext(D_711, uri_rdfs_Seq), true)=true))). % 31.28/18.40 tff(c_2640, plain, (![P_100]: (ifeq(iext(uri_rdfs_subPropertyOf, P_100, uri_rdfs_domain), true, ifeq(iext(P_100, uri_rdfs_seeAlso, uri_rdfs_Resource), true, true, true), true)=true))). % 31.28/18.40 tff(c_29808, plain, (![D_708]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_708), true, icext(D_708, uri_rdf_Bag), true)=true))). % 31.28/18.40 tff(c_29742, plain, (![D_706]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_706), true, icext(D_706, uri_rdfs_Datatype), true)=true))). % 31.28/18.40 tff(c_29560, plain, (![D_703]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_703), true, icext(D_703, uri_rdf_Alt), true)=true))). % 31.28/18.40 tff(c_2628, plain, (![P_100]: (ifeq(iext(uri_rdfs_subPropertyOf, P_100, uri_rdf_type), true, ifeq(iext(P_100, uri_rdf_rest, uri_rdf_Property), true, true, true), true)=true))). % 31.28/18.40 tff(c_29494, plain, (![D_701]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_701), true, icext(D_701, uri_rdfs_Container), true)=true))). % 31.28/18.40 tff(c_29427, plain, (![D_699]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_699), true, icext(D_699, uri_rdfs_Literal), true)=true))). % 31.28/18.40 tff(c_2427, plain, (![P_100]: (ifeq(iext(uri_rdfs_subPropertyOf, P_100, uri_rdf_type), true, ifeq(iext(P_100, uri_rdf_subject, uri_rdf_Property), true, true, true), true)=true))). % 31.28/18.40 tff(c_29244, plain, (![D_696]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_696), true, icext(D_696, uri_rdfs_label), true)=true))). % 31.28/18.40 tff(c_29178, plain, (![D_694]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_694), true, icext(D_694, uri_rdf_List), true)=true))). % 31.28/18.40 tff(c_28988, plain, (![D_691]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_691), true, icext(D_691, uri_rdfs_Statement), true)=true))). % 31.28/18.40 tff(c_2397, plain, (![P_100]: (ifeq(iext(uri_rdfs_subPropertyOf, P_100, uri_rdfs_range), true, ifeq(iext(P_100, uri_rdf__1, uri_rdfs_Resource), true, true, true), true)=true))). % 31.28/18.40 tff(c_28922, plain, (![D_689]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_689), true, icext(D_689, uri_rdfs_seeAlso), true)=true))). % 31.28/18.40 tff(c_28818, plain, (![C_686]: (ifeq(iext(uri_rdfs_subClassOf, C_686, uri_rdf_Bag), true, iext(uri_rdfs_subClassOf, C_686, uri_rdfs_Container), true)=true))). % 31.28/18.40 tff(c_28788, plain, (![D_685]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_685), true, icext(D_685, uri_rdf_predicate), true)=true))). % 31.28/18.40 tff(c_14165, 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))). % 31.28/18.40 tff(c_14027, 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))). % 31.28/18.40 tff(c_14117, 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))). % 31.28/18.40 tff(c_2361, plain, (![P_100]: (ifeq(iext(uri_rdfs_subPropertyOf, P_100, uri_rdfs_range), true, ifeq(iext(P_100, uri_rdf__2, uri_rdfs_Resource), true, true, true), true)=true))). % 31.28/18.40 tff(c_13961, 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))). % 31.28/18.40 tff(c_13864, 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))). % 31.28/18.40 tff(c_28424, plain, (![D_673]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_673), true, icext(D_673, uri_rdf_type), true)=true))). % 31.28/18.40 tff(c_13640, 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))). % 31.28/18.40 tff(c_28358, plain, (![C_670]: (ifeq(iext(uri_rdfs_subClassOf, C_670, uri_rdfs_Datatype), true, iext(uri_rdfs_subClassOf, C_670, uri_rdfs_Class), true)=true))). % 31.28/18.40 tff(c_14833, 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))). % 31.28/18.40 tff(c_13212, 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))). % 31.28/18.40 tff(c_13278, 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))). % 31.28/18.40 tff(c_13280, 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))). % 31.28/18.40 tff(c_13501, 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))). % 31.28/18.40 tff(c_2355, plain, (![P_100]: (ifeq(iext(uri_rdfs_subPropertyOf, P_100, uri_rdfs_range), true, ifeq(iext(P_100, uri_rdf__3, uri_rdfs_Resource), true, true, true), true)=true))). % 31.28/18.40 tff(c_13437, 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))). % 31.28/18.40 tff(c_13503, 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))). % 31.28/18.40 tff(c_12399, 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))). % 31.28/18.40 tff(c_27928, plain, (![D_656]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, D_656), true, icext(D_656, uri_rdf_XMLLiteral), true)=true))). % 31.28/18.40 tff(c_12544, 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))). % 31.28/18.40 tff(c_12925, 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))). % 31.28/18.40 tff(c_12997, 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))). % 31.28/18.40 tff(c_2457, plain, (![P_100]: (ifeq(iext(uri_rdfs_subPropertyOf, P_100, uri_rdfs_range), true, ifeq(iext(P_100, uri_rdfs_comment, uri_rdfs_Literal), true, true, true), true)=true))). % 31.28/18.40 tff(c_13122, 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))). % 31.28/18.40 tff(c_12447, 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))). % 31.28/18.40 tff(c_12877, 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))). % 31.28/18.40 tff(c_27641, plain, (![D_647]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_647), true, icext(D_647, uri_rdf__3), true)=true))). % 31.28/18.40 tff(c_13046, 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))). % 31.28/18.40 tff(c_27559, plain, (![C_644]: (ifeq(iext(uri_rdfs_subClassOf, C_644, uri_rdf_Alt), true, iext(uri_rdfs_subClassOf, C_644, uri_rdfs_Container), true)=true))). % 31.28/18.40 tff(c_12497, 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))). % 31.28/18.40 tff(c_12665, 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))). % 31.28/18.40 tff(c_12216, 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))). % 31.28/18.40 tff(c_12304, 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))). % 31.28/18.40 tff(c_12352, 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))). % 31.28/18.40 tff(c_6421, 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))). % 31.28/18.40 tff(c_2517, plain, (![P_100]: (ifeq(iext(uri_rdfs_subPropertyOf, P_100, uri_rdfs_domain), true, ifeq(iext(P_100, uri_rdfs_member, uri_rdfs_Resource), true, true, true), true)=true))). % 31.28/18.40 tff(c_6996, 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))). % 31.28/18.40 tff(c_9224, 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))). % 31.28/18.41 tff(c_8896, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_48), true, iext(Q_48, uri_owl_sameAs, uri_owl_sameAs), true)=true))). % 31.28/18.41 tff(c_9453, 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))). % 31.28/18.41 tff(c_2586, plain, (![P_100]: (ifeq(iext(uri_rdfs_subPropertyOf, P_100, uri_rdfs_domain), true, ifeq(iext(P_100, uri_rdfs_subPropertyOf, uri_rdf_Property), true, true, true), true)=true))). % 31.28/18.41 tff(c_10151, 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))). % 31.28/18.41 tff(c_9742, 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))). % 31.28/18.41 tff(c_8099, 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))). % 31.28/18.41 tff(c_8098, 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))). % 31.28/18.41 tff(c_9549, 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))). % 31.28/18.41 tff(c_4789, 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))). % 31.28/18.41 tff(c_5095, 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))). % 31.28/18.41 tff(c_10153, 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))). % 31.28/18.41 tff(c_6502, 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))). % 31.28/18.41 tff(c_26702, plain, (![D_613]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, D_613), true, icext(D_613, uri_rdf__1), true)=true))). % 31.28/18.41 tff(c_9222, 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))). % 31.28/18.41 tff(c_9290, 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))). % 31.28/18.41 tff(c_2616, plain, (![P_100]: (ifeq(iext(uri_rdfs_subPropertyOf, P_100, uri_rdf_type), true, ifeq(iext(P_100, uri_rdf_XMLLiteral, uri_rdfs_Datatype), true, true, true), true)=true))). % 31.28/18.41 tff(c_9052, 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))). % 31.28/18.41 tff(c_4937, 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))). % 31.28/18.41 tff(c_8705, 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))). % 31.28/18.41 tff(c_6050, 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))). % 31.28/18.41 tff(c_26354, plain, (![X_599, Y_600]: (ifeq(iext(uri_rdfs_isDefinedBy, X_599, Y_600), true, iext(uri_rdfs_seeAlso, X_599, Y_600), true)=true))). % 31.28/18.41 tff(c_6601, 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))). % 31.28/18.41 tff(c_11587, 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))). % 31.28/18.41 tff(c_7269, 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))). % 31.28/18.41 tff(c_26227, plain, (![D_594]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_594), true, icext(D_594, uri_rdf_Property), true)=true))). % 31.28/18.41 tff(c_11986, 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))). % 31.28/18.41 tff(c_2493, plain, (![P_100]: (ifeq(iext(uri_rdfs_subPropertyOf, P_100, uri_rdfs_domain), true, ifeq(iext(P_100, uri_rdf__3, uri_rdfs_Resource), true, true, true), true)=true))). % 31.28/18.41 tff(c_7547, 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))). % 31.28/18.41 tff(c_8795, 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))). % 31.28/18.41 tff(c_11335, 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))). % 31.28/18.41 tff(c_25914, plain, (![D_585]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_585), true, icext(D_585, uri_rdf_rest), true)=true))). % 31.28/18.41 tff(c_5244, 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))). % 31.28/18.41 tff(c_5346, 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))). % 31.28/18.41 tff(c_9288, 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))). % 31.28/18.41 tff(c_4936, 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))). % 31.28/18.41 tff(c_25689, plain, (![D_577]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_577), true, icext(D_577, uri_rdf__2), true)=true))). % 31.28/18.41 tff(c_11041, 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))). % 31.28/18.41 tff(c_5922, 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))). % 31.28/18.41 tff(c_6315, 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))). % 31.28/18.41 tff(c_2580, plain, (![P_100]: (ifeq(iext(uri_rdfs_subPropertyOf, P_100, uri_rdfs_subPropertyOf), true, ifeq(iext(P_100, uri_rdfs_isDefinedBy, uri_rdfs_seeAlso), true, true, true), true)=true))). % 31.28/18.41 tff(c_4678, 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))). % 31.28/18.41 tff(c_11775, 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))). % 31.28/18.41 tff(c_6801, 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))). % 31.28/18.41 tff(c_8793, 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))). % 31.28/18.41 tff(c_11492, 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))). % 31.28/18.41 tff(c_6602, 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))). % 31.28/18.41 tff(c_9388, 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))). % 31.28/18.41 tff(c_2373, plain, (![P_100]: (ifeq(iext(uri_rdfs_subPropertyOf, P_100, uri_rdfs_range), true, ifeq(iext(P_100, uri_rdfs_isDefinedBy, uri_rdfs_Resource), true, true, true), true)=true))). % 31.28/18.41 tff(c_8986, 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))). % 31.28/18.41 tff(c_25099, plain, (![D_559]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_559), true, icext(D_559, uri_rdf_first), true)=true))). % 31.28/18.41 tff(c_9117, 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))). % 31.28/18.41 tff(c_11720, 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))). % 31.28/18.41 tff(c_10331, 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))). % 31.28/18.41 tff(c_2463, plain, (![P_100]: (ifeq(iext(uri_rdfs_subPropertyOf, P_100, uri_rdfs_range), true, ifeq(iext(P_100, uri_rdfs_member, uri_rdfs_Resource), true, true, true), true)=true))). % 31.28/18.41 tff(c_5988, 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))). % 31.28/18.41 tff(c_24783, plain, (![D_550]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_550), true, icext(D_550, uri_rdf_object), true)=true))). % 31.28/18.41 tff(c_6503, 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))). % 31.28/18.41 tff(c_7187, 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))). % 31.28/18.41 tff(c_5347, 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))). % 31.28/18.41 tff(c_2433, plain, (![P_100]: (ifeq(iext(uri_rdfs_subPropertyOf, P_100, uri_rdfs_domain), true, ifeq(iext(P_100, uri_rdf__1, uri_rdfs_Resource), true, true, true), true)=true))). % 31.28/18.41 tff(c_7548, 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))). % 31.28/18.41 tff(c_11589, 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))). % 31.28/18.41 tff(c_4869, 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))). % 31.28/18.41 tff(c_24472, plain, (![D_541]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, D_541), true, icext(D_541, uri_rdf__3), true)=true))). % 31.28/18.41 tff(c_12077, 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))). % 31.28/18.41 tff(c_2661, plain, (![Q_101]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_owl_sameAs, Q_101), true, iext(Q_101, uri_ex_u, literal_plain(dat_str_abc)), true)=true))). % 31.28/18.41 tff(c_8362, 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))). % 31.28/18.41 tff(c_6799, 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))). % 31.28/18.41 tff(c_24232, plain, (![D_532]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_532), true, icext(D_532, uri_rdfs_comment), true)=true))). % 31.28/18.41 tff(c_5642, 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))). % 31.28/18.41 tff(c_2662, plain, (![Q_101]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_owl_sameAs, Q_101), true, iext(Q_101, sK1_testcase_premise_fullish_006_Literal_Values_represented_by_URIs_and_Blank_Nodes_BNODE_x, literal_plain(dat_str_abc)), true)=true))). % 31.28/18.41 tff(c_14711, 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))). % 31.28/18.41 tff(c_5806, 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))). % 31.28/18.41 tff(c_7799, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, uri_owl_sameAs, uri_rdf_Property), true)=true))). % 31.28/18.41 tff(c_12075, 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))). % 31.28/18.41 tff(c_4576, plain, (![Q_48, X_140]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, X_140, uri_rdfs_Resource), true)=true))). % 31.28/18.41 tff(c_2701, plain, (![Q_101]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_101), true, iext(Q_101, uri_rdfs_subPropertyOf, uri_rdf_Property), true)=true))). % 31.28/18.41 tff(c_2682, plain, (![Q_101]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_101), true, iext(Q_101, uri_rdf_subject, uri_rdfs_Resource), true)=true))). % 31.28/18.41 tff(c_2664, plain, (![Q_101]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_101), true, iext(Q_101, uri_rdf_nil, uri_rdf_List), true)=true))). % 31.28/18.41 tff(c_2702, plain, (![Q_101]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_101), true, iext(Q_101, uri_rdf_type, uri_rdfs_Class), true)=true))). % 31.28/18.41 tff(c_2685, plain, (![Q_101]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_101), true, iext(Q_101, uri_rdf__1, uri_rdfs_Resource), true)=true))). % 31.28/18.41 tff(c_2666, plain, (![Q_101]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_101), true, iext(Q_101, uri_rdf__3, uri_rdfs_ContainerMembershipProperty), true)=true))). % 31.28/18.41 tff(c_2718, plain, (![Q_101]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_101), true, iext(Q_101, uri_rdfs_range, uri_rdf_Property), true)=true))). % 31.28/18.41 tff(c_2693, plain, (![Q_101]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_101), true, iext(Q_101, uri_rdf_object, uri_rdfs_Statement), true)=true))). % 31.28/18.41 tff(c_2669, plain, (![Q_101]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_101), true, iext(Q_101, uri_rdf_subject, uri_rdfs_Statement), true)=true))). % 31.28/18.41 tff(c_2717, plain, (![Q_101]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_101), true, iext(Q_101, uri_rdf_rest, uri_rdf_Property), true)=true))). % 31.28/18.41 tff(c_2710, plain, (![Q_101]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_101), true, iext(Q_101, uri_rdfs_subPropertyOf, uri_rdf_Property), true)=true))). % 31.28/18.41 tff(c_2678, plain, (![Q_101]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_101), true, iext(Q_101, uri_rdf_type, uri_rdf_Property), true)=true))). % 31.28/18.41 tff(c_2722, plain, (![Q_101]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_101), true, iext(Q_101, uri_rdf_type, uri_rdfs_Resource), true)=true))). % 31.28/18.41 tff(c_1830, plain, (![C_93]: (ifeq(iext(uri_rdfs_range, uri_owl_sameAs, C_93), true, icext(C_93, literal_plain(dat_str_abc)), true)=true))). % 31.28/18.41 tff(c_2815, plain, (![E_105]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, E_105), true, iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, E_105), true)=true))). % 31.28/18.41 tff(c_2719, plain, (![Q_101]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_101), true, iext(Q_101, uri_rdfs_seeAlso, uri_rdfs_Resource), true)=true))). % 31.28/18.41 tff(c_2668, plain, (![Q_101]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_101), true, iext(Q_101, uri_rdf__2, uri_rdfs_ContainerMembershipProperty), true)=true))). % 31.28/18.41 tff(c_2694, plain, (![Q_101]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_101), true, iext(Q_101, uri_rdf_object, uri_rdf_Property), true)=true))). % 31.28/18.41 tff(c_2810, plain, (![E_105]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Container, E_105), true, iext(uri_rdfs_subClassOf, uri_rdfs_Seq, E_105), true)=true))). % 31.28/18.41 tff(c_2688, plain, (![Q_101]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_101), true, iext(Q_101, uri_rdfs_isDefinedBy, uri_rdfs_Resource), true)=true))). % 31.28/18.41 tff(c_2681, plain, (![Q_101]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_101), true, iext(Q_101, uri_rdf__2, uri_rdf_Property), true)=true))). % 31.28/18.41 tff(c_2673, plain, (![Q_101]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_101), true, iext(Q_101, uri_rdf__2, uri_rdfs_Resource), true)=true))). % 31.28/18.41 tff(c_2813, plain, (![E_105]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Container, E_105), true, iext(uri_rdfs_subClassOf, uri_rdf_Bag, E_105), true)=true))). % 31.28/18.41 tff(c_23371, plain, (![D_496]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_496), true, icext(D_496, uri_rdf_subject), true)=true))). % 31.28/18.41 tff(c_2712, plain, (![Q_101]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_101), true, iext(Q_101, uri_rdf_value, uri_rdf_Property), true)=true))). % 31.28/18.41 tff(c_2667, plain, (![Q_101]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_101), true, iext(Q_101, uri_rdfs_subClassOf, uri_rdfs_Class), true)=true))). % 31.28/18.41 tff(c_2714, plain, (![Q_101]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_101), true, iext(Q_101, uri_rdf_rest, uri_rdf_List), true)=true))). % 31.28/18.41 tff(c_2691, plain, (![Q_101]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_101), true, iext(Q_101, uri_rdf_value, uri_rdfs_Resource), true)=true))). % 31.28/18.41 tff(c_2663, plain, (![Q_101]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_101), true, iext(Q_101, uri_rdf_Property, uri_rdfs_Class), true)=true))). % 31.28/18.41 tff(c_2706, plain, (![Q_101]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_101), true, iext(Q_101, uri_rdf_rest, uri_rdf_List), true)=true))). % 31.28/18.41 tff(c_2679, plain, (![Q_101]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_101), true, iext(Q_101, uri_rdf__1, uri_rdfs_Resource), true)=true))). % 31.28/18.41 tff(c_2675, plain, (![Q_101]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_101), true, iext(Q_101, uri_rdfs_isDefinedBy, uri_rdfs_Resource), true)=true))). % 31.28/18.41 tff(c_2711, plain, (![Q_101]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_101), true, iext(Q_101, uri_rdfs_range, uri_rdfs_Class), true)=true))). % 31.28/18.41 tff(c_2709, plain, (![Q_101]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_101), true, iext(Q_101, uri_rdfs_isDefinedBy, uri_rdfs_seeAlso), true)=true))). % 31.28/18.41 tff(c_2689, plain, (![Q_101]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_101), true, iext(Q_101, uri_rdfs_comment, uri_rdfs_Literal), true)=true))). % 31.28/18.41 tff(c_2697, plain, (![Q_101]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_101), true, iext(Q_101, uri_rdfs_Datatype, uri_rdfs_Class), true)=true))). % 31.28/18.41 tff(c_2700, plain, (![Q_101]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_101), true, iext(Q_101, uri_rdf_Bag, uri_rdfs_Container), true)=true))). % 31.28/18.42 tff(c_2684, plain, (![Q_101]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_101), true, iext(Q_101, uri_rdf_subject, uri_rdf_Property), true)=true))). % 31.28/18.42 tff(c_2676, plain, (![Q_101]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_101), true, iext(Q_101, uri_rdf_predicate, uri_rdfs_Statement), true)=true))). % 31.28/18.42 tff(c_2720, plain, (![Q_101]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_101), true, iext(Q_101, uri_rdfs_seeAlso, uri_rdfs_Resource), true)=true))). % 31.28/18.42 tff(c_23002, plain, (![D_478]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_List, D_478), true, icext(D_478, uri_rdf_nil), true)=true))). % 31.28/18.42 tff(c_2686, plain, (![Q_101]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_101), true, iext(Q_101, uri_rdf__3, uri_rdf_Property), true)=true))). % 31.28/18.42 tff(c_2677, plain, (![Q_101]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_101), true, iext(Q_101, uri_rdfs_Seq, uri_rdfs_Container), true)=true))). % 31.28/18.42 tff(c_2707, plain, (![Q_101]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_101), true, iext(Q_101, uri_rdfs_ContainerMembershipProperty, uri_rdf_Property), true)=true))). % 31.28/18.42 tff(c_2814, plain, (![E_105]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Literal, E_105), true, iext(uri_rdfs_subClassOf, uri_rdf_XMLLiteral, E_105), true)=true))). % 31.28/18.42 tff(c_2671, plain, (![Q_101]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_owl_sameAs, Q_101), true, iext(Q_101, sK1_testcase_premise_fullish_006_Literal_Values_represented_by_URIs_and_Blank_Nodes_BNODE_x, uri_ex_w), true)=true))). % 31.28/18.42 tff(c_2690, plain, (![Q_101]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_101), true, iext(Q_101, uri_rdfs_member, uri_rdfs_Resource), true)=true))). % 31.28/18.42 tff(c_2704, plain, (![Q_101]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_101), true, iext(Q_101, uri_rdfs_subClassOf, uri_rdfs_Class), true)=true))). % 31.28/18.42 tff(c_22806, plain, (![D_469]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_469), true, icext(D_469, uri_rdf_value), true)=true))). % 31.28/18.42 tff(c_2665, plain, (![Q_101]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_101), true, iext(Q_101, uri_rdf__1, uri_rdfs_ContainerMembershipProperty), true)=true))). % 31.28/18.42 tff(c_2674, plain, (![Q_101]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_101), true, iext(Q_101, uri_rdf_predicate, uri_rdfs_Resource), true)=true))). % 31.28/18.42 tff(c_14029, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_predicate), true)=true))). % 31.28/18.42 tff(c_14028, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_predicate), true)=true))). % 31.28/18.42 tff(c_14118, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_label), true)=true))). % 31.28/18.42 tff(c_14119, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_label), true)=true))). % 31.28/18.42 tff(c_14834, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_comment), true)=true))). % 31.28/18.42 tff(c_14835, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_comment), true)=true))). % 31.28/18.42 tff(c_13962, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_member), true)=true))). % 31.28/18.42 tff(c_2672, plain, (![Q_101]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_101), true, iext(Q_101, uri_rdf__3, uri_rdfs_Resource), true)=true))). % 31.28/18.42 tff(c_13865, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdfs_Resource), true)=true))). % 31.28/18.42 tff(c_22459, plain, (![D_456]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, D_456), true, icext(D_456, uri_rdf__2), true)=true))). % 31.28/18.42 tff(c_2692, plain, (![Q_101]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_101), true, iext(Q_101, uri_rdf_first, uri_rdf_Property), true)=true))). % 31.28/18.42 tff(c_13213, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdf_List), true)=true))). % 31.28/18.42 tff(c_13214, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdf_List), true)=true))). % 31.28/18.42 tff(c_13439, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdfs_Statement), true)=true))). % 31.28/18.42 tff(c_13438, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdfs_Statement), true)=true))). % 31.28/18.42 tff(c_2680, plain, (![Q_101]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_101), true, iext(Q_101, uri_rdf__1, uri_rdf_Property), true)=true))). % 31.28/18.42 tff(c_2695, plain, (![Q_101]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_101), true, iext(Q_101, uri_rdf__3, uri_rdfs_Resource), true)=true))). % 31.28/18.42 tff(c_2721, plain, (![Q_101]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_101), true, iext(Q_101, uri_rdf_first, uri_rdf_List), true)=true))). % 31.28/18.42 tff(c_22187, plain, (![D_446]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_446), true, icext(D_446, uri_rdf__1), true)=true))). % 31.28/18.42 tff(c_2698, plain, (![Q_101]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_101), true, iext(Q_101, uri_rdfs_comment, uri_rdfs_Resource), true)=true))). % 31.28/18.42 tff(c_21780, plain, (![D_441, X_442]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Resource, D_441), true, icext(D_441, X_442), true)=true))). % 31.28/18.42 tff(c_9390, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_object), true)=true))). % 31.28/18.42 tff(c_8988, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdf_XMLLiteral), true)=true))). % 31.28/18.42 tff(c_2705, plain, (![Q_101]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_101), true, iext(Q_101, uri_rdfs_domain, uri_rdf_Property), true)=true))). % 31.28/18.42 tff(c_9118, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_type), true)=true))). % 31.28/18.42 tff(c_21514, plain, (![C_89, X_61]: (ifeq(icext(C_89, X_61), true, true, true)=true))). % 31.28/18.42 tff(c_2708, plain, (![Q_101]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_101), true, iext(Q_101, uri_rdf_first, uri_rdfs_Resource), true)=true))). % 31.28/18.42 tff(c_4791, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdfs_ContainerMembershipProperty), true)=true))). % 31.28/18.42 tff(c_21417, plain, (![X_429, Y_430]: (ifeq(iext(uri_rdf_rest, X_429, Y_430), true, icext(uri_rdf_List, X_429), true)=true))). % 31.28/18.42 tff(c_8101, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_member), true)=true))). % 31.28/18.42 tff(c_2713, plain, (![Q_101]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_101), true, iext(Q_101, uri_rdfs_label, uri_rdfs_Literal), true)=true))). % 31.28/18.42 tff(c_9455, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_subPropertyOf), true)=true))). % 31.28/18.42 tff(c_8707, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_first), true)=true))). % 31.28/18.42 tff(c_20984, plain, (![X_421, Y_422]: (ifeq(iext(uri_rdfs_range, X_421, Y_422), true, icext(uri_rdfs_Class, Y_422), true)=true))). % 31.28/18.42 tff(c_9744, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdf_Alt), true)=true))). % 31.28/18.42 tff(c_2699, plain, (![Q_101]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_101), true, iext(Q_101, uri_rdfs_member, uri_rdfs_Resource), true)=true))). % 31.28/18.42 tff(c_6998, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_subject), true)=true))). % 31.28/18.42 tff(c_20874, plain, (![X_414, Y_415]: (ifeq(iext(uri_rdf_subject, X_414, Y_415), true, icext(uri_rdfs_Statement, X_414), true)=true))). % 31.28/18.42 tff(c_8897, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_owl_sameAs), true)=true))). % 31.28/18.42 tff(c_2811, plain, (![E_105]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Container, E_105), true, iext(uri_rdfs_subClassOf, uri_rdf_Alt, E_105), true)=true))). % 31.28/18.42 tff(c_6423, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_isDefinedBy), true)=true))). % 31.28/18.42 tff(c_9054, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdf_Bag), true)=true))). % 31.28/18.42 tff(c_9550, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdfs_Literal), true)=true))). % 31.28/18.42 tff(c_20433, plain, (![X_405, Y_406]: (ifeq(iext(uri_rdfs_domain, X_405, Y_406), true, icext(uri_rdfs_Class, Y_406), true)=true))). % 31.28/18.42 tff(c_11337, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf__2), true)=true))). % 31.28/18.42 tff(c_11721, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_subClassOf), true)=true))). % 31.28/18.42 tff(c_2703, plain, (![Q_101]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_101), true, iext(Q_101, uri_rdf_XMLLiteral, uri_rdfs_Literal), true)=true))). % 31.28/18.42 tff(c_6997, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_subject), true)=true))). % 31.28/18.42 tff(c_9389, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_object), true)=true))). % 31.28/18.42 tff(c_20280, plain, (![X_396, Y_397]: (ifeq(iext(uri_rdf_object, X_396, Y_397), true, icext(uri_rdfs_Statement, X_396), true)=true))). % 31.28/18.42 tff(c_4680, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf__1), true)=true))). % 31.28/18.42 tff(c_8898, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_owl_sameAs), true)=true))). % 31.28/18.42 tff(c_5097, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_rest), true)=true))). % 31.28/18.42 tff(c_2683, plain, (![Q_101]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_101), true, iext(Q_101, uri_rdf__2, uri_rdfs_Resource), true)=true))). % 31.28/18.42 tff(c_9119, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_type), true)=true))). % 31.28/18.42 tff(c_19561, plain, (![X_386, Y_387]: (ifeq(iext(uri_rdfs_subClassOf, X_386, Y_387), true, icext(uri_rdfs_Class, X_386), true)=true))). % 31.28/18.42 tff(c_7189, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdfs_Datatype), true)=true))). % 31.28/18.42 tff(c_9454, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_subPropertyOf), true)=true))). % 31.28/18.42 tff(c_2848, plain, (![R_108]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_seeAlso, R_108), true, iext(uri_rdfs_subPropertyOf, uri_rdfs_isDefinedBy, R_108), true)=true))). % 31.28/18.42 tff(c_19140, plain, (![X_379, Y_380]: (ifeq(iext(uri_rdfs_range, X_379, Y_380), true, icext(uri_rdf_Property, X_379), true)=true))). % 31.28/18.42 tff(c_8706, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_first), true)=true))). % 31.28/18.42 tff(c_2687, plain, (![Q_101]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_101), true, iext(Q_101, uri_rdfs_domain, uri_rdfs_Class), true)=true))). % 31.28/18.42 tff(c_10332, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf__3), true)=true))). % 31.28/18.42 tff(c_18671, plain, (![X_372, Y_373]: (ifeq(iext(uri_rdfs_subPropertyOf, X_372, Y_373), true, icext(uri_rdf_Property, Y_373), true)=true))). % 31.28/18.42 tff(c_11336, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf__2), true)=true))). % 31.28/18.42 tff(c_10333, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf__3), true)=true))). % 31.28/18.42 tff(c_2716, plain, (![Q_101]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_101), true, iext(Q_101, uri_rdfs_label, uri_rdfs_Resource), true)=true))). % 31.28/18.42 tff(c_4870, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_value), true)=true))). % 31.28/18.42 tff(c_18181, plain, (![X_364, Y_365]: (ifeq(iext(uri_rdfs_subPropertyOf, X_364, Y_365), true, icext(uri_rdf_Property, X_364), true)=true))). % 31.28/18.42 tff(c_5245, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdf_Property), true)=true))). % 31.28/18.42 tff(c_11494, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdfs_Seq), true)=true))). % 31.28/18.42 tff(c_2670, plain, (![Q_101]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_101), true, iext(Q_101, uri_rdf_value, uri_rdfs_Resource), true)=true))). % 31.28/18.42 tff(c_11042, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_seeAlso), true)=true))). % 31.28/18.42 tff(c_6504, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf__1), true)=true))). % 31.28/18.42 tff(c_18019, plain, (![X_355, Y_356]: (ifeq(iext(uri_rdfs_label, X_355, Y_356), true, icext(uri_rdfs_Literal, Y_356), true)=true))). % 31.28/18.42 tff(c_2696, plain, (![Q_101]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_101), true, iext(Q_101, uri_rdf_Alt, uri_rdfs_Container), true)=true))). % 31.28/18.42 tff(c_6052, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_range), true)=true))). % 31.28/18.42 tff(c_5808, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_domain), true)=true))). % 31.28/18.42 tff(c_17910, plain, (![X_348, Y_349]: (ifeq(iext(uri_rdf_rest, X_348, Y_349), true, icext(uri_rdf_List, Y_349), true)=true))). % 31.28/18.42 tff(c_5989, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdfs_Class), true)=true))). % 31.28/18.42 tff(c_12078, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdfs_Container), true)=true))). % 31.28/18.42 tff(c_2812, plain, (![E_105]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, E_105), true, iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, E_105), true)=true))). % 31.28/18.42 tff(c_6051, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_range), true)=true))). % 31.28/18.42 tff(c_5096, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_rest), true)=true))). % 31.28/18.42 tff(c_12079, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdfs_Resource), true)=true))). % 31.28/18.42 tff(c_17297, plain, (![X_338, Y_339]: (ifeq(iext(uri_rdf_type, X_338, Y_339), true, icext(uri_rdfs_Class, Y_339), true)=true))). % 31.28/18.42 tff(c_11722, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_subClassOf), true)=true))). % 31.28/18.42 tff(c_5807, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_domain), true)=true))). % 31.28/18.42 tff(c_2715, plain, (![Q_101]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_101), true, iext(Q_101, uri_rdf_XMLLiteral, uri_rdfs_Datatype), true)=true))). % 31.28/18.42 tff(c_4871, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_value), true)=true))). % 31.28/18.42 tff(c_4578, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_29), true, icext(C_29, uri_rdfs_Resource), true)=true))). % 31.28/18.42 tff(c_4577, plain, (![C_19, X_140]: (ifeq(iext(uri_rdfs_domain, uri_rdf_type, C_19), true, icext(C_19, X_140), true)=true))). % 31.28/18.42 tff(c_16952, plain, (![X_327, Y_328]: (ifeq(iext(uri_rdfs_comment, X_327, Y_328), true, icext(uri_rdfs_Literal, Y_328), true)=true))). % 31.28/18.42 tff(c_16865, plain, (![X_321, Y_322]: (ifeq(iext(uri_rdf_first, X_321, Y_322), true, icext(uri_rdf_List, X_321), true)=true))). % 31.28/18.42 tff(c_2193, plain, (![C_97]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_97), true, icext(C_97, uri_rdfs_comment), true)=true))). % 31.28/18.42 tff(c_2224, plain, (![C_97]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_97), true, icext(C_97, uri_rdfs_label), true)=true))). % 31.28/18.42 tff(c_1893, plain, (![C_93]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_93), true, icext(C_93, uri_rdfs_Datatype), true)=true))). % 31.28/18.42 tff(c_2209, plain, (![C_97]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_97), true, icext(C_97, uri_rdf_type), true)=true))). % 31.28/18.42 tff(c_1880, plain, (![C_93]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_93), true, icext(C_93, uri_rdfs_Literal), true)=true))). % 31.28/18.42 tff(c_2217, plain, (![C_97]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_97), true, icext(C_97, uri_rdfs_subPropertyOf), true)=true))). % 31.28/18.42 tff(c_2169, plain, (![C_97]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_97), true, icext(C_97, uri_rdf_subject), true)=true))). % 31.28/18.42 tff(c_1887, plain, (![C_93]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_93), true, icext(C_93, uri_rdfs_seeAlso), true)=true))). % 31.28/18.42 tff(c_2194, plain, (![C_97]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_97), true, icext(C_97, uri_rdfs_member), true)=true))). % 31.28/18.42 tff(c_2211, plain, (![C_97]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_97), true, icext(C_97, uri_rdfs_subClassOf), true)=true))). % 31.28/18.42 tff(c_2208, plain, (![C_97]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_97), true, icext(C_97, uri_rdfs_subPropertyOf), true)=true))). % 31.28/18.42 tff(c_16354, plain, (![X_299, Y_300]: (ifeq(iext(uri_rdf_predicate, X_299, Y_300), true, icext(uri_rdfs_Statement, X_299), true)=true))). % 31.28/18.42 tff(c_2185, plain, (![C_97]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_97), true, icext(C_97, uri_rdf__2), true)=true))). % 31.28/18.42 tff(c_2210, plain, (![C_97]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_97), true, icext(C_97, uri_rdf_XMLLiteral), true)=true))). % 31.28/18.42 tff(c_2230, plain, (![C_97]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_97), true, icext(C_97, uri_rdf_first), true)=true))). % 31.28/18.42 tff(c_2206, plain, (![C_97]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_97), true, icext(C_97, uri_rdfs_member), true)=true))). % 31.28/18.42 tff(c_2207, plain, (![C_97]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_97), true, icext(C_97, uri_rdf_Bag), true)=true))). % 31.28/18.42 tff(c_2204, plain, (![C_97]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_97), true, icext(C_97, uri_rdfs_comment), true)=true))). % 31.28/18.42 tff(c_2212, plain, (![C_97]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_97), true, icext(C_97, uri_rdfs_domain), true)=true))). % 31.28/18.42 tff(c_2218, plain, (![C_97]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_97), true, icext(C_97, uri_rdfs_range), true)=true))). % 31.28/18.42 tff(c_2175, plain, (![C_97]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_97), true, icext(C_97, uri_rdf_predicate), true)=true))). % 31.28/18.42 tff(c_2176, plain, (![C_97]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_97), true, icext(C_97, uri_rdfs_isDefinedBy), true)=true))). % 31.28/18.43 tff(c_2201, plain, (![C_97]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_97), true, icext(C_97, uri_rdf_Alt), true)=true))). % 31.28/18.43 tff(c_2216, plain, (![C_97]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_97), true, icext(C_97, uri_rdfs_isDefinedBy), true)=true))). % 31.28/18.43 tff(c_15637, plain, (![X_282, Y_283]: (ifeq(iext(uri_rdfs_subClassOf, X_282, Y_283), true, icext(uri_rdfs_Class, Y_283), true)=true))). % 31.28/18.43 tff(c_2192, plain, (![C_97]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_97), true, icext(C_97, uri_rdfs_isDefinedBy), true)=true))). % 31.28/18.43 tff(c_1832, plain, (![C_93]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_93), true, icext(C_93, uri_rdfs_Class), true)=true))). % 31.28/18.43 tff(c_1874, plain, (![C_93]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_93), true, icext(C_93, uri_rdfs_Class), true)=true))). % 31.28/18.43 tff(c_1882, plain, (![C_93]: (ifeq(iext(uri_rdfs_range, uri_rdfs_domain, C_93), true, icext(C_93, uri_rdf_Property), true)=true))). % 31.28/18.43 tff(c_2214, plain, (![C_97]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_97), true, icext(C_97, uri_rdfs_ContainerMembershipProperty), true)=true))). % 31.28/18.43 tff(c_2228, plain, (![C_97]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_97), true, icext(C_97, uri_rdfs_seeAlso), true)=true))). % 31.28/18.43 tff(c_1892, plain, (![C_93]: (ifeq(iext(uri_rdfs_range, uri_rdfs_domain, C_93), true, icext(C_93, uri_rdf_List), true)=true))). % 31.28/18.43 tff(c_2221, plain, (![C_97]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_97), true, icext(C_97, uri_rdf_rest), true)=true))). % 31.28/18.43 tff(c_1840, plain, (![C_93]: (ifeq(iext(uri_rdfs_range, uri_owl_sameAs, C_93), true, icext(C_93, uri_ex_w), true)=true))). % 31.28/18.43 tff(c_2167, plain, (![C_97]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_97), true, icext(C_97, uri_rdfs_subClassOf), true)=true))). % 31.28/18.43 tff(c_2171, plain, (![C_97]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_97), true, icext(C_97, uri_rdf_value), true)=true))). % 31.28/18.43 tff(c_2215, plain, (![C_97]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_97), true, icext(C_97, uri_rdf_first), true)=true))). % 31.28/18.43 tff(c_2195, plain, (![C_97]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_97), true, icext(C_97, uri_rdf_value), true)=true))). % 31.28/18.43 tff(c_13215, plain, (![X_33]: (ifeq(icext(uri_rdf_List, X_33), true, icext(uri_rdf_List, X_33), true)=true))). % 31.28/18.43 tff(c_14357, plain, (![X_259, Y_260]: (ifeq(iext(uri_rdfs_domain, X_259, Y_260), true, icext(uri_rdf_Property, X_259), true)=true))). % 31.28/18.43 tff(c_13440, plain, (![X_33]: (ifeq(icext(uri_rdfs_Statement, X_33), true, icext(uri_rdfs_Statement, X_33), true)=true))). % 31.28/18.43 tff(c_5247, plain, (![X_33]: (ifeq(icext(uri_rdf_Property, X_33), true, icext(uri_rdf_Property, X_33), true)=true))). % 31.28/18.43 tff(c_8989, plain, (![X_33]: (ifeq(icext(uri_rdf_XMLLiteral, X_33), true, icext(uri_rdf_XMLLiteral, X_33), true)=true))). % 31.28/18.43 tff(c_9552, plain, (![X_33]: (ifeq(icext(uri_rdfs_Literal, X_33), true, icext(uri_rdfs_Literal, X_33), true)=true))). % 31.28/18.43 tff(c_9055, plain, (![X_33]: (ifeq(icext(uri_rdf_Bag, X_33), true, icext(uri_rdf_Bag, X_33), true)=true))). % 31.28/18.43 tff(c_14780, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_comment, uri_rdfs_comment)=true)). % 31.28/18.43 tff(c_14739, plain, (ip(uri_rdfs_comment)=true)). % 31.28/18.43 tff(c_2162, plain, (![C_97]: (ifeq(iext(uri_rdfs_domain, uri_owl_sameAs, C_97), true, icext(C_97, sK1_testcase_premise_fullish_006_Literal_Values_represented_by_URIs_and_Blank_Nodes_BNODE_x), true)=true))). % 31.28/18.43 tff(c_14669, plain, (iext(uri_rdf_type, uri_rdfs_comment, uri_rdf_Property)=true)). % 31.28/18.43 tff(c_14510, plain, (icext(uri_rdf_Property, uri_rdfs_comment)=true)). % 31.28/18.43 tff(c_7190, plain, (![X_33]: (ifeq(icext(uri_rdfs_Datatype, X_33), true, icext(uri_rdfs_Datatype, X_33), true)=true))). % 31.28/18.43 tff(c_5991, plain, (![X_33]: (ifeq(icext(uri_rdfs_Class, X_33), true, icext(uri_rdfs_Class, X_33), true)=true))). % 31.28/18.43 tff(c_11495, plain, (![X_33]: (ifeq(icext(uri_rdfs_Seq, X_33), true, icext(uri_rdfs_Seq, X_33), true)=true))). % 31.28/18.43 tff(c_5925, plain, (![X_33]: (ifeq(icext(uri_rdfs_Container, X_33), true, icext(uri_rdfs_Container, X_33), true)=true))). % 31.28/18.43 tff(c_9745, plain, (![X_33]: (ifeq(icext(uri_rdf_Alt, X_33), true, icext(uri_rdf_Alt, X_33), true)=true))). % 31.28/18.43 tff(c_4792, plain, (![X_33]: (ifeq(icext(uri_rdfs_ContainerMembershipProperty, X_33), true, icext(uri_rdfs_ContainerMembershipProperty, X_33), true)=true))). % 31.28/18.43 tff(c_14129, plain, (iext(uri_rdf_type, uri_rdfs_Resource, uri_rdfs_Class)=true)). % 31.28/18.43 tff(c_14064, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_label, uri_rdfs_label)=true)). % 31.28/18.43 tff(c_2178, plain, (![C_97]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_97), true, icext(C_97, uri_rdfs_Seq), true)=true))). % 31.28/18.43 tff(c_13974, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_predicate, uri_rdf_predicate)=true)). % 31.28/18.43 tff(c_13905, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_member, uri_rdfs_member)=true)). % 31.28/18.43 tff(c_1850, plain, (![C_93]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_93), true, icext(C_93, uri_rdfs_Container), true)=true))). % 31.28/18.43 tff(c_13808, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Resource, uri_rdfs_Resource)=true)). % 31.28/18.43 tff(c_13652, plain, (icext(uri_rdf_Property, uri_rdfs_member)=true)). % 31.28/18.43 tff(c_13581, plain, (iext(uri_rdf_type, uri_rdfs_member, uri_rdf_Property)=true)). % 31.28/18.43 tff(c_2161, plain, (![C_97]: (ifeq(iext(uri_rdfs_domain, uri_owl_sameAs, C_97), true, icext(C_97, uri_ex_u), true)=true))). % 31.28/18.43 tff(c_13450, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Statement, uri_rdfs_Resource)=true)). % 31.28/18.43 tff(c_13359, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Statement, uri_rdfs_Statement)=true)). % 31.28/18.43 tff(c_2190, plain, (![C_97]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_97), true, icext(C_97, uri_rdfs_domain), true)=true))). % 31.28/18.43 tff(c_13227, plain, (iext(uri_rdfs_subClassOf, uri_rdf_List, uri_rdfs_Resource)=true)). % 31.28/18.43 tff(c_13134, plain, (iext(uri_rdfs_subClassOf, uri_rdf_List, uri_rdf_List)=true)). % 31.28/18.43 tff(c_13086, plain, (iext(uri_rdf_type, uri_rdfs_ContainerMembershipProperty, uri_rdfs_Class)=true)). % 31.28/18.43 tff(c_1891, plain, (![C_93]: (ifeq(iext(uri_rdfs_range, uri_rdfs_range, C_93), true, icext(C_93, uri_rdfs_Literal), true)=true))). % 31.28/18.43 tff(c_13010, plain, (iext(uri_rdf_type, uri_rdfs_Literal, uri_rdfs_Class)=true)). % 31.28/18.43 tff(c_12961, plain, (iext(uri_rdf_type, uri_rdfs_Container, uri_rdfs_Class)=true)). % 31.28/18.43 tff(c_1884, plain, (![C_93]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_93), true, icext(C_93, uri_rdf_Property), true)=true))). % 31.28/18.43 tff(c_12889, plain, (iext(uri_rdf_type, uri_rdfs_Class, uri_rdfs_Class)=true)). % 31.28/18.43 tff(c_12841, plain, (iext(uri_rdf_type, uri_rdfs_Datatype, uri_rdfs_Class)=true)). % 31.28/18.43 tff(c_2200, plain, (![C_97]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_97), true, icext(C_97, uri_rdf__3), true)=true))). % 31.28/18.43 tff(c_12676, plain, (ip(uri_rdfs_label)=true)). % 31.28/18.43 tff(c_12623, plain, (iext(uri_rdf_type, uri_rdfs_label, uri_rdf_Property)=true)). % 31.28/18.43 tff(c_12575, plain, (icext(uri_rdf_Property, uri_rdfs_label)=true)). % 31.28/18.43 tff(c_2220, plain, (![C_97]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_97), true, icext(C_97, uri_rdfs_label), true)=true))). % 31.28/18.43 tff(c_12508, plain, (iext(uri_rdf_type, uri_rdfs_Seq, uri_rdfs_Class)=true)). % 31.28/18.43 tff(c_12461, plain, (iext(uri_rdf_type, uri_rdf_Alt, uri_rdfs_Class)=true)). % 31.28/18.43 tff(c_12411, plain, (iext(uri_rdf_type, uri_rdf_Bag, uri_rdfs_Class)=true)). % 31.28/18.43 tff(c_12363, plain, (iext(uri_rdf_type, uri_rdf_XMLLiteral, uri_rdfs_Class)=true)). % 31.28/18.43 tff(c_12316, plain, (iext(uri_rdf_type, uri_rdfs_Statement, uri_rdfs_Class)=true)). % 31.28/18.43 tff(c_12268, plain, (iext(uri_rdf_type, uri_rdf_List, uri_rdfs_Class)=true)). % 31.28/18.43 tff(c_12227, plain, (ip(uri_rdf_predicate)=true)). % 31.28/18.43 tff(c_12149, plain, (iext(uri_rdf_type, uri_rdf_predicate, uri_rdf_Property)=true)). % 31.28/18.43 tff(c_1878, plain, (![C_93]: (ifeq(iext(uri_rdfs_range, uri_rdfs_range, C_93), true, icext(C_93, uri_rdf_Property), true)=true))). % 31.28/18.43 tff(c_12024, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Container, uri_rdfs_Resource)=true)). % 31.28/18.43 tff(c_2183, plain, (![C_97]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_97), true, icext(C_97, uri_rdf_subject), true)=true))). % 31.28/18.43 tff(c_11944, plain, (iext(uri_rdf_type, uri_rdfs_seeAlso, uri_rdf_Property)=true)). % 31.28/18.43 tff(c_11812, plain, (icext(uri_rdf_Property, uri_rdfs_subPropertyOf)=true)). % 31.28/18.43 tff(c_2232, plain, (![C_97]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_97), true, icext(C_97, uri_rdf_type), true)=true))). % 31.28/18.43 tff(c_11733, plain, (iext(uri_rdf_type, uri_rdfs_subPropertyOf, uri_rdf_Property)=true)). % 31.28/18.43 tff(c_11667, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, uri_rdfs_subClassOf)=true)). % 31.28/18.43 tff(c_11507, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, uri_rdfs_Resource)=true)). % 31.28/18.43 tff(c_11439, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Seq, uri_rdfs_Seq)=true)). % 31.28/18.43 tff(c_1135, plain, (![S_5, O_6]: (ifeq(iext(uri_rdfs_subPropertyOf, S_5, O_6), true, true, true)=true))). % 31.28/18.43 tff(c_11250, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf__2, uri_rdf__2)=true)). % 31.28/18.43 tff(c_2173, plain, (![C_97]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_97), true, icext(C_97, uri_rdf__3), true)=true))). % 31.28/18.43 tff(c_11131, plain, (ic(uri_rdfs_Statement)=true)). % 31.28/18.43 tff(c_11073, plain, (icext(uri_rdfs_Class, uri_rdfs_Statement)=true)). % 31.28/18.43 tff(c_1849, plain, (![C_93]: (ifeq(iext(uri_rdfs_range, uri_rdfs_domain, C_93), true, icext(C_93, uri_rdfs_Statement), true)=true))). % 31.28/18.43 tff(c_10985, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_seeAlso, uri_rdfs_seeAlso)=true)). % 31.28/18.43 tff(c_10730, plain, (icext(uri_rdf_Property, uri_rdf_predicate)=true)). % 31.28/18.43 tff(c_2177, plain, (![C_97]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_97), true, icext(C_97, uri_rdf_predicate), true)=true))). % 31.28/18.43 tff(c_10275, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf__3, uri_rdf__3)=true)). % 31.28/18.43 tff(c_800, plain, (![S_5, O_6]: (ifeq(iext(uri_rdfs_range, S_5, O_6), true, true, true)=true))). % 31.28/18.43 tff(c_10100, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Seq, uri_rdfs_Resource)=true)). % 31.28/18.43 tff(c_2188, plain, (![C_97]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_97), true, icext(C_97, uri_rdf__1), true)=true))). % 31.28/18.43 tff(c_823, plain, (![S_5, O_6]: (ifeq(iext(uri_rdfs_domain, S_5, O_6), true, true, true)=true))). % 31.28/18.43 tff(c_9689, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Alt, uri_rdf_Alt)=true)). % 31.28/18.43 tff(c_9465, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Literal, uri_rdfs_Literal)=true)). % 31.28/18.43 tff(c_2180, plain, (![C_97]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_97), true, icext(C_97, uri_rdf__1), true)=true))). % 31.28/18.43 tff(c_9401, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf)=true)). % 31.28/18.43 tff(c_9335, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_object, uri_rdf_object)=true)). % 31.28/18.43 tff(c_9237, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Bag, uri_rdfs_Resource)=true)). % 31.28/18.43 tff(c_9171, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf__3, uri_rdfs_member)=true)). % 31.28/18.43 tff(c_9065, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_type, uri_rdf_type)=true)). % 31.28/18.43 tff(c_8999, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Bag, uri_rdf_Bag)=true)). % 31.28/18.43 tff(c_8933, plain, (iext(uri_rdfs_subClassOf, uri_rdf_XMLLiteral, uri_rdf_XMLLiteral)=true)). % 31.28/18.43 tff(c_1901, plain, (![C_93]: (ifeq(iext(uri_rdfs_range, uri_rdfs_domain, C_93), true, icext(C_93, uri_rdfs_Resource), true)=true))). % 31.28/18.43 tff(c_8840, plain, (iext(uri_rdfs_subPropertyOf, uri_owl_sameAs, uri_owl_sameAs)=true)). % 31.28/18.43 tff(c_8742, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Literal, uri_rdfs_Resource)=true)). % 31.28/18.43 tff(c_8653, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_first, uri_rdf_first)=true)). % 31.28/18.43 tff(c_8374, plain, (icext(uri_rdf_Property, uri_rdfs_subClassOf)=true)). % 31.28/18.43 tff(c_8320, plain, (iext(uri_rdf_type, uri_rdfs_subClassOf, uri_rdf_Property)=true)). % 31.28/18.43 tff(c_2197, plain, (![C_97]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_97), true, icext(C_97, uri_rdf_object), true)=true))). % 31.28/18.43 tff(c_8050, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf__2, uri_rdfs_member)=true)). % 31.28/18.43 tff(c_1848, plain, (![C_93]: (ifeq(iext(uri_rdfs_range, uri_rdfs_range, C_93), true, icext(C_93, uri_rdfs_Resource), true)=true))). % 31.28/18.43 tff(c_7811, plain, (icext(uri_rdf_Property, uri_owl_sameAs)=true)). % 31.28/18.43 tff(c_7757, plain, (iext(uri_rdf_type, uri_owl_sameAs, uri_rdf_Property)=true)). % 31.28/18.43 tff(c_2174, plain, (![C_97]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_97), true, icext(C_97, uri_rdf__2), true)=true))). % 31.28/18.43 tff(c_1567, plain, (![S_5, O_6]: (ifeq(iext(uri_rdfs_subClassOf, S_5, O_6), true, true, true)=true))). % 31.28/18.43 tff(c_7499, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Property, uri_rdfs_Resource)=true)). % 31.28/18.43 tff(c_2213, plain, (![C_97]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_97), true, icext(C_97, uri_rdf_rest), true)=true))). % 31.28/18.43 tff(c_1168, plain, (![S_5, O_6]: (ifeq(iext(uri_rdf_object, S_5, O_6), true, true, true)=true))). % 31.28/18.43 tff(c_7308, plain, (icext(uri_rdf_Property, uri_rdfs_isDefinedBy)=true)). % 31.28/18.43 tff(c_1881, plain, (![C_93]: (ifeq(iext(uri_rdfs_range, uri_rdfs_domain, C_93), true, icext(C_93, uri_rdfs_Class), true)=true))). % 31.28/18.43 tff(c_7227, plain, (iext(uri_rdf_type, uri_rdfs_isDefinedBy, uri_rdf_Property)=true)). % 31.28/18.43 tff(c_7138, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, uri_rdfs_Datatype)=true)). % 31.28/18.43 tff(c_2202, plain, (![C_97]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_97), true, icext(C_97, uri_rdfs_Datatype), true)=true))). % 31.28/18.43 tff(c_3169, plain, (![S_5, O_6]: (ifeq(iext(uri_rdf_rest, S_5, O_6), true, true, true)=true))). % 31.28/18.43 tff(c_6947, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_subject, uri_rdf_subject)=true)). % 31.28/18.43 tff(c_2226, plain, (![C_97]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_97), true, icext(C_97, uri_rdfs_range), true)=true))). % 31.28/18.43 tff(c_6748, plain, (iext(uri_rdfs_subClassOf, uri_rdf_XMLLiteral, uri_rdfs_Resource)=true)). % 31.28/18.43 tff(c_1855, plain, (![C_93]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_93), true, icext(C_93, uri_rdf_Property), true)=true))). % 31.28/18.43 tff(c_6553, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, uri_rdfs_Resource)=true)). % 31.28/18.43 tff(c_6515, plain, (ip(uri_rdfs_member)=true)). % 31.28/18.43 tff(c_6454, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf__1, uri_rdfs_member)=true)). % 31.28/18.43 tff(c_6372, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_isDefinedBy, uri_rdfs_isDefinedBy)=true)). % 31.28/18.43 tff(c_6326, plain, (icext(uri_rdf_Property, uri_rdfs_domain)=true)). % 31.28/18.43 tff(c_6273, plain, (iext(uri_rdf_type, uri_rdfs_domain, uri_rdf_Property)=true)). % 31.28/18.43 tff(c_1889, plain, (![C_93]: (ifeq(iext(uri_rdfs_range, uri_rdfs_range, C_93), true, icext(C_93, uri_rdfs_Class), true)=true))). % 31.28/18.43 tff(c_6080, plain, (icext(uri_rdf_Property, uri_rdfs_seeAlso)=true)). % 31.28/18.43 tff(c_2229, plain, (![C_97]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_97), true, icext(C_97, uri_rdfs_seeAlso), true)=true))). % 31.28/18.43 tff(c_6001, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_range, uri_rdfs_range)=true)). % 31.28/18.43 tff(c_5939, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Class, uri_rdfs_Class)=true)). % 31.28/18.43 tff(c_5849, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Container, uri_rdfs_Container)=true)). % 31.28/18.43 tff(c_1834, plain, (![C_93]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_93), true, icext(C_93, uri_rdfs_ContainerMembershipProperty), true)=true))). % 31.28/18.43 tff(c_5754, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, uri_rdfs_domain)=true)). % 31.28/18.43 tff(c_5653, plain, (icext(uri_rdf_Property, uri_rdfs_range)=true)). % 31.28/18.43 tff(c_5600, plain, (iext(uri_rdf_type, uri_rdfs_range, uri_rdf_Property)=true)). % 31.28/18.43 tff(c_1833, plain, (![C_93]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_93), true, icext(C_93, uri_rdf_List), true)=true))). % 31.28/18.43 tff(c_5524, plain, (ic(uri_rdf_List)=true)). % 31.28/18.43 tff(c_5468, plain, (icext(uri_rdfs_Class, uri_rdf_List)=true)). % 31.28/18.43 tff(c_1883, plain, (![C_93]: (ifeq(iext(uri_rdfs_range, uri_rdfs_range, C_93), true, icext(C_93, uri_rdf_List), true)=true))). % 31.28/18.43 tff(c_5298, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Class, uri_rdfs_Resource)=true)). % 31.28/18.43 tff(c_1530, plain, (![X_90]: (ifeq(icext(uri_rdfs_Seq, X_90), true, icext(uri_rdfs_Container, X_90), true)=true))). % 31.28/18.43 tff(c_5195, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Property, uri_rdf_Property)=true)). % 31.28/18.43 tff(c_1535, plain, (![X_90]: (ifeq(icext(uri_rdfs_ContainerMembershipProperty, X_90), true, icext(uri_rdf_Property, X_90), true)=true))). % 31.28/18.43 tff(c_740, plain, (![S_5, O_6]: (ifeq(iext(uri_owl_sameAs, S_5, O_6), true, true, true)=true))). % 31.28/18.43 tff(c_5046, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_rest, uri_rdf_rest)=true)). % 31.28/18.43 tff(c_4991, plain, (icext(uri_rdfs_Class, uri_rdfs_Resource)=true)). % 31.28/18.43 tff(c_1533, plain, (![X_90]: (ifeq(icext(uri_rdf_Bag, X_90), true, icext(uri_rdfs_Container, X_90), true)=true))). % 31.28/18.43 tff(c_4949, plain, (ic(uri_rdfs_Resource)=true)). % 31.28/18.43 tff(c_4888, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Alt, uri_rdfs_Resource)=true)). % 31.28/18.43 tff(c_1531, plain, (![X_90]: (ifeq(icext(uri_rdf_Alt, X_90), true, icext(uri_rdfs_Container, X_90), true)=true))). % 31.28/18.43 tff(c_4820, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_value, uri_rdf_value)=true)). % 31.28/18.43 tff(c_4740, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, uri_rdfs_ContainerMembershipProperty)=true)). % 31.28/18.43 tff(c_1534, plain, (![X_90]: (ifeq(icext(uri_rdf_XMLLiteral, X_90), true, icext(uri_rdfs_Literal, X_90), true)=true))). % 31.28/18.43 tff(c_4587, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf__1, uri_rdf__1)=true)). % 31.28/18.43 tff(c_1532, plain, (![X_90]: (ifeq(icext(uri_rdfs_Datatype, X_90), true, icext(uri_rdfs_Class, X_90), true)=true))). % 31.28/18.43 tff(c_4536, plain, (![X_139]: (iext(uri_rdf_type, X_139, uri_rdfs_Resource)=true))). % 31.28/18.43 tff(c_2231, plain, (![X_98, Y_99]: (ifeq(iext(uri_rdf_type, X_98, Y_99), true, true, true)=true))). % 31.28/18.43 tff(c_1856, plain, (![X_94, Y_95]: (ifeq(iext(uri_rdf_subject, X_94, Y_95), true, true, true)=true))). % 31.28/18.43 tff(c_2203, plain, (![X_98, Y_99]: (ifeq(iext(uri_rdfs_comment, X_98, Y_99), true, true, true)=true))). % 31.28/18.43 tff(c_2223, plain, (![X_98, Y_99]: (ifeq(iext(uri_rdfs_label, X_98, Y_99), true, true, true)=true))). % 31.28/18.43 tff(c_1845, plain, (![X_94, Y_95]: (ifeq(iext(uri_rdf_predicate, X_94, Y_95), true, true, true)=true))). % 31.28/18.43 tff(c_2170, plain, (![X_98, Y_99]: (ifeq(iext(uri_rdf_value, X_98, Y_99), true, true, true)=true))). % 31.28/18.44 tff(c_2205, plain, (![X_98, Y_99]: (ifeq(iext(uri_rdfs_member, X_98, Y_99), true, true, true)=true))). % 31.28/18.44 tff(c_1898, plain, (![X_94, Y_95]: (ifeq(iext(uri_rdfs_seeAlso, X_94, Y_95), true, true, true)=true))). % 31.28/18.44 tff(c_2184, plain, (![X_98, Y_99]: (ifeq(iext(uri_rdf__2, X_98, Y_99), true, true, true)=true))). % 31.28/18.44 tff(c_4346, plain, (icext(uri_rdfs_Class, uri_rdfs_ContainerMembershipProperty)=true)). % 31.28/18.44 tff(c_4301, plain, (icext(uri_rdfs_Class, uri_rdf_XMLLiteral)=true)). % 31.28/18.44 tff(c_2187, plain, (![X_98, Y_99]: (ifeq(iext(uri_rdf__1, X_98, Y_99), true, true, true)=true))). % 31.28/18.44 tff(c_4249, plain, (icext(uri_rdfs_Class, uri_rdfs_Literal)=true)). % 31.28/18.44 tff(c_4204, plain, (icext(uri_rdfs_Class, uri_rdf_Alt)=true)). % 31.28/18.44 tff(c_4151, plain, (icext(uri_rdfs_Class, uri_rdfs_Datatype)=true)). % 31.28/18.44 tff(c_2199, plain, (![X_98, Y_99]: (ifeq(iext(uri_rdf__3, X_98, Y_99), true, true, true)=true))). % 31.28/18.44 tff(c_1885, plain, (![X_94, Y_95]: (ifeq(iext(uri_rdf_first, X_94, Y_95), true, true, true)=true))). % 31.28/18.44 tff(c_4085, plain, (icext(uri_rdfs_Class, uri_rdfs_Container)=true)). % 31.28/18.44 tff(c_4038, plain, (icext(uri_rdfs_Class, uri_rdfs_Seq)=true)). % 31.28/18.44 tff(c_3995, plain, (icext(uri_rdfs_Class, uri_rdf_Bag)=true)). % 31.28/18.44 tff(c_2191, plain, (![X_98, Y_99]: (ifeq(iext(uri_rdfs_isDefinedBy, X_98, Y_99), true, true, true)=true))). % 31.28/18.44 tff(c_3939, plain, (icext(uri_rdfs_Class, uri_rdfs_Class)=true)). % 31.28/18.44 tff(c_3895, plain, (icext(uri_rdf_Property, uri_rdf_first)=true)). % 31.28/18.44 tff(c_3852, plain, (icext(uri_rdf_Property, uri_rdf__2)=true)). % 31.28/18.44 tff(c_3813, plain, (icext(uri_rdf_Property, uri_rdf_value)=true)). % 31.28/18.44 tff(c_3774, plain, (icext(uri_rdf_Property, uri_rdf__3)=true)). % 31.28/18.44 tff(c_3732, plain, (icext(uri_rdf_Property, uri_rdf_type)=true)). % 31.28/18.44 tff(c_3693, plain, (icext(uri_rdf_Property, uri_rdf_rest)=true)). % 31.28/18.44 tff(c_3652, plain, (icext(uri_rdf_Property, uri_rdf_subject)=true)). % 31.28/18.44 tff(c_3610, plain, (icext(uri_rdfs_ContainerMembershipProperty, uri_rdf__2)=true)). % 31.28/18.44 tff(c_3562, plain, (icext(uri_rdfs_Datatype, uri_rdf_XMLLiteral)=true)). % 31.28/18.44 tff(c_3525, plain, (icext(uri_rdf_Property, uri_rdf__1)=true)). % 31.28/18.44 tff(c_3479, plain, (icext(uri_rdf_Property, uri_rdf_object)=true)). % 31.28/18.44 tff(c_3439, plain, (icext(uri_rdfs_ContainerMembershipProperty, uri_rdf__1)=true)). % 31.28/18.44 tff(c_3358, plain, (icext(uri_rdfs_Class, uri_rdf_Property)=true)). % 31.28/18.44 tff(c_3348, plain, (icext(uri_rdfs_ContainerMembershipProperty, uri_rdf__3)=true)). % 31.28/18.44 tff(c_3303, plain, (icext(uri_rdf_List, uri_rdf_nil)=true)). % 31.28/18.44 tff(c_3267, plain, (ic(uri_rdfs_ContainerMembershipProperty)=true)). % 31.28/18.44 tff(c_3232, plain, (ic(uri_rdfs_Seq)=true)). % 31.28/18.44 tff(c_3192, plain, (ip(uri_rdf__1)=true)). % 31.28/18.44 tff(c_3140, plain, (ip(uri_rdf_rest)=true)). % 31.28/18.44 tff(c_3100, plain, (ip(uri_rdf_subject)=true)). % 31.28/18.44 tff(c_3065, plain, (ic(uri_rdf_XMLLiteral)=true)). % 31.28/18.44 tff(c_3030, plain, (ic(uri_rdf_Property)=true)). % 31.28/18.44 tff(c_2977, plain, (ip(uri_rdf_first)=true)). % 31.28/18.44 tff(c_2933, plain, (ic(uri_rdfs_Class)=true)). % 31.28/18.44 tff(c_2893, plain, (ip(uri_rdf_value)=true)). % 31.28/18.44 tff(c_2855, plain, (ic(uri_rdf_Bag)=true)). % 31.28/18.44 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))). % 31.28/18.44 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))). % 31.28/18.44 tff(c_2272, plain, (ic(uri_rdf_Alt)=true)). % 31.28/18.44 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))). % 31.28/18.44 tff(c_2237, plain, (ic(uri_rdfs_Container)=true)). % 31.28/18.44 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))). % 31.28/18.44 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))). % 31.28/18.44 tff(c_1540, plain, (ip(uri_rdfs_subClassOf)=true)). % 31.28/18.44 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))). % 31.28/18.44 tff(c_1468, plain, (ip(uri_rdfs_seeAlso)=true)). % 31.28/18.44 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))). % 31.28/18.44 tff(c_1375, plain, (ip(uri_rdf__3)=true)). % 31.28/18.44 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))). % 31.28/18.44 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))). % 31.28/18.44 tff(c_1319, plain, (ic(uri_rdfs_Datatype)=true)). % 31.28/18.44 tff(c_1230, plain, (ip(uri_rdf__2)=true)). % 31.28/18.44 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))). % 31.28/18.44 tff(c_162, plain, (![P_43, Q_44]: (ifeq(iext(uri_rdfs_subPropertyOf, P_43, Q_44), true, ip(Q_44), true)=true))). % 31.28/18.44 tff(c_1144, plain, (ip(uri_rdf_object)=true)). % 31.28/18.44 tff(c_1075, plain, (ip(uri_rdfs_subPropertyOf)=true)). % 31.28/18.44 tff(c_152, plain, (![C_37, D_38]: (ifeq(iext(uri_rdfs_subClassOf, C_37, D_38), true, ic(C_37), true)=true))). % 31.28/18.44 tff(c_30, plain, (![P_10]: (ifeq(iext(uri_rdf_type, P_10, uri_rdf_Property), true, ip(P_10), true)=true))). % 31.28/18.44 tff(c_981, plain, (ip(uri_rdfs_isDefinedBy)=true)). % 31.28/18.44 tff(c_164, plain, (![P_45, Q_46]: (ifeq(iext(uri_rdfs_subPropertyOf, P_45, Q_46), true, ip(P_45), true)=true))). % 31.28/18.44 tff(c_919, plain, (ic(uri_rdfs_Literal)=true)). % 31.28/18.44 tff(c_156, plain, (![C_39]: (ifeq(ic(C_39), true, iext(uri_rdfs_subClassOf, C_39, C_39), true)=true))). % 31.28/18.44 tff(c_874, plain, (ip(uri_rdf_type)=true)). % 31.28/18.44 tff(c_150, plain, (![C_35, D_36]: (ifeq(iext(uri_rdfs_subClassOf, C_35, D_36), true, ic(D_36), true)=true))). % 31.28/18.44 tff(c_170, plain, (![P_51]: (ifeq(ip(P_51), true, iext(uri_rdfs_subPropertyOf, P_51, P_51), true)=true))). % 31.28/18.44 tff(c_808, plain, (ip(uri_rdfs_domain)=true)). % 31.28/18.44 tff(c_785, plain, (ip(uri_rdfs_range)=true)). % 31.28/18.44 tff(c_28, plain, (![P_9]: (ifeq(ip(P_9), true, iext(uri_rdf_type, P_9, uri_rdf_Property), true)=true))). % 31.28/18.44 tff(c_728, plain, (ip(uri_owl_sameAs)=true)). % 31.28/18.44 tff(c_4, plain, (![P_4, S_5, O_6]: (ifeq(iext(P_4, S_5, O_6), true, ip(P_4), true)=true))). % 31.28/18.44 tff(c_58, plain, (![C_15]: (ifeq(ic(C_15), true, iext(uri_rdfs_subClassOf, C_15, uri_rdfs_Resource), true)=true))). % 31.28/18.44 tff(c_114, plain, (![X_22]: (ifeq(ic(X_22), true, icext(uri_rdfs_Class, X_22), true)=true))). % 31.28/18.44 tff(c_122, plain, (![X_26]: (ifeq(icext(uri_rdfs_Literal, X_26), true, lv(X_26), true)=true))). % 31.28/18.44 tff(c_116, plain, (![X_23]: (ifeq(icext(uri_rdfs_Class, X_23), true, ic(X_23), true)=true))). % 31.28/18.44 tff(c_124, plain, (![X_27]: (ifeq(lv(X_27), true, icext(uri_rdfs_Literal, X_27), true)=true))). % 31.28/18.44 tff(c_477, plain, (![X_61]: (icext(uri_rdfs_Resource, X_61)=true))). % 31.28/18.44 tff(c_193, plain, (![X_8]: (ifeq(lv(X_8), true, true, true)=true))). % 31.28/18.44 tff(c_186, plain, (iext(uri_owl_sameAs, uri_ex_u, literal_plain(dat_str_abc))=true)). % 31.28/18.44 tff(c_2, plain, (![A_1, B_2, C_3]: (ifeq(A_1, A_1, B_2, C_3)=B_2))). % 31.28/18.44 tff(c_182, plain, (iext(uri_owl_sameAs, sK1_testcase_premise_fullish_006_Literal_Values_represented_by_URIs_and_Blank_Nodes_BNODE_x, literal_plain(dat_str_abc))=true)). % 31.28/18.44 tff(c_126, plain, (iext(uri_rdf_type, uri_rdf_Property, uri_rdfs_Class)=true)). % 31.28/18.44 tff(c_12, plain, (iext(uri_rdf_type, uri_rdf_nil, uri_rdf_List)=true)). % 31.28/18.44 tff(c_92, plain, (iext(uri_rdf_type, uri_rdf__1, uri_rdfs_ContainerMembershipProperty)=true)). % 31.28/18.44 tff(c_96, plain, (iext(uri_rdf_type, uri_rdf__3, uri_rdfs_ContainerMembershipProperty)=true)). % 31.28/18.44 tff(c_154, plain, (iext(uri_rdfs_range, uri_rdfs_subClassOf, uri_rdfs_Class)=true)). % 31.28/18.44 tff(c_94, plain, (iext(uri_rdf_type, uri_rdf__2, uri_rdfs_ContainerMembershipProperty)=true)). % 31.28/18.44 tff(c_142, plain, (iext(uri_rdfs_domain, uri_rdf_subject, uri_rdfs_Statement)=true)). % 31.28/18.44 tff(c_178, plain, (iext(uri_rdfs_domain, uri_rdf_value, uri_rdfs_Resource)=true)). % 31.28/18.44 tff(c_184, plain, (iext(uri_owl_sameAs, sK1_testcase_premise_fullish_006_Literal_Values_represented_by_URIs_and_Blank_Nodes_BNODE_x, uri_ex_w)=true)). % 31.28/18.44 tff(c_90, plain, (iext(uri_rdfs_range, uri_rdf__3, uri_rdfs_Resource)=true)). % 31.28/18.44 tff(c_88, plain, (iext(uri_rdfs_range, uri_rdf__2, uri_rdfs_Resource)=true)). % 31.28/18.44 tff(c_140, plain, (iext(uri_rdfs_range, uri_rdf_predicate, uri_rdfs_Resource)=true)). % 31.28/18.44 tff(c_42, plain, (iext(uri_rdfs_range, uri_rdfs_isDefinedBy, uri_rdfs_Resource)=true)). % 31.28/18.44 tff(c_138, plain, (iext(uri_rdfs_domain, uri_rdf_predicate, uri_rdfs_Statement)=true)). % 31.28/18.44 tff(c_98, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Seq, uri_rdfs_Container)=true)). % 31.28/18.44 tff(c_34, plain, (iext(uri_rdf_type, uri_rdf_type, uri_rdf_Property)=true)). % 31.28/18.44 tff(c_86, plain, (iext(uri_rdfs_range, uri_rdf__1, uri_rdfs_Resource)=true)). % 31.28/18.44 tff(c_16, plain, (iext(uri_rdf_type, uri_rdf__1, uri_rdf_Property)=true)). % 31.28/18.44 tff(c_18, plain, (iext(uri_rdf_type, uri_rdf__2, uri_rdf_Property)=true)). % 31.28/18.44 tff(c_144, plain, (iext(uri_rdfs_range, uri_rdf_subject, uri_rdfs_Resource)=true)). % 31.28/18.44 tff(c_82, plain, (iext(uri_rdfs_domain, uri_rdf__2, uri_rdfs_Resource)=true)). % 31.28/18.44 tff(c_26, plain, (iext(uri_rdf_type, uri_rdf_subject, uri_rdf_Property)=true)). % 31.28/18.44 tff(c_80, plain, (iext(uri_rdfs_domain, uri_rdf__1, uri_rdfs_Resource)=true)). % 31.28/18.44 tff(c_20, plain, (iext(uri_rdf_type, uri_rdf__3, uri_rdf_Property)=true)). % 31.28/18.44 tff(c_112, plain, (iext(uri_rdfs_range, uri_rdfs_domain, uri_rdfs_Class)=true)). % 31.28/18.44 tff(c_40, plain, (iext(uri_rdfs_domain, uri_rdfs_isDefinedBy, uri_rdfs_Resource)=true)). % 31.28/18.44 tff(c_38, plain, (iext(uri_rdfs_range, uri_rdfs_comment, uri_rdfs_Literal)=true)). % 31.28/18.44 tff(c_78, plain, (iext(uri_rdfs_range, uri_rdfs_member, uri_rdfs_Resource)=true)). % 31.28/18.44 tff(c_180, plain, (iext(uri_rdfs_range, uri_rdf_value, uri_rdfs_Resource)=true)). % 31.28/18.44 tff(c_10, plain, (iext(uri_rdf_type, uri_rdf_first, uri_rdf_Property)=true)). % 31.28/18.44 tff(c_134, plain, (iext(uri_rdfs_domain, uri_rdf_object, uri_rdfs_Statement)=true)). % 31.28/18.44 tff(c_22, plain, (iext(uri_rdf_type, uri_rdf_object, uri_rdf_Property)=true)). % 31.28/18.44 tff(c_84, plain, (iext(uri_rdfs_domain, uri_rdf__3, uri_rdfs_Resource)=true)). % 31.28/18.44 tff(c_68, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Alt, uri_rdfs_Container)=true)). % 31.28/18.44 tff(c_106, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, uri_rdfs_Class)=true)). % 31.28/18.44 tff(c_36, plain, (iext(uri_rdfs_domain, uri_rdfs_comment, uri_rdfs_Resource)=true)). % 31.28/18.44 tff(c_76, plain, (iext(uri_rdfs_domain, uri_rdfs_member, uri_rdfs_Resource)=true)). % 31.28/18.44 tff(c_70, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Bag, uri_rdfs_Container)=true)). % 31.28/18.44 tff(c_168, plain, (iext(uri_rdfs_range, uri_rdfs_subPropertyOf, uri_rdf_Property)=true)). % 31.28/18.44 tff(c_176, plain, (iext(uri_rdfs_range, uri_rdf_type, uri_rdfs_Class)=true)). % 31.28/18.44 tff(c_100, plain, (iext(uri_rdfs_subClassOf, uri_rdf_XMLLiteral, uri_rdfs_Literal)=true)). % 31.28/18.44 tff(c_146, plain, (iext(uri_rdfs_domain, uri_rdfs_subClassOf, uri_rdfs_Class)=true)). % 31.28/18.44 tff(c_108, plain, (iext(uri_rdfs_domain, uri_rdfs_domain, uri_rdf_Property)=true)). % 31.28/18.44 tff(c_66, plain, (iext(uri_rdfs_range, uri_rdf_rest, uri_rdf_List)=true)). % 31.28/18.44 tff(c_74, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, uri_rdf_Property)=true)). % 31.28/18.44 tff(c_62, plain, (iext(uri_rdfs_range, uri_rdf_first, uri_rdfs_Resource)=true)). % 31.28/18.44 tff(c_44, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_isDefinedBy, uri_rdfs_seeAlso)=true)). % 31.28/18.44 tff(c_160, plain, (iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, uri_rdf_Property)=true)). % 31.28/18.44 tff(c_132, plain, (iext(uri_rdfs_range, uri_rdfs_range, uri_rdfs_Class)=true)). % 31.28/18.44 tff(c_24, plain, (iext(uri_rdf_type, uri_rdf_value, uri_rdf_Property)=true)). % 31.28/18.44 tff(c_48, plain, (iext(uri_rdfs_range, uri_rdfs_label, uri_rdfs_Literal)=true)). % 31.28/18.44 tff(c_64, plain, (iext(uri_rdfs_domain, uri_rdf_rest, uri_rdf_List)=true)). % 31.28/18.44 tff(c_102, plain, (iext(uri_rdf_type, uri_rdf_XMLLiteral, uri_rdfs_Datatype)=true)). % 31.28/18.44 tff(c_46, plain, (iext(uri_rdfs_domain, uri_rdfs_label, uri_rdfs_Resource)=true)). % 31.28/18.44 tff(c_14, plain, (iext(uri_rdf_type, uri_rdf_rest, uri_rdf_Property)=true)). % 31.28/18.44 tff(c_128, plain, (iext(uri_rdfs_domain, uri_rdfs_range, uri_rdf_Property)=true)). % 31.28/18.44 tff(c_50, plain, (iext(uri_rdfs_domain, uri_rdfs_seeAlso, uri_rdfs_Resource)=true)). % 31.28/18.44 tff(c_52, plain, (iext(uri_rdfs_range, uri_rdfs_seeAlso, uri_rdfs_Resource)=true)). % 31.28/18.44 tff(c_60, plain, (iext(uri_rdfs_domain, uri_rdf_first, uri_rdf_List)=true)). % 31.28/18.44 tff(c_174, plain, (iext(uri_rdfs_domain, uri_rdf_type, uri_rdfs_Resource)=true)). % 31.28/18.44 tff(c_188, plain, (iext(uri_owl_sameAs, uri_ex_u, uri_ex_w)!=true)). % 31.28/18.44 tff(c_6, plain, (![X_7]: (ir(X_7)=true))). % 31.28/18.44 % SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 31.28/18.44 %------------------------------------------------------------------------------