%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : SWB023-10 : TPTP v9.0.0. Released v7.5.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 : n031.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:54 PM UTC 2025 % Result : Satisfiable 36.25s 23.67s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.13 % Problem : SWB023-10 : TPTP v9.0.0. Released v7.5.0. % 0.03/0.14 % 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.14/0.35 % Computer : n031.cluster.edu % 0.14/0.35 % Model : x86_64 x86_64 % 0.14/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.14/0.35 % Memory : 8042.1875MB % 0.14/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.14/0.35 % CPULimit : 300 % 0.14/0.35 % WCLimit : 300 % 0.14/0.35 % DateTime : Wed Apr 9 01:00:22 EDT 2025 % 0.14/0.36 % CPUTime : % 36.25/23.67 % 36.25/23.67 % SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 36.25/23.67 % 36.25/23.67 % SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 36.25/23.69 %$ ifeq > iext > tuple > icext > #nlpp > lv > ir > ip > ic > uri_rdfs_subPropertyOf > uri_rdfs_subClassOf > uri_rdfs_seeAlso > uri_rdfs_range > uri_rdfs_member > uri_rdfs_label > uri_rdfs_isDefinedBy > uri_rdfs_domain > uri_rdfs_comment > uri_rdfs_Statement > uri_rdfs_Seq > uri_rdfs_Resource > uri_rdfs_Literal > uri_rdfs_Datatype > uri_rdfs_ContainerMembershipProperty > uri_rdfs_Container > uri_rdfs_Class > uri_rdf_value > uri_rdf_type > uri_rdf_subject > uri_rdf_rest > uri_rdf_predicate > uri_rdf_object > uri_rdf_nil > uri_rdf_first > uri_rdf__3 > uri_rdf__2 > uri_rdf__1 > uri_rdf_XMLLiteral > uri_rdf_Property > uri_rdf_List > uri_rdf_Bag > uri_rdf_Alt > uri_owl_sameAs > uri_owl_oneOf > uri_owl_FunctionalProperty > uri_owl_Class > uri_ex_w > uri_ex_v > uri_ex_u > true > sK2_testcase_premise_fullish_023_Unique_List_Components_BNODE_l > sK1_testcase_premise_fullish_023_Unique_List_Components_BNODE_o % 36.25/23.69 % 36.25/23.69 %Foreground sorts: % 36.25/23.69 % 36.25/23.69 % 36.25/23.69 %Background operators: % 36.25/23.69 % 36.25/23.69 % 36.25/23.69 %Foreground operators: % 36.25/23.69 tff(uri_rdfs_Datatype, type, uri_rdfs_Datatype: $i). % 36.25/23.69 tff(uri_rdfs_ContainerMembershipProperty, type, uri_rdfs_ContainerMembershipProperty: $i). % 36.25/23.69 tff(uri_owl_oneOf, type, uri_owl_oneOf: $i). % 36.25/23.69 tff(uri_rdfs_Resource, type, uri_rdfs_Resource: $i). % 36.25/23.69 tff(uri_rdf_Property, type, uri_rdf_Property: $i). % 36.25/23.69 tff(uri_rdf_subject, type, uri_rdf_subject: $i). % 36.25/23.69 tff(uri_rdf_type, type, uri_rdf_type: $i). % 36.25/23.69 tff(uri_rdfs_subPropertyOf, type, uri_rdfs_subPropertyOf: $i). % 36.25/23.69 tff(uri_ex_u, type, uri_ex_u: $i). % 36.25/23.69 tff(uri_rdfs_seeAlso, type, uri_rdfs_seeAlso: $i). % 36.25/23.69 tff(icext, type, icext: ($i * $i) > $i). % 36.25/23.69 tff(uri_rdfs_range, type, uri_rdfs_range: $i). % 36.25/23.69 tff(uri_rdf_XMLLiteral, type, uri_rdf_XMLLiteral: $i). % 36.25/23.69 tff(uri_rdf_List, type, uri_rdf_List: $i). % 36.25/23.69 tff(uri_rdf_first, type, uri_rdf_first: $i). % 36.25/23.69 tff(sK2_testcase_premise_fullish_023_Unique_List_Components_BNODE_l, type, sK2_testcase_premise_fullish_023_Unique_List_Components_BNODE_l: $i). % 36.25/23.69 tff(uri_rdf_predicate, type, uri_rdf_predicate: $i). % 36.25/23.69 tff(tuple, type, tuple: ($i * $i) > $i). % 36.25/23.69 tff(ir, type, ir: $i > $i). % 36.25/23.69 tff(lv, type, lv: $i > $i). % 36.25/23.69 tff(uri_ex_v, type, uri_ex_v: $i). % 36.25/23.69 tff(uri_rdf__3, type, uri_rdf__3: $i). % 36.25/23.69 tff(uri_rdf_value, type, uri_rdf_value: $i). % 36.25/23.69 tff(uri_owl_FunctionalProperty, type, uri_owl_FunctionalProperty: $i). % 36.25/23.69 tff(ic, type, ic: $i > $i). % 36.25/23.69 tff(uri_rdfs_Statement, type, uri_rdfs_Statement: $i). % 36.25/23.69 tff(uri_rdf__1, type, uri_rdf__1: $i). % 36.25/23.69 tff(iext, type, iext: ($i * $i * $i) > $i). % 36.25/23.69 tff(uri_ex_w, type, uri_ex_w: $i). % 36.25/23.69 tff(uri_rdf_rest, type, uri_rdf_rest: $i). % 36.25/23.69 tff(uri_rdfs_label, type, uri_rdfs_label: $i). % 36.25/23.69 tff(uri_rdfs_Container, type, uri_rdfs_Container: $i). % 36.25/23.69 tff(uri_rdfs_subClassOf, type, uri_rdfs_subClassOf: $i). % 36.25/23.69 tff(sK1_testcase_premise_fullish_023_Unique_List_Components_BNODE_o, type, sK1_testcase_premise_fullish_023_Unique_List_Components_BNODE_o: $i). % 36.25/23.69 tff(uri_owl_sameAs, type, uri_owl_sameAs: $i). % 36.25/23.69 tff(uri_rdf_object, type, uri_rdf_object: $i). % 36.25/23.69 tff(ip, type, ip: $i > $i). % 36.25/23.69 tff(uri_rdfs_Class, type, uri_rdfs_Class: $i). % 36.25/23.69 tff(uri_rdfs_Seq, type, uri_rdfs_Seq: $i). % 36.25/23.69 tff(uri_owl_Class, type, uri_owl_Class: $i). % 36.25/23.69 tff(uri_rdfs_member, type, uri_rdfs_member: $i). % 36.25/23.69 tff(uri_rdf_Bag, type, uri_rdf_Bag: $i). % 36.25/23.69 tff(uri_rdf__2, type, uri_rdf__2: $i). % 36.25/23.69 tff(uri_rdfs_comment, type, uri_rdfs_comment: $i). % 36.25/23.69 tff(uri_rdfs_Literal, type, uri_rdfs_Literal: $i). % 36.25/23.69 tff(true, type, true: $i). % 36.25/23.69 tff(uri_rdf_Alt, type, uri_rdf_Alt: $i). % 36.25/23.69 tff(uri_rdf_nil, type, uri_rdf_nil: $i). % 36.25/23.69 tff(uri_rdfs_isDefinedBy, type, uri_rdfs_isDefinedBy: $i). % 36.25/23.69 tff(uri_rdfs_domain, type, uri_rdfs_domain: $i). % 36.25/23.69 tff(ifeq, type, ifeq: ($i * $i * $i * $i) > $i). % 36.25/23.69 % 36.25/23.69 %Saturated clause set: % 36.25/23.69 tff(c_75247, plain, (![X_1287, Y_1288]: (ifeq(iext(uri_rdfs_comment, X_1287, Y_1288), true, iext(uri_rdfs_comment, X_1287, Y_1288), true)=true))). % 36.25/23.69 tff(c_16156, 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))). % 36.25/23.69 tff(c_17367, 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))). % 36.25/23.69 tff(c_74973, plain, (![X_1279, Y_1280]: (ifeq(iext(uri_rdfs_label, X_1279, Y_1280), true, iext(uri_rdfs_label, X_1279, Y_1280), true)=true))). % 36.25/23.69 tff(c_74965, plain, (![X_1277, Y_1278]: (ifeq(iext(uri_rdf_predicate, X_1277, Y_1278), true, iext(uri_rdf_predicate, X_1277, Y_1278), true)=true))). % 36.25/23.69 tff(c_16221, 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))). % 36.25/23.69 tff(c_74817, plain, (![X_1272, Y_1273]: (ifeq(iext(uri_rdfs_member, X_1272, Y_1273), true, iext(uri_rdfs_member, X_1272, Y_1273), true)=true))). % 36.25/23.69 tff(c_16058, 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))). % 36.25/23.69 tff(c_15272, 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))). % 36.25/23.69 tff(c_18373, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subClassOf), true, ifeq(iext(P_47, uri_owl_FunctionalProperty, uri_owl_FunctionalProperty), true, true, true), true)=true))). % 36.25/23.69 tff(c_18200, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subClassOf), true, ifeq(iext(P_47, uri_owl_FunctionalProperty, uri_rdfs_Resource), true, true, true), true)=true))). % 36.25/23.69 tff(c_74189, plain, (![C_1266]: (ifeq(iext(uri_rdfs_subClassOf, C_1266, uri_rdfs_Statement), true, iext(uri_rdfs_subClassOf, C_1266, uri_rdfs_Resource), true)=true))). % 36.25/23.69 tff(c_15580, 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))). % 36.25/23.69 tff(c_18801, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subClassOf), true, ifeq(iext(P_47, uri_owl_Class, uri_rdfs_Resource), true, true, true), true)=true))). % 36.25/23.69 tff(c_73783, plain, (![C_1262]: (ifeq(iext(uri_rdfs_subClassOf, C_1262, sK1_testcase_premise_fullish_023_Unique_List_Components_BNODE_o), true, iext(uri_rdfs_subClassOf, C_1262, uri_rdfs_Resource), true)=true))). % 36.25/23.69 tff(c_15904, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subClassOf), true, ifeq(iext(P_47, sK1_testcase_premise_fullish_023_Unique_List_Components_BNODE_o, uri_rdfs_Resource), true, true, true), true)=true))). % 36.25/23.69 tff(c_15514, 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))). % 36.25/23.69 tff(c_73385, plain, (![C_1258]: (ifeq(iext(uri_rdfs_subClassOf, C_1258, uri_owl_FunctionalProperty), true, iext(uri_rdfs_subClassOf, C_1258, uri_rdfs_Resource), true)=true))). % 36.25/23.69 tff(c_73222, plain, (![C_1256]: (ifeq(iext(uri_rdfs_subClassOf, C_1256, uri_rdf_List), true, iext(uri_rdfs_subClassOf, C_1256, uri_rdfs_Resource), true)=true))). % 36.25/23.69 tff(c_15338, 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))). % 36.25/23.69 tff(c_18981, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subClassOf), true, ifeq(iext(P_47, uri_owl_Class, uri_owl_Class), true, true, true), true)=true))). % 36.25/23.69 tff(c_15812, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subClassOf), true, ifeq(iext(P_47, sK1_testcase_premise_fullish_023_Unique_List_Components_BNODE_o, sK1_testcase_premise_fullish_023_Unique_List_Components_BNODE_o), true, true, true), true)=true))). % 36.25/23.69 tff(c_15740, 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))). % 36.25/23.69 tff(c_72587, plain, (![C_1250]: (ifeq(iext(uri_rdfs_subClassOf, C_1250, uri_owl_Class), true, iext(uri_rdfs_subClassOf, C_1250, uri_rdfs_Resource), true)=true))). % 36.25/23.69 tff(c_7519, 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))). % 36.25/23.69 tff(c_14431, 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))). % 36.25/23.69 tff(c_11540, 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))). % 36.25/23.69 tff(c_5021, 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))). % 36.25/23.69 tff(c_14721, 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))). % 36.25/23.69 tff(c_5018, 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))). % 36.25/23.69 tff(c_7776, 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))). % 36.25/23.70 tff(c_14647, 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))). % 36.25/23.70 tff(c_15187, 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))). % 36.25/23.70 tff(c_7522, 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))). % 36.25/23.70 tff(c_14849, 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))). % 36.25/23.70 tff(c_14526, 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))). % 36.25/23.70 tff(c_7995, 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))). % 36.25/23.70 tff(c_7773, 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))). % 36.25/23.70 tff(c_8747, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdf_Property), true, ifeq(iext(P_28, X_30, uri_owl_oneOf), true, true, true), true)=true))). % 36.25/23.70 tff(c_7992, 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))). % 36.25/23.70 tff(c_14598, 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))). % 36.25/23.70 tff(c_14769, 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))). % 36.25/23.70 tff(c_8750, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdf_Property), true, ifeq(iext(P_18, uri_owl_oneOf, Y_21), true, true, true), true)=true))). % 36.25/23.70 tff(c_14479, 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))). % 36.25/23.70 tff(c_11537, 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))). % 36.25/23.70 tff(c_14146, 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))). % 36.25/23.70 tff(c_14309, 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))). % 36.25/23.70 tff(c_14356, 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))). % 36.25/23.70 tff(c_17146, 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))). % 36.25/23.70 tff(c_18026, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, uri_owl_FunctionalProperty, uri_rdfs_Class), true, true, true), true)=true))). % 36.25/23.70 tff(c_14241, 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))). % 36.25/23.70 tff(c_18745, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, uri_owl_Class, uri_rdfs_Class), true, true, true), true)=true))). % 36.25/23.70 tff(c_13783, 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))). % 36.25/23.70 tff(c_13997, 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))). % 36.25/23.70 tff(c_15139, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, sK1_testcase_premise_fullish_023_Unique_List_Components_BNODE_o, uri_rdfs_Class), true, true, true), true)=true))). % 36.25/23.70 tff(c_13882, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, sK2_testcase_premise_fullish_023_Unique_List_Components_BNODE_l, uri_rdf_List), true, true, true), true)=true))). % 36.25/23.70 tff(c_13640, 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))). % 36.25/23.70 tff(c_9477, 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))). % 36.25/23.70 tff(c_13258, 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))). % 36.25/23.70 tff(c_4520, 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))). % 36.25/23.70 tff(c_68233, plain, (![X_1197, Y_1198]: (ifeq(iext(uri_rdf_value, X_1197, Y_1198), true, iext(uri_rdf_value, X_1197, Y_1198), true)=true))). % 36.25/23.70 tff(c_5266, 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))). % 36.25/23.70 tff(c_67946, plain, (![C_1194]: (ifeq(iext(uri_rdfs_subClassOf, C_1194, uri_rdfs_Literal), true, iext(uri_rdfs_subClassOf, C_1194, uri_rdfs_Resource), true)=true))). % 36.25/23.70 tff(c_67919, plain, (![X_1190, Y_1191]: (ifeq(iext(uri_rdfs_isDefinedBy, X_1190, Y_1191), true, iext(uri_rdfs_isDefinedBy, X_1190, Y_1191), true)=true))). % 36.25/23.70 tff(c_67773, plain, (![X_1185, Y_1186]: (ifeq(iext(uri_rdf__1, X_1185, Y_1186), true, iext(uri_rdfs_member, X_1185, Y_1186), true)=true))). % 36.25/23.70 tff(c_8295, 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))). % 36.25/23.70 tff(c_67714, plain, (![X_1181, Y_1182]: (ifeq(iext(uri_rdf_first, X_1181, Y_1182), true, iext(uri_rdf_first, X_1181, Y_1182), true)=true))). % 36.25/23.70 tff(c_13031, 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))). % 36.25/23.70 tff(c_5575, 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))). % 36.25/23.70 tff(c_67200, plain, (![C_1176]: (ifeq(iext(uri_rdfs_subClassOf, C_1176, uri_rdf_Bag), true, iext(uri_rdfs_subClassOf, C_1176, uri_rdfs_Resource), true)=true))). % 36.25/23.70 tff(c_10498, 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))). % 36.25/23.70 tff(c_6653, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subPropertyOf), true, ifeq(iext(P_47, uri_owl_oneOf, uri_owl_oneOf), true, true, true), true)=true))). % 36.25/23.70 tff(c_67054, plain, (![X_1171, Y_1172]: (ifeq(iext(uri_rdf__1, X_1171, Y_1172), true, iext(uri_rdf__1, X_1171, Y_1172), true)=true))). % 36.25/23.70 tff(c_8110, 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))). % 36.25/23.70 tff(c_13326, 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))). % 36.25/23.70 tff(c_4322, 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))). % 36.25/23.70 tff(c_8798, 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))). % 36.25/23.70 tff(c_7941, 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))). % 36.25/23.70 tff(c_65891, plain, (![X_1161, Y_1162]: (ifeq(iext(uri_rdfs_subPropertyOf, X_1161, Y_1162), true, iext(uri_rdfs_subPropertyOf, X_1161, Y_1162), true)=true))). % 36.25/23.70 tff(c_65848, plain, (![X_1157, Y_1158]: (ifeq(iext(uri_rdf_rest, X_1157, Y_1158), true, iext(uri_rdf_rest, X_1157, Y_1158), true)=true))). % 36.25/23.70 tff(c_4910, 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))). % 36.25/23.70 tff(c_4568, 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))). % 36.25/23.70 tff(c_64652, plain, (![X_1149, Y_1150]: (ifeq(iext(uri_rdf_type, X_1149, Y_1150), true, iext(uri_rdf_type, X_1149, Y_1150), true)=true))). % 36.25/23.70 tff(c_64364, plain, (![C_1146]: (ifeq(iext(uri_rdfs_subClassOf, C_1146, uri_rdfs_Container), true, iext(uri_rdfs_subClassOf, C_1146, uri_rdfs_Resource), true)=true))). % 36.25/23.70 tff(c_64033, plain, (![X_1142, Y_1143]: (ifeq(iext(uri_rdfs_domain, X_1142, Y_1143), true, iext(uri_rdfs_domain, X_1142, Y_1143), true)=true))). % 36.25/23.70 tff(c_4468, 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))). % 36.25/23.70 tff(c_63871, plain, (![X_1136, Y_1137]: (ifeq(iext(uri_rdf__2, X_1136, Y_1137), true, iext(uri_rdfs_member, X_1136, Y_1137), true)=true))). % 36.25/23.70 tff(c_4517, 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))). % 36.25/23.70 tff(c_10726, 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))). % 36.25/23.70 tff(c_63581, plain, (![X_1129, Y_1130]: (ifeq(iext(uri_owl_oneOf, X_1129, Y_1130), true, iext(uri_owl_oneOf, X_1129, Y_1130), true)=true))). % 36.25/23.70 tff(c_8695, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, uri_owl_oneOf, uri_rdf_Property), true, true, true), true)=true))). % 36.25/23.70 tff(c_4465, 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))). % 36.25/23.70 tff(c_62983, plain, (![P_1122]: (ifeq(iext(uri_rdfs_subPropertyOf, P_1122, uri_rdf__2), true, iext(uri_rdfs_subPropertyOf, P_1122, uri_rdfs_member), true)=true))). % 36.25/23.71 tff(c_9601, 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))). % 36.25/23.71 tff(c_4420, 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))). % 36.25/23.71 tff(c_4365, 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))). % 36.25/23.71 tff(c_6348, 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))). % 36.25/23.71 tff(c_9043, 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))). % 36.25/23.71 tff(c_7619, 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))). % 36.25/23.71 tff(c_61931, plain, (![X_1108, Y_1109]: (ifeq(iext(uri_rdf__2, X_1108, Y_1109), true, iext(uri_rdf__2, X_1108, Y_1109), true)=true))). % 36.25/23.71 tff(c_4181, 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))). % 36.25/23.71 tff(c_4970, 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))). % 36.25/23.71 tff(c_6570, 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))). % 36.25/23.71 tff(c_12769, 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))). % 36.25/23.71 tff(c_60992, plain, (![C_1099]: (ifeq(iext(uri_rdfs_subClassOf, C_1099, uri_rdf_Alt), true, iext(uri_rdfs_subClassOf, C_1099, uri_rdfs_Resource), true)=true))). % 36.25/23.71 tff(c_60965, plain, (![X_1095, Y_1096]: (ifeq(iext(uri_rdf__3, X_1095, Y_1096), true, iext(uri_rdf__3, X_1095, Y_1096), true)=true))). % 36.25/23.71 tff(c_4224, 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))). % 36.25/23.71 tff(c_4423, 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))). % 36.25/23.71 tff(c_9173, 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))). % 36.25/23.71 tff(c_11483, 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))). % 36.25/23.71 tff(c_11910, 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))). % 36.25/23.71 tff(c_59611, plain, (![C_1082]: (ifeq(iext(uri_rdfs_subClassOf, C_1082, uri_rdfs_Datatype), true, iext(uri_rdfs_subClassOf, C_1082, uri_rdfs_Resource), true)=true))). % 36.25/23.71 tff(c_12498, 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))). % 36.25/23.71 tff(c_59395, plain, (![P_1078]: (ifeq(iext(uri_rdfs_subPropertyOf, P_1078, uri_rdf__1), true, iext(uri_rdfs_subPropertyOf, P_1078, uri_rdfs_member), true)=true))). % 36.25/23.71 tff(c_59362, plain, (![P_1077]: (ifeq(iext(uri_rdfs_subPropertyOf, P_1077, uri_rdf__3), true, iext(uri_rdfs_subPropertyOf, P_1077, uri_rdfs_member), true)=true))). % 36.25/23.71 tff(c_5944, 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))). % 36.25/23.71 tff(c_7238, 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))). % 36.25/23.71 tff(c_6924, 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))). % 36.25/23.71 tff(c_12214, 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))). % 36.25/23.71 tff(c_58006, plain, (![X_1065, Y_1066]: (ifeq(iext(uri_rdfs_range, X_1065, Y_1066), true, iext(uri_rdfs_range, X_1065, Y_1066), true)=true))). % 36.25/23.71 tff(c_6983, 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))). % 36.25/23.71 tff(c_57720, plain, (![C_1062]: (ifeq(iext(uri_rdfs_subClassOf, C_1062, uri_rdfs_Class), true, iext(uri_rdfs_subClassOf, C_1062, uri_rdfs_Resource), true)=true))). % 36.25/23.71 tff(c_57024, plain, (![X_1058, Y_1059]: (ifeq(iext(uri_rdfs_subClassOf, X_1058, Y_1059), true, iext(uri_rdfs_subClassOf, X_1058, Y_1059), true)=true))). % 36.25/23.71 tff(c_5866, 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))). % 36.25/23.71 tff(c_56746, plain, (![C_1055]: (ifeq(iext(uri_rdfs_subClassOf, C_1055, uri_rdfs_Seq), true, iext(uri_rdfs_subClassOf, C_1055, uri_rdfs_Resource), true)=true))). % 36.25/23.71 tff(c_11758, 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))). % 36.25/23.71 tff(c_4842, 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))). % 36.25/23.71 tff(c_56489, plain, (![X_1049, Y_1050]: (ifeq(iext(uri_rdf_subject, X_1049, Y_1050), true, iext(uri_rdf_subject, X_1049, Y_1050), true)=true))). % 36.25/23.71 tff(c_4565, 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))). % 36.25/23.71 tff(c_10092, 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))). % 36.25/23.71 tff(c_55491, plain, (![C_1040]: (ifeq(iext(uri_rdfs_subClassOf, C_1040, uri_rdfs_ContainerMembershipProperty), true, iext(uri_rdfs_subClassOf, C_1040, uri_rdfs_Resource), true)=true))). % 36.25/23.71 tff(c_55464, plain, (![X_1036, Y_1037]: (ifeq(iext(uri_rdf__3, X_1036, Y_1037), true, iext(uri_rdfs_member, X_1036, Y_1037), true)=true))). % 36.25/23.71 tff(c_4279, 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))). % 36.25/23.71 tff(c_5695, 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))). % 36.25/23.71 tff(c_8556, 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))). % 36.25/23.71 tff(c_7691, 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))). % 36.25/23.71 tff(c_4319, 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))). % 36.25/23.71 tff(c_4184, 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))). % 36.25/23.71 tff(c_6283, 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))). % 36.25/23.71 tff(c_54153, plain, (![C_1022]: (ifeq(iext(uri_rdfs_subClassOf, C_1022, uri_rdf_Property), true, iext(uri_rdfs_subClassOf, C_1022, uri_rdfs_Resource), true)=true))). % 36.25/23.71 tff(c_4362, 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))). % 36.25/23.71 tff(c_11665, 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))). % 36.25/23.71 tff(c_12962, 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))). % 36.25/23.71 tff(c_4276, 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))). % 36.25/23.71 tff(c_4227, 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))). % 36.25/23.71 tff(c_52290, plain, (![X_1002, Y_1003]: (ifeq(iext(uri_rdfs_seeAlso, X_1002, Y_1003), true, iext(uri_rdfs_seeAlso, X_1002, Y_1003), true)=true))). % 36.25/23.71 tff(c_11187, 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))). % 36.25/23.71 tff(c_52012, plain, (![C_999]: (ifeq(iext(uri_rdfs_subClassOf, C_999, uri_rdf_XMLLiteral), true, iext(uri_rdfs_subClassOf, C_999, uri_rdfs_Resource), true)=true))). % 36.25/23.71 tff(c_11118, 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))). % 36.25/23.71 tff(c_7468, 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))). % 36.25/23.71 tff(c_51755, plain, (![X_993, Y_994]: (ifeq(iext(uri_rdf_object, X_993, Y_994), true, iext(uri_rdf_object, X_993, Y_994), true)=true))). % 36.25/23.71 tff(c_5335, 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))). % 36.25/23.71 tff(c_11996, 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))). % 36.25/23.71 tff(c_17911, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdfs_Class), true, ifeq(iext(P_18, uri_owl_FunctionalProperty, Y_21), true, true, true), true)=true))). % 36.25/23.71 tff(c_6110, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdf_List), true, ifeq(iext(P_28, X_30, sK2_testcase_premise_fullish_023_Unique_List_Components_BNODE_l), true, true, true), true)=true))). % 36.25/23.71 tff(c_9232, 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))). % 36.25/23.71 tff(c_14929, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdfs_Class), true, ifeq(iext(P_18, sK1_testcase_premise_fullish_023_Unique_List_Components_BNODE_o, Y_21), true, true, true), true)=true))). % 36.25/23.71 tff(c_17102, 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))). % 36.25/23.71 tff(c_18504, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdfs_Class), true, ifeq(iext(P_18, uri_owl_Class, Y_21), true, true, true), true)=true))). % 36.25/23.71 tff(c_8368, 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))). % 36.25/23.71 tff(c_18501, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdfs_Class), true, ifeq(iext(P_28, X_30, uri_owl_Class), true, true, true), true)=true))). % 36.25/23.71 tff(c_8371, 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))). % 36.25/23.72 tff(c_6718, 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))). % 36.25/23.72 tff(c_6715, 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))). % 36.25/23.72 tff(c_6820, 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))). % 36.25/23.72 tff(c_17099, 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))). % 36.25/23.72 tff(c_6008, 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))). % 36.25/23.72 tff(c_9229, 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))). % 36.25/23.72 tff(c_6011, 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))). % 36.25/23.72 tff(c_6113, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdf_List), true, ifeq(iext(P_18, sK2_testcase_premise_fullish_023_Unique_List_Components_BNODE_l, Y_21), true, true, true), true)=true))). % 36.25/23.72 tff(c_13952, 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))). % 36.25/23.72 tff(c_17908, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdfs_Class), true, ifeq(iext(P_28, X_30, uri_owl_FunctionalProperty), true, true, true), true)=true))). % 36.25/23.72 tff(c_11999, 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))). % 36.25/23.72 tff(c_6823, 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))). % 36.25/23.72 tff(c_4691, plain, (![P_47, X_133]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, X_133, uri_rdfs_Resource), true, true, true), true)=true))). % 36.25/23.72 tff(c_14926, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdfs_Class), true, ifeq(iext(P_28, X_30, sK1_testcase_premise_fullish_023_Unique_List_Components_BNODE_o), true, true, true), true)=true))). % 36.25/23.72 tff(c_13955, 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))). % 36.25/23.72 tff(c_3417, 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))). % 36.25/23.72 tff(c_3719, 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))). % 36.25/23.72 tff(c_3506, 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))). % 36.25/23.72 tff(c_4057, 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))). % 36.25/23.72 tff(c_3465, 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))). % 36.25/23.72 tff(c_3462, 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))). % 36.25/23.72 tff(c_3561, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_owl_Class), true, ifeq(iext(P_28, X_30, sK1_testcase_premise_fullish_023_Unique_List_Components_BNODE_o), true, true, true), true)=true))). % 36.25/23.72 tff(c_3924, 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))). % 36.25/23.72 tff(c_3645, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_owl_FunctionalProperty), true, ifeq(iext(P_18, uri_rdf_first, Y_21), true, true, true), true)=true))). % 36.25/23.72 tff(c_3764, 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))). % 36.25/23.72 tff(c_3888, 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))). % 36.25/23.72 tff(c_3642, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_owl_FunctionalProperty), true, ifeq(iext(P_28, X_30, uri_rdf_first), true, true, true), true)=true))). % 36.25/23.72 tff(c_4060, 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))). % 36.25/23.72 tff(c_3607, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, sK1_testcase_premise_fullish_023_Unique_List_Components_BNODE_o), true, ifeq(iext(P_18, uri_ex_w, Y_21), true, true, true), true)=true))). % 36.25/23.72 tff(c_3966, 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))). % 36.25/23.72 tff(c_4132, 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))). % 36.25/23.72 tff(c_3685, 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))). % 36.25/23.72 tff(c_3850, 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))). % 36.25/23.72 tff(c_3927, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdf_Property), true, ifeq(iext(P_18, uri_rdf_subject, Y_21), true, true, true), true)=true))). % 36.25/23.72 tff(c_4092, 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))). % 36.25/23.72 tff(c_4135, 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))). % 36.25/23.72 tff(c_4007, 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))). % 36.25/23.72 tff(c_3682, 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))). % 36.25/23.72 tff(c_4089, 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))). % 36.25/23.72 tff(c_3806, 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))). % 36.25/23.72 tff(c_3564, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_owl_Class), true, ifeq(iext(P_18, sK1_testcase_premise_fullish_023_Unique_List_Components_BNODE_o, Y_21), true, true, true), true)=true))). % 36.25/23.72 tff(c_3503, 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))). % 36.25/23.72 tff(c_3885, 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))). % 36.25/23.72 tff(c_3761, 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))). % 36.25/23.72 tff(c_3604, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, sK1_testcase_premise_fullish_023_Unique_List_Components_BNODE_o), true, ifeq(iext(P_28, X_30, uri_ex_w), true, true, true), true)=true))). % 36.25/23.72 tff(c_3803, 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))). % 36.25/23.72 tff(c_3420, 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))). % 36.25/23.72 tff(c_3722, 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))). % 36.25/23.72 tff(c_3963, 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))). % 36.25/23.72 tff(c_3847, 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))). % 36.25/23.72 tff(c_4010, 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))). % 36.25/23.72 tff(c_2069, plain, (![P_96, X_98, X_62]: (ifeq(iext(uri_rdfs_range, P_96, uri_rdfs_Resource), true, ifeq(iext(P_96, X_98, X_62), true, true, true), true)=true))). % 36.25/23.72 tff(c_1694, plain, (![P_92, X_62, Y_95]: (ifeq(iext(uri_rdfs_domain, P_92, uri_rdfs_Resource), true, ifeq(iext(P_92, X_62, Y_95), true, true, true), true)=true))). % 36.25/23.72 tff(c_42022, plain, (![C_862]: (ifeq(iext(uri_rdfs_subClassOf, C_862, uri_rdfs_ContainerMembershipProperty), true, iext(uri_rdfs_subClassOf, C_862, uri_rdf_Property), true)=true))). % 36.25/23.72 tff(c_41955, plain, (![C_860]: (ifeq(iext(uri_rdfs_subClassOf, C_860, uri_rdf_Alt), true, iext(uri_rdfs_subClassOf, C_860, uri_rdfs_Container), true)=true))). % 36.25/23.72 tff(c_41888, plain, (![C_858]: (ifeq(iext(uri_rdfs_subClassOf, C_858, uri_rdfs_Seq), true, iext(uri_rdfs_subClassOf, C_858, uri_rdfs_Container), true)=true))). % 36.25/23.72 tff(c_2697, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdfs_domain), true, ifeq(iext(P_103, uri_rdfs_subClassOf, uri_rdfs_Class), true, true, true), true)=true))). % 36.25/23.72 tff(c_2709, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdfs_range), true, ifeq(iext(P_103, uri_rdf__2, uri_rdfs_Resource), true, true, true), true)=true))). % 36.25/23.72 tff(c_2565, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdfs_domain), true, ifeq(iext(P_103, uri_rdfs_domain, uri_rdf_Property), true, true, true), true)=true))). % 36.25/23.72 tff(c_2613, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdfs_range), true, ifeq(iext(P_103, uri_rdfs_seeAlso, uri_rdfs_Resource), true, true, true), true)=true))). % 36.25/23.72 tff(c_41374, plain, (![X_850, Y_851]: (ifeq(iext(uri_rdfs_isDefinedBy, X_850, Y_851), true, iext(uri_rdfs_seeAlso, X_850, Y_851), true)=true))). % 36.25/23.72 tff(c_2751, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdfs_range), true, ifeq(iext(P_103, uri_rdfs_comment, uri_rdfs_Literal), true, true, true), true)=true))). % 36.25/23.72 tff(c_2667, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdfs_domain), true, ifeq(iext(P_103, uri_rdf__2, uri_rdfs_Resource), true, true, true), true)=true))). % 36.25/23.72 tff(c_2862, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdfs_subClassOf), true, ifeq(iext(P_103, uri_rdfs_Datatype, uri_rdfs_Class), true, true, true), true)=true))). % 36.25/23.72 tff(c_2733, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdfs_domain), true, ifeq(iext(P_103, uri_rdf__1, uri_rdfs_Resource), true, true, true), true)=true))). % 36.25/23.72 tff(c_2826, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdfs_range), true, ifeq(iext(P_103, uri_rdf_subject, uri_rdfs_Resource), true, true, true), true)=true))). % 36.25/23.72 tff(c_2850, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdf_type), true, ifeq(iext(P_103, uri_rdf_value, uri_rdf_Property), true, true, true), true)=true))). % 36.25/23.72 tff(c_2808, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdfs_domain), true, ifeq(iext(P_103, uri_rdf_predicate, uri_rdfs_Statement), true, true, true), true)=true))). % 36.25/23.72 tff(c_2715, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdfs_range), true, ifeq(iext(P_103, uri_rdf__3, uri_rdfs_Resource), true, true, true), true)=true))). % 36.25/23.72 tff(c_2559, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdf_type), true, ifeq(iext(P_103, uri_rdf__3, uri_rdf_Property), true, true, true), true)=true))). % 36.25/23.72 tff(c_2886, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdfs_range), true, ifeq(iext(P_103, uri_rdfs_range, uri_rdfs_Class), true, true, true), true)=true))). % 36.25/23.72 tff(c_2619, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdfs_subClassOf), true, ifeq(iext(P_103, uri_rdf_XMLLiteral, uri_rdfs_Literal), true, true, true), true)=true))). % 36.25/23.72 tff(c_2814, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdfs_range), true, ifeq(iext(P_103, uri_rdf_first, uri_rdfs_Resource), true, true, true), true)=true))). % 36.25/23.72 tff(c_2892, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_owl_oneOf), true, ifeq(iext(P_103, sK1_testcase_premise_fullish_023_Unique_List_Components_BNODE_o, sK2_testcase_premise_fullish_023_Unique_List_Components_BNODE_l), true, true, true), true)=true))). % 36.25/23.72 tff(c_2655, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdfs_range), true, ifeq(iext(P_103, uri_rdfs_label, uri_rdfs_Literal), true, true, true), true)=true))). % 36.25/23.72 tff(c_2505, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdf_first), true, ifeq(iext(P_103, sK2_testcase_premise_fullish_023_Unique_List_Components_BNODE_l, uri_ex_v), true, true, true), true)=true))). % 36.25/23.72 tff(c_2601, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdf_type), true, ifeq(iext(P_103, uri_rdf_type, uri_rdf_Property), true, true, true), true)=true))). % 36.25/23.72 tff(c_2703, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdf_rest), true, ifeq(iext(P_103, sK2_testcase_premise_fullish_023_Unique_List_Components_BNODE_l, uri_rdf_nil), true, true, true), true)=true))). % 36.25/23.72 tff(c_2637, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdfs_domain), true, ifeq(iext(P_103, uri_rdf__3, uri_rdfs_Resource), true, true, true), true)=true))). % 36.25/23.72 tff(c_2547, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdfs_domain), true, ifeq(iext(P_103, uri_rdfs_subPropertyOf, uri_rdf_Property), true, true, true), true)=true))). % 36.25/23.72 tff(c_2577, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdf_first), true, ifeq(iext(P_103, sK2_testcase_premise_fullish_023_Unique_List_Components_BNODE_l, uri_ex_u), true, true, true), true)=true))). % 36.25/23.72 tff(c_2571, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdfs_subClassOf), true, ifeq(iext(P_103, uri_rdfs_Seq, uri_rdfs_Container), true, true, true), true)=true))). % 36.25/23.72 tff(c_2583, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdf_type), true, ifeq(iext(P_103, uri_rdf_nil, uri_rdf_List), true, true, true), true)=true))). % 36.25/23.72 tff(c_2745, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdf_type), true, ifeq(iext(P_103, uri_rdf_object, uri_rdf_Property), true, true, true), true)=true))). % 36.25/23.72 tff(c_2856, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdfs_range), true, ifeq(iext(P_103, uri_rdfs_domain, uri_rdfs_Class), true, true, true), true)=true))). % 36.25/23.72 tff(c_2535, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdf_type), true, ifeq(iext(P_103, uri_rdf_first, uri_rdf_Property), true, true, true), true)=true))). % 36.25/23.72 tff(c_2661, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdf_type), true, ifeq(iext(P_103, uri_rdf__1, uri_rdfs_ContainerMembershipProperty), true, true, true), true)=true))). % 36.25/23.73 tff(c_2784, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdfs_subClassOf), true, ifeq(iext(P_103, uri_rdfs_ContainerMembershipProperty, uri_rdf_Property), true, true, true), true)=true))). % 36.25/23.73 tff(c_2631, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdfs_range), true, ifeq(iext(P_103, uri_rdf_type, uri_rdfs_Class), true, true, true), true)=true))). % 36.25/23.73 tff(c_2796, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdfs_range), true, ifeq(iext(P_103, uri_rdfs_member, uri_rdfs_Resource), true, true, true), true)=true))). % 36.25/23.73 tff(c_37919, plain, (![C_819]: (ifeq(iext(uri_rdfs_subClassOf, C_819, uri_rdf_XMLLiteral), true, iext(uri_rdfs_subClassOf, C_819, uri_rdfs_Literal), true)=true))). % 36.25/23.73 tff(c_2685, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdf_type), true, ifeq(iext(P_103, uri_rdf_subject, uri_rdf_Property), true, true, true), true)=true))). % 36.25/23.73 tff(c_2643, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdfs_domain), true, ifeq(iext(P_103, uri_rdfs_member, uri_rdfs_Resource), true, true, true), true)=true))). % 36.25/23.73 tff(c_2625, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdfs_domain), true, ifeq(iext(P_103, uri_rdf_first, uri_rdf_List), true, true, true), true)=true))). % 36.25/23.73 tff(c_2778, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdf_type), true, ifeq(iext(P_103, uri_rdf__3, uri_rdfs_ContainerMembershipProperty), true, true, true), true)=true))). % 36.25/23.73 tff(c_2772, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdfs_range), true, ifeq(iext(P_103, uri_rdf__1, uri_rdfs_Resource), true, true, true), true)=true))). % 36.25/23.73 tff(c_2673, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdfs_domain), true, ifeq(iext(P_103, uri_rdf_subject, uri_rdfs_Statement), true, true, true), true)=true))). % 36.25/23.73 tff(c_37141, plain, (![D_811]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_811), true, icext(D_811, uri_rdfs_seeAlso), true)=true))). % 36.25/23.73 tff(c_37075, plain, (![D_809]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_809), true, icext(D_809, uri_rdfs_subClassOf), true)=true))). % 36.25/23.73 tff(c_37009, plain, (![D_807]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_807), true, icext(D_807, uri_rdfs_subPropertyOf), true)=true))). % 36.25/23.73 tff(c_36819, plain, (![D_804]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_804), true, icext(D_804, uri_rdfs_domain), true)=true))). % 36.25/23.73 tff(c_2691, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdfs_domain), true, ifeq(iext(P_103, uri_rdfs_seeAlso, uri_rdfs_Resource), true, true, true), true)=true))). % 36.25/23.73 tff(c_36753, plain, (![D_802]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_802), true, icext(D_802, uri_rdfs_isDefinedBy), true)=true))). % 36.25/23.73 tff(c_36687, plain, (![D_800]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_800), true, icext(D_800, uri_owl_oneOf), true)=true))). % 36.25/23.73 tff(c_36497, plain, (![D_797]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_797), true, icext(D_797, uri_rdfs_Datatype), true)=true))). % 36.25/23.73 tff(c_2595, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdfs_range), true, ifeq(iext(P_103, uri_rdf_value, uri_rdfs_Resource), true, true, true), true)=true))). % 36.25/23.73 tff(c_36430, plain, (![D_795]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_795), true, icext(D_795, uri_rdf_Alt), true)=true))). % 36.25/23.73 tff(c_36242, plain, (![D_792]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_792), true, icext(D_792, uri_rdf_Bag), true)=true))). % 36.25/23.73 tff(c_2820, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdfs_range), true, ifeq(iext(P_103, uri_rdf_predicate, uri_rdfs_Resource), true, true, true), true)=true))). % 36.25/23.73 tff(c_36173, plain, (![D_790]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_790), true, icext(D_790, uri_rdfs_ContainerMembershipProperty), true)=true))). % 36.25/23.73 tff(c_35987, plain, (![D_787]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_787), true, icext(D_787, uri_rdfs_Container), true)=true))). % 36.25/23.73 tff(c_2511, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdfs_domain), true, ifeq(iext(P_103, uri_rdfs_label, uri_rdfs_Resource), true, true, true), true)=true))). % 36.25/23.73 tff(c_35921, plain, (![D_785]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_785), true, icext(D_785, uri_rdfs_Literal), true)=true))). % 36.25/23.73 tff(c_35847, plain, (![D_783]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_783), true, icext(D_783, uri_rdf_XMLLiteral), true)=true))). % 36.25/23.73 tff(c_35661, plain, (![D_780]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_780), true, icext(D_780, uri_rdfs_Seq), true)=true))). % 36.25/23.73 tff(c_2790, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdfs_domain), true, ifeq(iext(P_103, uri_rdfs_comment, uri_rdfs_Resource), true, true, true), true)=true))). % 36.25/23.73 tff(c_35564, plain, (![D_778]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_778), true, icext(D_778, uri_rdfs_Class), true)=true))). % 36.25/23.73 tff(c_35379, plain, (![D_775]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_775), true, icext(D_775, uri_owl_Class), true)=true))). % 36.25/23.73 tff(c_2529, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdfs_domain), true, ifeq(iext(P_103, uri_rdf_rest, uri_rdf_List), true, true, true), true)=true))). % 36.25/23.73 tff(c_35313, plain, (![D_773]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_773), true, icext(D_773, uri_rdfs_Statement), true)=true))). % 36.25/23.73 tff(c_35247, plain, (![D_771]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_771), true, icext(D_771, uri_rdf_predicate), true)=true))). % 36.25/23.73 tff(c_35066, plain, (![D_768]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_768), true, icext(D_768, uri_owl_FunctionalProperty), true)=true))). % 36.25/23.73 tff(c_2679, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdf_type), true, ifeq(iext(P_103, uri_rdf_Property, uri_rdfs_Class), true, true, true), true)=true))). % 36.25/23.73 tff(c_35000, plain, (![D_766]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_766), true, icext(D_766, uri_rdfs_label), true)=true))). % 36.25/23.73 tff(c_34934, plain, (![D_764]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_764), true, icext(D_764, uri_rdfs_Resource), true)=true))). % 36.25/23.73 tff(c_34883, plain, (![C_762]: (ifeq(iext(uri_rdfs_subClassOf, C_762, uri_rdfs_Datatype), true, iext(uri_rdfs_subClassOf, C_762, uri_rdfs_Class), true)=true))). % 36.25/23.73 tff(c_34816, plain, (![D_760]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_760), true, icext(D_760, uri_rdfs_member), true)=true))). % 36.25/23.73 tff(c_34740, plain, (![D_758]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_758), true, icext(D_758, sK1_testcase_premise_fullish_023_Unique_List_Components_BNODE_o), true)=true))). % 36.25/23.73 tff(c_2739, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdf_type), true, ifeq(iext(P_103, sK1_testcase_premise_fullish_023_Unique_List_Components_BNODE_o, uri_owl_Class), true, true, true), true)=true))). % 36.25/23.73 tff(c_34559, plain, (![D_755]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_755), true, icext(D_755, uri_rdf_List), true)=true))). % 36.25/23.73 tff(c_34492, plain, (![D_753]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_753), true, icext(D_753, uri_rdfs_comment), true)=true))). % 36.25/23.73 tff(c_34311, plain, (![D_750]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_List, D_750), true, icext(D_750, sK2_testcase_premise_fullish_023_Unique_List_Components_BNODE_l), true)=true))). % 36.25/23.73 tff(c_2880, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdfs_subClassOf), true, ifeq(iext(P_103, uri_rdf_Alt, uri_rdfs_Container), true, true, true), true)=true))). % 36.25/23.73 tff(c_34245, plain, (![D_748]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_748), true, icext(D_748, uri_rdfs_range), true)=true))). % 36.25/23.73 tff(c_34179, plain, (![D_746]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_List, D_746), true, icext(D_746, uri_rdf_nil), true)=true))). % 36.25/23.73 tff(c_2868, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdfs_range), true, ifeq(iext(P_103, uri_rdfs_subPropertyOf, uri_rdf_Property), true, true, true), true)=true))). % 36.25/23.73 tff(c_17398, 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))). % 36.25/23.73 tff(c_16187, 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))). % 36.25/23.73 tff(c_33891, plain, (![D_738]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_738), true, icext(D_738, uri_rdf_type), true)=true))). % 36.25/23.73 tff(c_16252, 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))). % 36.25/23.73 tff(c_16092, 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))). % 36.25/23.73 tff(c_2589, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdfs_domain), true, ifeq(iext(P_103, uri_rdfs_range, uri_rdf_Property), true, true, true), true)=true))). % 36.25/23.73 tff(c_18227, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_48), true, iext(Q_48, uri_owl_FunctionalProperty, uri_rdfs_Resource), true)=true))). % 36.25/23.73 tff(c_15607, 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))). % 36.25/23.73 tff(c_15541, 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))). % 36.25/23.73 tff(c_15365, 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))). % 36.25/23.73 tff(c_15363, 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))). % 36.25/23.73 tff(c_15299, 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))). % 36.25/23.73 tff(c_15929, plain, (![E_41]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Resource, E_41), true, iext(uri_rdfs_subClassOf, sK1_testcase_premise_fullish_023_Unique_List_Components_BNODE_o, E_41), true)=true))). % 36.25/23.73 tff(c_2721, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdfs_subClassOf), true, ifeq(iext(P_103, uri_rdf_Bag, uri_rdfs_Container), true, true, true), true)=true))). % 36.25/23.73 tff(c_15839, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_48), true, iext(Q_48, sK1_testcase_premise_fullish_023_Unique_List_Components_BNODE_o, sK1_testcase_premise_fullish_023_Unique_List_Components_BNODE_o), true)=true))). % 36.25/23.73 tff(c_33301, plain, (![D_720]: (ifeq(iext(uri_rdfs_subClassOf, sK1_testcase_premise_fullish_023_Unique_List_Components_BNODE_o, D_720), true, icext(D_720, uri_ex_w), true)=true))). % 36.25/23.73 tff(c_18400, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_48), true, iext(Q_48, uri_owl_FunctionalProperty, uri_owl_FunctionalProperty), true)=true))). % 36.25/23.73 tff(c_15605, 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))). % 36.25/23.73 tff(c_2757, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdfs_domain), true, ifeq(iext(P_103, uri_rdfs_isDefinedBy, uri_rdfs_Resource), true, true, true), true)=true))). % 36.25/23.73 tff(c_18225, plain, (![E_41]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Resource, E_41), true, iext(uri_rdfs_subClassOf, uri_owl_FunctionalProperty, E_41), true)=true))). % 36.25/23.73 tff(c_19008, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_48), true, iext(Q_48, uri_owl_Class, uri_owl_Class), true)=true))). % 36.25/23.73 tff(c_18828, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_48), true, iext(Q_48, uri_owl_Class, uri_rdfs_Resource), true)=true))). % 36.25/23.73 tff(c_15770, 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))). % 36.25/23.73 tff(c_18826, plain, (![E_41]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Resource, E_41), true, iext(uri_rdfs_subClassOf, uri_owl_Class, E_41), true)=true))). % 36.25/23.73 tff(c_15931, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_48), true, iext(Q_48, sK1_testcase_premise_fullish_023_Unique_List_Components_BNODE_o, uri_rdfs_Resource), true)=true))). % 36.25/23.73 tff(c_2844, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdfs_domain), true, ifeq(iext(P_103, uri_rdf_object, uri_rdfs_Statement), true, true, true), true)=true))). % 36.25/23.73 tff(c_14868, 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))). % 36.25/23.73 tff(c_14666, 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))). % 36.25/23.73 tff(c_14788, 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))). % 36.25/23.73 tff(c_32698, plain, (![D_702]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, D_702), true, icext(D_702, uri_rdf__2), true)=true))). % 36.25/23.73 tff(c_14740, 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))). % 36.25/23.73 tff(c_14617, 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))). % 36.25/23.73 tff(c_15206, 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))). % 36.25/23.73 tff(c_2523, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdf_type), true, ifeq(iext(P_103, uri_rdf_first, uri_owl_FunctionalProperty), true, true, true), true)=true))). % 36.25/23.73 tff(c_14498, 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))). % 36.25/23.73 tff(c_14545, 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))). % 36.25/23.73 tff(c_14450, 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))). % 36.25/23.73 tff(c_32423, plain, (![D_693]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_693), true, icext(D_693, uri_rdf_Property), true)=true))). % 36.25/23.73 tff(c_17171, 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))). % 36.25/23.73 tff(c_18045, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, uri_owl_FunctionalProperty, uri_rdfs_Class), true)=true))). % 36.25/23.73 tff(c_15158, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, sK1_testcase_premise_fullish_023_Unique_List_Components_BNODE_o, uri_rdfs_Class), true)=true))). % 36.25/23.73 tff(c_2607, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdfs_domain), true, ifeq(iext(P_103, uri_rdf_type, uri_rdfs_Resource), true, true, true), true)=true))). % 36.25/23.73 tff(c_13901, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, sK2_testcase_premise_fullish_023_Unique_List_Components_BNODE_l, uri_rdf_List), true)=true))). % 36.25/23.73 tff(c_13808, 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))). % 36.25/23.73 tff(c_14171, 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))). % 36.25/23.73 tff(c_32131, plain, (![D_684]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, D_684), true, icext(D_684, uri_rdf_XMLLiteral), true)=true))). % 36.25/23.73 tff(c_14375, 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))). % 36.25/23.73 tff(c_14328, 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))). % 36.25/23.73 tff(c_14260, 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))). % 36.25/23.73 tff(c_2838, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdf_type), true, ifeq(iext(P_103, uri_rdf_rest, uri_rdf_Property), true, true, true), true)=true))). % 36.25/23.73 tff(c_14022, 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))). % 36.25/23.73 tff(c_18764, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, uri_owl_Class, uri_rdfs_Class), true)=true))). % 36.25/23.73 tff(c_31828, plain, (![D_675]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, D_675), true, icext(D_675, uri_rdf__3), true)=true))). % 36.25/23.73 tff(c_7644, 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))). % 36.25/23.73 tff(c_13290, 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))). % 36.25/23.73 tff(c_9197, 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))). % 36.25/23.73 tff(c_2541, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdf_type), true, ifeq(iext(P_103, uri_rdf__2, uri_rdf_Property), true, true, true), true)=true))). % 36.25/23.73 tff(c_8823, 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))). % 36.25/23.74 tff(c_11508, 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))). % 36.25/23.74 tff(c_31500, plain, (![D_666]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_666), true, icext(D_666, uri_rdf__1), true)=true))). % 36.25/23.74 tff(c_5296, 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))). % 36.25/23.74 tff(c_31416, plain, (![P_663]: (ifeq(iext(uri_rdfs_subPropertyOf, P_663, uri_rdfs_isDefinedBy), true, iext(uri_rdfs_subPropertyOf, P_663, uri_rdfs_seeAlso), true)=true))). % 36.25/23.74 tff(c_5361, 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))). % 36.25/23.74 tff(c_13665, 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))). % 36.25/23.74 tff(c_12801, 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))). % 36.25/23.74 tff(c_12239, 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))). % 36.25/23.74 tff(c_12241, 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))). % 36.25/23.74 tff(c_6375, 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))). % 36.25/23.74 tff(c_9198, 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))). % 36.25/23.74 tff(c_11149, 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))). % 36.25/23.74 tff(c_31101, plain, (![D_650]: (ifeq(iext(uri_rdfs_subClassOf, uri_owl_FunctionalProperty, D_650), true, icext(D_650, uri_rdf_first), true)=true))). % 36.25/23.74 tff(c_7268, 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))). % 36.25/23.74 tff(c_12525, 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))). % 36.25/23.74 tff(c_2517, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdfs_range), true, ifeq(iext(P_103, uri_rdfs_subClassOf, uri_rdfs_Class), true, true, true), true)=true))). % 36.25/23.74 tff(c_11218, 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))). % 36.25/23.74 tff(c_10523, 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))). % 36.25/23.74 tff(c_11697, 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))). % 36.25/23.74 tff(c_30794, plain, (![D_641]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, D_641), true, icext(D_641, uri_rdf__1), true)=true))). % 36.25/23.74 tff(c_6950, 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))). % 36.25/23.74 tff(c_2649, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdf_type), true, ifeq(iext(P_103, uri_rdf__2, uri_rdfs_ContainerMembershipProperty), true, true, true), true)=true))). % 36.25/23.74 tff(c_9632, 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))). % 36.25/23.74 tff(c_7646, 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))). % 36.25/23.74 tff(c_9504, 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))). % 36.25/23.74 tff(c_8320, 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))). % 36.25/23.74 tff(c_12994, 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))). % 36.25/23.74 tff(c_9068, 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))). % 36.25/23.74 tff(c_11942, 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))). % 36.25/23.74 tff(c_2766, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdfs_subPropertyOf), true, ifeq(iext(P_103, uri_rdfs_isDefinedBy, uri_rdfs_seeAlso), true, true, true), true)=true))). % 36.25/23.74 tff(c_5601, 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))). % 36.25/23.74 tff(c_4940, 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))). % 36.25/23.74 tff(c_10753, 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))). % 36.25/23.74 tff(c_6309, 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))). % 36.25/23.74 tff(c_30145, plain, (![C_620]: (ifeq(iext(uri_rdfs_subClassOf, C_620, uri_rdf_Bag), true, iext(uri_rdfs_subClassOf, C_620, uri_rdfs_Container), true)=true))). % 36.25/23.74 tff(c_10525, 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))). % 36.25/23.74 tff(c_11219, 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))). % 36.25/23.74 tff(c_13667, 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))). % 36.25/23.74 tff(c_10751, 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))). % 36.25/23.74 tff(c_4995, 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))). % 36.25/23.74 tff(c_2898, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdf_type), true, ifeq(iext(P_103, uri_ex_w, sK1_testcase_premise_fullish_023_Unique_List_Components_BNODE_o), true, true, true), true)=true))). % 36.25/23.74 tff(c_8822, 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))). % 36.25/23.74 tff(c_8138, 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))). % 36.25/23.74 tff(c_7716, 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))). % 36.25/23.74 tff(c_29724, plain, (![D_606]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_606), true, icext(D_606, uri_rdf_object), true)=true))). % 36.25/23.74 tff(c_5976, 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))). % 36.25/23.74 tff(c_4872, 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))). % 36.25/23.74 tff(c_2802, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdfs_domain), true, ifeq(iext(P_103, uri_rdf_value, uri_rdfs_Resource), true, true, true), true)=true))). % 36.25/23.74 tff(c_6601, 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))). % 36.25/23.74 tff(c_13358, 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))). % 36.25/23.74 tff(c_8586, 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))). % 36.25/23.74 tff(c_29436, plain, (![D_597]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_597), true, icext(D_597, uri_rdf_subject), true)=true))). % 36.25/23.74 tff(c_10116, 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))). % 36.25/23.74 tff(c_5891, 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))). % 36.25/23.74 tff(c_2874, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdfs_range), true, ifeq(iext(P_103, uri_rdf_rest, uri_rdf_List), true, true, true), true)=true))). % 36.25/23.74 tff(c_9502, 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))). % 36.25/23.74 tff(c_13063, 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))). % 36.25/23.74 tff(c_8720, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, uri_owl_oneOf, uri_rdf_Property), true)=true))). % 36.25/23.74 tff(c_7493, 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))). % 36.25/23.74 tff(c_5720, 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))). % 36.25/23.74 tff(c_2832, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdf_type), true, ifeq(iext(P_103, uri_rdf__1, uri_rdf_Property), true, true, true), true)=true))). % 36.25/23.74 tff(c_10117, 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))). % 36.25/23.74 tff(c_11788, 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))). % 36.25/23.74 tff(c_7269, 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))). % 36.25/23.74 tff(c_7014, 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))). % 36.25/23.74 tff(c_2553, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdf_type), true, ifeq(iext(P_103, uri_rdf_XMLLiteral, uri_rdfs_Datatype), true, true, true), true)=true))). % 36.25/23.74 tff(c_9070, 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))). % 36.25/23.74 tff(c_11150, 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))). % 36.25/23.74 tff(c_7966, 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))). % 36.25/23.74 tff(c_6684, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_48), true, iext(Q_48, uri_owl_oneOf, uri_owl_oneOf), true)=true))). % 36.25/23.74 tff(c_4710, plain, (![Q_48, X_133]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, X_133, uri_rdfs_Resource), true)=true))). % 36.25/23.74 tff(c_2727, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdfs_range), true, ifeq(iext(P_103, uri_rdfs_isDefinedBy, uri_rdfs_Resource), true, true, true), true)=true))). % 36.25/23.74 tff(c_2941, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_104), true, iext(Q_104, uri_rdf__1, uri_rdfs_Resource), true)=true))). % 36.25/23.74 tff(c_2952, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_104), true, iext(Q_104, uri_rdf_value, uri_rdfs_Resource), true)=true))). % 36.25/23.74 tff(c_2933, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_104), true, iext(Q_104, uri_rdf_subject, uri_rdf_Property), true)=true))). % 36.25/23.74 tff(c_28082, plain, (![D_560]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_560), true, icext(D_560, uri_rdf__2), true)=true))). % 36.25/23.74 tff(c_2906, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_104), true, iext(Q_104, uri_rdf_first, uri_owl_FunctionalProperty), true)=true))). % 36.25/23.74 tff(c_2958, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_104), true, iext(Q_104, uri_rdf_rest, uri_rdf_Property), true)=true))). % 36.25/23.74 tff(c_2928, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_104), true, iext(Q_104, uri_rdfs_label, uri_rdfs_Literal), true)=true))). % 36.25/23.74 tff(c_2950, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_104), true, iext(Q_104, uri_rdfs_comment, uri_rdfs_Resource), true)=true))). % 36.25/23.74 tff(c_2916, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_104), true, iext(Q_104, uri_rdf_nil, uri_rdf_List), true)=true))). % 36.25/23.74 tff(c_2917, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_104), true, iext(Q_104, uri_rdfs_range, uri_rdf_Property), true)=true))). % 36.25/23.74 tff(c_2905, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_104), true, iext(Q_104, uri_rdfs_subClassOf, uri_rdfs_Class), true)=true))). % 36.25/23.74 tff(c_27898, plain, (![D_551]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_551), true, icext(D_551, uri_rdf_value), true)=true))). % 36.25/23.74 tff(c_2966, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_104), true, iext(Q_104, uri_rdfs_range, uri_rdfs_Class), true)=true))). % 36.25/23.74 tff(c_2942, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_104), true, iext(Q_104, sK1_testcase_premise_fullish_023_Unique_List_Components_BNODE_o, uri_owl_Class), true)=true))). % 36.25/23.74 tff(c_2961, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_104), true, iext(Q_104, uri_rdfs_domain, uri_rdfs_Class), true)=true))). % 36.25/23.74 tff(c_2949, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_104), true, iext(Q_104, uri_rdfs_ContainerMembershipProperty, uri_rdf_Property), true)=true))). % 36.25/23.74 tff(c_3069, plain, (![E_108]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Container, E_108), true, iext(uri_rdfs_subClassOf, uri_rdfs_Seq, E_108), true)=true))). % 36.25/23.74 tff(c_2921, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_104), true, iext(Q_104, uri_rdfs_seeAlso, uri_rdfs_Resource), true)=true))). % 36.25/23.74 tff(c_2962, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_104), true, iext(Q_104, uri_rdfs_Datatype, uri_rdfs_Class), true)=true))). % 36.25/23.74 tff(c_2919, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_104), true, iext(Q_104, uri_rdf_type, uri_rdf_Property), true)=true))). % 36.25/23.74 tff(c_2925, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_104), true, iext(Q_104, uri_rdf__3, uri_rdfs_Resource), true)=true))). % 36.25/23.74 tff(c_3072, plain, (![E_108]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, E_108), true, iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, E_108), true)=true))). % 36.25/23.74 tff(c_3073, plain, (![E_108]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, E_108), true, iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, E_108), true)=true))). % 36.25/23.74 tff(c_2913, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_104), true, iext(Q_104, uri_rdfs_domain, uri_rdf_Property), true)=true))). % 36.25/23.74 tff(c_2954, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_104), true, iext(Q_104, uri_rdf_first, uri_rdfs_Resource), true)=true))). % 36.25/23.74 tff(c_2967, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_owl_oneOf, Q_104), true, iext(Q_104, sK1_testcase_premise_fullish_023_Unique_List_Components_BNODE_o, sK2_testcase_premise_fullish_023_Unique_List_Components_BNODE_l), true)=true))). % 36.25/23.74 tff(c_2935, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_104), true, iext(Q_104, uri_rdfs_subClassOf, uri_rdfs_Class), true)=true))). % 36.25/23.74 tff(c_2909, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_104), true, iext(Q_104, uri_rdf__2, uri_rdf_Property), true)=true))). % 36.25/23.74 tff(c_2955, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_104), true, iext(Q_104, uri_rdf_predicate, uri_rdfs_Resource), true)=true))). % 36.25/23.74 tff(c_2945, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_104), true, iext(Q_104, uri_rdfs_isDefinedBy, uri_rdfs_Resource), true)=true))). % 36.25/23.74 tff(c_2953, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_104), true, iext(Q_104, uri_rdf_predicate, uri_rdfs_Statement), true)=true))). % 36.25/23.74 tff(c_2963, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_104), true, iext(Q_104, uri_rdfs_subPropertyOf, uri_rdf_Property), true)=true))). % 36.25/23.74 tff(c_3070, plain, (![E_108]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Literal, E_108), true, iext(uri_rdfs_subClassOf, uri_rdf_XMLLiteral, E_108), true)=true))). % 36.25/23.74 tff(c_2908, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_104), true, iext(Q_104, uri_rdf_first, uri_rdf_Property), true)=true))). % 36.25/23.74 tff(c_2948, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_104), true, iext(Q_104, uri_rdf__3, uri_rdfs_ContainerMembershipProperty), true)=true))). % 36.25/23.74 tff(c_2907, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_104), true, iext(Q_104, uri_rdf_rest, uri_rdf_List), true)=true))). % 36.25/23.74 tff(c_2926, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_104), true, iext(Q_104, uri_rdfs_member, uri_rdfs_Resource), true)=true))). % 36.25/23.74 tff(c_2957, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_104), true, iext(Q_104, uri_rdf__1, uri_rdf_Property), true)=true))). % 36.25/23.74 tff(c_2943, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_104), true, iext(Q_104, uri_rdf_object, uri_rdf_Property), true)=true))). % 36.25/23.74 tff(c_2904, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_104), true, iext(Q_104, uri_rdfs_label, uri_rdfs_Resource), true)=true))). % 36.25/23.74 tff(c_3074, plain, (![E_108]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Container, E_108), true, iext(uri_rdfs_subClassOf, uri_rdf_Alt, E_108), true)=true))). % 36.25/23.74 tff(c_2965, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_104), true, iext(Q_104, uri_rdf_Alt, uri_rdfs_Container), true)=true))). % 36.25/23.74 tff(c_2923, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_104), true, iext(Q_104, uri_rdf_first, uri_rdf_List), true)=true))). % 36.25/23.74 tff(c_2934, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_104), true, iext(Q_104, uri_rdfs_seeAlso, uri_rdfs_Resource), true)=true))). % 36.25/23.74 tff(c_2959, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_104), true, iext(Q_104, uri_rdf_object, uri_rdfs_Statement), true)=true))). % 36.25/23.75 tff(c_2915, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_first, Q_104), true, iext(Q_104, sK2_testcase_premise_fullish_023_Unique_List_Components_BNODE_l, uri_ex_u), true)=true))). % 36.25/23.75 tff(c_27145, plain, (![D_515]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_515), true, icext(D_515, uri_rdf_rest), true)=true))). % 36.25/23.75 tff(c_2960, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_104), true, iext(Q_104, uri_rdf_value, uri_rdf_Property), true)=true))). % 36.25/23.75 tff(c_2936, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_rest, Q_104), true, iext(Q_104, sK2_testcase_premise_fullish_023_Unique_List_Components_BNODE_l, uri_rdf_nil), true)=true))). % 36.25/23.75 tff(c_2911, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_104), true, iext(Q_104, uri_rdf_XMLLiteral, uri_rdfs_Datatype), true)=true))). % 36.25/23.75 tff(c_2946, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_104), true, iext(Q_104, uri_rdfs_isDefinedBy, uri_rdfs_seeAlso), true)=true))). % 36.25/23.75 tff(c_2918, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_104), true, iext(Q_104, uri_rdf_value, uri_rdfs_Resource), true)=true))). % 36.25/23.75 tff(c_17402, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_predicate), true)=true))). % 36.25/23.75 tff(c_16256, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_comment), true)=true))). % 36.25/23.75 tff(c_16191, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_label), true)=true))). % 36.25/23.75 tff(c_16190, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_label), true)=true))). % 36.25/23.75 tff(c_17401, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_predicate), true)=true))). % 36.25/23.75 tff(c_16255, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_comment), true)=true))). % 36.25/23.75 tff(c_16096, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_member), true)=true))). % 36.25/23.75 tff(c_2910, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_104), true, iext(Q_104, uri_rdfs_subPropertyOf, uri_rdf_Property), true)=true))). % 36.25/23.75 tff(c_26785, plain, (![D_500]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_500), true, icext(D_500, uri_rdf__3), true)=true))). % 36.25/23.75 tff(c_15300, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdf_List), true)=true))). % 36.25/23.75 tff(c_15542, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdfs_Statement), true)=true))). % 36.25/23.75 tff(c_15841, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, sK1_testcase_premise_fullish_023_Unique_List_Components_BNODE_o), true)=true))). % 36.25/23.75 tff(c_2927, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_104), true, iext(Q_104, uri_rdf__2, uri_rdfs_ContainerMembershipProperty), true)=true))). % 36.25/23.75 tff(c_15772, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdfs_Resource), true)=true))). % 36.25/23.75 tff(c_2903, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_first, Q_104), true, iext(Q_104, sK2_testcase_premise_fullish_023_Unique_List_Components_BNODE_l, uri_ex_v), true)=true))). % 36.25/23.75 tff(c_18401, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_owl_FunctionalProperty), true)=true))). % 36.25/23.75 tff(c_15840, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, sK1_testcase_premise_fullish_023_Unique_List_Components_BNODE_o), true)=true))). % 36.25/23.75 tff(c_15301, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdf_List), true)=true))). % 36.25/23.75 tff(c_15543, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdfs_Statement), true)=true))). % 36.25/23.75 tff(c_18830, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_owl_Class), true)=true))). % 36.25/23.75 tff(c_19009, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_owl_Class), true)=true))). % 36.25/23.75 tff(c_18402, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_owl_FunctionalProperty), true)=true))). % 36.25/23.75 tff(c_2922, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_104), true, iext(Q_104, uri_rdf_XMLLiteral, uri_rdfs_Literal), true)=true))). % 36.25/23.75 tff(c_26370, plain, (![D_484]: (ifeq(iext(uri_rdfs_subClassOf, uri_owl_Class, D_484), true, icext(D_484, sK1_testcase_premise_fullish_023_Unique_List_Components_BNODE_o), true)=true))). % 36.25/23.75 tff(c_2940, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_104), true, iext(Q_104, uri_rdfs_isDefinedBy, uri_rdfs_Resource), true)=true))). % 36.25/23.75 tff(c_2920, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_104), true, iext(Q_104, uri_rdf_type, uri_rdfs_Resource), true)=true))). % 36.25/23.75 tff(c_26237, plain, (![D_480]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_480), true, icext(D_480, uri_rdf_first), true)=true))). % 36.25/23.75 tff(c_2938, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_104), true, iext(Q_104, uri_rdf__3, uri_rdfs_Resource), true)=true))). % 36.25/23.75 tff(c_2964, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_104), true, iext(Q_104, uri_rdf_rest, uri_rdf_List), true)=true))). % 36.25/23.75 tff(c_2937, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_104), true, iext(Q_104, uri_rdf__2, uri_rdfs_Resource), true)=true))). % 36.62/23.75 tff(c_5980, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_subject), true)=true))). % 36.62/23.75 tff(c_12804, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_isDefinedBy), true)=true))). % 36.62/23.75 tff(c_25915, plain, (![C_89, X_62]: (ifeq(icext(C_89, X_62), true, true, true)=true))). % 36.62/23.75 tff(c_8588, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_domain), true)=true))). % 36.62/23.75 tff(c_8589, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_domain), true)=true))). % 36.62/23.75 tff(c_2924, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_104), true, iext(Q_104, uri_rdf_type, uri_rdfs_Class), true)=true))). % 36.62/23.75 tff(c_25414, plain, (![D_466, X_467]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Resource, D_466), true, icext(D_466, X_467), true)=true))). % 36.62/23.75 tff(c_12526, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdfs_Seq), true)=true))). % 36.62/23.75 tff(c_2929, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_104), true, iext(Q_104, uri_rdf__1, uri_rdfs_ContainerMembershipProperty), true)=true))). % 36.62/23.75 tff(c_13362, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_object), true)=true))). % 36.62/23.75 tff(c_25281, plain, (![X_459, Y_460]: (ifeq(iext(uri_rdf_first, X_459, Y_460), true, icext(uri_rdf_List, X_459), true)=true))). % 36.62/23.75 tff(c_5299, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_subPropertyOf), true)=true))). % 36.62/23.75 tff(c_2462, plain, (![R_101]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_seeAlso, R_101), true, iext(uri_rdfs_subPropertyOf, uri_rdfs_isDefinedBy, R_101), true)=true))). % 36.62/23.75 tff(c_11946, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf__3), true)=true))). % 36.62/23.75 tff(c_24812, plain, (![X_452, Y_453]: (ifeq(iext(uri_rdfs_domain, X_452, Y_453), true, icext(uri_rdf_Property, X_452), true)=true))). % 36.62/23.75 tff(c_2947, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_104), true, iext(Q_104, uri_rdf__1, uri_rdfs_Resource), true)=true))). % 36.62/23.75 tff(c_11945, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf__3), true)=true))). % 36.62/23.75 tff(c_7018, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_subClassOf), true)=true))). % 36.62/23.75 tff(c_24698, plain, (![X_445, Y_446]: (ifeq(iext(uri_rdf_predicate, X_445, Y_446), true, icext(uri_rdfs_Statement, X_445), true)=true))). % 36.62/23.75 tff(c_2968, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_104), true, iext(Q_104, uri_ex_w, sK1_testcase_premise_fullish_023_Unique_List_Components_BNODE_o), true)=true))). % 36.62/23.75 tff(c_4874, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_value), true)=true))). % 36.62/23.75 tff(c_24257, plain, (![X_439, Y_440]: (ifeq(iext(uri_rdfs_subPropertyOf, X_439, Y_440), true, icext(uri_rdf_Property, Y_440), true)=true))). % 36.62/23.75 tff(c_3071, plain, (![E_108]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Container, E_108), true, iext(uri_rdfs_subClassOf, uri_rdf_Bag, E_108), true)=true))). % 36.62/23.75 tff(c_6951, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdfs_Datatype), true)=true))). % 36.62/23.75 tff(c_23483, plain, (![X_432, Y_433]: (ifeq(iext(uri_rdfs_subClassOf, X_432, Y_433), true, icext(uri_rdfs_Class, X_432), true)=true))). % 36.62/23.75 tff(c_11790, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_rest), true)=true))). % 36.62/23.75 tff(c_2930, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_104), true, iext(Q_104, uri_rdf__2, uri_rdfs_Resource), true)=true))). % 36.62/23.75 tff(c_4942, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_type), true)=true))). % 36.62/23.75 tff(c_8140, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdfs_Class), true)=true))). % 36.62/23.75 tff(c_22833, plain, (![X_424, Y_425]: (ifeq(iext(uri_rdf_type, X_424, Y_425), true, icext(uri_rdfs_Class, Y_425), true)=true))). % 36.62/23.75 tff(c_9072, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdfs_Literal), true)=true))). % 36.62/23.75 tff(c_5893, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdf_Property), true)=true))). % 36.62/23.75 tff(c_2956, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_104), true, iext(Q_104, uri_rdf_subject, uri_rdfs_Resource), true)=true))). % 36.62/23.75 tff(c_6604, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf__1), true)=true))). % 36.62/23.75 tff(c_4875, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_value), true)=true))). % 36.62/23.75 tff(c_22675, plain, (![X_415, Y_416]: (ifeq(iext(uri_rdf_object, X_415, Y_416), true, icext(uri_rdfs_Statement, X_415), true)=true))). % 36.62/23.75 tff(c_6603, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf__1), true)=true))). % 36.62/23.75 tff(c_6686, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_owl_oneOf), true)=true))). % 36.62/23.75 tff(c_2939, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_104), true, iext(Q_104, uri_rdf_Bag, uri_rdfs_Container), true)=true))). % 36.62/23.75 tff(c_22250, plain, (![X_408, Y_409]: (ifeq(iext(uri_rdfs_range, X_408, Y_409), true, icext(uri_rdfs_Class, Y_409), true)=true))). % 36.62/23.75 tff(c_13361, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_object), true)=true))). % 36.62/23.75 tff(c_12998, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_range), true)=true))). % 36.62/23.75 tff(c_4943, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_type), true)=true))). % 36.62/23.75 tff(c_2944, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_104), true, iext(Q_104, uri_rdfs_comment, uri_rdfs_Literal), true)=true))). % 36.62/23.75 tff(c_5721, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdf_Alt), true)=true))). % 36.62/23.75 tff(c_5363, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdfs_Container), true)=true))). % 36.62/23.75 tff(c_22077, plain, (![X_398, Y_399]: (ifeq(iext(uri_rdfs_comment, X_398, Y_399), true, icext(uri_rdfs_Literal, Y_399), true)=true))). % 36.62/23.75 tff(c_12997, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_range), true)=true))). % 36.62/23.75 tff(c_2914, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_104), true, iext(Q_104, uri_rdfs_Seq, uri_rdfs_Container), true)=true))). % 36.62/23.75 tff(c_13066, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_first), true)=true))). % 36.62/23.75 tff(c_7647, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdfs_Resource), true)=true))). % 36.62/23.75 tff(c_6310, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdfs_ContainerMembershipProperty), true)=true))). % 36.62/23.75 tff(c_21572, plain, (![X_389, Y_390]: (ifeq(iext(uri_rdfs_subPropertyOf, X_389, Y_390), true, icext(uri_rdf_Property, X_389), true)=true))). % 36.62/23.75 tff(c_11791, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_rest), true)=true))). % 36.62/23.75 tff(c_13067, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_first), true)=true))). % 36.62/23.75 tff(c_5298, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_subPropertyOf), true)=true))). % 36.62/23.75 tff(c_2912, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_104), true, iext(Q_104, uri_rdf__3, uri_rdf_Property), true)=true))). % 36.62/23.75 tff(c_5602, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdf_Bag), true)=true))). % 36.62/23.75 tff(c_20846, plain, (![X_379, Y_380]: (ifeq(iext(uri_rdfs_subClassOf, X_379, Y_380), true, icext(uri_rdfs_Class, Y_380), true)=true))). % 36.62/23.75 tff(c_13294, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf__2), true)=true))). % 36.62/23.75 tff(c_6376, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdf_XMLLiteral), true)=true))). % 36.62/23.75 tff(c_2932, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_104), true, iext(Q_104, uri_rdf_Property, uri_rdfs_Class), true)=true))). % 36.62/23.75 tff(c_11701, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_seeAlso), true)=true))). % 36.62/23.75 tff(c_13293, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf__2), true)=true))). % 36.62/23.75 tff(c_7270, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_member), true)=true))). % 36.62/23.75 tff(c_20369, plain, (![X_369, Y_370]: (ifeq(iext(uri_rdfs_domain, X_369, Y_370), true, icext(uri_rdfs_Class, Y_370), true)=true))). % 36.62/23.75 tff(c_7017, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_subClassOf), true)=true))). % 36.62/23.75 tff(c_5979, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_subject), true)=true))). % 36.62/23.75 tff(c_2951, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_104), true, iext(Q_104, uri_rdfs_member, uri_rdfs_Resource), true)=true))). % 36.62/23.75 tff(c_6687, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_owl_oneOf), true)=true))). % 36.62/23.75 tff(c_20235, plain, (![X_361, Y_362]: (ifeq(iext(uri_rdf_subject, X_361, Y_362), true, icext(uri_rdfs_Statement, X_361), true)=true))). % 36.62/23.75 tff(c_4712, plain, (![C_19, X_133]: (ifeq(iext(uri_rdfs_domain, uri_rdf_type, C_19), true, icext(C_19, X_133), true)=true))). % 36.62/23.75 tff(c_4711, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_29), true, icext(C_29, uri_rdfs_Resource), true)=true))). % 36.62/23.75 tff(c_2931, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_104), true, iext(Q_104, uri_rdf_subject, uri_rdfs_Statement), true)=true))). % 36.62/23.75 tff(c_19828, plain, (![X_350, Y_351]: (ifeq(iext(uri_rdf_rest, X_350, Y_351), true, icext(uri_rdf_List, X_350), true)=true))). % 36.62/23.75 tff(c_1990, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_93), true, icext(C_93, uri_rdfs_subClassOf), true)=true))). % 36.62/23.75 tff(c_2006, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_93), true, icext(C_93, uri_rdfs_ContainerMembershipProperty), true)=true))). % 36.62/23.75 tff(c_1989, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_93), true, icext(C_93, uri_rdfs_seeAlso), true)=true))). % 36.62/23.75 tff(c_2024, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_93), true, icext(C_93, uri_rdf_Alt), true)=true))). % 36.62/23.75 tff(c_1994, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_93), true, icext(C_93, uri_rdf_Bag), true)=true))). % 36.62/23.75 tff(c_1981, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_93), true, icext(C_93, uri_rdfs_label), true)=true))). % 36.62/23.75 tff(c_2394, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdfs_range, C_97), true, icext(C_97, uri_rdf_Property), true)=true))). % 36.62/23.75 tff(c_2026, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_owl_oneOf, C_93), true, icext(C_93, sK1_testcase_premise_fullish_023_Unique_List_Components_BNODE_o), true)=true))). % 36.62/23.75 tff(c_2023, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_93), true, icext(C_93, uri_rdf_rest), true)=true))). % 36.62/23.75 tff(c_1979, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_93), true, icext(C_93, uri_rdfs_member), true)=true))). % 36.62/23.75 tff(c_19158, plain, (![X_331, Y_332]: (ifeq(iext(uri_rdfs_range, X_331, Y_332), true, icext(uri_rdf_Property, X_331), true)=true))). % 36.62/23.75 tff(c_1975, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_93), true, icext(C_93, uri_rdf_type), true)=true))). % 36.62/23.75 tff(c_1964, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_93), true, icext(C_93, uri_rdfs_Seq), true)=true))). % 36.62/23.75 tff(c_2376, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_97), true, icext(C_97, uri_rdf_Property), true)=true))). % 36.62/23.75 tff(c_2025, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_93), true, icext(C_93, uri_rdfs_range), true)=true))). % 36.62/23.75 tff(c_1993, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_93), true, icext(C_93, uri_rdf__3), true)=true))). % 36.62/23.75 tff(c_19011, plain, (![X_33]: (ifeq(icext(uri_owl_Class, X_33), true, icext(uri_owl_Class, X_33), true)=true))). % 36.62/23.75 tff(c_2355, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_97), true, icext(C_97, uri_rdfs_Class), true)=true))). % 36.62/23.75 tff(c_18955, plain, (iext(uri_rdfs_subClassOf, uri_owl_Class, uri_owl_Class)=true)). % 36.62/23.76 tff(c_18775, plain, (iext(uri_rdfs_subClassOf, uri_owl_Class, uri_rdfs_Resource)=true)). % 36.62/23.76 tff(c_18703, plain, (iext(uri_rdf_type, uri_owl_Class, uri_rdfs_Class)=true)). % 36.62/23.76 tff(c_18537, plain, (ic(uri_owl_Class)=true)). % 36.62/23.76 tff(c_18475, plain, (icext(uri_rdfs_Class, uri_owl_Class)=true)). % 36.62/23.76 tff(c_2368, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_97), true, icext(C_97, uri_owl_Class), true)=true))). % 36.62/23.76 tff(c_2372, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_97), true, icext(C_97, uri_rdfs_seeAlso), true)=true))). % 36.62/23.76 tff(c_18403, plain, (![X_33]: (ifeq(icext(uri_owl_FunctionalProperty, X_33), true, icext(uri_owl_FunctionalProperty, X_33), true)=true))). % 36.62/23.76 tff(c_18347, plain, (iext(uri_rdfs_subClassOf, uri_owl_FunctionalProperty, uri_owl_FunctionalProperty)=true)). % 36.62/23.76 tff(c_18174, plain, (iext(uri_rdfs_subClassOf, uri_owl_FunctionalProperty, uri_rdfs_Resource)=true)). % 36.62/23.76 tff(c_18009, plain, (iext(uri_rdf_type, uri_owl_FunctionalProperty, uri_rdfs_Class)=true)). % 36.62/23.76 tff(c_17944, plain, (ic(uri_owl_FunctionalProperty)=true)). % 36.62/23.76 tff(c_2008, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_93), true, icext(C_93, uri_rdfs_comment), true)=true))). % 36.62/23.76 tff(c_17882, plain, (icext(uri_rdfs_Class, uri_owl_FunctionalProperty)=true)). % 36.62/23.76 tff(c_2327, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_97), true, icext(C_97, uri_owl_FunctionalProperty), true)=true))). % 36.62/23.76 tff(c_1960, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_93), true, icext(C_93, uri_rdfs_subPropertyOf), true)=true))). % 36.62/23.76 tff(c_1995, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_93), true, icext(C_93, uri_rdfs_isDefinedBy), true)=true))). % 36.62/23.76 tff(c_1977, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_93), true, icext(C_93, uri_rdf__3), true)=true))). % 36.62/23.76 tff(c_2346, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdfs_domain, C_97), true, icext(C_97, uri_rdf_List), true)=true))). % 36.62/23.76 tff(c_1985, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_93), true, icext(C_93, uri_rdf_subject), true)=true))). % 36.62/23.76 tff(c_17543, plain, (![X_303, Y_304]: (ifeq(iext(uri_rdfs_label, X_303, Y_304), true, icext(uri_rdfs_Literal, Y_304), true)=true))). % 36.62/23.76 tff(c_2345, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_97), true, icext(C_97, uri_rdfs_Literal), true)=true))). % 36.62/23.76 tff(c_2011, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_93), true, icext(C_93, uri_rdf_value), true)=true))). % 36.62/23.76 tff(c_1984, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_93), true, icext(C_93, uri_rdf__2), true)=true))). % 36.62/23.76 tff(c_2012, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_93), true, icext(C_93, uri_rdf_predicate), true)=true))). % 36.62/23.76 tff(c_2336, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdf_first, C_97), true, icext(C_97, uri_ex_u), true)=true))). % 36.62/23.76 tff(c_2020, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_93), true, icext(C_93, uri_rdfs_domain), true)=true))). % 36.62/23.76 tff(c_2393, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_97), true, icext(C_97, uri_rdfs_Class), true)=true))). % 36.62/23.76 tff(c_17347, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_predicate, uri_rdf_predicate)=true)). % 36.62/23.76 tff(c_17186, plain, (ip(uri_rdf_predicate)=true)). % 36.62/23.76 tff(c_17129, plain, (iext(uri_rdf_type, uri_rdf_predicate, uri_rdf_Property)=true)). % 36.62/23.76 tff(c_17073, plain, (icext(uri_rdf_Property, uri_rdf_predicate)=true)). % 36.62/23.76 tff(c_2014, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_93), true, icext(C_93, uri_rdf_predicate), true)=true))). % 36.62/23.76 tff(c_1963, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_93), true, icext(C_93, uri_rdfs_domain), true)=true))). % 36.62/23.76 tff(c_2015, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_93), true, icext(C_93, uri_rdf_subject), true)=true))). % 36.62/23.76 tff(c_2370, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdfs_range, C_97), true, icext(C_97, uri_rdfs_Literal), true)=true))). % 36.62/23.76 tff(c_2021, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_93), true, icext(C_93, uri_rdfs_Datatype), true)=true))). % 36.62/23.76 tff(c_2003, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_93), true, icext(C_93, uri_rdfs_isDefinedBy), true)=true))). % 36.62/23.76 tff(c_1974, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_93), true, icext(C_93, uri_rdf_first), true)=true))). % 36.62/23.76 tff(c_2359, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdf_rest, C_97), true, icext(C_97, uri_rdf_nil), true)=true))). % 36.62/23.76 tff(c_1971, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_93), true, icext(C_93, uri_rdf_type), true)=true))). % 36.62/23.76 tff(c_16347, plain, (![X_273, Y_274]: (ifeq(iext(uri_rdf_rest, X_273, Y_274), true, icext(uri_rdf_List, Y_274), true)=true))). % 36.62/23.76 tff(c_15302, plain, (![X_33]: (ifeq(icext(uri_rdf_List, X_33), true, icext(uri_rdf_List, X_33), true)=true))). % 36.62/23.76 tff(c_15842, plain, (![X_33]: (ifeq(icext(sK1_testcase_premise_fullish_023_Unique_List_Components_BNODE_o, X_33), true, icext(sK1_testcase_premise_fullish_023_Unique_List_Components_BNODE_o, X_33), true)=true))). % 36.62/23.76 tff(c_15544, plain, (![X_33]: (ifeq(icext(uri_rdfs_Statement, X_33), true, icext(uri_rdfs_Statement, X_33), true)=true))). % 36.62/23.76 tff(c_1997, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_93), true, icext(C_93, uri_rdf__1), true)=true))). % 36.62/23.76 tff(c_12528, plain, (![X_33]: (ifeq(icext(uri_rdfs_Seq, X_33), true, icext(uri_rdfs_Seq, X_33), true)=true))). % 36.62/23.76 tff(c_6378, plain, (![X_33]: (ifeq(icext(uri_rdf_XMLLiteral, X_33), true, icext(uri_rdf_XMLLiteral, X_33), true)=true))). % 36.62/23.76 tff(c_8141, plain, (![X_33]: (ifeq(icext(uri_rdfs_Class, X_33), true, icext(uri_rdfs_Class, X_33), true)=true))). % 36.62/23.76 tff(c_5894, plain, (![X_33]: (ifeq(icext(uri_rdf_Property, X_33), true, icext(uri_rdf_Property, X_33), true)=true))). % 36.62/23.76 tff(c_6312, plain, (![X_33]: (ifeq(icext(uri_rdfs_ContainerMembershipProperty, X_33), true, icext(uri_rdfs_ContainerMembershipProperty, X_33), true)=true))). % 36.62/23.76 tff(c_6953, plain, (![X_33]: (ifeq(icext(uri_rdfs_Datatype, X_33), true, icext(uri_rdfs_Datatype, X_33), true)=true))). % 36.62/23.76 tff(c_5723, plain, (![X_33]: (ifeq(icext(uri_rdf_Alt, X_33), true, icext(uri_rdf_Alt, X_33), true)=true))). % 36.62/23.76 tff(c_5364, plain, (![X_33]: (ifeq(icext(uri_rdfs_Container, X_33), true, icext(uri_rdfs_Container, X_33), true)=true))). % 36.62/23.76 tff(c_2337, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_97), true, icext(C_97, uri_rdf_List), true)=true))). % 36.62/23.76 tff(c_5604, plain, (![X_33]: (ifeq(icext(uri_rdf_Bag, X_33), true, icext(uri_rdf_Bag, X_33), true)=true))). % 36.62/23.76 tff(c_9635, plain, (![X_33]: (ifeq(icext(uri_rdfs_Literal, X_33), true, icext(uri_rdfs_Literal, X_33), true)=true))). % 36.62/23.76 tff(c_16201, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_comment, uri_rdfs_comment)=true)). % 36.62/23.76 tff(c_16136, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_label, uri_rdfs_label)=true)). % 36.62/23.76 tff(c_2013, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_93), true, icext(C_93, uri_rdf_first), true)=true))). % 36.62/23.76 tff(c_16038, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_member, uri_rdfs_member)=true)). % 36.62/23.76 tff(c_15853, plain, (iext(uri_rdfs_subClassOf, sK1_testcase_premise_fullish_023_Unique_List_Components_BNODE_o, uri_rdfs_Resource)=true)). % 36.62/23.76 tff(c_2022, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_93), true, icext(C_93, uri_rdfs_subPropertyOf), true)=true))). % 36.62/23.76 tff(c_15786, plain, (iext(uri_rdfs_subClassOf, sK1_testcase_premise_fullish_023_Unique_List_Components_BNODE_o, sK1_testcase_premise_fullish_023_Unique_List_Components_BNODE_o)=true)). % 36.62/23.76 tff(c_15713, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Resource, uri_rdfs_Resource)=true)). % 36.62/23.76 tff(c_15554, plain, (iext(uri_rdfs_subClassOf, uri_rdf_List, uri_rdfs_Resource)=true)). % 36.62/23.76 tff(c_15488, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Statement, uri_rdfs_Statement)=true)). % 36.62/23.76 tff(c_2324, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdf_first, C_97), true, icext(C_97, uri_ex_v), true)=true))). % 36.62/23.76 tff(c_15312, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Statement, uri_rdfs_Resource)=true)). % 36.62/23.76 tff(c_15246, plain, (iext(uri_rdfs_subClassOf, uri_rdf_List, uri_rdf_List)=true)). % 36.62/23.76 tff(c_2397, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdfs_range, C_97), true, icext(C_97, uri_rdfs_Class), true)=true))). % 36.62/23.76 tff(c_15170, plain, (iext(uri_rdf_type, uri_rdf_Bag, uri_rdfs_Class)=true)). % 36.62/23.76 tff(c_15097, plain, (iext(uri_rdf_type, sK1_testcase_premise_fullish_023_Unique_List_Components_BNODE_o, uri_rdfs_Class)=true)). % 36.62/23.76 tff(c_2396, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_97), true, icext(C_97, uri_rdfs_Container), true)=true))). % 36.62/23.76 tff(c_14960, plain, (ic(sK1_testcase_premise_fullish_023_Unique_List_Components_BNODE_o)=true)). % 36.62/23.76 tff(c_14906, plain, (icext(uri_rdfs_Class, sK1_testcase_premise_fullish_023_Unique_List_Components_BNODE_o)=true)). % 36.62/23.76 tff(c_2399, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_97), true, icext(C_97, sK1_testcase_premise_fullish_023_Unique_List_Components_BNODE_o), true)=true))). % 36.62/23.76 tff(c_14832, plain, (iext(uri_rdf_type, uri_rdfs_Datatype, uri_rdfs_Class)=true)). % 36.62/23.76 tff(c_1973, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_93), true, icext(C_93, uri_rdf_XMLLiteral), true)=true))). % 36.62/23.76 tff(c_14752, plain, (iext(uri_rdf_type, uri_rdfs_Container, uri_rdfs_Class)=true)). % 36.62/23.76 tff(c_14704, plain, (iext(uri_rdf_type, uri_rdf_XMLLiteral, uri_rdfs_Class)=true)). % 36.62/23.76 tff(c_1952, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdf_first, C_93), true, icext(C_93, sK2_testcase_premise_fullish_023_Unique_List_Components_BNODE_l), true)=true))). % 36.62/23.76 tff(c_14630, plain, (iext(uri_rdf_type, uri_rdf_Alt, uri_rdfs_Class)=true)). % 36.62/23.76 tff(c_14581, plain, (iext(uri_rdf_type, uri_rdfs_ContainerMembershipProperty, uri_rdfs_Class)=true)). % 36.62/23.76 tff(c_14509, plain, (iext(uri_rdf_type, uri_rdfs_Literal, uri_rdfs_Class)=true)). % 36.62/23.76 tff(c_14462, plain, (iext(uri_rdf_type, uri_rdfs_Class, uri_rdfs_Class)=true)). % 36.62/23.76 tff(c_14389, plain, (iext(uri_rdf_type, uri_rdfs_Seq, uri_rdfs_Class)=true)). % 36.62/23.76 tff(c_1955, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_93), true, icext(C_93, uri_rdfs_subClassOf), true)=true))). % 36.62/23.76 tff(c_14339, plain, (iext(uri_rdf_type, uri_rdfs_Statement, uri_rdfs_Class)=true)). % 36.62/23.76 tff(c_14271, plain, (iext(uri_rdf_type, uri_rdfs_Resource, uri_rdfs_Class)=true)). % 36.62/23.76 tff(c_2398, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_owl_oneOf, C_97), true, icext(C_97, sK2_testcase_premise_fullish_023_Unique_List_Components_BNODE_l), true)=true))). % 36.62/23.76 tff(c_14224, plain, (iext(uri_rdf_type, uri_rdf_List, uri_rdfs_Class)=true)). % 36.62/23.76 tff(c_14183, plain, (ip(uri_rdfs_comment)=true)). % 36.62/23.76 tff(c_14129, plain, (iext(uri_rdf_type, uri_rdfs_comment, uri_rdf_Property)=true)). % 36.62/23.76 tff(c_13980, plain, (iext(uri_rdf_type, uri_rdfs_member, uri_rdf_Property)=true)). % 36.62/23.76 tff(c_13932, plain, (icext(uri_rdf_Property, uri_rdfs_comment)=true)). % 36.62/23.76 tff(c_2000, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_93), true, icext(C_93, uri_rdfs_comment), true)=true))). % 36.62/23.76 tff(c_13865, plain, (iext(uri_rdf_type, sK2_testcase_premise_fullish_023_Unique_List_Components_BNODE_l, uri_rdf_List)=true)). % 36.62/23.76 tff(c_13823, plain, (ip(uri_rdfs_label)=true)). % 36.62/23.76 tff(c_13765, plain, (iext(uri_rdf_type, uri_rdfs_label, uri_rdf_Property)=true)). % 36.62/23.76 tff(c_13614, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, uri_rdfs_Resource)=true)). % 36.62/23.76 tff(c_3383, plain, (![S_5, O_6]: (ifeq(iext(uri_rdfs_subPropertyOf, S_5, O_6), true, true, true)=true))). % 36.62/23.76 tff(c_13304, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_object, uri_rdf_object)=true)). % 36.62/23.76 tff(c_13236, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf__2, uri_rdf__2)=true)). % 36.62/23.76 tff(c_13009, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_first, uri_rdf_first)=true)). % 36.62/23.76 tff(c_12940, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_range, uri_rdfs_range)=true)). % 36.62/23.76 tff(c_1618, plain, (![S_5, O_6]: (ifeq(iext(uri_rdfs_subClassOf, S_5, O_6), true, true, true)=true))). % 36.62/23.76 tff(c_2002, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_93), true, icext(C_93, uri_rdfs_isDefinedBy), true)=true))). % 36.62/23.76 tff(c_12747, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_isDefinedBy, uri_rdfs_isDefinedBy)=true)). % 36.62/23.76 tff(c_1214, plain, (![S_5, O_6]: (ifeq(iext(uri_rdfs_range, S_5, O_6), true, true, true)=true))). % 36.62/23.76 tff(c_12472, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Seq, uri_rdfs_Seq)=true)). % 36.62/23.76 tff(c_2358, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdfs_domain, C_97), true, icext(C_97, uri_rdfs_Class), true)=true))). % 36.62/23.76 tff(c_12188, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Seq, uri_rdfs_Resource)=true)). % 36.62/23.76 tff(c_11976, plain, (icext(uri_rdf_Property, uri_rdfs_label)=true)). % 36.62/23.76 tff(c_1954, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_93), true, icext(C_93, uri_rdfs_label), true)=true))). % 36.62/23.76 tff(c_11888, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf__3, uri_rdf__3)=true)). % 36.62/23.76 tff(c_1571, plain, (![S_5, O_6]: (ifeq(iext(uri_owl_oneOf, S_5, O_6), true, true, true)=true))). % 36.62/23.76 tff(c_11740, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_rest, uri_rdf_rest)=true)). % 36.62/23.76 tff(c_11643, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_seeAlso, uri_rdfs_seeAlso)=true)). % 36.62/23.76 tff(c_11520, plain, (icext(uri_rdf_Property, uri_rdfs_subPropertyOf)=true)). % 36.62/23.76 tff(c_11465, plain, (iext(uri_rdf_type, uri_rdfs_subPropertyOf, uri_rdf_Property)=true)). % 36.62/23.76 tff(c_11167, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf__2, uri_rdfs_member)=true)). % 36.62/23.76 tff(c_11074, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf__1, uri_rdfs_member)=true)). % 36.62/23.76 tff(c_1968, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_93), true, icext(C_93, uri_rdf_value), true)=true))). % 36.62/23.76 tff(c_10700, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Class, uri_rdfs_Resource)=true)). % 36.62/23.76 tff(c_10472, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Bag, uri_rdfs_Resource)=true)). % 36.62/23.76 tff(c_10067, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, uri_rdfs_Resource)=true)). % 36.62/23.76 tff(c_9573, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Literal, uri_rdfs_Literal)=true)). % 36.62/23.76 tff(c_9451, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Container, uri_rdfs_Resource)=true)). % 36.62/23.76 tff(c_9261, plain, (ic(uri_rdfs_Statement)=true)). % 36.62/23.76 tff(c_9211, plain, (icext(uri_rdfs_Class, uri_rdfs_Statement)=true)). % 36.62/23.76 tff(c_9130, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Property, uri_rdfs_Resource)=true)). % 36.62/23.76 tff(c_2381, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdfs_domain, C_97), true, icext(C_97, uri_rdfs_Statement), true)=true))). % 36.62/23.76 tff(c_9017, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Literal, uri_rdfs_Resource)=true)). % 36.62/23.76 tff(c_2352, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_97), true, icext(C_97, uri_rdfs_ContainerMembershipProperty), true)=true))). % 36.62/23.76 tff(c_8774, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Alt, uri_rdfs_Resource)=true)). % 36.62/23.76 tff(c_8731, plain, (icext(uri_rdf_Property, uri_owl_oneOf)=true)). % 36.62/23.76 tff(c_8678, plain, (iext(uri_rdf_type, uri_owl_oneOf, uri_rdf_Property)=true)). % 36.62/23.76 tff(c_8538, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, uri_rdfs_domain)=true)). % 36.62/23.76 tff(c_1957, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_93), true, icext(C_93, uri_rdf_rest), true)=true))). % 36.62/23.76 tff(c_8350, plain, (icext(uri_rdf_Property, uri_rdfs_range)=true)). % 36.62/23.76 tff(c_1967, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_93), true, icext(C_93, uri_rdfs_range), true)=true))). % 36.62/23.76 tff(c_8278, plain, (iext(uri_rdf_type, uri_rdfs_range, uri_rdf_Property)=true)). % 36.62/23.76 tff(c_1246, plain, (![S_5, O_6]: (ifeq(iext(uri_rdfs_domain, S_5, O_6), true, true, true)=true))). % 36.62/23.76 tff(c_8082, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Class, uri_rdfs_Class)=true)). % 36.62/23.76 tff(c_1992, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_93), true, icext(C_93, uri_rdf__2), true)=true))). % 36.62/23.76 tff(c_7977, plain, (icext(uri_rdf_Property, uri_rdfs_subClassOf)=true)). % 36.62/23.76 tff(c_7900, plain, (iext(uri_rdf_type, uri_rdfs_subClassOf, uri_rdf_Property)=true)). % 36.62/23.76 tff(c_1972, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_93), true, icext(C_93, uri_rdfs_seeAlso), true)=true))). % 36.62/23.76 tff(c_7756, plain, (icext(uri_rdf_Property, uri_rdfs_isDefinedBy)=true)). % 36.62/23.76 tff(c_2377, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdfs_domain, C_97), true, icext(C_97, uri_rdfs_Resource), true)=true))). % 36.62/23.76 tff(c_7674, plain, (iext(uri_rdf_type, uri_rdfs_isDefinedBy, uri_rdf_Property)=true)). % 36.62/23.76 tff(c_7593, plain, (iext(uri_rdfs_subClassOf, uri_rdf_XMLLiteral, uri_rdfs_Resource)=true)). % 36.62/23.76 tff(c_2332, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_97), true, icext(C_97, uri_rdfs_Datatype), true)=true))). % 36.62/23.76 tff(c_7504, plain, (icext(uri_rdf_Property, uri_rdfs_seeAlso)=true)). % 36.62/23.76 tff(c_7451, plain, (iext(uri_rdf_type, uri_rdfs_seeAlso, uri_rdf_Property)=true)). % 36.62/23.76 tff(c_2389, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_97), true, icext(C_97, uri_rdf_Property), true)=true))). % 36.62/23.76 tff(c_7280, plain, (ip(uri_rdfs_member)=true)). % 36.62/23.76 tff(c_7220, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf__3, uri_rdfs_member)=true)). % 36.62/23.76 tff(c_2018, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_93), true, icext(C_93, uri_rdf_object), true)=true))). % 36.62/23.76 tff(c_6963, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, uri_rdfs_subClassOf)=true)). % 36.62/23.76 tff(c_6898, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, uri_rdfs_Datatype)=true)). % 36.62/23.76 tff(c_6851, plain, (ic(uri_rdf_List)=true)). % 36.62/23.76 tff(c_6802, plain, (icext(uri_rdfs_Class, uri_rdf_List)=true)). % 36.62/23.76 tff(c_2395, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdfs_range, C_97), true, icext(C_97, uri_rdf_List), true)=true))). % 36.62/23.76 tff(c_6697, plain, (icext(uri_rdf_Property, uri_rdfs_member)=true)). % 36.62/23.76 tff(c_6614, plain, (iext(uri_rdfs_subPropertyOf, uri_owl_oneOf, uri_owl_oneOf)=true)). % 36.62/23.76 tff(c_2009, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_93), true, icext(C_93, uri_rdfs_member), true)=true))). % 36.62/23.76 tff(c_6550, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf__1, uri_rdf__1)=true)). % 36.62/23.76 tff(c_6322, plain, (iext(uri_rdfs_subClassOf, uri_rdf_XMLLiteral, uri_rdf_XMLLiteral)=true)). % 36.62/23.76 tff(c_6257, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, uri_rdfs_ContainerMembershipProperty)=true)). % 36.62/23.76 tff(c_2041, plain, (![S_5, O_6]: (ifeq(iext(uri_rdf_rest, S_5, O_6), true, true, true)=true))). % 36.62/23.76 tff(c_2334, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdfs_domain, C_97), true, icext(C_97, uri_rdf_Property), true)=true))). % 36.62/23.76 tff(c_6095, plain, (icext(uri_rdf_List, sK2_testcase_premise_fullish_023_Unique_List_Components_BNODE_l)=true)). % 36.62/23.76 tff(c_1991, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdf_rest, C_93), true, icext(C_93, sK2_testcase_premise_fullish_023_Unique_List_Components_BNODE_l), true)=true))). % 36.62/23.76 tff(c_6039, plain, (ic(uri_rdfs_Resource)=true)). % 36.62/23.76 tff(c_5990, plain, (icext(uri_rdfs_Class, uri_rdfs_Resource)=true)). % 36.62/23.76 tff(c_5904, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_subject, uri_rdf_subject)=true)). % 36.62/23.76 tff(c_2361, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdfs_range, C_97), true, icext(C_97, uri_rdfs_Resource), true)=true))). % 36.62/23.76 tff(c_5842, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Property, uri_rdf_Property)=true)). % 36.62/23.76 tff(c_2004, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_93), true, icext(C_93, uri_rdf__1), true)=true))). % 36.62/23.76 tff(c_1162, plain, (![S_5, O_6]: (ifeq(iext(uri_rdf_object, S_5, O_6), true, true, true)=true))). % 36.62/23.76 tff(c_5671, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Alt, uri_rdf_Alt)=true)). % 36.62/23.76 tff(c_5549, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Bag, uri_rdf_Bag)=true)). % 36.62/23.76 tff(c_1665, plain, (![X_90]: (ifeq(icext(uri_rdf_XMLLiteral, X_90), true, icext(uri_rdfs_Literal, X_90), true)=true))). % 36.62/23.77 tff(c_1666, plain, (![X_90]: (ifeq(icext(uri_rdf_Bag, X_90), true, icext(uri_rdfs_Container, X_90), true)=true))). % 36.62/23.77 tff(c_5309, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Container, uri_rdfs_Container)=true)). % 36.62/23.77 tff(c_5248, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf)=true)). % 36.62/23.77 tff(c_1664, plain, (![X_90]: (ifeq(icext(uri_rdfs_Seq, X_90), true, icext(uri_rdfs_Container, X_90), true)=true))). % 36.62/23.77 tff(c_1667, plain, (![X_90]: (ifeq(icext(uri_rdfs_ContainerMembershipProperty, X_90), true, icext(uri_rdf_Property, X_90), true)=true))). % 36.62/23.77 tff(c_1668, plain, (![X_90]: (ifeq(icext(uri_rdfs_Datatype, X_90), true, icext(uri_rdfs_Class, X_90), true)=true))). % 36.62/23.77 tff(c_5006, plain, (icext(uri_rdf_Property, uri_rdfs_domain)=true)). % 36.62/23.77 tff(c_4953, plain, (iext(uri_rdf_type, uri_rdfs_domain, uri_rdf_Property)=true)). % 36.62/23.77 tff(c_4892, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_type, uri_rdf_type)=true)). % 36.62/23.77 tff(c_1669, plain, (![X_90]: (ifeq(icext(uri_rdf_Alt, X_90), true, icext(uri_rdfs_Container, X_90), true)=true))). % 36.62/23.77 tff(c_4824, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_value, uri_rdf_value)=true)). % 36.62/23.77 tff(c_1970, plain, (![X_94, Y_95]: (ifeq(iext(uri_rdf_type, X_94, Y_95), true, true, true)=true))). % 36.62/23.77 tff(c_2386, plain, (![X_98, Y_99]: (ifeq(iext(uri_rdf_subject, X_98, Y_99), true, true, true)=true))). % 36.62/23.77 tff(c_1953, plain, (![X_94, Y_95]: (ifeq(iext(uri_rdfs_label, X_94, Y_95), true, true, true)=true))). % 36.62/23.77 tff(c_4673, plain, (![X_132]: (iext(uri_rdf_type, X_132, uri_rdfs_Resource)=true))). % 36.62/23.77 tff(c_2382, plain, (![X_98, Y_99]: (ifeq(iext(uri_rdf_first, X_98, Y_99), true, true, true)=true))). % 36.62/23.77 tff(c_2384, plain, (![X_98, Y_99]: (ifeq(iext(uri_rdf_predicate, X_98, Y_99), true, true, true)=true))). % 36.62/23.77 tff(c_1996, plain, (![X_94, Y_95]: (ifeq(iext(uri_rdf__1, X_94, Y_95), true, true, true)=true))). % 36.62/23.77 tff(c_2007, plain, (![X_94, Y_95]: (ifeq(iext(uri_rdfs_comment, X_94, Y_95), true, true, true)=true))). % 36.62/23.77 tff(c_1976, plain, (![X_94, Y_95]: (ifeq(iext(uri_rdf__3, X_94, Y_95), true, true, true)=true))). % 36.62/23.77 tff(c_2360, plain, (![X_98, Y_99]: (ifeq(iext(uri_rdf__2, X_98, Y_99), true, true, true)=true))). % 36.62/23.77 tff(c_4551, plain, (icext(uri_rdfs_Class, uri_rdf_Bag)=true)). % 36.62/23.77 tff(c_4496, plain, (icext(uri_rdfs_Class, uri_rdfs_Seq)=true)). % 36.62/23.77 tff(c_1988, plain, (![X_94, Y_95]: (ifeq(iext(uri_rdfs_seeAlso, X_94, Y_95), true, true, true)=true))). % 36.62/23.77 tff(c_4451, plain, (icext(uri_rdfs_Class, uri_rdf_Alt)=true)). % 36.62/23.77 tff(c_4408, plain, (icext(uri_rdfs_Class, uri_rdfs_Container)=true)). % 36.62/23.77 tff(c_1978, plain, (![X_94, Y_95]: (ifeq(iext(uri_rdfs_member, X_94, Y_95), true, true, true)=true))). % 36.62/23.77 tff(c_4350, plain, (icext(uri_rdfs_Class, uri_rdfs_Class)=true)). % 36.62/23.77 tff(c_4307, plain, (icext(uri_rdfs_Class, uri_rdfs_Datatype)=true)). % 36.62/23.77 tff(c_4264, plain, (icext(uri_rdfs_Class, uri_rdfs_ContainerMembershipProperty)=true)). % 36.62/23.77 tff(c_2339, plain, (![X_98, Y_99]: (ifeq(iext(uri_rdf_value, X_98, Y_99), true, true, true)=true))). % 36.62/23.77 tff(c_4212, plain, (icext(uri_rdfs_Class, uri_rdf_XMLLiteral)=true)). % 36.62/23.77 tff(c_4169, plain, (icext(uri_rdfs_Class, uri_rdfs_Literal)=true)). % 36.62/23.77 tff(c_2365, plain, (![X_98, Y_99]: (ifeq(iext(uri_rdfs_isDefinedBy, X_98, Y_99), true, true, true)=true))). % 36.62/23.77 tff(c_4118, plain, (icext(uri_rdf_Property, uri_rdf__1)=true)). % 36.62/23.77 tff(c_4043, plain, (icext(uri_rdf_Property, uri_rdf_value)=true)). % 36.62/23.77 tff(c_4033, plain, (icext(uri_rdfs_ContainerMembershipProperty, uri_rdf__1)=true)). % 36.62/23.77 tff(c_3993, plain, (icext(uri_rdf_List, uri_rdf_nil)=true)). % 36.62/23.77 tff(c_3949, plain, (icext(uri_rdf_Property, uri_rdf_rest)=true)). % 36.62/23.77 tff(c_3910, plain, (icext(uri_rdf_Property, uri_rdf_subject)=true)). % 36.62/23.77 tff(c_3873, plain, (icext(uri_rdf_Property, uri_rdf__2)=true)). % 36.62/23.77 tff(c_3832, plain, (icext(uri_rdf_Property, uri_rdf_object)=true)). % 36.62/23.77 tff(c_3789, plain, (icext(uri_rdfs_ContainerMembershipProperty, uri_rdf__3)=true)). % 36.62/23.77 tff(c_3749, plain, (icext(uri_rdfs_ContainerMembershipProperty, uri_rdf__2)=true)). % 36.62/23.77 tff(c_3707, plain, (icext(uri_rdf_Property, uri_rdf__3)=true)). % 36.62/23.77 tff(c_3668, plain, (icext(uri_rdf_Property, uri_rdf_first)=true)). % 36.62/23.77 tff(c_3629, plain, (icext(uri_owl_FunctionalProperty, uri_rdf_first)=true)). % 36.62/23.77 tff(c_3590, plain, (icext(sK1_testcase_premise_fullish_023_Unique_List_Components_BNODE_o, uri_ex_w)=true)). % 36.62/23.77 tff(c_3549, plain, (icext(uri_owl_Class, sK1_testcase_premise_fullish_023_Unique_List_Components_BNODE_o)=true)). % 36.62/23.77 tff(c_3491, plain, (icext(uri_rdfs_Datatype, uri_rdf_XMLLiteral)=true)). % 36.62/23.77 tff(c_3450, plain, (icext(uri_rdf_Property, uri_rdf_type)=true)). % 36.62/23.77 tff(c_3405, plain, (icext(uri_rdfs_Class, uri_rdf_Property)=true)). % 36.62/23.77 tff(c_3365, plain, (ip(uri_rdfs_subPropertyOf)=true)). % 36.62/23.77 tff(c_3321, plain, (ic(uri_rdfs_Seq)=true)). % 36.62/23.77 tff(c_3279, plain, (ic(uri_rdf_Property)=true)). % 36.62/23.77 tff(c_3240, plain, (ip(uri_rdf_value)=true)). % 36.62/23.77 tff(c_3204, plain, (ic(uri_rdf_Bag)=true)). % 36.62/23.77 tff(c_3155, plain, (ic(uri_rdfs_Class)=true)). % 36.62/23.77 tff(c_3116, plain, (ic(uri_rdfs_ContainerMembershipProperty)=true)). % 36.62/23.77 tff(c_3079, plain, (ic(uri_rdf_XMLLiteral)=true)). % 36.62/23.77 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))). % 36.62/23.77 tff(c_2975, plain, (ip(uri_rdf__3)=true)). % 36.62/23.77 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))). % 36.62/23.77 tff(c_2439, plain, (ic(uri_rdfs_Literal)=true)). % 36.62/23.77 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))). % 36.62/23.77 tff(c_2403, plain, (ip(uri_rdfs_isDefinedBy)=true)). % 36.62/23.77 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))). % 36.62/23.77 tff(c_1677, plain, (ip(uri_rdf_rest)=true)). % 36.62/23.77 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))). % 36.62/23.77 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))). % 36.62/23.77 tff(c_1600, plain, (ip(uri_rdfs_subClassOf)=true)). % 36.62/23.77 tff(c_196, plain, (tuple(iext(uri_owl_sameAs, uri_ex_w, uri_ex_v), iext(uri_owl_sameAs, uri_ex_w, uri_ex_u))!=tuple(true, true))). % 36.62/23.77 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))). % 36.62/23.77 tff(c_1489, plain, (ip(uri_owl_oneOf)=true)). % 36.62/23.77 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))). % 36.62/23.77 tff(c_1454, plain, (ic(uri_rdfs_Datatype)=true)). % 36.62/23.77 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))). % 36.62/23.77 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))). % 36.62/23.77 tff(c_1337, plain, (ic(uri_rdf_Alt)=true)). % 36.62/23.77 tff(c_152, plain, (![C_37, D_38]: (ifeq(iext(uri_rdfs_subClassOf, C_37, D_38), true, ic(C_37), true)=true))). % 36.62/23.77 tff(c_170, plain, (![P_51]: (ifeq(ip(P_51), true, iext(uri_rdfs_subPropertyOf, P_51, P_51), true)=true))). % 36.62/23.77 tff(c_1231, plain, (ip(uri_rdfs_domain)=true)). % 36.62/23.77 tff(c_1181, plain, (ip(uri_rdfs_range)=true)). % 36.62/23.77 tff(c_156, plain, (![C_39]: (ifeq(ic(C_39), true, iext(uri_rdfs_subClassOf, C_39, C_39), true)=true))). % 36.62/23.77 tff(c_1085, plain, (ip(uri_rdf_object)=true)). % 36.62/23.77 tff(c_28, plain, (![P_9]: (ifeq(ip(P_9), true, iext(uri_rdf_type, P_9, uri_rdf_Property), true)=true))). % 36.62/23.77 tff(c_1055, plain, (ip(uri_rdf_type)=true)). % 36.62/23.77 tff(c_4, plain, (![P_4, S_5, O_6]: (ifeq(iext(P_4, S_5, O_6), true, ip(P_4), true)=true))). % 36.62/23.77 tff(c_782, plain, (ip(uri_rdf_subject)=true)). % 36.62/23.77 tff(c_164, plain, (![P_45, Q_46]: (ifeq(iext(uri_rdfs_subPropertyOf, P_45, Q_46), true, ip(P_45), true)=true))). % 36.62/23.77 tff(c_723, plain, (ic(uri_rdfs_Container)=true)). % 36.62/23.77 tff(c_699, plain, (ip(uri_rdf__2)=true)). % 36.62/23.77 tff(c_150, plain, (![C_35, D_36]: (ifeq(iext(uri_rdfs_subClassOf, C_35, D_36), true, ic(D_36), true)=true))). % 36.62/23.77 tff(c_650, plain, (ip(uri_rdf__1)=true)). % 36.62/23.77 tff(c_58, plain, (![C_15]: (ifeq(ic(C_15), true, iext(uri_rdfs_subClassOf, C_15, uri_rdfs_Resource), true)=true))). % 36.62/23.77 tff(c_619, plain, (ip(uri_rdf_first)=true)). % 36.62/23.77 tff(c_562, plain, (ip(uri_rdfs_seeAlso)=true)). % 36.62/23.77 tff(c_30, plain, (![P_10]: (ifeq(iext(uri_rdf_type, P_10, uri_rdf_Property), true, ip(P_10), true)=true))). % 36.62/23.77 tff(c_162, plain, (![P_43, Q_44]: (ifeq(iext(uri_rdfs_subPropertyOf, P_43, Q_44), true, ip(Q_44), true)=true))). % 36.62/23.77 tff(c_116, plain, (![X_23]: (ifeq(icext(uri_rdfs_Class, X_23), true, ic(X_23), true)=true))). % 36.62/23.77 tff(c_124, plain, (![X_27]: (ifeq(lv(X_27), true, icext(uri_rdfs_Literal, X_27), true)=true))). % 36.62/23.77 tff(c_122, plain, (![X_26]: (ifeq(icext(uri_rdfs_Literal, X_26), true, lv(X_26), true)=true))). % 36.62/23.77 tff(c_508, plain, (![X_62]: (icext(uri_rdfs_Resource, X_62)=true))). % 36.62/23.77 tff(c_114, plain, (![X_22]: (ifeq(ic(X_22), true, icext(uri_rdfs_Class, X_22), true)=true))). % 36.62/23.77 tff(c_201, plain, (![X_8]: (ifeq(lv(X_8), true, true, true)=true))). % 36.62/23.77 tff(c_2, plain, (![A_1, B_2, C_3]: (ifeq(A_1, A_1, B_2, C_3)=B_2))). % 36.62/23.77 tff(c_188, plain, (iext(uri_rdf_first, sK2_testcase_premise_fullish_023_Unique_List_Components_BNODE_l, uri_ex_v)=true)). % 36.62/23.77 tff(c_46, plain, (iext(uri_rdfs_domain, uri_rdfs_label, uri_rdfs_Resource)=true)). % 36.62/23.77 tff(c_154, plain, (iext(uri_rdfs_range, uri_rdfs_subClassOf, uri_rdfs_Class)=true)). % 36.62/23.77 tff(c_192, plain, (iext(uri_rdf_type, uri_rdf_first, uri_owl_FunctionalProperty)=true)). % 36.62/23.77 tff(c_64, plain, (iext(uri_rdfs_domain, uri_rdf_rest, uri_rdf_List)=true)). % 36.62/23.77 tff(c_10, plain, (iext(uri_rdf_type, uri_rdf_first, uri_rdf_Property)=true)). % 36.62/23.77 tff(c_18, plain, (iext(uri_rdf_type, uri_rdf__2, uri_rdf_Property)=true)). % 36.62/23.77 tff(c_160, plain, (iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, uri_rdf_Property)=true)). % 36.62/23.77 tff(c_102, plain, (iext(uri_rdf_type, uri_rdf_XMLLiteral, uri_rdfs_Datatype)=true)). % 36.62/23.77 tff(c_20, plain, (iext(uri_rdf_type, uri_rdf__3, uri_rdf_Property)=true)). % 36.62/23.77 tff(c_108, plain, (iext(uri_rdfs_domain, uri_rdfs_domain, uri_rdf_Property)=true)). % 36.62/23.77 tff(c_98, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Seq, uri_rdfs_Container)=true)). % 36.62/23.77 tff(c_186, plain, (iext(uri_rdf_first, sK2_testcase_premise_fullish_023_Unique_List_Components_BNODE_l, uri_ex_u)=true)). % 36.62/23.77 tff(c_12, plain, (iext(uri_rdf_type, uri_rdf_nil, uri_rdf_List)=true)). % 36.62/23.77 tff(c_128, plain, (iext(uri_rdfs_domain, uri_rdfs_range, uri_rdf_Property)=true)). % 36.62/23.77 tff(c_180, plain, (iext(uri_rdfs_range, uri_rdf_value, uri_rdfs_Resource)=true)). % 36.62/23.77 tff(c_34, plain, (iext(uri_rdf_type, uri_rdf_type, uri_rdf_Property)=true)). % 36.62/23.77 tff(c_174, plain, (iext(uri_rdfs_domain, uri_rdf_type, uri_rdfs_Resource)=true)). % 36.62/23.77 tff(c_52, plain, (iext(uri_rdfs_range, uri_rdfs_seeAlso, uri_rdfs_Resource)=true)). % 36.62/23.77 tff(c_100, plain, (iext(uri_rdfs_subClassOf, uri_rdf_XMLLiteral, uri_rdfs_Literal)=true)). % 36.62/23.77 tff(c_60, plain, (iext(uri_rdfs_domain, uri_rdf_first, uri_rdf_List)=true)). % 36.62/23.77 tff(c_176, plain, (iext(uri_rdfs_range, uri_rdf_type, uri_rdfs_Class)=true)). % 36.62/23.77 tff(c_84, plain, (iext(uri_rdfs_domain, uri_rdf__3, uri_rdfs_Resource)=true)). % 36.62/23.77 tff(c_76, plain, (iext(uri_rdfs_domain, uri_rdfs_member, uri_rdfs_Resource)=true)). % 36.62/23.77 tff(c_94, plain, (iext(uri_rdf_type, uri_rdf__2, uri_rdfs_ContainerMembershipProperty)=true)). % 36.62/23.77 tff(c_48, plain, (iext(uri_rdfs_range, uri_rdfs_label, uri_rdfs_Literal)=true)). % 36.62/23.77 tff(c_92, plain, (iext(uri_rdf_type, uri_rdf__1, uri_rdfs_ContainerMembershipProperty)=true)). % 36.62/23.77 tff(c_82, plain, (iext(uri_rdfs_domain, uri_rdf__2, uri_rdfs_Resource)=true)). % 36.62/23.77 tff(c_142, plain, (iext(uri_rdfs_domain, uri_rdf_subject, uri_rdfs_Statement)=true)). % 36.62/23.77 tff(c_126, plain, (iext(uri_rdf_type, uri_rdf_Property, uri_rdfs_Class)=true)). % 36.62/23.77 tff(c_26, plain, (iext(uri_rdf_type, uri_rdf_subject, uri_rdf_Property)=true)). % 36.62/23.77 tff(c_50, plain, (iext(uri_rdfs_domain, uri_rdfs_seeAlso, uri_rdfs_Resource)=true)). % 36.62/23.77 tff(c_146, plain, (iext(uri_rdfs_domain, uri_rdfs_subClassOf, uri_rdfs_Class)=true)). % 36.62/23.77 tff(c_184, plain, (iext(uri_rdf_rest, sK2_testcase_premise_fullish_023_Unique_List_Components_BNODE_l, uri_rdf_nil)=true)). % 36.62/23.77 tff(c_88, plain, (iext(uri_rdfs_range, uri_rdf__2, uri_rdfs_Resource)=true)). % 36.62/23.77 tff(c_90, plain, (iext(uri_rdfs_range, uri_rdf__3, uri_rdfs_Resource)=true)). % 36.62/23.77 tff(c_70, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Bag, uri_rdfs_Container)=true)). % 36.62/23.77 tff(c_42, plain, (iext(uri_rdfs_range, uri_rdfs_isDefinedBy, uri_rdfs_Resource)=true)). % 36.62/23.77 tff(c_80, plain, (iext(uri_rdfs_domain, uri_rdf__1, uri_rdfs_Resource)=true)). % 36.62/23.77 tff(c_190, plain, (iext(uri_rdf_type, sK1_testcase_premise_fullish_023_Unique_List_Components_BNODE_o, uri_owl_Class)=true)). % 36.62/23.77 tff(c_22, plain, (iext(uri_rdf_type, uri_rdf_object, uri_rdf_Property)=true)). % 36.62/23.77 tff(c_38, plain, (iext(uri_rdfs_range, uri_rdfs_comment, uri_rdfs_Literal)=true)). % 36.62/23.77 tff(c_40, plain, (iext(uri_rdfs_domain, uri_rdfs_isDefinedBy, uri_rdfs_Resource)=true)). % 36.62/23.77 tff(c_44, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_isDefinedBy, uri_rdfs_seeAlso)=true)). % 36.62/23.77 tff(c_86, plain, (iext(uri_rdfs_range, uri_rdf__1, uri_rdfs_Resource)=true)). % 36.62/23.77 tff(c_96, plain, (iext(uri_rdf_type, uri_rdf__3, uri_rdfs_ContainerMembershipProperty)=true)). % 36.62/23.77 tff(c_74, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, uri_rdf_Property)=true)). % 36.62/23.77 tff(c_36, plain, (iext(uri_rdfs_domain, uri_rdfs_comment, uri_rdfs_Resource)=true)). % 36.62/23.77 tff(c_78, plain, (iext(uri_rdfs_range, uri_rdfs_member, uri_rdfs_Resource)=true)). % 36.62/23.77 tff(c_178, plain, (iext(uri_rdfs_domain, uri_rdf_value, uri_rdfs_Resource)=true)). % 36.62/23.77 tff(c_138, plain, (iext(uri_rdfs_domain, uri_rdf_predicate, uri_rdfs_Statement)=true)). % 36.62/23.77 tff(c_62, plain, (iext(uri_rdfs_range, uri_rdf_first, uri_rdfs_Resource)=true)). % 36.62/23.77 tff(c_140, plain, (iext(uri_rdfs_range, uri_rdf_predicate, uri_rdfs_Resource)=true)). % 36.62/23.77 tff(c_144, plain, (iext(uri_rdfs_range, uri_rdf_subject, uri_rdfs_Resource)=true)). % 36.62/23.77 tff(c_16, plain, (iext(uri_rdf_type, uri_rdf__1, uri_rdf_Property)=true)). % 36.62/23.77 tff(c_14, plain, (iext(uri_rdf_type, uri_rdf_rest, uri_rdf_Property)=true)). % 36.62/23.77 tff(c_134, plain, (iext(uri_rdfs_domain, uri_rdf_object, uri_rdfs_Statement)=true)). % 36.62/23.77 tff(c_24, plain, (iext(uri_rdf_type, uri_rdf_value, uri_rdf_Property)=true)). % 36.62/23.77 tff(c_112, plain, (iext(uri_rdfs_range, uri_rdfs_domain, uri_rdfs_Class)=true)). % 36.62/23.77 tff(c_106, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, uri_rdfs_Class)=true)). % 36.62/23.77 tff(c_168, plain, (iext(uri_rdfs_range, uri_rdfs_subPropertyOf, uri_rdf_Property)=true)). % 36.62/23.77 tff(c_66, plain, (iext(uri_rdfs_range, uri_rdf_rest, uri_rdf_List)=true)). % 36.62/23.77 tff(c_68, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Alt, uri_rdfs_Container)=true)). % 36.62/23.77 tff(c_132, plain, (iext(uri_rdfs_range, uri_rdfs_range, uri_rdfs_Class)=true)). % 36.62/23.77 tff(c_182, plain, (iext(uri_owl_oneOf, sK1_testcase_premise_fullish_023_Unique_List_Components_BNODE_o, sK2_testcase_premise_fullish_023_Unique_List_Components_BNODE_l)=true)). % 36.62/23.77 tff(c_194, plain, (iext(uri_rdf_type, uri_ex_w, sK1_testcase_premise_fullish_023_Unique_List_Components_BNODE_o)=true)). % 36.62/23.77 tff(c_6, plain, (![X_7]: (ir(X_7)=true))). % 36.62/23.77 % SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 36.62/23.77 %------------------------------------------------------------------------------