%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : SWB014-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 : n028.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:50 PM UTC 2025 % Result : Satisfiable 33.55s 21.57s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.10/0.12 % Problem : SWB014-10 : TPTP v9.0.0. Released v7.5.0. % 0.10/0.13 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % 0.12/0.33 % Computer : n028.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 300 % 0.12/0.33 % DateTime : Wed Apr 9 00:56:49 EDT 2025 % 0.12/0.33 % CPUTime : % 33.55/21.56 % 33.55/21.57 % SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 33.55/21.57 % 33.55/21.57 % SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 33.68/21.59 %$ 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_unionOf > uri_ex_harry > uri_ex_Species > uri_ex_Falcon > uri_ex_Eagle > true > sK3_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_l1 > sK2_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_u > sK1_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_l2 % 33.68/21.59 % 33.68/21.59 %Foreground sorts: % 33.68/21.59 % 33.68/21.59 % 33.68/21.59 %Background operators: % 33.68/21.59 % 33.68/21.59 % 33.68/21.59 %Foreground operators: % 33.68/21.59 tff(uri_rdfs_Datatype, type, uri_rdfs_Datatype: $i). % 33.68/21.59 tff(uri_ex_harry, type, uri_ex_harry: $i). % 33.68/21.59 tff(uri_rdfs_ContainerMembershipProperty, type, uri_rdfs_ContainerMembershipProperty: $i). % 33.68/21.59 tff(uri_rdfs_Resource, type, uri_rdfs_Resource: $i). % 33.68/21.59 tff(uri_rdf_Property, type, uri_rdf_Property: $i). % 33.68/21.59 tff(uri_rdf_subject, type, uri_rdf_subject: $i). % 33.68/21.59 tff(uri_ex_Falcon, type, uri_ex_Falcon: $i). % 33.68/21.59 tff(uri_rdf_type, type, uri_rdf_type: $i). % 33.68/21.59 tff(uri_rdfs_subPropertyOf, type, uri_rdfs_subPropertyOf: $i). % 33.68/21.59 tff(uri_rdfs_seeAlso, type, uri_rdfs_seeAlso: $i). % 33.68/21.59 tff(icext, type, icext: ($i * $i) > $i). % 33.68/21.59 tff(uri_rdfs_range, type, uri_rdfs_range: $i). % 33.68/21.59 tff(uri_rdf_XMLLiteral, type, uri_rdf_XMLLiteral: $i). % 33.68/21.59 tff(uri_rdf_List, type, uri_rdf_List: $i). % 33.68/21.59 tff(uri_rdf_first, type, uri_rdf_first: $i). % 33.68/21.59 tff(uri_rdf_predicate, type, uri_rdf_predicate: $i). % 33.68/21.59 tff(tuple, type, tuple: ($i * $i) > $i). % 33.68/21.59 tff(ir, type, ir: $i > $i). % 33.68/21.59 tff(lv, type, lv: $i > $i). % 33.68/21.59 tff(uri_rdf__3, type, uri_rdf__3: $i). % 33.68/21.59 tff(uri_ex_Eagle, type, uri_ex_Eagle: $i). % 33.68/21.59 tff(sK3_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_l1, type, sK3_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_l1: $i). % 33.68/21.59 tff(uri_rdf_value, type, uri_rdf_value: $i). % 33.68/21.59 tff(sK1_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_l2, type, sK1_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_l2: $i). % 33.68/21.59 tff(ic, type, ic: $i > $i). % 33.68/21.59 tff(uri_rdfs_Statement, type, uri_rdfs_Statement: $i). % 33.68/21.59 tff(uri_rdf__1, type, uri_rdf__1: $i). % 33.68/21.59 tff(sK2_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_u, type, sK2_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_u: $i). % 33.68/21.59 tff(iext, type, iext: ($i * $i * $i) > $i). % 33.68/21.59 tff(uri_owl_unionOf, type, uri_owl_unionOf: $i). % 33.68/21.59 tff(uri_rdf_rest, type, uri_rdf_rest: $i). % 33.68/21.59 tff(uri_rdfs_label, type, uri_rdfs_label: $i). % 33.68/21.59 tff(uri_ex_Species, type, uri_ex_Species: $i). % 33.68/21.59 tff(uri_rdfs_Container, type, uri_rdfs_Container: $i). % 33.68/21.59 tff(uri_rdfs_subClassOf, type, uri_rdfs_subClassOf: $i). % 33.68/21.59 tff(uri_rdf_object, type, uri_rdf_object: $i). % 33.68/21.59 tff(ip, type, ip: $i > $i). % 33.68/21.59 tff(uri_rdfs_Class, type, uri_rdfs_Class: $i). % 33.68/21.59 tff(uri_rdfs_Seq, type, uri_rdfs_Seq: $i). % 33.68/21.59 tff(uri_rdfs_member, type, uri_rdfs_member: $i). % 33.68/21.59 tff(uri_rdf_Bag, type, uri_rdf_Bag: $i). % 33.68/21.59 tff(uri_rdf__2, type, uri_rdf__2: $i). % 33.68/21.59 tff(uri_rdfs_comment, type, uri_rdfs_comment: $i). % 33.68/21.59 tff(uri_rdfs_Literal, type, uri_rdfs_Literal: $i). % 33.68/21.59 tff(true, type, true: $i). % 33.68/21.59 tff(uri_rdf_Alt, type, uri_rdf_Alt: $i). % 33.68/21.59 tff(uri_rdf_nil, type, uri_rdf_nil: $i). % 33.68/21.59 tff(uri_rdfs_isDefinedBy, type, uri_rdfs_isDefinedBy: $i). % 33.68/21.59 tff(uri_rdfs_domain, type, uri_rdfs_domain: $i). % 33.68/21.59 tff(ifeq, type, ifeq: ($i * $i * $i * $i) > $i). % 33.68/21.59 % 33.68/21.59 %Saturated clause set: % 33.68/21.59 tff(c_13140, 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))). % 33.68/21.59 tff(c_13143, 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))). % 33.68/21.59 tff(c_13304, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, uri_rdfs_Resource, uri_rdfs_Class), true, true, true), true)=true))). % 33.68/21.59 tff(c_15558, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subPropertyOf), true, ifeq(iext(P_47, uri_rdf_predicate, uri_rdf_predicate), true, true, true), true)=true))). % 33.68/21.59 tff(c_69259, plain, (![X_1227, Y_1228]: (ifeq(iext(uri_rdfs_label, X_1227, Y_1228), true, iext(uri_rdfs_label, X_1227, Y_1228), true)=true))). % 33.68/21.59 tff(c_16087, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subPropertyOf), true, ifeq(iext(P_47, uri_rdfs_label, uri_rdfs_label), true, true, true), true)=true))). % 33.68/21.59 tff(c_16690, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subPropertyOf), true, ifeq(iext(P_47, uri_rdfs_comment, uri_rdfs_comment), true, true, true), true)=true))). % 33.68/21.59 tff(c_69001, plain, (![X_1221, Y_1222]: (ifeq(iext(uri_rdf_predicate, X_1221, Y_1222), true, iext(uri_rdf_predicate, X_1221, Y_1222), true)=true))). % 33.68/21.59 tff(c_68972, plain, (![X_1217, Y_1218]: (ifeq(iext(uri_rdfs_comment, X_1217, Y_1218), true, iext(uri_rdfs_comment, X_1217, Y_1218), true)=true))). % 33.68/21.59 tff(c_12921, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subClassOf), true, ifeq(iext(P_47, uri_rdfs_Resource, uri_rdfs_Resource), true, true, true), true)=true))). % 33.68/21.59 tff(c_68825, plain, (![X_1212, Y_1213]: (ifeq(iext(uri_rdfs_member, X_1212, Y_1213), true, iext(uri_rdfs_member, X_1212, Y_1213), true)=true))). % 33.68/21.59 tff(c_5047, 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))). % 33.68/21.59 tff(c_5044, 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))). % 33.68/21.59 tff(c_13086, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, uri_rdfs_member, uri_rdf_Property), true, true, true), true)=true))). % 33.68/21.59 tff(c_12994, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subPropertyOf), true, ifeq(iext(P_47, uri_rdfs_member, uri_rdfs_member), true, true, true), true)=true))). % 33.68/21.59 tff(c_15290, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subClassOf), true, ifeq(iext(P_47, uri_rdfs_Statement, uri_rdfs_Statement), true, true, true), true)=true))). % 33.68/21.59 tff(c_67931, plain, (![C_1203]: (ifeq(iext(uri_rdfs_subClassOf, C_1203, uri_rdfs_Statement), true, iext(uri_rdfs_subClassOf, C_1203, uri_rdfs_Resource), true)=true))). % 33.68/21.60 tff(c_15360, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subClassOf), true, ifeq(iext(P_47, uri_rdfs_Statement, uri_rdfs_Resource), true, true, true), true)=true))). % 33.68/21.60 tff(c_67655, plain, (![C_1200]: (ifeq(iext(uri_rdfs_subClassOf, C_1200, uri_rdf_List), true, iext(uri_rdfs_subClassOf, C_1200, uri_rdfs_Resource), true)=true))). % 33.68/21.60 tff(c_12233, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subClassOf), true, ifeq(iext(P_47, uri_rdf_List, uri_rdfs_Resource), true, true, true), true)=true))). % 33.68/21.60 tff(c_12299, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subClassOf), true, ifeq(iext(P_47, sK2_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_u, uri_rdfs_Resource), true, true, true), true)=true))). % 33.68/21.60 tff(c_12658, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subClassOf), true, ifeq(iext(P_47, uri_ex_Species, uri_rdfs_Resource), true, true, true), true)=true))). % 33.68/21.60 tff(c_12138, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subClassOf), true, ifeq(iext(P_47, uri_rdf_List, uri_rdf_List), true, true, true), true)=true))). % 33.68/21.60 tff(c_12825, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subClassOf), true, ifeq(iext(P_47, sK2_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_u, sK2_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_u), true, true, true), true)=true))). % 33.68/21.60 tff(c_66909, plain, (![C_1193]: (ifeq(iext(uri_rdfs_subClassOf, C_1193, uri_ex_Species), true, iext(uri_rdfs_subClassOf, C_1193, uri_rdfs_Resource), true)=true))). % 33.68/21.60 tff(c_66754, plain, (![C_1191]: (ifeq(iext(uri_rdfs_subClassOf, C_1191, sK2_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_u), true, iext(uri_rdfs_subClassOf, C_1191, uri_rdfs_Resource), true)=true))). % 33.68/21.60 tff(c_12592, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subClassOf), true, ifeq(iext(P_47, uri_ex_Species, uri_ex_Species), true, true, true), true)=true))). % 33.68/21.60 tff(c_10873, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdf_Property), true, ifeq(iext(P_18, uri_rdfs_domain, Y_21), true, true, true), true)=true))). % 33.68/21.60 tff(c_6663, 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))). % 33.68/21.60 tff(c_11924, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, uri_rdfs_ContainerMembershipProperty, uri_rdfs_Class), true, true, true), true)=true))). % 33.68/21.60 tff(c_11682, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, uri_rdfs_Datatype, uri_rdfs_Class), true, true, true), true)=true))). % 33.74/21.60 tff(c_11604, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, uri_rdfs_Class, uri_rdfs_Class), true, true, true), true)=true))). % 33.74/21.60 tff(c_8599, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdf_Property), true, ifeq(iext(P_18, uri_rdfs_subPropertyOf, Y_21), true, true, true), true)=true))). % 33.74/21.60 tff(c_10138, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdf_Property), true, ifeq(iext(P_28, X_30, uri_rdfs_isDefinedBy), true, true, true), true)=true))). % 33.74/21.60 tff(c_12043, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, uri_rdf_Bag, uri_rdfs_Class), true, true, true), true)=true))). % 33.74/21.60 tff(c_11801, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, uri_rdf_Alt, uri_rdfs_Class), true, true, true), true)=true))). % 33.74/21.60 tff(c_9353, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdf_Property), true, ifeq(iext(P_28, X_30, uri_owl_unionOf), true, true, true), true)=true))). % 33.74/21.60 tff(c_9350, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdf_Property), true, ifeq(iext(P_18, uri_owl_unionOf, Y_21), true, true, true), true)=true))). % 33.74/21.60 tff(c_10876, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdf_Property), true, ifeq(iext(P_28, X_30, uri_rdfs_domain), true, true, true), true)=true))). % 33.74/21.60 tff(c_11971, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, uri_rdfs_Seq, uri_rdfs_Class), true, true, true), true)=true))). % 33.74/21.60 tff(c_8807, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdf_Property), true, ifeq(iext(P_28, X_30, uri_rdfs_subClassOf), true, true, true), true)=true))). % 33.74/21.60 tff(c_6660, 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))). % 33.74/21.60 tff(c_11850, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, uri_rdf_XMLLiteral, uri_rdfs_Class), true, true, true), true)=true))). % 33.74/21.60 tff(c_11729, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, uri_rdfs_Container, uri_rdfs_Class), true, true, true), true)=true))). % 33.74/21.60 tff(c_8602, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdf_Property), true, ifeq(iext(P_28, X_30, uri_rdfs_subPropertyOf), true, true, true), true)=true))). % 33.74/21.60 tff(c_12091, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, uri_rdfs_Literal, uri_rdfs_Class), true, true, true), true)=true))). % 33.74/21.60 tff(c_8804, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdf_Property), true, ifeq(iext(P_18, uri_rdfs_subClassOf, Y_21), true, true, true), true)=true))). % 33.74/21.60 tff(c_10135, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdf_Property), true, ifeq(iext(P_18, uri_rdfs_isDefinedBy, Y_21), true, true, true), true)=true))). % 33.74/21.60 tff(c_11343, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, uri_rdf_List, uri_rdfs_Class), true, true, true), true)=true))). % 33.74/21.60 tff(c_11485, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, sK2_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_u, uri_rdfs_Class), true, true, true), true)=true))). % 33.74/21.60 tff(c_15163, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, uri_rdf_predicate, uri_rdf_Property), true, true, true), true)=true))). % 33.74/21.60 tff(c_14942, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, uri_rdfs_Statement, uri_rdfs_Class), true, true, true), true)=true))). % 33.74/21.60 tff(c_11438, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, sK3_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_l1, uri_rdf_List), true, true, true), true)=true))). % 33.74/21.60 tff(c_11557, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, uri_ex_Species, uri_rdfs_Class), true, true, true), true)=true))). % 33.74/21.60 tff(c_15960, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, uri_rdfs_label, uri_rdf_Property), true, true, true), true)=true))). % 33.74/21.60 tff(c_16564, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, uri_rdfs_comment, uri_rdf_Property), true, true, true), true)=true))). % 33.74/21.60 tff(c_11391, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, sK1_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_l2, uri_rdf_List), true, true, true), true)=true))). % 33.74/21.60 tff(c_4275, 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))). % 33.74/21.60 tff(c_4278, 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))). % 33.74/21.60 tff(c_4231, 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))). % 33.74/21.60 tff(c_4329, 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))). % 33.74/21.60 tff(c_6783, 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))). % 33.74/21.60 tff(c_62290, plain, (![X_1135, Y_1136]: (ifeq(iext(uri_rdf__1, X_1135, Y_1136), true, iext(uri_rdfs_member, X_1135, Y_1136), true)=true))). % 33.74/21.60 tff(c_9234, 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))). % 33.74/21.60 tff(c_4228, 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))). % 33.74/21.60 tff(c_4525, 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))). % 33.74/21.60 tff(c_4570, 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))). % 33.74/21.60 tff(c_61637, plain, (![C_1126]: (ifeq(iext(uri_rdfs_subClassOf, C_1126, uri_rdfs_Datatype), true, iext(uri_rdfs_subClassOf, C_1126, uri_rdfs_Resource), true)=true))). % 33.74/21.60 tff(c_10728, 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))). % 33.74/21.61 tff(c_8387, 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))). % 33.74/21.61 tff(c_61341, plain, (![X_1119, Y_1120]: (ifeq(iext(uri_rdf__3, X_1119, Y_1120), true, iext(uri_rdfs_member, X_1119, Y_1120), true)=true))). % 33.74/21.61 tff(c_61308, plain, (![P_1118]: (ifeq(iext(uri_rdfs_subPropertyOf, P_1118, uri_rdf__3), true, iext(uri_rdfs_subPropertyOf, P_1118, uri_rdfs_member), true)=true))). % 33.74/21.61 tff(c_7576, 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))). % 33.74/21.61 tff(c_4427, 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))). % 33.74/21.61 tff(c_4567, 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))). % 33.74/21.61 tff(c_4372, 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))). % 33.74/21.61 tff(c_4617, 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))). % 33.74/21.61 tff(c_4522, 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))). % 33.74/21.61 tff(c_60367, plain, (![C_1105]: (ifeq(iext(uri_rdfs_subClassOf, C_1105, uri_rdfs_Class), true, iext(uri_rdfs_subClassOf, C_1105, uri_rdfs_Resource), true)=true))). % 33.74/21.61 tff(c_9498, 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))). % 33.74/21.61 tff(c_60220, plain, (![X_1100, Y_1101]: (ifeq(iext(uri_rdfs_isDefinedBy, X_1100, Y_1101), true, iext(uri_rdfs_isDefinedBy, X_1100, Y_1101), true)=true))). % 33.74/21.61 tff(c_8521, 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))). % 33.74/21.61 tff(c_11046, 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))). % 33.74/21.61 tff(c_9296, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, uri_owl_unionOf, uri_rdf_Property), true, true, true), true)=true))). % 33.74/21.61 tff(c_59807, plain, (![X_1093, Y_1094]: (ifeq(iext(uri_rdf_first, X_1093, Y_1094), true, iext(uri_rdf_first, X_1093, Y_1094), true)=true))). % 33.74/21.61 tff(c_59780, plain, (![X_1089, Y_1090]: (ifeq(iext(uri_rdf__2, X_1089, Y_1090), true, iext(uri_rdf__2, X_1089, Y_1090), true)=true))). % 33.74/21.61 tff(c_10556, 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))). % 33.74/21.61 tff(c_6404, 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))). % 33.74/21.61 tff(c_9897, 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))). % 33.74/21.61 tff(c_11109, 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))). % 33.74/21.61 tff(c_59146, plain, (![C_1083]: (ifeq(iext(uri_rdfs_subClassOf, C_1083, uri_rdf_Bag), true, iext(uri_rdfs_subClassOf, C_1083, uri_rdfs_Resource), true)=true))). % 33.74/21.61 tff(c_4332, 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))). % 33.74/21.61 tff(c_5980, 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))). % 33.74/21.61 tff(c_7411, 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))). % 33.74/21.61 tff(c_58592, plain, (![C_1077]: (ifeq(iext(uri_rdfs_subClassOf, C_1077, uri_rdfs_Container), true, iext(uri_rdfs_subClassOf, C_1077, uri_rdfs_Resource), true)=true))). % 33.74/21.61 tff(c_6603, 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))). % 33.74/21.61 tff(c_7480, 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))). % 33.74/21.61 tff(c_58333, plain, (![X_1071, Y_1072]: (ifeq(iext(uri_rdf_object, X_1071, Y_1072), true, iext(uri_rdf_object, X_1071, Y_1072), true)=true))). % 33.74/21.61 tff(c_58178, plain, (![C_1069]: (ifeq(iext(uri_rdfs_subClassOf, C_1069, uri_rdfs_ContainerMembershipProperty), true, iext(uri_rdfs_subClassOf, C_1069, uri_rdfs_Resource), true)=true))). % 33.74/21.61 tff(c_6272, 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))). % 33.74/21.61 tff(c_9832, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subPropertyOf), true, ifeq(iext(P_47, uri_owl_unionOf, uri_owl_unionOf), true, true, true), true)=true))). % 33.74/21.61 tff(c_57888, plain, (![X_1063, Y_1064]: (ifeq(iext(uri_rdf_rest, X_1063, Y_1064), true, iext(uri_rdf_rest, X_1063, Y_1064), true)=true))). % 33.74/21.61 tff(c_5130, 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))). % 33.74/21.61 tff(c_5370, 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))). % 33.74/21.61 tff(c_4472, 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))). % 33.74/21.61 tff(c_57372, plain, (![P_1056]: (ifeq(iext(uri_rdfs_subPropertyOf, P_1056, uri_rdf__1), true, iext(uri_rdfs_subPropertyOf, P_1056, uri_rdfs_member), true)=true))). % 33.74/21.61 tff(c_57291, plain, (![C_1055]: (ifeq(iext(uri_rdfs_subClassOf, C_1055, uri_rdfs_Literal), true, iext(uri_rdfs_subClassOf, C_1055, uri_rdfs_Resource), true)=true))). % 33.74/21.61 tff(c_6342, 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))). % 33.74/21.61 tff(c_56636, plain, (![X_1050, Y_1051]: (ifeq(iext(uri_rdfs_subPropertyOf, X_1050, Y_1051), true, iext(uri_rdfs_subPropertyOf, X_1050, Y_1051), true)=true))). % 33.74/21.61 tff(c_8074, 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))). % 33.74/21.61 tff(c_7937, 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))). % 33.74/21.61 tff(c_4430, 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))). % 33.74/21.61 tff(c_7669, 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))). % 33.74/21.61 tff(c_55400, plain, (![X_1041, Y_1042]: (ifeq(iext(uri_rdf_type, X_1041, Y_1042), true, iext(uri_rdf_type, X_1041, Y_1042), true)=true))). % 33.74/21.61 tff(c_5594, 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))). % 33.74/21.61 tff(c_55252, plain, (![X_1036, Y_1037]: (ifeq(iext(uri_rdf_subject, X_1036, Y_1037), true, iext(uri_rdf_subject, X_1036, Y_1037), true)=true))). % 33.74/21.61 tff(c_10062, 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))). % 33.74/21.61 tff(c_8004, 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))). % 33.74/21.61 tff(c_54501, plain, (![C_1029]: (ifeq(iext(uri_rdfs_subClassOf, C_1029, uri_rdf_XMLLiteral), true, iext(uri_rdfs_subClassOf, C_1029, uri_rdfs_Resource), true)=true))). % 33.74/21.61 tff(c_54424, plain, (![C_1028]: (ifeq(iext(uri_rdfs_subClassOf, C_1028, uri_rdf_Alt), true, iext(uri_rdfs_subClassOf, C_1028, uri_rdfs_Resource), true)=true))). % 33.74/21.61 tff(c_11285, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, uri_rdfs_range, uri_rdf_Property), true, true, true), true)=true))). % 33.74/21.61 tff(c_9020, 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))). % 33.74/21.61 tff(c_5195, 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))). % 33.74/21.61 tff(c_4375, 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))). % 33.74/21.61 tff(c_53328, plain, (![X_1015, Y_1016]: (ifeq(iext(uri_rdf_value, X_1015, Y_1016), true, iext(uri_rdf_value, X_1015, Y_1016), true)=true))). % 33.74/21.61 tff(c_53301, plain, (![X_1011, Y_1012]: (ifeq(iext(uri_rdf__3, X_1011, Y_1012), true, iext(uri_rdf__3, X_1011, Y_1012), true)=true))). % 33.74/21.61 tff(c_7872, 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))). % 33.74/21.61 tff(c_10463, 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))). % 33.74/21.61 tff(c_7050, 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))). % 33.74/21.61 tff(c_5793, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subPropertyOf), true, ifeq(iext(P_47, uri_rdf_subject, uri_rdf_subject), true, true, true), true)=true))). % 33.74/21.62 tff(c_52798, plain, (![X_1003, Y_1004]: (ifeq(iext(uri_owl_unionOf, X_1003, Y_1004), true, iext(uri_owl_unionOf, X_1003, Y_1004), true)=true))). % 33.74/21.62 tff(c_7313, 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))). % 33.74/21.62 tff(c_6502, 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))). % 33.74/21.62 tff(c_52540, plain, (![X_997, Y_998]: (ifeq(iext(uri_rdf__2, X_997, Y_998), true, iext(uri_rdfs_member, X_997, Y_998), true)=true))). % 33.74/21.62 tff(c_4620, 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))). % 33.74/21.62 tff(c_10819, 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))). % 33.74/21.62 tff(c_51680, plain, (![X_988, Y_989]: (ifeq(iext(uri_rdfs_range, X_988, Y_989), true, iext(uri_rdfs_range, X_988, Y_989), true)=true))). % 33.74/21.62 tff(c_4475, 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))). % 33.74/21.62 tff(c_51061, plain, (![X_978, Y_979]: (ifeq(iext(uri_rdf__1, X_978, Y_979), true, iext(uri_rdf__1, X_978, Y_979), true)=true))). % 33.74/21.62 tff(c_50896, plain, (![X_976, Y_977]: (ifeq(iext(uri_rdfs_domain, X_976, Y_977), true, iext(uri_rdfs_domain, X_976, Y_977), true)=true))). % 33.74/21.62 tff(c_50869, plain, (![X_972, Y_973]: (ifeq(iext(uri_rdfs_seeAlso, X_972, Y_973), true, iext(uri_rdfs_seeAlso, X_972, Y_973), true)=true))). % 33.74/21.62 tff(c_50706, plain, (![C_970]: (ifeq(iext(uri_rdfs_subClassOf, C_970, uri_rdf_Property), true, iext(uri_rdfs_subClassOf, C_970, uri_rdfs_Resource), true)=true))). % 33.74/21.62 tff(c_50639, plain, (![P_968]: (ifeq(iext(uri_rdfs_subPropertyOf, P_968, uri_rdf__2), true, iext(uri_rdfs_subPropertyOf, P_968, uri_rdfs_member), true)=true))). % 33.74/21.62 tff(c_5489, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subPropertyOf), true, ifeq(iext(P_47, uri_rdf_first, uri_rdf_first), true, true, true), true)=true))). % 33.74/21.62 tff(c_4895, 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))). % 33.74/21.62 tff(c_49751, plain, (![X_962, Y_963]: (ifeq(iext(uri_rdfs_subClassOf, X_962, Y_963), true, iext(uri_rdfs_subClassOf, X_962, Y_963), true)=true))). % 33.74/21.62 tff(c_8226, 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))). % 33.74/21.62 tff(c_8722, 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))). % 33.74/21.62 tff(c_8164, 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))). % 33.74/21.62 tff(c_8937, 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))). % 33.74/21.62 tff(c_48426, plain, (![C_951]: (ifeq(iext(uri_rdfs_subClassOf, C_951, uri_rdfs_Seq), true, iext(uri_rdfs_subClassOf, C_951, uri_rdfs_Resource), true)=true))). % 33.74/21.62 tff(c_7734, 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))). % 33.74/21.62 tff(c_6044, 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))). % 33.74/21.62 tff(c_6147, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdf_List), true, ifeq(iext(P_28, X_30, sK1_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_l2), true, true, true), true)=true))). % 33.74/21.62 tff(c_6875, 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))). % 33.74/21.62 tff(c_14998, 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))). % 33.74/21.62 tff(c_14705, 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))). % 33.74/21.62 tff(c_7176, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdf_Property), true, ifeq(iext(P_28, X_30, uri_rdfs_range), true, true, true), true)=true))). % 33.74/21.62 tff(c_6144, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdf_List), true, ifeq(iext(P_18, sK1_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_l2, Y_21), true, true, true), true)=true))). % 33.74/21.62 tff(c_9087, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdf_List), true, ifeq(iext(P_28, X_30, sK3_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_l1), true, true, true), true)=true))). % 33.74/21.62 tff(c_15001, 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))). % 33.74/21.62 tff(c_15786, 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))). % 33.74/21.62 tff(c_6872, 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))). % 33.74/21.62 tff(c_7173, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdf_Property), true, ifeq(iext(P_18, uri_rdfs_range, Y_21), true, true, true), true)=true))). % 33.74/21.62 tff(c_10182, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdfs_Class), true, ifeq(iext(P_18, sK2_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_u, Y_21), true, true, true), true)=true))). % 33.74/21.62 tff(c_15789, 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))). % 33.74/21.62 tff(c_4830, plain, (![P_47, X_141]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, X_141, uri_rdfs_Resource), true, true, true), true)=true))). % 33.74/21.62 tff(c_10185, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdfs_Class), true, ifeq(iext(P_28, X_30, sK2_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_u), true, true, true), true)=true))). % 33.74/21.62 tff(c_14708, 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))). % 33.74/21.62 tff(c_16394, 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))). % 33.74/21.62 tff(c_9649, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdfs_Class), true, ifeq(iext(P_18, uri_ex_Species, Y_21), true, true, true), true)=true))). % 33.74/21.62 tff(c_9652, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdfs_Class), true, ifeq(iext(P_28, X_30, uri_ex_Species), true, true, true), true)=true))). % 33.74/21.62 tff(c_16391, 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))). % 33.74/21.62 tff(c_9084, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdf_List), true, ifeq(iext(P_18, sK3_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_l1, Y_21), true, true, true), true)=true))). % 33.74/21.62 tff(c_3625, 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))). % 33.74/21.62 tff(c_3904, 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))). % 33.74/21.62 tff(c_3665, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, sK2_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_u), true, ifeq(iext(P_28, X_30, uri_ex_harry), true, true, true), true)=true))). % 33.74/21.62 tff(c_3708, 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))). % 33.74/21.62 tff(c_3941, 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))). % 33.74/21.62 tff(c_3787, 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))). % 33.74/21.62 tff(c_4141, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_ex_Species), true, ifeq(iext(P_18, uri_ex_Falcon, Y_21), true, true, true), true)=true))). % 33.74/21.62 tff(c_4100, 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))). % 33.74/21.62 tff(c_3662, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, sK2_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_u), true, ifeq(iext(P_18, uri_ex_harry, Y_21), true, true, true), true)=true))). % 33.74/21.62 tff(c_4024, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_ex_Species), true, ifeq(iext(P_28, X_30, uri_ex_Eagle), true, true, true), true)=true))). % 33.74/21.62 tff(c_3790, 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))). % 33.74/21.62 tff(c_3472, 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))). % 33.74/21.62 tff(c_3705, 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))). % 33.74/21.62 tff(c_3985, 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))). % 33.74/21.62 tff(c_3576, 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))). % 33.74/21.62 tff(c_3541, 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))). % 33.74/21.62 tff(c_3748, 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))). % 33.74/21.62 tff(c_3982, 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))). % 33.74/21.62 tff(c_4144, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_ex_Species), true, ifeq(iext(P_28, X_30, uri_ex_Falcon), true, true, true), true)=true))). % 33.74/21.62 tff(c_3475, 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))). % 33.87/21.62 tff(c_4061, 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))). % 33.87/21.62 tff(c_3944, 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))). % 33.87/21.62 tff(c_4181, 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))). % 33.87/21.62 tff(c_3544, 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))). % 33.87/21.62 tff(c_3868, 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))). % 33.87/21.63 tff(c_4184, 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))). % 33.87/21.63 tff(c_4097, 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))). % 33.87/21.63 tff(c_3907, 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))). % 33.87/21.63 tff(c_3826, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdf_Property), true, ifeq(iext(P_18, uri_rdf_first, Y_21), true, true, true), true)=true))). % 33.87/21.63 tff(c_3829, 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))). % 33.87/21.63 tff(c_3579, 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))). % 33.87/21.63 tff(c_4058, 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))). % 33.87/21.63 tff(c_3865, 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))). % 33.87/21.63 tff(c_3628, 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))). % 33.87/21.63 tff(c_3751, 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))). % 33.87/21.63 tff(c_4021, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_ex_Species), true, ifeq(iext(P_18, uri_ex_Eagle, Y_21), true, true, true), true)=true))). % 33.87/21.63 tff(c_1709, plain, (![P_94, X_96, X_63]: (ifeq(iext(uri_rdfs_range, P_94, uri_rdfs_Resource), true, ifeq(iext(P_94, X_96, X_63), true, true, true), true)=true))). % 33.87/21.63 tff(c_2089, plain, (![P_98, X_63, Y_101]: (ifeq(iext(uri_rdfs_domain, P_98, uri_rdfs_Resource), true, ifeq(iext(P_98, X_63, Y_101), true, true, true), true)=true))). % 33.87/21.63 tff(c_2734, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdfs_subClassOf), true, ifeq(iext(P_108, uri_rdfs_Seq, uri_rdfs_Container), true, true, true), true)=true))). % 33.87/21.63 tff(c_2809, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdfs_domain), true, ifeq(iext(P_108, uri_rdf__2, uri_rdfs_Resource), true, true, true), true)=true))). % 33.87/21.63 tff(c_2947, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdfs_range), true, ifeq(iext(P_108, uri_rdfs_comment, uri_rdfs_Literal), true, true, true), true)=true))). % 33.87/21.63 tff(c_38773, plain, (![C_823]: (ifeq(iext(uri_rdfs_subClassOf, C_823, uri_rdfs_ContainerMembershipProperty), true, iext(uri_rdfs_subClassOf, C_823, uri_rdf_Property), true)=true))). % 33.87/21.63 tff(c_2965, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdfs_subClassOf), true, ifeq(iext(P_108, uri_rdf_Alt, uri_rdfs_Container), true, true, true), true)=true))). % 33.87/21.63 tff(c_2668, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdfs_domain), true, ifeq(iext(P_108, uri_rdfs_seeAlso, uri_rdfs_Resource), true, true, true), true)=true))). % 33.87/21.63 tff(c_2839, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdfs_domain), true, ifeq(iext(P_108, uri_rdf__1, uri_rdfs_Resource), true, true, true), true)=true))). % 33.87/21.63 tff(c_38343, plain, (![C_818]: (ifeq(iext(uri_rdfs_subClassOf, C_818, uri_rdf_Alt), true, iext(uri_rdfs_subClassOf, C_818, uri_rdfs_Container), true)=true))). % 33.87/21.63 tff(c_2788, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdfs_domain), true, ifeq(iext(P_108, uri_rdfs_comment, uri_rdfs_Resource), true, true, true), true)=true))). % 33.87/21.63 tff(c_2803, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdfs_subPropertyOf), true, ifeq(iext(P_108, uri_rdfs_isDefinedBy, uri_rdfs_seeAlso), true, true, true), true)=true))). % 33.87/21.63 tff(c_2674, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdf_type), true, ifeq(iext(P_108, uri_rdf__1, uri_rdf_Property), true, true, true), true)=true))). % 33.87/21.63 tff(c_2752, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdf_type), true, ifeq(iext(P_108, uri_rdf__3, uri_rdf_Property), true, true, true), true)=true))). % 33.87/21.63 tff(c_2911, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdf_type), true, ifeq(iext(P_108, uri_ex_Falcon, uri_ex_Species), true, true, true), true)=true))). % 33.87/21.63 tff(c_2821, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdfs_range), true, ifeq(iext(P_108, uri_rdf__2, uri_rdfs_Resource), true, true, true), true)=true))). % 33.87/21.63 tff(c_2941, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdf_type), true, ifeq(iext(P_108, uri_rdf_rest, uri_rdf_Property), true, true, true), true)=true))). % 33.87/21.63 tff(c_2851, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdfs_domain), true, ifeq(iext(P_108, uri_rdfs_isDefinedBy, uri_rdfs_Resource), true, true, true), true)=true))). % 33.87/21.63 tff(c_2710, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdfs_domain), true, ifeq(iext(P_108, uri_rdfs_subPropertyOf, uri_rdf_Property), true, true, true), true)=true))). % 33.87/21.63 tff(c_37209, plain, (![C_807]: (ifeq(iext(uri_rdfs_subClassOf, C_807, uri_rdfs_Seq), true, iext(uri_rdfs_subClassOf, C_807, uri_rdfs_Container), true)=true))). % 33.87/21.63 tff(c_2770, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdf_type), true, ifeq(iext(P_108, uri_rdf__2, uri_rdfs_ContainerMembershipProperty), true, true, true), true)=true))). % 33.87/21.63 tff(c_3001, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdf_rest), true, ifeq(iext(P_108, sK1_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_l2, uri_rdf_nil), true, true, true), true)=true))). % 33.87/21.63 tff(c_2833, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdf_type), true, ifeq(iext(P_108, uri_rdf_subject, uri_rdf_Property), true, true, true), true)=true))). % 33.87/21.63 tff(c_2722, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_owl_unionOf), true, ifeq(iext(P_108, sK2_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_u, sK3_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_l1), true, true, true), true)=true))). % 33.87/21.63 tff(c_2650, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdf_type), true, ifeq(iext(P_108, uri_rdf_nil, uri_rdf_List), true, true, true), true)=true))). % 33.87/21.63 tff(c_2608, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdfs_range), true, ifeq(iext(P_108, uri_rdfs_seeAlso, uri_rdfs_Resource), true, true, true), true)=true))). % 33.87/21.63 tff(c_2764, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdfs_domain), true, ifeq(iext(P_108, uri_rdfs_range, uri_rdf_Property), true, true, true), true)=true))). % 33.87/21.63 tff(c_2983, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdfs_subClassOf), true, ifeq(iext(P_108, uri_rdf_Bag, uri_rdfs_Container), true, true, true), true)=true))). % 33.87/21.63 tff(c_2656, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdfs_subClassOf), true, ifeq(iext(P_108, uri_rdf_XMLLiteral, uri_rdfs_Literal), true, true, true), true)=true))). % 33.87/21.63 tff(c_2638, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdfs_domain), true, ifeq(iext(P_108, uri_rdf_value, uri_rdfs_Resource), true, true, true), true)=true))). % 33.87/21.63 tff(c_2989, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdfs_domain), true, ifeq(iext(P_108, uri_rdf_object, uri_rdfs_Statement), true, true, true), true)=true))). % 33.87/21.63 tff(c_2899, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdf_first), true, ifeq(iext(P_108, sK3_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_l1, uri_ex_Eagle), true, true, true), true)=true))). % 33.87/21.63 tff(c_2893, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdfs_subClassOf), true, ifeq(iext(P_108, uri_rdfs_ContainerMembershipProperty, uri_rdf_Property), true, true, true), true)=true))). % 33.87/21.63 tff(c_2923, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdfs_domain), true, ifeq(iext(P_108, uri_rdf_subject, uri_rdfs_Statement), true, true, true), true)=true))). % 33.87/21.63 tff(c_2632, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdfs_range), true, ifeq(iext(P_108, uri_rdfs_subClassOf, uri_rdfs_Class), true, true, true), true)=true))). % 33.87/21.63 tff(c_2692, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdfs_domain), true, ifeq(iext(P_108, uri_rdf_rest, uri_rdf_List), true, true, true), true)=true))). % 33.87/21.63 tff(c_2881, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdfs_domain), true, ifeq(iext(P_108, uri_rdf__3, uri_rdfs_Resource), true, true, true), true)=true))). % 33.87/21.63 tff(c_2959, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdf_type), true, ifeq(iext(P_108, uri_rdf_type, uri_rdf_Property), true, true, true), true)=true))). % 33.87/21.63 tff(c_2863, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdfs_domain), true, ifeq(iext(P_108, uri_rdfs_label, uri_rdfs_Resource), true, true, true), true)=true))). % 33.87/21.63 tff(c_2776, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdfs_domain), true, ifeq(iext(P_108, uri_rdf_type, uri_rdfs_Resource), true, true, true), true)=true))). % 33.87/21.63 tff(c_2626, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdf_type), true, ifeq(iext(P_108, uri_rdf_first, uri_rdf_Property), true, true, true), true)=true))). % 33.87/21.63 tff(c_2971, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdfs_subClassOf), true, ifeq(iext(P_108, uri_rdfs_Datatype, uri_rdfs_Class), true, true, true), true)=true))). % 33.87/21.63 tff(c_2995, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdfs_range), true, ifeq(iext(P_108, uri_rdfs_subPropertyOf, uri_rdf_Property), true, true, true), true)=true))). % 33.87/21.63 tff(c_34448, plain, (![P_782]: (ifeq(iext(uri_rdfs_subPropertyOf, P_782, uri_rdfs_isDefinedBy), true, iext(uri_rdfs_subPropertyOf, P_782, uri_rdfs_seeAlso), true)=true))). % 33.87/21.63 tff(c_2644, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdf_type), true, ifeq(iext(P_108, uri_rdf__2, uri_rdf_Property), true, true, true), true)=true))). % 33.87/21.63 tff(c_2875, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdfs_domain), true, ifeq(iext(P_108, uri_rdfs_member, uri_rdfs_Resource), true, true, true), true)=true))). % 33.87/21.63 tff(c_3007, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdf_type), true, ifeq(iext(P_108, uri_ex_harry, sK2_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_u), true, true, true), true)=true))). % 33.87/21.63 tff(c_2953, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdfs_domain), true, ifeq(iext(P_108, uri_rdf_predicate, uri_rdfs_Statement), true, true, true), true)=true))). % 33.87/21.63 tff(c_33913, plain, (![D_776]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_776), true, icext(D_776, uri_rdfs_member), true)=true))). % 33.87/21.63 tff(c_33731, plain, (![D_773]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_773), true, icext(D_773, uri_rdfs_Resource), true)=true))). % 33.87/21.63 tff(c_2662, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdf_type), true, ifeq(iext(P_108, uri_rdf_object, uri_rdf_Property), true, true, true), true)=true))). % 33.87/21.63 tff(c_33665, plain, (![D_771]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_771), true, icext(D_771, uri_rdfs_domain), true)=true))). % 33.87/21.63 tff(c_33599, plain, (![D_769]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_769), true, icext(D_769, uri_rdfs_subPropertyOf), true)=true))). % 33.87/21.63 tff(c_33414, plain, (![D_766]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_766), true, icext(D_766, uri_owl_unionOf), true)=true))). % 33.87/21.63 tff(c_2905, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdfs_domain), true, ifeq(iext(P_108, uri_rdfs_domain, uri_rdf_Property), true, true, true), true)=true))). % 33.87/21.63 tff(c_33348, plain, (![D_764]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_764), true, icext(D_764, uri_rdfs_isDefinedBy), true)=true))). % 33.87/21.63 tff(c_33282, plain, (![D_762]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_762), true, icext(D_762, uri_rdfs_seeAlso), true)=true))). % 33.87/21.63 tff(c_33092, plain, (![D_759]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_759), true, icext(D_759, uri_rdfs_subClassOf), true)=true))). % 33.87/21.63 tff(c_2887, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdfs_range), true, ifeq(iext(P_108, uri_rdf_value, uri_rdfs_Resource), true, true, true), true)=true))). % 33.87/21.63 tff(c_33023, plain, (![D_757]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_757), true, icext(D_757, uri_rdf_Alt), true)=true))). % 33.87/21.63 tff(c_2929, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdfs_domain), true, ifeq(iext(P_108, uri_rdfs_subClassOf, uri_rdfs_Class), true, true, true), true)=true))). % 33.87/21.63 tff(c_32834, plain, (![D_754]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_754), true, icext(D_754, uri_rdfs_Datatype), true)=true))). % 33.87/21.63 tff(c_32740, plain, (![D_752]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_752), true, icext(D_752, uri_rdfs_Class), true)=true))). % 33.87/21.63 tff(c_2686, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdf_type), true, ifeq(iext(P_108, uri_rdf__3, uri_rdfs_ContainerMembershipProperty), true, true, true), true)=true))). % 33.87/21.63 tff(c_32559, plain, (![D_749]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_749), true, icext(D_749, uri_rdfs_Literal), true)=true))). % 33.87/21.63 tff(c_32484, plain, (![D_747]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_747), true, icext(D_747, uri_rdf_XMLLiteral), true)=true))). % 33.87/21.63 tff(c_32416, plain, (![C_745]: (ifeq(iext(uri_rdfs_subClassOf, C_745, uri_rdf_Bag), true, iext(uri_rdfs_subClassOf, C_745, uri_rdfs_Container), true)=true))). % 33.87/21.63 tff(c_32350, plain, (![D_743]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_743), true, icext(D_743, uri_rdf_Bag), true)=true))). % 33.87/21.63 tff(c_32284, plain, (![D_741]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_741), true, icext(D_741, uri_rdfs_ContainerMembershipProperty), true)=true))). % 33.87/21.63 tff(c_32218, plain, (![D_739]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_739), true, icext(D_739, uri_rdfs_Container), true)=true))). % 33.87/21.63 tff(c_2680, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdf_first), true, ifeq(iext(P_108, sK1_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_l2, uri_ex_Falcon), true, true, true), true)=true))). % 33.87/21.63 tff(c_32037, plain, (![D_736]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_736), true, icext(D_736, uri_rdfs_Seq), true)=true))). % 33.87/21.63 tff(c_31971, plain, (![D_734]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_List, D_734), true, icext(D_734, sK3_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_l1), true)=true))). % 33.87/21.63 tff(c_31905, plain, (![D_732]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_732), true, icext(D_732, sK2_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_u), true)=true))). % 33.87/21.63 tff(c_2614, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdf_rest), true, ifeq(iext(P_108, sK3_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_l1, sK1_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_l2), true, true, true), true)=true))). % 33.87/21.63 tff(c_31723, plain, (![D_729]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_729), true, icext(D_729, uri_rdfs_comment), true)=true))). % 33.87/21.63 tff(c_31657, plain, (![D_727]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_727), true, icext(D_727, uri_rdf_predicate), true)=true))). % 33.87/21.63 tff(c_31476, plain, (![D_724]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_List, D_724), true, icext(D_724, sK1_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_l2), true)=true))). % 33.87/21.63 tff(c_2857, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdf_type), true, ifeq(iext(P_108, uri_rdf_value, uri_rdf_Property), true, true, true), true)=true))). % 33.87/21.63 tff(c_31410, plain, (![D_722]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_722), true, icext(D_722, uri_rdf_List), true)=true))). % 33.87/21.63 tff(c_31344, plain, (![D_720]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_720), true, icext(D_720, uri_rdfs_Statement), true)=true))). % 33.87/21.63 tff(c_31163, plain, (![D_717]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_717), true, icext(D_717, uri_rdfs_range), true)=true))). % 33.87/21.63 tff(c_2698, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdfs_domain), true, ifeq(iext(P_108, uri_rdf_first, uri_rdf_List), true, true, true), true)=true))). % 33.87/21.63 tff(c_31097, plain, (![D_715]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_715), true, icext(D_715, uri_ex_Species), true)=true))). % 33.87/21.63 tff(c_31031, plain, (![D_713]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_713), true, icext(D_713, uri_rdfs_label), true)=true))). % 33.87/21.64 tff(c_2620, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdf_type), true, ifeq(iext(P_108, uri_ex_Eagle, uri_ex_Species), true, true, true), true)=true))). % 33.87/21.64 tff(c_30849, plain, (![D_710]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_List, D_710), true, icext(D_710, uri_rdf_nil), true)=true))). % 33.87/21.64 tff(c_13323, 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))). % 33.87/21.64 tff(c_16118, 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))). % 33.87/21.64 tff(c_16721, 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))). % 33.87/21.64 tff(c_15589, 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))). % 33.87/21.64 tff(c_2794, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdfs_range), true, ifeq(iext(P_108, uri_rdfs_domain, uri_rdfs_Class), true, true, true), true)=true))). % 33.87/21.64 tff(c_13028, 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))). % 33.87/21.64 tff(c_13111, 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))). % 33.87/21.64 tff(c_30500, plain, (![D_698]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_698), true, icext(D_698, uri_rdf__3), true)=true))). % 33.87/21.64 tff(c_12958, 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))). % 33.87/21.64 tff(c_2869, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdfs_range), true, ifeq(iext(P_108, uri_rdfs_label, uri_rdfs_Literal), true, true, true), true)=true))). % 33.87/21.64 tff(c_12626, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_48), true, iext(Q_48, uri_ex_Species, uri_ex_Species), true)=true))). % 33.87/21.64 tff(c_12692, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_48), true, iext(Q_48, uri_ex_Species, uri_rdfs_Resource), true)=true))). % 33.87/21.64 tff(c_15396, 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))). % 33.87/21.64 tff(c_12859, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_48), true, iext(Q_48, sK2_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_u, sK2_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_u), true)=true))). % 33.87/21.64 tff(c_12334, plain, (![E_41]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Resource, E_41), true, iext(uri_rdfs_subClassOf, sK2_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_u, E_41), true)=true))). % 33.87/21.64 tff(c_15395, 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))). % 33.87/21.64 tff(c_12268, 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))). % 33.87/21.64 tff(c_2704, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdfs_range), true, ifeq(iext(P_108, uri_rdfs_range, uri_rdfs_Class), true, true, true), true)=true))). % 33.87/21.64 tff(c_12333, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_48), true, iext(Q_48, sK2_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_u, uri_rdfs_Resource), true)=true))). % 33.87/21.64 tff(c_12172, 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))). % 33.87/21.64 tff(c_12267, 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))). % 33.87/21.64 tff(c_12693, plain, (![E_41]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Resource, E_41), true, iext(uri_rdfs_subClassOf, uri_ex_Species, E_41), true)=true))). % 33.87/21.64 tff(c_15325, 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))). % 33.87/21.64 tff(c_2728, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdf_type), true, ifeq(iext(P_108, uri_rdf_XMLLiteral, uri_rdfs_Datatype), true, true, true), true)=true))). % 33.87/21.64 tff(c_11623, 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))). % 33.87/21.64 tff(c_11820, 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))). % 33.87/21.64 tff(c_11701, 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))). % 33.87/21.64 tff(c_11943, 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))). % 33.87/21.64 tff(c_11748, 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))). % 33.87/21.64 tff(c_12062, 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))). % 33.87/21.64 tff(c_11990, 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))). % 33.87/21.64 tff(c_12110, 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))). % 33.87/21.64 tff(c_2917, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdfs_range), true, ifeq(iext(P_108, uri_rdfs_member, uri_rdfs_Resource), true, true, true), true)=true))). % 33.87/21.64 tff(c_11869, 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))). % 33.87/21.64 tff(c_16589, 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))). % 33.87/21.64 tff(c_15188, 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))). % 33.87/21.64 tff(c_29367, plain, (![D_662]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, D_662), true, icext(D_662, uri_rdf__1), true)=true))). % 33.87/21.64 tff(c_11576, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, uri_ex_Species, uri_rdfs_Class), true)=true))). % 33.87/21.64 tff(c_11410, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, sK1_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_l2, uri_rdf_List), true)=true))). % 33.87/21.64 tff(c_14961, 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))). % 33.87/21.64 tff(c_2935, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdfs_range), true, ifeq(iext(P_108, uri_rdf_rest, uri_rdf_List), true, true, true), true)=true))). % 33.87/21.64 tff(c_15985, 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))). % 33.87/21.64 tff(c_11504, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, sK2_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_u, uri_rdfs_Class), true)=true))). % 33.87/21.64 tff(c_11457, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, sK3_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_l1, uri_rdf_List), true)=true))). % 33.87/21.64 tff(c_11362, 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))). % 33.87/21.64 tff(c_7971, 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))). % 33.87/21.64 tff(c_7446, 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))). % 33.87/21.64 tff(c_9321, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, uri_owl_unionOf, uri_rdf_Property), true)=true))). % 33.87/21.64 tff(c_2740, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdf_type), true, ifeq(iext(P_108, uri_rdf__1, uri_rdfs_ContainerMembershipProperty), true, true, true), true)=true))). % 33.87/21.64 tff(c_10087, 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))). % 33.87/21.64 tff(c_9533, 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))). % 33.87/21.64 tff(c_28816, plain, (![D_644]: (ifeq(iext(uri_rdfs_subClassOf, uri_ex_Species, D_644), true, icext(D_644, uri_ex_Falcon), true)=true))). % 33.87/21.64 tff(c_9532, 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))). % 33.87/21.64 tff(c_8747, 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))). % 33.87/21.64 tff(c_2845, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdfs_range), true, ifeq(iext(P_108, uri_rdf_subject, uri_rdfs_Resource), true, true, true), true)=true))). % 33.87/21.64 tff(c_5824, 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))). % 33.87/21.64 tff(c_7081, 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))). % 33.87/21.64 tff(c_8546, 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))). % 33.87/21.64 tff(c_9265, 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))). % 33.87/21.64 tff(c_10760, 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))). % 33.87/21.64 tff(c_7445, 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))). % 33.87/21.64 tff(c_2758, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdfs_range), true, ifeq(iext(P_108, uri_rdfs_isDefinedBy, uri_rdfs_Resource), true, true, true), true)=true))). % 33.87/21.64 tff(c_6077, 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))). % 33.87/21.64 tff(c_9863, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_48), true, iext(Q_48, uri_owl_unionOf, uri_owl_unionOf), true)=true))). % 33.87/21.64 tff(c_5404, 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))). % 33.87/21.64 tff(c_28204, plain, (![D_626]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_626), true, icext(D_626, uri_rdf__2), true)=true))). % 33.87/21.64 tff(c_28154, plain, (![X_621, Y_622]: (ifeq(iext(uri_rdfs_isDefinedBy, X_621, Y_622), true, iext(uri_rdfs_seeAlso, X_621, Y_622), true)=true))). % 33.87/21.64 tff(c_7511, 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))). % 33.87/21.64 tff(c_10494, 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))). % 33.87/21.64 tff(c_28019, plain, (![D_616]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, D_616), true, icext(D_616, uri_rdf__2), true)=true))). % 33.87/21.64 tff(c_8260, 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))). % 33.87/21.64 tff(c_2827, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdfs_range), true, ifeq(iext(P_108, uri_rdf__3, uri_rdfs_Resource), true, true, true), true)=true))). % 33.87/21.64 tff(c_10590, 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))). % 33.87/21.64 tff(c_8195, 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))). % 33.87/21.64 tff(c_6373, 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))). % 33.87/21.64 tff(c_6820, 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))). % 33.87/21.64 tff(c_6536, 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))). % 33.87/21.64 tff(c_7607, 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))). % 33.87/21.64 tff(c_2815, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdf_type), true, ifeq(iext(P_108, uri_rdf_Property, uri_rdfs_Class), true, true, true), true)=true))). % 33.87/21.64 tff(c_11077, 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))). % 33.87/21.64 tff(c_5520, 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))). % 33.87/21.64 tff(c_27411, plain, (![D_598]: (ifeq(iext(uri_rdfs_subClassOf, sK2_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_u, D_598), true, icext(D_598, uri_ex_harry), true)=true))). % 33.87/21.64 tff(c_6628, 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))). % 33.87/21.64 tff(c_8261, 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))). % 33.87/21.64 tff(c_8105, 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))). % 33.87/21.64 tff(c_2782, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdfs_range), true, ifeq(iext(P_108, uri_rdf_first, uri_rdfs_Resource), true, true, true), true)=true))). % 33.87/21.64 tff(c_7347, 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))). % 33.87/21.64 tff(c_6303, 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))). % 33.87/21.64 tff(c_5163, 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))). % 33.87/21.64 tff(c_27131, plain, (![D_589]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_589), true, icext(D_589, uri_rdf_subject), true)=true))). % 33.87/21.64 tff(c_10759, 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))). % 33.87/21.64 tff(c_7700, 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))). % 33.87/21.64 tff(c_9054, 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))). % 33.87/21.64 tff(c_6438, 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))). % 33.87/21.64 tff(c_10844, 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))). % 33.87/21.64 tff(c_26883, plain, (![C_578]: (ifeq(iext(uri_rdfs_subClassOf, C_578, uri_rdf_XMLLiteral), true, iext(uri_rdfs_subClassOf, C_578, uri_rdfs_Literal), true)=true))). % 33.87/21.64 tff(c_4928, 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))). % 33.87/21.64 tff(c_8038, 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))). % 33.87/21.64 tff(c_26751, plain, (![D_573]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_573), true, icext(D_573, uri_rdf_object), true)=true))). % 33.87/21.64 tff(c_11143, 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))). % 33.87/21.64 tff(c_7903, 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))). % 33.87/21.64 tff(c_2977, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdfs_range), true, ifeq(iext(P_108, uri_rdf_predicate, uri_rdfs_Resource), true, true, true), true)=true))). % 33.87/21.64 tff(c_5225, 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))). % 33.87/21.64 tff(c_5403, 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))). % 33.87/21.64 tff(c_26426, plain, (![D_564]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, D_564), true, icext(D_564, uri_rdf__3), true)=true))). % 33.87/21.64 tff(c_4929, 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))). % 33.87/21.64 tff(c_8968, 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))). % 33.87/21.65 tff(c_5627, 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))). % 33.87/21.65 tff(c_11310, 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))). % 33.87/21.65 tff(c_7082, 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))). % 33.87/21.65 tff(c_6014, 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))). % 33.87/21.65 tff(c_2746, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdfs_range), true, ifeq(iext(P_108, uri_rdf__1, uri_rdfs_Resource), true, true, true), true)=true))). % 33.87/21.65 tff(c_9931, 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))). % 33.87/21.65 tff(c_8421, 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))). % 33.87/21.65 tff(c_5628, 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))). % 33.87/21.65 tff(c_25897, plain, (![D_547]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_547), true, icext(D_547, uri_rdf_type), true)=true))). % 33.87/21.65 tff(c_6078, 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))). % 33.87/21.65 tff(c_10591, 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))). % 33.87/21.65 tff(c_2716, plain, (![P_108]: (ifeq(iext(uri_rdfs_subPropertyOf, P_108, uri_rdfs_range), true, ifeq(iext(P_108, uri_rdf_type, uri_rdfs_Class), true, true, true), true)=true))). % 33.87/21.65 tff(c_9932, 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))). % 33.87/21.65 tff(c_7766, 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))). % 33.87/21.65 tff(c_7765, 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))). % 33.87/21.65 tff(c_8422, 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))). % 33.87/21.65 tff(c_4854, plain, (![Q_48, X_141]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, X_141, uri_rdfs_Resource), true)=true))). % 33.87/21.65 tff(c_25389, plain, (![C_534]: (ifeq(iext(uri_rdfs_subClassOf, C_534, uri_rdfs_Datatype), true, iext(uri_rdfs_subClassOf, C_534, uri_rdfs_Class), true)=true))). % 33.87/21.65 tff(c_3071, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_109), true, iext(Q_109, uri_rdf_Alt, uri_rdfs_Container), true)=true))). % 33.87/21.65 tff(c_3030, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_109), true, iext(Q_109, uri_rdf_type, uri_rdfs_Class), true)=true))). % 33.87/21.65 tff(c_3014, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_109), true, iext(Q_109, uri_ex_Eagle, uri_ex_Species), true)=true))). % 33.87/21.65 tff(c_25278, plain, (![D_529]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_529), true, icext(D_529, uri_rdf_first), true)=true))). % 33.87/21.65 tff(c_2581, plain, (![E_106]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Literal, E_106), true, iext(uri_rdfs_subClassOf, uri_rdf_XMLLiteral, E_106), true)=true))). % 33.87/21.65 tff(c_3052, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_109), true, iext(Q_109, uri_rdfs_isDefinedBy, uri_rdfs_Resource), true)=true))). % 33.87/21.65 tff(c_3033, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_109), true, iext(Q_109, uri_rdfs_Seq, uri_rdfs_Container), true)=true))). % 33.87/21.65 tff(c_3069, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_109), true, iext(Q_109, uri_rdf_predicate, uri_rdfs_Statement), true)=true))). % 33.87/21.65 tff(c_3050, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_109), true, iext(Q_109, uri_rdf__1, uri_rdfs_Resource), true)=true))). % 33.87/21.65 tff(c_3043, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_109), true, iext(Q_109, uri_rdfs_domain, uri_rdfs_Class), true)=true))). % 33.87/21.65 tff(c_3016, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_109), true, iext(Q_109, uri_rdfs_subClassOf, uri_rdfs_Class), true)=true))). % 33.87/21.65 tff(c_3031, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_owl_unionOf, Q_109), true, iext(Q_109, sK2_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_u, sK3_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_l1), true)=true))). % 33.87/21.65 tff(c_3019, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_109), true, iext(Q_109, uri_rdf_nil, uri_rdf_List), true)=true))). % 33.87/21.65 tff(c_3049, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_109), true, iext(Q_109, uri_rdf_subject, uri_rdf_Property), true)=true))). % 33.87/21.65 tff(c_3024, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_first, Q_109), true, iext(Q_109, sK1_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_l2, uri_ex_Falcon), true)=true))). % 33.87/21.65 tff(c_3073, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_109), true, iext(Q_109, uri_rdf_predicate, uri_rdfs_Resource), true)=true))). % 33.87/21.65 tff(c_3042, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_109), true, iext(Q_109, uri_rdfs_comment, uri_rdfs_Resource), true)=true))). % 33.87/21.65 tff(c_3078, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_109), true, iext(Q_109, uri_ex_harry, sK2_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_u), true)=true))). % 33.87/21.65 tff(c_2484, plain, (![R_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_seeAlso, R_103), true, iext(uri_rdfs_subPropertyOf, uri_rdfs_isDefinedBy, R_103), true)=true))). % 33.87/21.65 tff(c_3074, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_109), true, iext(Q_109, uri_rdf_Bag, uri_rdfs_Container), true)=true))). % 33.87/21.65 tff(c_24907, plain, (![D_511]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, D_511), true, icext(D_511, uri_rdf_XMLLiteral), true)=true))). % 33.87/21.65 tff(c_3077, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_rest, Q_109), true, iext(Q_109, sK1_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_l2, uri_rdf_nil), true)=true))). % 33.87/21.65 tff(c_3063, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_109), true, iext(Q_109, uri_rdfs_member, uri_rdfs_Resource), true)=true))). % 33.87/21.65 tff(c_3067, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_109), true, iext(Q_109, uri_rdf_rest, uri_rdf_Property), true)=true))). % 33.87/21.65 tff(c_3070, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_109), true, iext(Q_109, uri_rdf_type, uri_rdf_Property), true)=true))). % 33.87/21.65 tff(c_3055, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_109), true, iext(Q_109, uri_rdfs_label, uri_rdfs_Literal), true)=true))). % 33.87/21.65 tff(c_2584, plain, (![E_106]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Container, E_106), true, iext(uri_rdfs_subClassOf, uri_rdf_Alt, E_106), true)=true))). % 33.87/21.65 tff(c_3034, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_109), true, iext(Q_109, uri_rdf__1, uri_rdfs_ContainerMembershipProperty), true)=true))). % 33.87/21.65 tff(c_24705, plain, (![D_502]: (ifeq(iext(uri_rdfs_subClassOf, uri_ex_Species, D_502), true, icext(D_502, uri_ex_Eagle), true)=true))). % 33.87/21.65 tff(c_2583, plain, (![E_106]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, E_106), true, iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, E_106), true)=true))). % 33.87/21.65 tff(c_3065, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_109), true, iext(Q_109, uri_rdfs_subClassOf, uri_rdfs_Class), true)=true))). % 33.87/21.65 tff(c_3039, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_109), true, iext(Q_109, uri_rdf__2, uri_rdfs_ContainerMembershipProperty), true)=true))). % 33.87/21.65 tff(c_3054, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_109), true, iext(Q_109, uri_rdfs_label, uri_rdfs_Resource), true)=true))). % 33.87/21.65 tff(c_3061, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_109), true, iext(Q_109, uri_rdfs_domain, uri_rdf_Property), true)=true))). % 33.87/21.65 tff(c_3047, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_109), true, iext(Q_109, uri_rdf__2, uri_rdfs_Resource), true)=true))). % 33.87/21.65 tff(c_3046, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_109), true, iext(Q_109, uri_rdf_Property, uri_rdfs_Class), true)=true))). % 33.87/21.65 tff(c_24490, plain, (![D_493]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_493), true, icext(D_493, uri_rdf_Property), true)=true))). % 33.87/21.65 tff(c_2582, plain, (![E_106]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Container, E_106), true, iext(uri_rdfs_subClassOf, uri_rdfs_Seq, E_106), true)=true))). % 33.87/21.65 tff(c_3022, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_109), true, iext(Q_109, uri_rdfs_seeAlso, uri_rdfs_Resource), true)=true))). % 33.87/21.65 tff(c_3013, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_rest, Q_109), true, iext(Q_109, sK3_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_l1, sK1_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_l2), true)=true))). % 33.87/21.65 tff(c_3012, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_109), true, iext(Q_109, uri_rdfs_seeAlso, uri_rdfs_Resource), true)=true))). % 33.87/21.65 tff(c_3058, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_109), true, iext(Q_109, uri_rdf_value, uri_rdfs_Resource), true)=true))). % 33.87/21.65 tff(c_3053, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_109), true, iext(Q_109, uri_rdf_value, uri_rdf_Property), true)=true))). % 33.87/21.65 tff(c_3036, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_109), true, iext(Q_109, uri_rdf__3, uri_rdf_Property), true)=true))). % 33.87/21.65 tff(c_3051, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_109), true, iext(Q_109, uri_rdf_subject, uri_rdfs_Resource), true)=true))). % 33.87/21.65 tff(c_3064, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_109), true, iext(Q_109, uri_rdf_subject, uri_rdfs_Statement), true)=true))). % 33.87/21.65 tff(c_3018, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_109), true, iext(Q_109, uri_rdf__2, uri_rdf_Property), true)=true))). % 33.87/21.65 tff(c_3020, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_109), true, iext(Q_109, uri_rdf_XMLLiteral, uri_rdfs_Literal), true)=true))). % 33.87/21.65 tff(c_3023, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_109), true, iext(Q_109, uri_rdf__1, uri_rdf_Property), true)=true))). % 33.87/21.65 tff(c_3072, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_109), true, iext(Q_109, uri_rdfs_Datatype, uri_rdfs_Class), true)=true))). % 33.87/21.65 tff(c_3027, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_109), true, iext(Q_109, uri_rdf_first, uri_rdf_List), true)=true))). % 33.87/21.65 tff(c_3056, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_109), true, iext(Q_109, uri_rdfs_member, uri_rdfs_Resource), true)=true))). % 33.87/21.65 tff(c_3035, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_109), true, iext(Q_109, uri_rdf__1, uri_rdfs_Resource), true)=true))). % 33.87/21.65 tff(c_24117, plain, (![D_475]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_475), true, icext(D_475, uri_rdf_value), true)=true))). % 33.87/21.65 tff(c_3037, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_109), true, iext(Q_109, uri_rdfs_isDefinedBy, uri_rdfs_Resource), true)=true))). % 33.87/21.65 tff(c_3059, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_109), true, iext(Q_109, uri_rdfs_ContainerMembershipProperty, uri_rdf_Property), true)=true))). % 33.87/21.65 tff(c_3029, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_109), true, iext(Q_109, uri_rdfs_subPropertyOf, uri_rdf_Property), true)=true))). % 33.87/21.65 tff(c_16725, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_comment), true)=true))). % 33.87/21.65 tff(c_16724, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_comment), true)=true))). % 33.87/21.65 tff(c_15593, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_predicate), true)=true))). % 33.87/21.65 tff(c_16122, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_label), true)=true))). % 33.87/21.65 tff(c_16121, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_label), true)=true))). % 33.87/21.65 tff(c_15592, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_predicate), true)=true))). % 33.87/21.65 tff(c_2585, plain, (![E_106]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, E_106), true, iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, E_106), true)=true))). % 33.87/21.65 tff(c_12961, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdfs_Resource), true)=true))). % 33.87/21.65 tff(c_23781, plain, (![D_462]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_462), true, icext(D_462, uri_rdf_rest), true)=true))). % 33.87/21.65 tff(c_13031, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_member), true)=true))). % 33.87/21.65 tff(c_3040, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_109), true, iext(Q_109, uri_rdf_type, uri_rdfs_Resource), true)=true))). % 33.87/21.65 tff(c_12695, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_ex_Species), true)=true))). % 33.87/21.65 tff(c_15329, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdfs_Statement), true)=true))). % 33.87/21.65 tff(c_12863, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, sK2_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_u), true)=true))). % 33.87/21.65 tff(c_12630, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_ex_Species), true)=true))). % 33.87/21.65 tff(c_3015, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_109), true, iext(Q_109, uri_rdf_first, uri_rdf_Property), true)=true))). % 33.87/21.65 tff(c_12862, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, sK2_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_u), true)=true))). % 33.87/21.65 tff(c_12176, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdf_List), true)=true))). % 33.87/21.65 tff(c_12175, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdf_List), true)=true))). % 33.87/21.65 tff(c_15328, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdfs_Statement), true)=true))). % 33.87/21.65 tff(c_3028, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_109), true, iext(Q_109, uri_rdfs_range, uri_rdfs_Class), true)=true))). % 33.87/21.65 tff(c_23407, plain, (![D_448]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_448), true, icext(D_448, uri_rdf__1), true)=true))). % 33.87/21.65 tff(c_3060, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_first, Q_109), true, iext(Q_109, sK3_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_l1, uri_ex_Eagle), true)=true))). % 33.87/21.65 tff(c_3075, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_109), true, iext(Q_109, uri_rdf_object, uri_rdfs_Statement), true)=true))). % 33.87/21.65 tff(c_3048, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_109), true, iext(Q_109, uri_rdf__3, uri_rdfs_Resource), true)=true))). % 33.87/21.65 tff(c_23144, plain, (![C_91, X_63]: (ifeq(icext(C_91, X_63), true, true, true)=true))). % 33.87/21.65 tff(c_3041, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_109), true, iext(Q_109, uri_rdf_first, uri_rdfs_Resource), true)=true))). % 33.87/21.65 tff(c_8108, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_rest), true)=true))). % 33.87/21.65 tff(c_22662, plain, (![D_437, X_438]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Resource, D_437), true, icext(D_437, X_438), true)=true))). % 33.87/21.65 tff(c_7704, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_type), true)=true))). % 33.87/21.65 tff(c_11080, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_range), true)=true))). % 33.87/21.65 tff(c_3068, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_109), true, iext(Q_109, uri_rdfs_comment, uri_rdfs_Literal), true)=true))). % 33.87/21.65 tff(c_22509, plain, (![X_430, Y_431]: (ifeq(iext(uri_rdf_rest, X_430, Y_431), true, icext(uri_rdf_List, X_430), true)=true))). % 33.87/21.65 tff(c_7515, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf__1), true)=true))). % 33.87/21.65 tff(c_7975, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdfs_Seq), true)=true))). % 33.87/21.65 tff(c_3032, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_109), true, iext(Q_109, uri_rdf_XMLLiteral, uri_rdfs_Datatype), true)=true))). % 33.87/21.65 tff(c_7351, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdf_Alt), true)=true))). % 33.87/21.65 tff(c_8109, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_rest), true)=true))). % 33.87/21.65 tff(c_21992, plain, (![X_421, Y_422]: (ifeq(iext(uri_rdfs_subPropertyOf, X_421, Y_422), true, icext(uri_rdf_Property, X_421), true)=true))). % 33.87/21.65 tff(c_3021, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_109), true, iext(Q_109, uri_rdf_object, uri_rdf_Property), true)=true))). % 33.87/21.65 tff(c_8972, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_domain), true)=true))). % 33.87/21.65 tff(c_8198, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_subPropertyOf), true)=true))). % 33.87/21.65 tff(c_21839, plain, (![X_414, Y_415]: (ifeq(iext(uri_rdf_first, X_414, Y_415), true, icext(uri_rdf_List, X_414), true)=true))). % 33.87/21.65 tff(c_7906, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf__2), true)=true))). % 33.87/21.65 tff(c_3045, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_109), true, iext(Q_109, uri_rdf__2, uri_rdfs_Resource), true)=true))). % 33.87/21.66 tff(c_5629, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdfs_Literal), true)=true))). % 33.87/21.66 tff(c_21373, plain, (![X_407, Y_408]: (ifeq(iext(uri_rdfs_subPropertyOf, X_407, Y_408), true, icext(uri_rdf_Property, Y_408), true)=true))). % 33.87/21.66 tff(c_9269, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_isDefinedBy), true)=true))). % 33.87/21.66 tff(c_3044, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_109), true, iext(Q_109, uri_rdfs_isDefinedBy, uri_rdfs_seeAlso), true)=true))). % 33.87/21.66 tff(c_8263, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdf_Property), true)=true))). % 33.87/21.66 tff(c_20772, plain, (![X_400, Y_401]: (ifeq(iext(uri_rdf_type, X_400, Y_401), true, icext(uri_rdfs_Class, Y_401), true)=true))). % 33.87/21.66 tff(c_7768, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf__3), true)=true))). % 33.87/21.66 tff(c_9867, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_owl_unionOf), true)=true))). % 33.87/21.66 tff(c_6018, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdf_Bag), true)=true))). % 33.87/21.66 tff(c_3025, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_109), true, iext(Q_109, uri_rdf__3, uri_rdfs_ContainerMembershipProperty), true)=true))). % 33.87/21.66 tff(c_20643, plain, (![X_392, Y_393]: (ifeq(iext(uri_rdf_object, X_392, Y_393), true, icext(uri_rdfs_Statement, X_392), true)=true))). % 33.87/21.66 tff(c_6376, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_subClassOf), true)=true))). % 33.87/21.66 tff(c_8199, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_subPropertyOf), true)=true))). % 33.87/21.66 tff(c_3026, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_109), true, iext(Q_109, uri_rdf_rest, uri_rdf_List), true)=true))). % 33.87/21.66 tff(c_7611, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf__3), true)=true))). % 33.87/21.66 tff(c_20186, plain, (![X_384, Y_385]: (ifeq(iext(uri_rdfs_range, X_384, Y_385), true, icext(uri_rdfs_Class, Y_385), true)=true))). % 33.87/21.66 tff(c_7085, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_member), true)=true))). % 33.87/21.66 tff(c_3076, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_109), true, iext(Q_109, uri_rdfs_subPropertyOf, uri_rdf_Property), true)=true))). % 33.87/21.66 tff(c_7084, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf__1), true)=true))). % 33.87/21.66 tff(c_19725, plain, (![X_377, Y_378]: (ifeq(iext(uri_rdfs_domain, X_377, Y_378), true, icext(uri_rdf_Property, X_377), true)=true))). % 33.87/21.66 tff(c_6307, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_object), true)=true))). % 33.87/21.66 tff(c_8971, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_domain), true)=true))). % 33.87/21.66 tff(c_3066, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_109), true, iext(Q_109, uri_rdf_rest, uri_rdf_List), true)=true))). % 33.87/21.66 tff(c_7907, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf__2), true)=true))). % 33.87/21.66 tff(c_9866, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_owl_unionOf), true)=true))). % 33.87/21.66 tff(c_19272, plain, (![X_368, Y_369]: (ifeq(iext(uri_rdfs_domain, X_368, Y_369), true, icext(uri_rdfs_Class, Y_369), true)=true))). % 33.87/21.66 tff(c_5227, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_seeAlso), true)=true))). % 33.87/21.66 tff(c_5827, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_subject), true)=true))). % 33.87/21.66 tff(c_3038, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_109), true, iext(Q_109, uri_rdfs_range, uri_rdf_Property), true)=true))). % 33.87/21.66 tff(c_10498, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_value), true)=true))). % 33.87/21.66 tff(c_18466, plain, (![X_359, Y_360]: (ifeq(iext(uri_rdfs_subClassOf, X_359, Y_360), true, icext(uri_rdfs_Class, X_359), true)=true))). % 33.87/21.66 tff(c_5524, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_first), true)=true))). % 33.87/21.66 tff(c_3017, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_109), true, iext(Q_109, uri_rdf_value, uri_rdfs_Resource), true)=true))). % 33.87/21.66 tff(c_7703, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_type), true)=true))). % 33.87/21.66 tff(c_6377, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_subClassOf), true)=true))). % 33.87/21.66 tff(c_18332, plain, (![X_351, Y_352]: (ifeq(iext(uri_rdf_subject, X_351, Y_352), true, icext(uri_rdfs_Statement, X_351), true)=true))). % 33.87/21.66 tff(c_6540, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdfs_ContainerMembershipProperty), true)=true))). % 33.87/21.66 tff(c_2586, plain, (![E_106]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Container, E_106), true, iext(uri_rdfs_subClassOf, uri_rdf_Bag, E_106), true)=true))). % 33.87/21.66 tff(c_4930, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdfs_Container), true)=true))). % 33.87/21.66 tff(c_5166, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdfs_Datatype), true)=true))). % 33.87/21.66 tff(c_17891, plain, (![X_343, Y_344]: (ifeq(iext(uri_rdfs_range, X_343, Y_344), true, icext(uri_rdf_Property, X_343), true)=true))). % 33.87/21.66 tff(c_11081, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_range), true)=true))). % 33.87/21.66 tff(c_6080, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdfs_Resource), true)=true))). % 33.87/21.66 tff(c_5828, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_subject), true)=true))). % 33.87/21.66 tff(c_3062, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_109), true, iext(Q_109, uri_ex_Falcon, uri_ex_Species), true)=true))). % 33.87/21.66 tff(c_10497, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_value), true)=true))). % 33.87/21.66 tff(c_8042, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdf_XMLLiteral), true)=true))). % 33.87/21.66 tff(c_6306, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_object), true)=true))). % 33.87/21.66 tff(c_17690, plain, (![X_332, Y_333]: (ifeq(iext(uri_rdfs_comment, X_332, Y_333), true, icext(uri_rdfs_Literal, Y_333), true)=true))). % 33.87/21.66 tff(c_5523, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_first), true)=true))). % 33.87/21.66 tff(c_11146, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdfs_Class), true)=true))). % 33.87/21.66 tff(c_4855, plain, (![C_19, X_141]: (ifeq(iext(uri_rdfs_domain, uri_rdf_type, C_19), true, icext(C_19, X_141), true)=true))). % 33.87/21.66 tff(c_3057, plain, (![Q_109]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_109), true, iext(Q_109, uri_rdf__3, uri_rdfs_Resource), true)=true))). % 33.87/21.66 tff(c_4856, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_29), true, icext(C_29, uri_rdfs_Resource), true)=true))). % 33.87/21.66 tff(c_2375, plain, (![C_99]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_99), true, icext(C_99, uri_rdf__1), true)=true))). % 33.87/21.66 tff(c_17157, plain, (![X_316, Y_317]: (ifeq(iext(uri_rdf_rest, X_316, Y_317), true, icext(uri_rdf_List, Y_317), true)=true))). % 33.87/21.66 tff(c_1987, plain, (![C_95]: (ifeq(iext(uri_rdfs_range, uri_owl_unionOf, C_95), true, icext(C_95, sK3_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_l1), true)=true))). % 33.87/21.66 tff(c_2370, plain, (![C_99]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_99), true, icext(C_99, uri_rdf_type), true)=true))). % 33.87/21.66 tff(c_2005, plain, (![C_95]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_95), true, icext(C_95, uri_rdfs_Class), true)=true))). % 33.87/21.66 tff(c_1976, plain, (![C_95]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_95), true, icext(C_95, uri_rdfs_Literal), true)=true))). % 33.87/21.66 tff(c_2403, plain, (![C_99]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_99), true, icext(C_99, uri_rdfs_member), true)=true))). % 33.87/21.66 tff(c_2411, plain, (![C_99]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_99), true, icext(C_99, uri_rdfs_member), true)=true))). % 33.87/21.66 tff(c_2381, plain, (![C_99]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_99), true, icext(C_99, uri_rdf_type), true)=true))). % 33.87/21.66 tff(c_2409, plain, (![C_99]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_99), true, icext(C_99, uri_rdfs_domain), true)=true))). % 33.87/21.66 tff(c_2362, plain, (![C_99]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_99), true, icext(C_99, uri_rdfs_seeAlso), true)=true))). % 33.87/21.66 tff(c_2412, plain, (![C_99]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_99), true, icext(C_99, uri_rdf_subject), true)=true))). % 33.87/21.66 tff(c_2416, plain, (![C_99]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_99), true, icext(C_99, uri_rdfs_comment), true)=true))). % 33.87/21.66 tff(c_2422, plain, (![C_99]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_99), true, icext(C_99, uri_rdf_Bag), true)=true))). % 33.87/21.66 tff(c_16139, plain, (![X_286, Y_287]: (ifeq(iext(uri_rdfs_label, X_286, Y_287), true, icext(uri_rdfs_Literal, Y_287), true)=true))). % 33.87/21.66 tff(c_2350, plain, (![C_99]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_99), true, icext(C_99, uri_rdfs_seeAlso), true)=true))). % 33.87/21.66 tff(c_2386, plain, (![C_99]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_99), true, icext(C_99, uri_rdfs_isDefinedBy), true)=true))). % 33.87/21.66 tff(c_2022, plain, (![C_95]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_95), true, icext(C_95, uri_rdf_Property), true)=true))). % 33.87/21.66 tff(c_16670, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_comment, uri_rdfs_comment)=true)). % 33.87/21.66 tff(c_16629, plain, (ip(uri_rdfs_comment)=true)). % 33.87/21.66 tff(c_2391, plain, (![C_99]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_99), true, icext(C_99, uri_rdf__3), true)=true))). % 33.87/21.66 tff(c_16547, plain, (iext(uri_rdf_type, uri_rdfs_comment, uri_rdf_Property)=true)). % 33.87/21.66 tff(c_16365, plain, (icext(uri_rdf_Property, uri_rdfs_comment)=true)). % 33.87/21.66 tff(c_2384, plain, (![C_99]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_99), true, icext(C_99, uri_rdfs_comment), true)=true))). % 33.87/21.66 tff(c_2414, plain, (![C_99]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_99), true, icext(C_99, uri_rdf_rest), true)=true))). % 33.87/21.66 tff(c_2395, plain, (![C_99]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_99), true, icext(C_99, uri_rdf_subject), true)=true))). % 33.87/21.66 tff(c_1980, plain, (![C_95]: (ifeq(iext(uri_rdfs_range, uri_rdf_first, C_95), true, icext(C_95, uri_ex_Falcon), true)=true))). % 33.87/21.66 tff(c_2364, plain, (![C_99]: (ifeq(iext(uri_rdfs_domain, uri_rdf_first, C_99), true, icext(C_99, sK1_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_l2), true)=true))). % 33.87/21.66 tff(c_2407, plain, (![C_99]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_99), true, icext(C_99, uri_rdfs_ContainerMembershipProperty), true)=true))). % 33.87/21.66 tff(c_2423, plain, (![C_99]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_99), true, icext(C_99, uri_rdf_object), true)=true))). % 33.87/21.66 tff(c_2382, plain, (![C_99]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_99), true, icext(C_99, uri_rdf_first), true)=true))). % 33.87/21.66 tff(c_16067, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_label, uri_rdfs_label)=true)). % 33.87/21.66 tff(c_2400, plain, (![C_99]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_99), true, icext(C_99, uri_rdfs_label), true)=true))). % 33.87/21.66 tff(c_16000, plain, (ip(uri_rdfs_label)=true)). % 33.87/21.66 tff(c_15943, plain, (iext(uri_rdf_type, uri_rdfs_label, uri_rdf_Property)=true)). % 33.87/21.66 tff(c_15760, plain, (icext(uri_rdf_Property, uri_rdfs_label)=true)). % 33.87/21.66 tff(c_2401, plain, (![C_99]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_99), true, icext(C_99, uri_rdfs_label), true)=true))). % 33.87/21.66 tff(c_2413, plain, (![C_99]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_99), true, icext(C_99, uri_rdfs_subClassOf), true)=true))). % 33.87/21.66 tff(c_2417, plain, (![C_99]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_99), true, icext(C_99, uri_rdf_predicate), true)=true))). % 33.87/21.66 tff(c_2041, plain, (![C_95]: (ifeq(iext(uri_rdfs_range, uri_rdfs_range, C_95), true, icext(C_95, uri_rdf_Property), true)=true))). % 33.87/21.66 tff(c_2030, plain, (![C_95]: (ifeq(iext(uri_rdfs_range, uri_rdfs_range, C_95), true, icext(C_95, uri_rdf_List), true)=true))). % 33.87/21.66 tff(c_2397, plain, (![C_99]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_99), true, icext(C_99, uri_rdfs_isDefinedBy), true)=true))). % 33.87/21.66 tff(c_15330, plain, (![X_33]: (ifeq(icext(uri_rdfs_Statement, X_33), true, icext(uri_rdfs_Statement, X_33), true)=true))). % 33.87/21.66 tff(c_15538, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_predicate, uri_rdf_predicate)=true)). % 33.87/21.66 tff(c_15340, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Statement, uri_rdfs_Resource)=true)). % 33.87/21.66 tff(c_15270, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Statement, uri_rdfs_Statement)=true)). % 33.87/21.66 tff(c_15228, plain, (ip(uri_rdf_predicate)=true)). % 33.87/21.66 tff(c_15146, plain, (iext(uri_rdf_type, uri_rdf_predicate, uri_rdf_Property)=true)). % 33.87/21.66 tff(c_14972, plain, (icext(uri_rdf_Property, uri_rdf_predicate)=true)). % 33.87/21.66 tff(c_14905, plain, (iext(uri_rdf_type, uri_rdfs_Statement, uri_rdfs_Class)=true)). % 33.87/21.66 tff(c_2421, plain, (![C_99]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_99), true, icext(C_99, uri_rdf_predicate), true)=true))). % 33.87/21.66 tff(c_14746, plain, (ic(uri_rdfs_Statement)=true)). % 33.87/21.66 tff(c_14676, plain, (icext(uri_rdfs_Class, uri_rdfs_Statement)=true)). % 33.87/21.66 tff(c_2033, plain, (![C_95]: (ifeq(iext(uri_rdfs_range, uri_rdfs_domain, C_95), true, icext(C_95, uri_rdfs_Statement), true)=true))). % 33.87/21.66 tff(c_2424, plain, (![C_99]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_99), true, icext(C_99, uri_rdfs_subPropertyOf), true)=true))). % 33.87/21.66 tff(c_13992, plain, (![X_261, Y_262]: (ifeq(iext(uri_rdfs_subClassOf, X_261, Y_262), true, icext(uri_rdfs_Class, Y_262), true)=true))). % 33.87/21.66 tff(c_2029, plain, (![C_95]: (ifeq(iext(uri_rdfs_range, uri_rdfs_domain, C_95), true, icext(C_95, uri_rdfs_Class), true)=true))). % 33.87/21.66 tff(c_1990, plain, (![C_95]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_95), true, icext(C_95, uri_rdfs_ContainerMembershipProperty), true)=true))). % 33.87/21.66 tff(c_1975, plain, (![C_95]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_95), true, icext(C_95, uri_rdf_List), true)=true))). % 33.87/21.66 tff(c_2405, plain, (![C_99]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_99), true, icext(C_99, uri_rdf__3), true)=true))). % 33.87/21.66 tff(c_2003, plain, (![C_95]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_95), true, icext(C_95, uri_rdfs_seeAlso), true)=true))). % 33.87/21.66 tff(c_1969, plain, (![C_95]: (ifeq(iext(uri_rdfs_range, uri_rdf_rest, C_95), true, icext(C_95, sK1_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_l2), true)=true))). % 33.87/21.66 tff(c_2406, plain, (![C_99]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_99), true, icext(C_99, uri_rdf_value), true)=true))). % 33.87/21.66 tff(c_2371, plain, (![C_99]: (ifeq(iext(uri_rdfs_domain, uri_owl_unionOf, C_99), true, icext(C_99, sK2_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_u), true)=true))). % 33.87/21.66 tff(c_2356, plain, (![C_99]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_99), true, icext(C_99, uri_rdf_value), true)=true))). % 33.87/21.66 tff(c_12177, plain, (![X_33]: (ifeq(icext(uri_rdf_List, X_33), true, icext(uri_rdf_List, X_33), true)=true))). % 33.87/21.66 tff(c_12631, plain, (![X_33]: (ifeq(icext(uri_ex_Species, X_33), true, icext(uri_ex_Species, X_33), true)=true))). % 33.87/21.66 tff(c_12864, plain, (![X_33]: (ifeq(icext(sK2_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_u, X_33), true, icext(sK2_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_u, X_33), true)=true))). % 33.87/21.66 tff(c_13399, plain, (![X_239, Y_240]: (ifeq(iext(uri_rdf_predicate, X_239, Y_240), true, icext(uri_rdfs_Statement, X_239), true)=true))). % 33.87/21.66 tff(c_5167, plain, (![X_33]: (ifeq(icext(uri_rdfs_Datatype, X_33), true, icext(uri_rdfs_Datatype, X_33), true)=true))). % 33.87/21.66 tff(c_8043, plain, (![X_33]: (ifeq(icext(uri_rdf_XMLLiteral, X_33), true, icext(uri_rdf_XMLLiteral, X_33), true)=true))). % 33.87/21.66 tff(c_9059, plain, (![X_33]: (ifeq(icext(uri_rdfs_Container, X_33), true, icext(uri_rdfs_Container, X_33), true)=true))). % 33.87/21.66 tff(c_11148, plain, (![X_33]: (ifeq(icext(uri_rdfs_Class, X_33), true, icext(uri_rdfs_Class, X_33), true)=true))). % 33.87/21.66 tff(c_6825, plain, (![X_33]: (ifeq(icext(uri_rdfs_Literal, X_33), true, icext(uri_rdfs_Literal, X_33), true)=true))). % 33.87/21.66 tff(c_7976, plain, (![X_33]: (ifeq(icext(uri_rdfs_Seq, X_33), true, icext(uri_rdfs_Seq, X_33), true)=true))). % 33.87/21.66 tff(c_6443, plain, (![X_33]: (ifeq(icext(uri_rdf_Property, X_33), true, icext(uri_rdf_Property, X_33), true)=true))). % 33.87/21.66 tff(c_6019, plain, (![X_33]: (ifeq(icext(uri_rdf_Bag, X_33), true, icext(uri_rdf_Bag, X_33), true)=true))). % 33.87/21.66 tff(c_6541, plain, (![X_33]: (ifeq(icext(uri_rdfs_ContainerMembershipProperty, X_33), true, icext(uri_rdfs_ContainerMembershipProperty, X_33), true)=true))). % 33.87/21.66 tff(c_7352, plain, (![X_33]: (ifeq(icext(uri_rdf_Alt, X_33), true, icext(uri_rdf_Alt, X_33), true)=true))). % 33.87/21.66 tff(c_2023, plain, (![C_95]: (ifeq(iext(uri_rdfs_range, uri_rdf_first, C_95), true, icext(C_95, uri_ex_Eagle), true)=true))). % 33.87/21.66 tff(c_13287, plain, (iext(uri_rdf_type, uri_rdfs_Resource, uri_rdfs_Class)=true)). % 33.87/21.66 tff(c_13123, plain, (icext(uri_rdf_Property, uri_rdfs_member)=true)). % 33.87/21.66 tff(c_13044, plain, (iext(uri_rdf_type, uri_rdfs_member, uri_rdf_Property)=true)). % 33.87/21.66 tff(c_2042, plain, (![C_95]: (ifeq(iext(uri_rdfs_range, uri_rdf_rest, C_95), true, icext(C_95, uri_rdf_nil), true)=true))). % 33.87/21.66 tff(c_12974, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_member, uri_rdfs_member)=true)). % 33.87/21.66 tff(c_12904, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Resource, uri_rdfs_Resource)=true)). % 33.87/21.66 tff(c_12808, plain, (iext(uri_rdfs_subClassOf, sK2_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_u, sK2_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_u)=true)). % 33.87/21.66 tff(c_12641, plain, (iext(uri_rdfs_subClassOf, uri_ex_Species, uri_rdfs_Resource)=true)). % 33.87/21.66 tff(c_12550, plain, (iext(uri_rdfs_subClassOf, uri_ex_Species, uri_ex_Species)=true)). % 33.87/21.66 tff(c_2385, plain, (![C_99]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_99), true, icext(C_99, uri_rdfs_domain), true)=true))). % 33.87/21.66 tff(c_12282, plain, (iext(uri_rdfs_subClassOf, sK2_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_u, uri_rdfs_Resource)=true)). % 33.87/21.66 tff(c_12216, plain, (iext(uri_rdfs_subClassOf, uri_rdf_List, uri_rdfs_Resource)=true)). % 33.87/21.66 tff(c_12121, plain, (iext(uri_rdfs_subClassOf, uri_rdf_List, uri_rdf_List)=true)). % 33.87/21.66 tff(c_12074, plain, (iext(uri_rdf_type, uri_rdfs_Literal, uri_rdfs_Class)=true)). % 33.87/21.66 tff(c_12001, plain, (iext(uri_rdf_type, uri_rdf_Bag, uri_rdfs_Class)=true)). % 33.87/21.66 tff(c_2377, plain, (![C_99]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_99), true, icext(C_99, uri_rdfs_isDefinedBy), true)=true))). % 33.87/21.66 tff(c_11954, plain, (iext(uri_rdf_type, uri_rdfs_Seq, uri_rdfs_Class)=true)). % 33.87/21.66 tff(c_11907, plain, (iext(uri_rdf_type, uri_rdfs_ContainerMembershipProperty, uri_rdfs_Class)=true)). % 33.87/21.66 tff(c_1985, plain, (![C_95]: (ifeq(iext(uri_rdfs_range, uri_rdfs_domain, C_95), true, icext(C_95, uri_rdf_Property), true)=true))). % 33.87/21.66 tff(c_11833, plain, (iext(uri_rdf_type, uri_rdf_XMLLiteral, uri_rdfs_Class)=true)). % 33.87/21.66 tff(c_11784, plain, (iext(uri_rdf_type, uri_rdf_Alt, uri_rdfs_Class)=true)). % 33.87/21.66 tff(c_2419, plain, (![C_99]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_99), true, icext(C_99, uri_rdf_Alt), true)=true))). % 33.87/21.66 tff(c_11712, plain, (iext(uri_rdf_type, uri_rdfs_Container, uri_rdfs_Class)=true)). % 33.87/21.66 tff(c_11665, plain, (iext(uri_rdf_type, uri_rdfs_Datatype, uri_rdfs_Class)=true)). % 33.87/21.66 tff(c_2378, plain, (![C_99]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_99), true, icext(C_99, uri_rdfs_range), true)=true))). % 33.87/21.66 tff(c_11587, plain, (iext(uri_rdf_type, uri_rdfs_Class, uri_rdfs_Class)=true)). % 33.87/21.66 tff(c_11540, plain, (iext(uri_rdf_type, uri_ex_Species, uri_rdfs_Class)=true)). % 33.87/21.66 tff(c_2420, plain, (![C_99]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_99), true, icext(C_99, uri_rdfs_Datatype), true)=true))). % 33.87/21.67 tff(c_11468, plain, (iext(uri_rdf_type, sK2_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_u, uri_rdfs_Class)=true)). % 33.87/21.67 tff(c_11421, plain, (iext(uri_rdf_type, sK3_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_l1, uri_rdf_List)=true)). % 33.87/21.67 tff(c_11374, plain, (iext(uri_rdf_type, sK1_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_l2, uri_rdf_List)=true)). % 33.87/21.67 tff(c_11326, plain, (iext(uri_rdf_type, uri_rdf_List, uri_rdfs_Class)=true)). % 33.87/21.67 tff(c_4840, plain, (tuple(iext(uri_rdf_type, uri_rdfs_Resource, uri_ex_Species), true)!=tuple(true, true))). % 33.87/21.67 tff(c_11268, plain, (iext(uri_rdf_type, uri_rdfs_range, uri_rdf_Property)=true)). % 33.87/21.67 tff(c_2354, plain, (![C_99]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_99), true, icext(C_99, uri_rdfs_subClassOf), true)=true))). % 33.87/21.67 tff(c_1100, plain, (![S_5, O_6]: (ifeq(iext(uri_rdfs_range, S_5, O_6), true, true, true)=true))). % 33.87/21.67 tff(c_11092, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Class, uri_rdfs_Class)=true)). % 33.87/21.67 tff(c_11026, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_range, uri_rdfs_range)=true)). % 33.87/21.67 tff(c_10856, plain, (icext(uri_rdf_Property, uri_rdfs_domain)=true)). % 33.87/21.67 tff(c_10802, plain, (iext(uri_rdf_type, uri_rdfs_domain, uri_rdf_Property)=true)). % 33.87/21.67 tff(c_1988, plain, (![C_95]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_95), true, icext(C_95, uri_rdfs_Datatype), true)=true))). % 33.87/21.67 tff(c_10708, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf__2, uri_rdfs_member)=true)). % 33.87/21.67 tff(c_10539, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, uri_rdfs_Resource)=true)). % 33.87/21.67 tff(c_2388, plain, (![C_99]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_99), true, icext(C_99, uri_rdf__2), true)=true))). % 33.87/21.67 tff(c_10443, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_value, uri_rdf_value)=true)). % 33.87/21.67 tff(c_10220, plain, (ic(sK2_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_u)=true)). % 33.87/21.67 tff(c_10162, plain, (icext(uri_rdfs_Class, sK2_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_u)=true)). % 33.87/21.67 tff(c_10099, plain, (icext(uri_rdf_Property, uri_rdfs_isDefinedBy)=true)). % 33.87/21.67 tff(c_2043, plain, (![C_95]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_95), true, icext(C_95, sK2_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_u), true)=true))). % 33.87/21.67 tff(c_10045, plain, (iext(uri_rdf_type, uri_rdfs_isDefinedBy, uri_rdf_Property)=true)). % 33.87/21.67 tff(c_2351, plain, (![C_99]: (ifeq(iext(uri_rdfs_domain, uri_rdf_rest, C_99), true, icext(C_99, sK3_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_l1), true)=true))). % 33.87/21.67 tff(c_9880, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Bag, uri_rdfs_Resource)=true)). % 33.87/21.67 tff(c_9812, plain, (iext(uri_rdfs_subPropertyOf, uri_owl_unionOf, uri_owl_unionOf)=true)). % 33.87/21.67 tff(c_9687, plain, (ic(uri_ex_Species)=true)). % 33.87/21.67 tff(c_9629, plain, (icext(uri_rdfs_Class, uri_ex_Species)=true)). % 33.87/21.67 tff(c_2025, plain, (![C_95]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_95), true, icext(C_95, uri_ex_Species), true)=true))). % 33.87/21.67 tff(c_9481, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Alt, uri_rdfs_Resource)=true)). % 33.87/21.67 tff(c_9333, plain, (icext(uri_rdf_Property, uri_owl_unionOf)=true)). % 33.87/21.67 tff(c_9279, plain, (iext(uri_rdf_type, uri_owl_unionOf, uri_rdf_Property)=true)). % 33.87/21.67 tff(c_9214, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_isDefinedBy, uri_rdfs_isDefinedBy)=true)). % 33.87/21.67 tff(c_2369, plain, (![C_99]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_99), true, icext(C_99, uri_rdfs_subPropertyOf), true)=true))). % 33.87/21.67 tff(c_9069, plain, (icext(uri_rdf_List, sK3_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_l1)=true)). % 33.87/21.67 tff(c_8984, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Container, uri_rdfs_Container)=true)). % 33.87/21.67 tff(c_2408, plain, (![C_99]: (ifeq(iext(uri_rdfs_domain, uri_rdf_first, C_99), true, icext(C_99, sK3_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_l1), true)=true))). % 33.87/21.67 tff(c_8917, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, uri_rdfs_domain)=true)). % 33.87/21.67 tff(c_8787, plain, (icext(uri_rdf_Property, uri_rdfs_subClassOf)=true)). % 33.87/21.67 tff(c_8705, plain, (iext(uri_rdf_type, uri_rdfs_subClassOf, uri_rdf_Property)=true)). % 33.87/21.67 tff(c_8582, plain, (icext(uri_rdf_Property, uri_rdfs_subPropertyOf)=true)). % 33.87/21.67 tff(c_2366, plain, (![C_99]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_99), true, icext(C_99, uri_rdf_rest), true)=true))). % 33.87/21.67 tff(c_8504, plain, (iext(uri_rdf_type, uri_rdfs_subPropertyOf, uri_rdf_Property)=true)). % 33.87/21.67 tff(c_8370, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Class, uri_rdfs_Resource)=true)). % 33.87/21.67 tff(c_2017, plain, (![C_95]: (ifeq(iext(uri_rdfs_range, uri_rdfs_range, C_95), true, icext(C_95, uri_rdfs_Literal), true)=true))). % 33.87/21.67 tff(c_8209, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Property, uri_rdfs_Resource)=true)). % 33.87/21.67 tff(c_8119, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf)=true)). % 33.87/21.67 tff(c_1984, plain, (![C_95]: (ifeq(iext(uri_rdfs_range, uri_rdfs_range, C_95), true, icext(C_95, uri_rdfs_Class), true)=true))). % 33.87/21.67 tff(c_8054, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_rest, uri_rdf_rest)=true)). % 33.87/21.67 tff(c_7987, plain, (iext(uri_rdfs_subClassOf, uri_rdf_XMLLiteral, uri_rdf_XMLLiteral)=true)). % 33.87/21.67 tff(c_7920, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Seq, uri_rdfs_Seq)=true)). % 33.87/21.67 tff(c_7852, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf__2, uri_rdf__2)=true)). % 33.87/21.67 tff(c_922, plain, (![S_5, O_6]: (ifeq(iext(uri_rdfs_domain, S_5, O_6), true, true, true)=true))). % 33.87/21.67 tff(c_7714, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf__3, uri_rdfs_member)=true)). % 33.87/21.67 tff(c_7649, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_type, uri_rdf_type)=true)). % 33.87/21.67 tff(c_2015, plain, (![C_95]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_95), true, icext(C_95, uri_rdf_Property), true)=true))). % 33.87/21.67 tff(c_7556, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf__3, uri_rdf__3)=true)). % 33.87/21.67 tff(c_7460, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf__1, uri_rdf__1)=true)). % 33.87/21.67 tff(c_7394, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Seq, uri_rdfs_Resource)=true)). % 33.87/21.67 tff(c_1978, plain, (![C_95]: (ifeq(iext(uri_rdfs_range, uri_rdfs_domain, C_95), true, icext(C_95, uri_rdfs_Resource), true)=true))). % 33.87/21.67 tff(c_7296, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Alt, uri_rdf_Alt)=true)). % 33.87/21.67 tff(c_2359, plain, (![C_99]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_99), true, icext(C_99, uri_rdf_XMLLiteral), true)=true))). % 33.87/21.67 tff(c_7155, plain, (icext(uri_rdf_Property, uri_rdfs_range)=true)). % 33.87/21.67 tff(c_7116, plain, (ip(uri_rdfs_member)=true)). % 33.87/21.67 tff(c_2368, plain, (![C_99]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_99), true, icext(C_99, uri_rdfs_range), true)=true))). % 33.87/21.67 tff(c_7030, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf__1, uri_rdfs_member)=true)). % 33.87/21.67 tff(c_2367, plain, (![C_99]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_99), true, icext(C_99, uri_rdf_first), true)=true))). % 33.87/21.67 tff(c_6905, plain, (ic(uri_rdf_List)=true)). % 33.87/21.67 tff(c_6854, plain, (icext(uri_rdfs_Class, uri_rdf_List)=true)). % 33.87/21.67 tff(c_1983, plain, (![C_95]: (ifeq(iext(uri_rdfs_range, uri_rdfs_domain, C_95), true, icext(C_95, uri_rdf_List), true)=true))). % 33.87/21.67 tff(c_6766, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Literal, uri_rdfs_Literal)=true)). % 33.87/21.67 tff(c_2373, plain, (![C_99]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_99), true, icext(C_99, uri_rdfs_Seq), true)=true))). % 33.87/21.67 tff(c_6643, plain, (icext(uri_rdf_Property, uri_rdfs_seeAlso)=true)). % 33.87/21.67 tff(c_6586, plain, (iext(uri_rdf_type, uri_rdfs_seeAlso, uri_rdf_Property)=true)). % 33.87/21.67 tff(c_2394, plain, (![C_99]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_99), true, icext(C_99, uri_rdf__1), true)=true))). % 33.87/21.67 tff(c_6485, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, uri_rdfs_ContainerMembershipProperty)=true)). % 33.87/21.67 tff(c_2039, plain, (![C_95]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_95), true, icext(C_95, uri_rdfs_Container), true)=true))). % 33.87/21.67 tff(c_6387, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Property, uri_rdf_Property)=true)). % 33.87/21.67 tff(c_6322, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, uri_rdfs_subClassOf)=true)). % 33.87/21.67 tff(c_6228, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_object, uri_rdf_object)=true)). % 33.87/21.67 tff(c_2036, plain, (![C_95]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_95), true, icext(C_95, uri_rdfs_Class), true)=true))). % 33.87/21.67 tff(c_1691, plain, (![S_5, O_6]: (ifeq(iext(uri_rdfs_subClassOf, S_5, O_6), true, true, true)=true))). % 33.87/21.67 tff(c_6129, plain, (icext(uri_rdf_List, sK1_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_l2)=true)). % 33.87/21.67 tff(c_2425, plain, (![C_99]: (ifeq(iext(uri_rdfs_domain, uri_rdf_rest, C_99), true, icext(C_99, sK1_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_l2), true)=true))). % 33.87/21.67 tff(c_6029, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, uri_rdfs_Resource)=true)). % 33.87/21.67 tff(c_5963, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Bag, uri_rdf_Bag)=true)). % 33.87/21.67 tff(c_2007, plain, (![C_95]: (ifeq(iext(uri_rdfs_range, uri_rdfs_range, C_95), true, icext(C_95, uri_rdfs_Resource), true)=true))). % 33.87/21.67 tff(c_5773, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_subject, uri_rdf_subject)=true)). % 33.87/21.67 tff(c_1181, plain, (![S_5, O_6]: (ifeq(iext(uri_owl_unionOf, S_5, O_6), true, true, true)=true))). % 33.87/21.67 tff(c_3110, plain, (![S_5, O_6]: (ifeq(iext(uri_rdfs_subPropertyOf, S_5, O_6), true, true, true)=true))). % 33.87/21.67 tff(c_2390, plain, (![C_99]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_99), true, icext(C_99, uri_rdf__2), true)=true))). % 33.87/21.67 tff(c_5579, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Literal, uri_rdfs_Resource)=true)). % 33.87/21.67 tff(c_3225, plain, (![S_5, O_6]: (ifeq(iext(uri_rdf_rest, S_5, O_6), true, true, true)=true))). % 33.87/21.67 tff(c_5469, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_first, uri_rdf_first)=true)). % 33.87/21.67 tff(c_1655, plain, (![X_92]: (ifeq(icext(uri_rdf_Alt, X_92), true, icext(uri_rdfs_Container, X_92), true)=true))). % 33.87/21.67 tff(c_5355, plain, (iext(uri_rdfs_subClassOf, uri_rdf_XMLLiteral, uri_rdfs_Resource)=true)). % 33.87/21.67 tff(c_1657, plain, (![X_92]: (ifeq(icext(uri_rdf_Bag, X_92), true, icext(uri_rdfs_Container, X_92), true)=true))). % 33.87/21.67 tff(c_1656, plain, (![X_92]: (ifeq(icext(uri_rdfs_Datatype, X_92), true, icext(uri_rdfs_Class, X_92), true)=true))). % 33.87/21.67 tff(c_5177, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_seeAlso, uri_rdfs_seeAlso)=true)). % 33.87/21.67 tff(c_5115, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, uri_rdfs_Datatype)=true)). % 33.87/21.67 tff(c_647, plain, (![S_71, O_72]: (ifeq(iext(uri_rdf_object, S_71, O_72), true, true, true)=true))). % 33.87/21.67 tff(c_1652, plain, (![X_92]: (ifeq(icext(uri_rdf_XMLLiteral, X_92), true, icext(uri_rdfs_Literal, X_92), true)=true))). % 33.87/21.67 tff(c_4983, plain, (icext(uri_rdfs_Class, uri_rdfs_Resource)=true)). % 33.87/21.67 tff(c_1654, plain, (![X_92]: (ifeq(icext(uri_rdfs_ContainerMembershipProperty, X_92), true, icext(uri_rdf_Property, X_92), true)=true))). % 33.87/21.67 tff(c_4941, plain, (ic(uri_rdfs_Resource)=true)). % 33.87/21.67 tff(c_4880, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Container, uri_rdfs_Resource)=true)). % 33.87/21.67 tff(c_1653, plain, (![X_92]: (ifeq(icext(uri_rdfs_Seq, X_92), true, icext(uri_rdfs_Container, X_92), true)=true))). % 33.87/21.67 tff(c_4810, plain, (![X_140]: (iext(uri_rdf_type, X_140, uri_rdfs_Resource)=true))). % 33.87/21.67 tff(c_2037, plain, (![X_96, Y_97]: (ifeq(iext(uri_rdf_predicate, X_96, Y_97), true, true, true)=true))). % 33.87/21.67 tff(c_1579, plain, (tuple(true, iext(uri_rdf_type, uri_ex_harry, uri_ex_Eagle))!=tuple(true, true))). % 33.87/21.67 tff(c_2399, plain, (![X_100, Y_101]: (ifeq(iext(uri_rdfs_label, X_100, Y_101), true, true, true)=true))). % 33.87/21.67 tff(c_1994, plain, (![X_96, Y_97]: (ifeq(iext(uri_rdfs_isDefinedBy, X_96, Y_97), true, true, true)=true))). % 33.87/21.67 tff(c_1582, plain, (tuple(true, iext(uri_rdf_type, uri_ex_harry, uri_ex_Falcon))!=tuple(true, true))). % 33.87/21.67 tff(c_1991, plain, (![X_96, Y_97]: (ifeq(iext(uri_rdf__1, X_96, Y_97), true, true, true)=true))). % 33.87/21.67 tff(c_1999, plain, (![X_96, Y_97]: (ifeq(iext(uri_rdf_first, X_96, Y_97), true, true, true)=true))). % 33.87/21.67 tff(c_1585, plain, (tuple(iext(uri_rdf_type, sK2_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_u, uri_ex_Species), true)!=tuple(true, true))). % 33.87/21.67 tff(c_2380, plain, (![X_100, Y_101]: (ifeq(iext(uri_rdf_type, X_100, Y_101), true, true, true)=true))). % 33.87/21.67 tff(c_2361, plain, (![X_100, Y_101]: (ifeq(iext(uri_rdfs_seeAlso, X_100, Y_101), true, true, true)=true))). % 33.87/21.67 tff(c_2012, plain, (![X_96, Y_97]: (ifeq(iext(uri_rdf_subject, X_96, Y_97), true, true, true)=true))). % 33.87/21.67 tff(c_2355, plain, (![X_100, Y_101]: (ifeq(iext(uri_rdf_value, X_100, Y_101), true, true, true)=true))). % 33.87/21.67 tff(c_2006, plain, (![X_96, Y_97]: (ifeq(iext(uri_rdf__2, X_96, Y_97), true, true, true)=true))). % 33.87/21.67 tff(c_4603, plain, (icext(uri_rdfs_Class, uri_rdfs_Literal)=true)). % 33.87/21.67 tff(c_4553, plain, (icext(uri_rdfs_Class, uri_rdf_Alt)=true)). % 33.87/21.67 tff(c_4503, plain, (icext(uri_rdfs_Class, uri_rdf_XMLLiteral)=true)). % 33.87/21.67 tff(c_2402, plain, (![X_100, Y_101]: (ifeq(iext(uri_rdfs_member, X_100, Y_101), true, true, true)=true))). % 33.87/21.67 tff(c_4458, plain, (icext(uri_rdfs_Class, uri_rdfs_ContainerMembershipProperty)=true)). % 33.87/21.67 tff(c_4415, plain, (icext(uri_rdfs_Class, uri_rdf_Bag)=true)). % 33.87/21.67 tff(c_2383, plain, (![X_100, Y_101]: (ifeq(iext(uri_rdfs_comment, X_100, Y_101), true, true, true)=true))). % 33.87/21.67 tff(c_4360, plain, (icext(uri_rdfs_Class, uri_rdfs_Datatype)=true)). % 33.87/21.67 tff(c_4315, plain, (icext(uri_rdfs_Class, uri_rdfs_Container)=true)). % 33.87/21.67 tff(c_2404, plain, (![X_100, Y_101]: (ifeq(iext(uri_rdf__3, X_100, Y_101), true, true, true)=true))). % 33.87/21.67 tff(c_4263, plain, (icext(uri_rdfs_Class, uri_rdfs_Seq)=true)). % 33.87/21.67 tff(c_4216, plain, (icext(uri_rdfs_Class, uri_rdfs_Class)=true)). % 33.87/21.67 tff(c_4167, plain, (icext(uri_rdfs_ContainerMembershipProperty, uri_rdf__1)=true)). % 33.87/21.67 tff(c_4127, plain, (icext(uri_ex_Species, uri_ex_Falcon)=true)). % 33.87/21.67 tff(c_4085, plain, (icext(uri_rdfs_ContainerMembershipProperty, uri_rdf__3)=true)). % 33.87/21.67 tff(c_4046, plain, (icext(uri_rdf_Property, uri_rdf__3)=true)). % 33.87/21.67 tff(c_4007, plain, (icext(uri_ex_Species, uri_ex_Eagle)=true)). % 33.87/21.67 tff(c_3970, plain, (icext(uri_rdf_Property, uri_rdf_value)=true)). % 33.87/21.67 tff(c_3929, plain, (icext(uri_rdf_Property, uri_rdf__1)=true)). % 33.87/21.67 tff(c_3890, plain, (icext(uri_rdf_Property, uri_rdf__2)=true)). % 33.87/21.67 tff(c_3851, plain, (icext(uri_rdf_Property, uri_rdf_subject)=true)). % 33.87/21.67 tff(c_3812, plain, (icext(uri_rdf_Property, uri_rdf_first)=true)). % 33.87/21.67 tff(c_3772, plain, (icext(uri_rdf_Property, uri_rdf_rest)=true)). % 33.87/21.67 tff(c_3734, plain, (icext(uri_rdf_Property, uri_rdf_type)=true)). % 33.87/21.67 tff(c_3691, plain, (icext(uri_rdfs_Datatype, uri_rdf_XMLLiteral)=true)). % 33.87/21.67 tff(c_3649, plain, (icext(sK2_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_u, uri_ex_harry)=true)). % 33.87/21.67 tff(c_3613, plain, (icext(uri_rdf_List, uri_rdf_nil)=true)). % 33.87/21.67 tff(c_3527, plain, (icext(uri_rdf_Property, uri_rdf_object)=true)). % 33.87/21.67 tff(c_3517, plain, (icext(uri_rdfs_Class, uri_rdf_Property)=true)). % 33.87/21.67 tff(c_3460, plain, (icext(uri_rdfs_ContainerMembershipProperty, uri_rdf__2)=true)). % 33.87/21.67 tff(c_3405, plain, (ip(uri_rdf_value)=true)). % 33.87/21.67 tff(c_3364, plain, (ip(uri_rdf__3)=true)). % 33.87/21.67 tff(c_3315, plain, (ic(uri_rdfs_Class)=true)). % 33.87/21.67 tff(c_3279, plain, (ic(uri_rdfs_Seq)=true)). % 33.87/21.67 tff(c_3243, plain, (ip(uri_rdfs_isDefinedBy)=true)). % 33.87/21.67 tff(c_3199, plain, (ip(uri_rdf_rest)=true)). % 33.87/21.67 tff(c_3160, plain, (ip(uri_rdf__2)=true)). % 33.87/21.67 tff(c_3121, plain, (ic(uri_rdfs_Datatype)=true)). % 33.87/21.67 tff(c_3086, plain, (ip(uri_rdfs_subPropertyOf)=true)). % 33.87/21.67 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))). % 33.87/21.67 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))). % 33.87/21.67 tff(c_2488, plain, (ic(uri_rdfs_Literal)=true)). % 33.87/21.67 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))). % 33.87/21.67 tff(c_2431, plain, (ip(uri_rdf__1)=true)). % 33.87/21.67 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))). % 33.87/21.67 tff(c_2048, plain, (ip(uri_rdfs_seeAlso)=true)). % 33.87/21.67 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))). % 33.87/21.67 tff(c_1667, plain, (ip(uri_rdfs_subClassOf)=true)). % 33.87/21.67 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))). % 33.87/21.67 tff(c_1589, plain, (ic(uri_rdf_Property)=true)). % 33.87/21.67 tff(c_198, plain, (![BNODE_x_55]: (tuple(iext(uri_rdf_type, BNODE_x_55, uri_ex_Species), iext(uri_rdf_type, uri_ex_harry, BNODE_x_55))!=tuple(true, true)))). % 33.87/21.67 tff(c_1543, plain, (ic(uri_rdf_XMLLiteral)=true)). % 33.87/21.67 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))). % 33.87/21.67 tff(c_1501, plain, (ic(uri_rdf_Alt)=true)). % 33.87/21.67 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))). % 33.87/21.67 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))). % 33.87/21.67 tff(c_1321, plain, (ic(uri_rdfs_Container)=true)). % 33.87/21.67 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))). % 33.87/21.67 tff(c_1286, plain, (ic(uri_rdfs_ContainerMembershipProperty)=true)). % 33.87/21.67 tff(c_156, plain, (![C_39]: (ifeq(ic(C_39), true, iext(uri_rdfs_subClassOf, C_39, C_39), true)=true))). % 33.87/21.67 tff(c_1228, plain, (ip(uri_rdf_subject)=true)). % 33.87/21.67 tff(c_150, plain, (![C_35, D_36]: (ifeq(iext(uri_rdfs_subClassOf, C_35, D_36), true, ic(D_36), true)=true))). % 33.87/21.67 tff(c_1157, plain, (ip(uri_owl_unionOf)=true)). % 33.87/21.67 tff(c_162, plain, (![P_43, Q_44]: (ifeq(iext(uri_rdfs_subPropertyOf, P_43, Q_44), true, ip(Q_44), true)=true))). % 33.87/21.67 tff(c_1079, plain, (ip(uri_rdfs_range)=true)). % 33.87/21.67 tff(c_164, plain, (![P_45, Q_46]: (ifeq(iext(uri_rdfs_subPropertyOf, P_45, Q_46), true, ip(P_45), true)=true))). % 33.87/21.67 tff(c_1019, plain, (ic(uri_rdf_Bag)=true)). % 33.87/21.67 tff(c_152, plain, (![C_37, D_38]: (ifeq(iext(uri_rdfs_subClassOf, C_37, D_38), true, ic(C_37), true)=true))). % 33.87/21.67 tff(c_28, plain, (![P_9]: (ifeq(ip(P_9), true, iext(uri_rdf_type, P_9, uri_rdf_Property), true)=true))). % 33.87/21.67 tff(c_907, plain, (ip(uri_rdfs_domain)=true)). % 33.87/21.67 tff(c_170, plain, (![P_51]: (ifeq(ip(P_51), true, iext(uri_rdfs_subPropertyOf, P_51, P_51), true)=true))). % 33.87/21.67 tff(c_865, plain, (ip(uri_rdf_type)=true)). % 33.87/21.67 tff(c_4, plain, (![P_4, S_5, O_6]: (ifeq(iext(P_4, S_5, O_6), true, ip(P_4), true)=true))). % 33.87/21.67 tff(c_620, plain, (ip(uri_rdf_object)=true)). % 33.87/21.67 tff(c_599, plain, (ip(uri_rdf_first)=true)). % 33.87/21.67 tff(c_30, plain, (![P_10]: (ifeq(iext(uri_rdf_type, P_10, uri_rdf_Property), true, ip(P_10), true)=true))). % 33.87/21.67 tff(c_58, plain, (![C_15]: (ifeq(ic(C_15), true, iext(uri_rdfs_subClassOf, C_15, uri_rdfs_Resource), true)=true))). % 33.87/21.67 tff(c_114, plain, (![X_22]: (ifeq(ic(X_22), true, icext(uri_rdfs_Class, X_22), true)=true))). % 33.87/21.67 tff(c_116, plain, (![X_23]: (ifeq(icext(uri_rdfs_Class, X_23), true, ic(X_23), true)=true))). % 33.87/21.67 tff(c_122, plain, (![X_26]: (ifeq(icext(uri_rdfs_Literal, X_26), true, lv(X_26), true)=true))). % 33.87/21.67 tff(c_514, plain, (![X_63]: (icext(uri_rdfs_Resource, X_63)=true))). % 33.87/21.68 tff(c_201, plain, (![X_8]: (ifeq(lv(X_8), true, true, true)=true))). % 33.87/21.68 tff(c_124, plain, (![X_27]: (ifeq(lv(X_27), true, icext(uri_rdfs_Literal, X_27), true)=true))). % 33.87/21.68 tff(c_2, plain, (![A_1, B_2, C_3]: (ifeq(A_1, A_1, B_2, C_3)=B_2))). % 33.87/21.68 tff(c_52, plain, (iext(uri_rdfs_range, uri_rdfs_seeAlso, uri_rdfs_Resource)=true)). % 33.87/21.68 tff(c_186, plain, (iext(uri_rdf_rest, sK3_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_l1, sK1_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_l2)=true)). % 33.87/21.68 tff(c_194, plain, (iext(uri_rdf_type, uri_ex_Eagle, uri_ex_Species)=true)). % 33.87/21.68 tff(c_10, plain, (iext(uri_rdf_type, uri_rdf_first, uri_rdf_Property)=true)). % 33.87/21.68 tff(c_154, plain, (iext(uri_rdfs_range, uri_rdfs_subClassOf, uri_rdfs_Class)=true)). % 33.87/21.68 tff(c_178, plain, (iext(uri_rdfs_domain, uri_rdf_value, uri_rdfs_Resource)=true)). % 33.87/21.68 tff(c_18, plain, (iext(uri_rdf_type, uri_rdf__2, uri_rdf_Property)=true)). % 33.87/21.68 tff(c_12, plain, (iext(uri_rdf_type, uri_rdf_nil, uri_rdf_List)=true)). % 33.87/21.68 tff(c_100, plain, (iext(uri_rdfs_subClassOf, uri_rdf_XMLLiteral, uri_rdfs_Literal)=true)). % 33.87/21.68 tff(c_22, plain, (iext(uri_rdf_type, uri_rdf_object, uri_rdf_Property)=true)). % 33.87/21.68 tff(c_50, plain, (iext(uri_rdfs_domain, uri_rdfs_seeAlso, uri_rdfs_Resource)=true)). % 33.87/21.68 tff(c_16, plain, (iext(uri_rdf_type, uri_rdf__1, uri_rdf_Property)=true)). % 33.87/21.68 tff(c_188, plain, (iext(uri_rdf_first, sK1_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_l2, uri_ex_Falcon)=true)). % 33.87/21.68 tff(c_96, plain, (iext(uri_rdf_type, uri_rdf__3, uri_rdfs_ContainerMembershipProperty)=true)). % 33.87/21.68 tff(c_64, plain, (iext(uri_rdfs_domain, uri_rdf_rest, uri_rdf_List)=true)). % 33.87/21.68 tff(c_60, plain, (iext(uri_rdfs_domain, uri_rdf_first, uri_rdf_List)=true)). % 33.87/21.68 tff(c_132, plain, (iext(uri_rdfs_range, uri_rdfs_range, uri_rdfs_Class)=true)). % 33.87/21.68 tff(c_160, plain, (iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, uri_rdf_Property)=true)). % 33.87/21.68 tff(c_176, plain, (iext(uri_rdfs_range, uri_rdf_type, uri_rdfs_Class)=true)). % 33.87/21.68 tff(c_182, plain, (iext(uri_owl_unionOf, sK2_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_u, sK3_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_l1)=true)). % 33.87/21.68 tff(c_102, plain, (iext(uri_rdf_type, uri_rdf_XMLLiteral, uri_rdfs_Datatype)=true)). % 33.87/21.68 tff(c_98, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Seq, uri_rdfs_Container)=true)). % 33.87/21.68 tff(c_92, plain, (iext(uri_rdf_type, uri_rdf__1, uri_rdfs_ContainerMembershipProperty)=true)). % 33.87/21.68 tff(c_86, plain, (iext(uri_rdfs_range, uri_rdf__1, uri_rdfs_Resource)=true)). % 33.87/21.68 tff(c_20, plain, (iext(uri_rdf_type, uri_rdf__3, uri_rdf_Property)=true)). % 33.87/21.68 tff(c_42, plain, (iext(uri_rdfs_range, uri_rdfs_isDefinedBy, uri_rdfs_Resource)=true)). % 33.87/21.68 tff(c_128, plain, (iext(uri_rdfs_domain, uri_rdfs_range, uri_rdf_Property)=true)). % 33.87/21.68 tff(c_94, plain, (iext(uri_rdf_type, uri_rdf__2, uri_rdfs_ContainerMembershipProperty)=true)). % 33.87/21.68 tff(c_174, plain, (iext(uri_rdfs_domain, uri_rdf_type, uri_rdfs_Resource)=true)). % 33.87/21.68 tff(c_62, plain, (iext(uri_rdfs_range, uri_rdf_first, uri_rdfs_Resource)=true)). % 33.87/21.68 tff(c_36, plain, (iext(uri_rdfs_domain, uri_rdfs_comment, uri_rdfs_Resource)=true)). % 33.87/21.68 tff(c_112, plain, (iext(uri_rdfs_range, uri_rdfs_domain, uri_rdfs_Class)=true)). % 33.87/21.68 tff(c_44, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_isDefinedBy, uri_rdfs_seeAlso)=true)). % 33.87/21.68 tff(c_82, plain, (iext(uri_rdfs_domain, uri_rdf__2, uri_rdfs_Resource)=true)). % 33.87/21.68 tff(c_126, plain, (iext(uri_rdf_type, uri_rdf_Property, uri_rdfs_Class)=true)). % 33.87/21.68 tff(c_88, plain, (iext(uri_rdfs_range, uri_rdf__2, uri_rdfs_Resource)=true)). % 33.87/21.68 tff(c_90, plain, (iext(uri_rdfs_range, uri_rdf__3, uri_rdfs_Resource)=true)). % 33.87/21.68 tff(c_26, plain, (iext(uri_rdf_type, uri_rdf_subject, uri_rdf_Property)=true)). % 33.87/21.68 tff(c_80, plain, (iext(uri_rdfs_domain, uri_rdf__1, uri_rdfs_Resource)=true)). % 33.87/21.68 tff(c_144, plain, (iext(uri_rdfs_range, uri_rdf_subject, uri_rdfs_Resource)=true)). % 33.87/21.68 tff(c_40, plain, (iext(uri_rdfs_domain, uri_rdfs_isDefinedBy, uri_rdfs_Resource)=true)). % 33.87/21.68 tff(c_24, plain, (iext(uri_rdf_type, uri_rdf_value, uri_rdf_Property)=true)). % 33.87/21.68 tff(c_46, plain, (iext(uri_rdfs_domain, uri_rdfs_label, uri_rdfs_Resource)=true)). % 33.87/21.68 tff(c_48, plain, (iext(uri_rdfs_range, uri_rdfs_label, uri_rdfs_Literal)=true)). % 33.87/21.68 tff(c_76, plain, (iext(uri_rdfs_domain, uri_rdfs_member, uri_rdfs_Resource)=true)). % 33.87/21.68 tff(c_84, plain, (iext(uri_rdfs_domain, uri_rdf__3, uri_rdfs_Resource)=true)). % 33.87/21.68 tff(c_180, plain, (iext(uri_rdfs_range, uri_rdf_value, uri_rdfs_Resource)=true)). % 33.87/21.68 tff(c_74, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, uri_rdf_Property)=true)). % 33.87/21.68 tff(c_190, plain, (iext(uri_rdf_first, sK3_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_l1, uri_ex_Eagle)=true)). % 33.87/21.68 tff(c_108, plain, (iext(uri_rdfs_domain, uri_rdfs_domain, uri_rdf_Property)=true)). % 33.87/21.68 tff(c_192, plain, (iext(uri_rdf_type, uri_ex_Falcon, uri_ex_Species)=true)). % 33.87/21.68 tff(c_78, plain, (iext(uri_rdfs_range, uri_rdfs_member, uri_rdfs_Resource)=true)). % 33.87/21.68 tff(c_142, plain, (iext(uri_rdfs_domain, uri_rdf_subject, uri_rdfs_Statement)=true)). % 33.87/21.68 tff(c_146, plain, (iext(uri_rdfs_domain, uri_rdfs_subClassOf, uri_rdfs_Class)=true)). % 33.87/21.68 tff(c_66, plain, (iext(uri_rdfs_range, uri_rdf_rest, uri_rdf_List)=true)). % 33.87/21.68 tff(c_14, plain, (iext(uri_rdf_type, uri_rdf_rest, uri_rdf_Property)=true)). % 33.87/21.68 tff(c_38, plain, (iext(uri_rdfs_range, uri_rdfs_comment, uri_rdfs_Literal)=true)). % 33.87/21.68 tff(c_138, plain, (iext(uri_rdfs_domain, uri_rdf_predicate, uri_rdfs_Statement)=true)). % 33.87/21.68 tff(c_34, plain, (iext(uri_rdf_type, uri_rdf_type, uri_rdf_Property)=true)). % 33.87/21.68 tff(c_68, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Alt, uri_rdfs_Container)=true)). % 33.87/21.68 tff(c_106, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, uri_rdfs_Class)=true)). % 33.87/21.68 tff(c_140, plain, (iext(uri_rdfs_range, uri_rdf_predicate, uri_rdfs_Resource)=true)). % 33.87/21.68 tff(c_70, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Bag, uri_rdfs_Container)=true)). % 33.87/21.68 tff(c_134, plain, (iext(uri_rdfs_domain, uri_rdf_object, uri_rdfs_Statement)=true)). % 33.87/21.68 tff(c_168, plain, (iext(uri_rdfs_range, uri_rdfs_subPropertyOf, uri_rdf_Property)=true)). % 33.87/21.68 tff(c_184, plain, (iext(uri_rdf_rest, sK1_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_l2, uri_rdf_nil)=true)). % 33.87/21.68 tff(c_196, plain, (iext(uri_rdf_type, uri_ex_harry, sK2_testcase_premise_fullish_014_Harry_belongs_to_some_Species_BNODE_u)=true)). % 33.87/21.68 tff(c_6, plain, (![X_7]: (ir(X_7)=true))). % 33.87/21.68 % SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 33.87/21.68 %------------------------------------------------------------------------------