%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : SWB027-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/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % Computer : n027.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:56 PM UTC 2025 % Result : Satisfiable 32.88s 20.83s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SWB027-10 : TPTP v9.0.0. Released v7.5.0. % 0.11/0.13 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % 0.13/0.34 % Computer : n027.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 300 % 0.13/0.34 % DateTime : Wed Apr 9 01:03:05 EDT 2025 % 0.13/0.34 % CPUTime : % 32.88/20.82 % 32.88/20.83 % SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 32.88/20.83 % 32.88/20.83 % SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 32.88/20.84 %$ ifeq > iext > icext > #nlpp > lv > ir > ip > ic > uri_rdfs_subPropertyOf > uri_rdfs_subClassOf > uri_rdfs_seeAlso > uri_rdfs_range > uri_rdfs_member > uri_rdfs_label > uri_rdfs_isDefinedBy > uri_rdfs_domain > uri_rdfs_comment > uri_rdfs_Statement > uri_rdfs_Seq > uri_rdfs_Resource > uri_rdfs_Literal > uri_rdfs_Datatype > uri_rdfs_ContainerMembershipProperty > uri_rdfs_Container > uri_rdfs_Class > uri_rdf_value > uri_rdf_type > uri_rdf_subject > uri_rdf_rest > uri_rdf_predicate > uri_rdf_object > uri_rdf_nil > uri_rdf_first > uri_rdf__3 > uri_rdf__2 > uri_rdf__1 > uri_rdf_XMLLiteral > uri_rdf_Property > uri_rdf_List > uri_rdf_Bag > uri_rdf_Alt > uri_owl_sameAs > uri_owl_propertyChainAxiom > uri_owl_inverseOf > uri_owl_InverseFunctionalProperty > uri_ex_p > true > sK3_testcase_premise_fullish_027_Inferred_Property_Characteristics_II_BNODE_l2 > sK2_testcase_premise_fullish_027_Inferred_Property_Characteristics_II_BNODE_l1 > sK1_testcase_premise_fullish_027_Inferred_Property_Characteristics_II_BNODE_v % 32.88/20.84 % 32.88/20.84 %Foreground sorts: % 32.88/20.85 % 32.88/20.85 % 32.88/20.85 %Background operators: % 32.88/20.85 % 32.88/20.85 % 32.88/20.85 %Foreground operators: % 32.88/20.85 tff(uri_owl_InverseFunctionalProperty, type, uri_owl_InverseFunctionalProperty: $i). % 32.88/20.85 tff(uri_rdfs_Datatype, type, uri_rdfs_Datatype: $i). % 32.88/20.85 tff(uri_rdfs_ContainerMembershipProperty, type, uri_rdfs_ContainerMembershipProperty: $i). % 32.88/20.85 tff(uri_rdfs_Resource, type, uri_rdfs_Resource: $i). % 32.88/20.85 tff(sK3_testcase_premise_fullish_027_Inferred_Property_Characteristics_II_BNODE_l2, type, sK3_testcase_premise_fullish_027_Inferred_Property_Characteristics_II_BNODE_l2: $i). % 32.88/20.85 tff(uri_rdf_Property, type, uri_rdf_Property: $i). % 32.88/20.85 tff(uri_rdf_subject, type, uri_rdf_subject: $i). % 32.88/20.85 tff(uri_rdf_type, type, uri_rdf_type: $i). % 32.88/20.85 tff(uri_rdfs_subPropertyOf, type, uri_rdfs_subPropertyOf: $i). % 32.88/20.85 tff(uri_rdfs_seeAlso, type, uri_rdfs_seeAlso: $i). % 32.88/20.85 tff(icext, type, icext: ($i * $i) > $i). % 32.88/20.85 tff(uri_rdfs_range, type, uri_rdfs_range: $i). % 32.88/20.85 tff(uri_rdf_XMLLiteral, type, uri_rdf_XMLLiteral: $i). % 32.88/20.85 tff(uri_rdf_List, type, uri_rdf_List: $i). % 32.88/20.85 tff(uri_rdf_first, type, uri_rdf_first: $i). % 32.88/20.85 tff(uri_rdf_predicate, type, uri_rdf_predicate: $i). % 32.88/20.85 tff(ir, type, ir: $i > $i). % 32.88/20.85 tff(lv, type, lv: $i > $i). % 32.88/20.85 tff(uri_owl_inverseOf, type, uri_owl_inverseOf: $i). % 32.88/20.85 tff(uri_rdf__3, type, uri_rdf__3: $i). % 32.88/20.85 tff(uri_rdf_value, type, uri_rdf_value: $i). % 32.88/20.85 tff(ic, type, ic: $i > $i). % 32.88/20.85 tff(uri_rdfs_Statement, type, uri_rdfs_Statement: $i). % 32.88/20.85 tff(uri_ex_p, type, uri_ex_p: $i). % 32.88/20.85 tff(uri_rdf__1, type, uri_rdf__1: $i). % 32.88/20.85 tff(iext, type, iext: ($i * $i * $i) > $i). % 32.88/20.85 tff(uri_rdf_rest, type, uri_rdf_rest: $i). % 32.88/20.85 tff(uri_rdfs_label, type, uri_rdfs_label: $i). % 32.88/20.85 tff(uri_rdfs_Container, type, uri_rdfs_Container: $i). % 32.88/20.85 tff(uri_owl_propertyChainAxiom, type, uri_owl_propertyChainAxiom: $i). % 32.88/20.85 tff(uri_rdfs_subClassOf, type, uri_rdfs_subClassOf: $i). % 32.88/20.85 tff(sK1_testcase_premise_fullish_027_Inferred_Property_Characteristics_II_BNODE_v, type, sK1_testcase_premise_fullish_027_Inferred_Property_Characteristics_II_BNODE_v: $i). % 32.88/20.85 tff(uri_owl_sameAs, type, uri_owl_sameAs: $i). % 32.88/20.85 tff(uri_rdf_object, type, uri_rdf_object: $i). % 32.88/20.85 tff(ip, type, ip: $i > $i). % 32.88/20.85 tff(uri_rdfs_Class, type, uri_rdfs_Class: $i). % 32.88/20.85 tff(uri_rdfs_Seq, type, uri_rdfs_Seq: $i). % 32.88/20.85 tff(uri_rdfs_member, type, uri_rdfs_member: $i). % 32.88/20.85 tff(uri_rdf_Bag, type, uri_rdf_Bag: $i). % 32.88/20.85 tff(uri_rdf__2, type, uri_rdf__2: $i). % 32.88/20.85 tff(sK2_testcase_premise_fullish_027_Inferred_Property_Characteristics_II_BNODE_l1, type, sK2_testcase_premise_fullish_027_Inferred_Property_Characteristics_II_BNODE_l1: $i). % 32.88/20.85 tff(uri_rdfs_comment, type, uri_rdfs_comment: $i). % 32.88/20.85 tff(uri_rdfs_Literal, type, uri_rdfs_Literal: $i). % 32.88/20.85 tff(true, type, true: $i). % 32.88/20.85 tff(uri_rdf_Alt, type, uri_rdf_Alt: $i). % 32.88/20.85 tff(uri_rdf_nil, type, uri_rdf_nil: $i). % 32.88/20.85 tff(uri_rdfs_isDefinedBy, type, uri_rdfs_isDefinedBy: $i). % 32.88/20.85 tff(uri_rdfs_domain, type, uri_rdfs_domain: $i). % 32.88/20.85 tff(ifeq, type, ifeq: ($i * $i * $i * $i) > $i). % 32.88/20.85 % 32.88/20.85 %Saturated clause set: % 32.88/20.85 tff(c_14876, 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))). % 32.88/20.85 tff(c_70168, plain, (![X_1216, Y_1217]: (ifeq(iext(uri_rdf_predicate, X_1216, Y_1217), true, iext(uri_rdf_predicate, X_1216, Y_1217), true)=true))). % 32.88/20.85 tff(c_16973, 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))). % 32.88/20.85 tff(c_14814, 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))). % 32.88/20.85 tff(c_14720, 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))). % 32.88/20.85 tff(c_69781, plain, (![X_1209, Y_1210]: (ifeq(iext(uri_rdfs_comment, X_1209, Y_1210), true, iext(uri_rdfs_comment, X_1209, Y_1210), true)=true))). % 32.88/20.85 tff(c_69754, plain, (![X_1205, Y_1206]: (ifeq(iext(uri_rdfs_label, X_1205, Y_1206), true, iext(uri_rdfs_label, X_1205, Y_1206), true)=true))). % 32.88/20.85 tff(c_14584, 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))). % 32.88/20.85 tff(c_69599, plain, (![X_1200, Y_1201]: (ifeq(iext(uri_rdfs_member, X_1200, Y_1201), true, iext(uri_rdfs_member, X_1200, Y_1201), true)=true))). % 32.88/20.85 tff(c_5186, 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))). % 32.88/20.85 tff(c_5189, 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))). % 32.88/20.85 tff(c_14651, 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))). % 32.88/20.85 tff(c_68945, plain, (![C_1193]: (ifeq(iext(uri_rdfs_subClassOf, C_1193, uri_rdf_List), true, iext(uri_rdfs_subClassOf, C_1193, uri_rdfs_Resource), true)=true))). % 32.88/20.85 tff(c_14391, 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))). % 32.88/20.85 tff(c_14304, 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))). % 32.88/20.85 tff(c_9336, 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))). % 32.88/20.85 tff(c_13296, 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))). % 32.88/20.85 tff(c_9969, 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))). % 32.88/20.85 tff(c_13370, 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))). % 32.88/20.85 tff(c_13419, 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))). % 32.88/20.85 tff(c_67932, plain, (![C_1182]: (ifeq(iext(uri_rdfs_subClassOf, C_1182, uri_rdfs_Statement), true, iext(uri_rdfs_subClassOf, C_1182, uri_rdfs_Resource), true)=true))). % 32.88/20.85 tff(c_15744, 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))). % 32.88/20.85 tff(c_13249, 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))). % 32.88/20.85 tff(c_12260, 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))). % 32.88/20.85 tff(c_13586, 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))). % 32.88/20.85 tff(c_14245, 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))). % 32.88/20.85 tff(c_8495, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdf_Property), true, ifeq(iext(P_18, uri_owl_propertyChainAxiom, Y_21), true, true, true), true)=true))). % 32.88/20.85 tff(c_13539, 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))). % 32.88/20.85 tff(c_12257, 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))). % 32.88/20.85 tff(c_6916, 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))). % 32.88/20.85 tff(c_12907, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdf_Property), true, ifeq(iext(P_18, uri_owl_inverseOf, Y_21), true, true, true), true)=true))). % 32.88/20.85 tff(c_8498, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdf_Property), true, ifeq(iext(P_28, X_30, uri_owl_propertyChainAxiom), true, true, true), true)=true))). % 32.88/20.85 tff(c_12910, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdf_Property), true, ifeq(iext(P_28, X_30, uri_owl_inverseOf), true, true, true), true)=true))). % 32.88/20.85 tff(c_15946, 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))). % 32.88/20.85 tff(c_9339, 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))). % 32.88/20.85 tff(c_14171, 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))). % 32.88/20.85 tff(c_8222, 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))). % 32.88/20.86 tff(c_6913, 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))). % 32.88/20.86 tff(c_9966, 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))). % 32.88/20.86 tff(c_13466, 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))). % 32.88/20.86 tff(c_8225, 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))). % 32.88/20.86 tff(c_14052, 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))). % 32.88/20.86 tff(c_16851, 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))). % 32.88/20.86 tff(c_13071, 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))). % 32.88/20.86 tff(c_15111, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, sK3_testcase_premise_fullish_027_Inferred_Property_Characteristics_II_BNODE_l2, uri_rdf_List), true, true, true), true)=true))). % 32.88/20.86 tff(c_13173, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, sK2_testcase_premise_fullish_027_Inferred_Property_Characteristics_II_BNODE_l1, uri_rdf_List), true, true, true), true)=true))). % 32.88/20.86 tff(c_13118, 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))). % 32.88/20.86 tff(c_13702, 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))). % 32.88/20.86 tff(c_8167, 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))). % 32.88/20.86 tff(c_64253, plain, (![C_1140]: (ifeq(iext(uri_rdfs_subClassOf, C_1140, uri_rdfs_Container), true, iext(uri_rdfs_subClassOf, C_1140, uri_rdfs_Resource), true)=true))). % 32.88/20.86 tff(c_64226, plain, (![X_1136, Y_1137]: (ifeq(iext(uri_rdf__3, X_1136, Y_1137), true, iext(uri_rdfs_member, X_1136, Y_1137), true)=true))). % 32.88/20.86 tff(c_6798, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subPropertyOf), true, ifeq(iext(P_47, uri_owl_propertyChainAxiom, uri_owl_propertyChainAxiom), true, true, true), true)=true))). % 32.88/20.86 tff(c_64078, plain, (![X_1131, Y_1132]: (ifeq(iext(uri_rdf__1, X_1131, Y_1132), true, iext(uri_rdfs_member, X_1131, Y_1132), true)=true))). % 32.88/20.86 tff(c_4310, 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))). % 32.88/20.86 tff(c_12656, 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))). % 32.88/20.86 tff(c_63501, plain, (![X_1124, Y_1125]: (ifeq(iext(uri_rdfs_range, X_1124, Y_1125), true, iext(uri_rdfs_range, X_1124, Y_1125), true)=true))). % 32.88/20.86 tff(c_7858, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subPropertyOf), true, ifeq(iext(P_47, uri_owl_inverseOf, uri_owl_inverseOf), true, true, true), true)=true))). % 32.88/20.86 tff(c_4313, 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))). % 32.88/20.86 tff(c_9385, 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))). % 32.88/20.86 tff(c_10391, 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))). % 32.88/20.86 tff(c_9720, 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))). % 32.88/20.86 tff(c_62820, plain, (![P_1116]: (ifeq(iext(uri_rdfs_subPropertyOf, P_1116, uri_rdf__3), true, iext(uri_rdfs_subPropertyOf, P_1116, uri_rdfs_member), true)=true))). % 32.88/20.86 tff(c_4066, 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))). % 32.88/20.86 tff(c_9656, 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))). % 32.88/20.86 tff(c_62535, plain, (![X_1109, Y_1110]: (ifeq(iext(uri_rdf__1, X_1109, Y_1110), true, iext(uri_rdf__1, X_1109, Y_1110), true)=true))). % 32.88/20.86 tff(c_4210, 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))). % 32.88/20.86 tff(c_62337, plain, (![X_1103, Y_1104]: (ifeq(iext(uri_rdf_rest, X_1103, Y_1104), true, iext(uri_rdf_rest, X_1103, Y_1104), true)=true))). % 32.88/20.86 tff(c_4406, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdfs_Class), true, ifeq(iext(P_18, uri_rdfs_ContainerMembershipProperty, Y_21), true, true, true), true)=true))). % 32.88/20.86 tff(c_61627, plain, (![X_1097, Y_1098]: (ifeq(iext(uri_rdfs_subPropertyOf, X_1097, Y_1098), true, iext(uri_rdfs_subPropertyOf, X_1097, Y_1098), true)=true))). % 32.88/20.86 tff(c_4785, 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))). % 32.88/20.86 tff(c_4455, 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))). % 32.88/20.86 tff(c_60997, plain, (![P_1090]: (ifeq(iext(uri_rdfs_subPropertyOf, P_1090, uri_rdf__1), true, iext(uri_rdfs_subPropertyOf, P_1090, uri_rdfs_member), true)=true))). % 32.88/20.86 tff(c_60559, plain, (![C_1086]: (ifeq(iext(uri_rdfs_subClassOf, C_1086, uri_rdf_XMLLiteral), true, iext(uri_rdfs_subClassOf, C_1086, uri_rdfs_Resource), true)=true))). % 32.88/20.86 tff(c_5293, 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))). % 32.88/20.86 tff(c_4365, 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))). % 32.88/20.86 tff(c_4213, 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))). % 32.88/20.86 tff(c_4886, 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))). % 32.88/20.86 tff(c_59911, plain, (![C_1078]: (ifeq(iext(uri_rdfs_subClassOf, C_1078, uri_rdfs_Seq), true, iext(uri_rdfs_subClassOf, C_1078, uri_rdfs_Resource), true)=true))). % 32.88/20.86 tff(c_59867, plain, (![X_1074, Y_1075]: (ifeq(iext(uri_owl_propertyChainAxiom, X_1074, Y_1075), true, iext(uri_owl_propertyChainAxiom, X_1074, Y_1075), true)=true))). % 32.88/20.86 tff(c_8760, 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))). % 32.88/20.86 tff(c_11115, 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))). % 32.88/20.86 tff(c_12853, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, uri_owl_inverseOf, uri_rdf_Property), true, true, true), true)=true))). % 32.88/20.86 tff(c_59475, plain, (![X_1067, Y_1068]: (ifeq(iext(uri_rdf__3, X_1067, Y_1068), true, iext(uri_rdf__3, X_1067, Y_1068), true)=true))). % 32.88/20.86 tff(c_10090, 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))). % 32.88/20.86 tff(c_4163, 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))). % 32.88/20.86 tff(c_12492, 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))). % 32.88/20.86 tff(c_6172, 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))). % 32.88/20.86 tff(c_58955, plain, (![X_1058, Y_1059]: (ifeq(iext(uri_rdf__2, X_1058, Y_1059), true, iext(uri_rdfs_member, X_1058, Y_1059), true)=true))). % 32.88/20.86 tff(c_4069, 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))). % 32.88/20.86 tff(c_11433, 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))). % 32.88/20.86 tff(c_7027, 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))). % 32.88/20.86 tff(c_58531, plain, (![X_1050, Y_1051]: (ifeq(iext(uri_owl_inverseOf, X_1050, Y_1051), true, iext(uri_owl_inverseOf, X_1050, Y_1051), true)=true))). % 32.88/20.86 tff(c_12140, 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))). % 32.88/20.86 tff(c_11682, 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))). % 32.88/20.86 tff(c_5538, 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))). % 32.88/20.86 tff(c_5057, 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))). % 32.88/20.86 tff(c_57711, plain, (![X_1040, Y_1041]: (ifeq(iext(uri_rdf_value, X_1040, Y_1041), true, iext(uri_rdf_value, X_1040, Y_1041), true)=true))). % 32.88/20.87 tff(c_57644, plain, (![P_1038]: (ifeq(iext(uri_rdfs_subPropertyOf, P_1038, uri_rdf__2), true, iext(uri_rdfs_subPropertyOf, P_1038, uri_rdfs_member), true)=true))). % 32.88/20.87 tff(c_4716, 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))). % 32.88/20.87 tff(c_8688, 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))). % 32.88/20.87 tff(c_11613, 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))). % 32.88/20.87 tff(c_7575, 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))). % 32.88/20.87 tff(c_4264, 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))). % 32.88/20.87 tff(c_4267, 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))). % 32.88/20.87 tff(c_6329, 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))). % 32.88/20.87 tff(c_4452, 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))). % 32.88/20.87 tff(c_12203, 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))). % 32.88/20.87 tff(c_15688, 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))). % 32.88/20.87 tff(c_55084, plain, (![X_1013, Y_1014]: (ifeq(iext(uri_rdf_object, X_1013, Y_1014), true, iext(uri_rdf_object, X_1013, Y_1014), true)=true))). % 32.88/20.87 tff(c_6859, 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))). % 32.88/20.87 tff(c_8106, 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))). % 32.88/20.87 tff(c_54704, plain, (![C_1009]: (ifeq(iext(uri_rdfs_subClassOf, C_1009, uri_rdfs_ContainerMembershipProperty), true, iext(uri_rdfs_subClassOf, C_1009, uri_rdfs_Resource), true)=true))). % 32.88/20.87 tff(c_4166, 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))). % 32.88/20.87 tff(c_7723, 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))). % 32.88/20.87 tff(c_8416, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, uri_owl_propertyChainAxiom, uri_rdf_Property), true, true, true), true)=true))). % 32.88/20.87 tff(c_54166, plain, (![C_1003]: (ifeq(iext(uri_rdfs_subClassOf, C_1003, uri_rdfs_Literal), true, iext(uri_rdfs_subClassOf, C_1003, uri_rdfs_Resource), true)=true))). % 32.88/20.87 tff(c_12426, 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))). % 32.88/20.87 tff(c_53307, plain, (![C_996]: (ifeq(iext(uri_rdfs_subClassOf, C_996, uri_rdf_Alt), true, iext(uri_rdfs_subClassOf, C_996, uri_rdfs_Resource), true)=true))). % 32.88/20.87 tff(c_12584, 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))). % 32.88/20.87 tff(c_52600, plain, (![X_991, Y_992]: (ifeq(iext(uri_rdfs_subClassOf, X_991, Y_992), true, iext(uri_rdfs_subClassOf, X_991, Y_992), true)=true))). % 32.88/20.87 tff(c_4362, 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))). % 32.88/20.87 tff(c_10695, 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))). % 32.88/20.87 tff(c_52126, plain, (![C_985]: (ifeq(iext(uri_rdfs_subClassOf, C_985, uri_rdf_Bag), true, iext(uri_rdfs_subClassOf, C_985, uri_rdfs_Resource), true)=true))). % 32.88/20.87 tff(c_52053, plain, (![C_984]: (ifeq(iext(uri_rdfs_subClassOf, C_984, uri_rdfs_Class), true, iext(uri_rdfs_subClassOf, C_984, uri_rdfs_Resource), true)=true))). % 32.88/20.87 tff(c_10300, 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))). % 32.88/20.87 tff(c_4943, 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))). % 32.88/20.87 tff(c_51582, plain, (![X_976, Y_977]: (ifeq(iext(uri_rdf_subject, X_976, Y_977), true, iext(uri_rdf_subject, X_976, Y_977), true)=true))). % 32.88/20.87 tff(c_6461, 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))). % 32.88/20.87 tff(c_4409, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdfs_Class), true, ifeq(iext(P_28, X_30, uri_rdfs_ContainerMembershipProperty), true, true, true), true)=true))). % 32.88/20.87 tff(c_9159, 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))). % 32.88/20.87 tff(c_50663, plain, (![X_964, Y_965]: (ifeq(iext(uri_rdf__2, X_964, Y_965), true, iext(uri_rdf__2, X_964, Y_965), true)=true))). % 32.88/20.87 tff(c_7390, 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))). % 32.88/20.87 tff(c_50399, plain, (![C_961]: (ifeq(iext(uri_rdfs_subClassOf, C_961, uri_rdfs_Datatype), true, iext(uri_rdfs_subClassOf, C_961, uri_rdfs_Resource), true)=true))). % 32.88/20.87 tff(c_50340, plain, (![X_957, Y_958]: (ifeq(iext(uri_rdf_first, X_957, Y_958), true, iext(uri_rdf_first, X_957, Y_958), true)=true))). % 32.88/20.87 tff(c_49641, plain, (![X_953, Y_954]: (ifeq(iext(uri_rdf_type, X_953, Y_954), true, iext(uri_rdf_type, X_953, Y_954), true)=true))). % 32.88/20.87 tff(c_4112, 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))). % 32.88/20.87 tff(c_11872, 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))). % 32.88/20.87 tff(c_5878, 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))). % 32.88/20.87 tff(c_48817, plain, (![C_945]: (ifeq(iext(uri_rdfs_subClassOf, C_945, uri_rdf_Property), true, iext(uri_rdfs_subClassOf, C_945, uri_rdfs_Resource), true)=true))). % 32.88/20.87 tff(c_7197, 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))). % 32.88/20.87 tff(c_8903, 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))). % 32.88/20.87 tff(c_48241, plain, (![X_939, Y_940]: (ifeq(iext(uri_rdfs_domain, X_939, Y_940), true, iext(uri_rdfs_domain, X_939, Y_940), true)=true))). % 32.88/20.87 tff(c_4109, 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))). % 32.88/20.87 tff(c_8611, 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))). % 32.88/20.87 tff(c_9257, 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))). % 32.88/20.87 tff(c_47837, plain, (![X_931, Y_932]: (ifeq(iext(uri_rdfs_isDefinedBy, X_931, Y_932), true, iext(uri_rdfs_isDefinedBy, X_931, Y_932), true)=true))). % 32.88/20.87 tff(c_47810, plain, (![X_927, Y_928]: (ifeq(iext(uri_rdfs_seeAlso, X_927, Y_928), true, iext(uri_rdfs_seeAlso, X_927, Y_928), true)=true))). % 32.88/20.87 tff(c_9912, 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))). % 32.88/20.87 tff(c_5628, 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))). % 32.88/20.87 tff(c_13822, 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))). % 32.88/20.87 tff(c_6542, 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))). % 32.88/20.87 tff(c_10176, 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))). % 32.88/20.87 tff(c_13819, 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))). % 32.88/20.87 tff(c_16693, 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))). % 32.88/20.87 tff(c_15070, 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_027_Inferred_Property_Characteristics_II_BNODE_l2), true, true, true), true)=true))). % 32.88/20.87 tff(c_6539, 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))). % 32.88/20.87 tff(c_13660, 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))). % 32.88/20.87 tff(c_13657, 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))). % 32.88/20.87 tff(c_10179, 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))). % 32.88/20.87 tff(c_10579, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdf_List), true, ifeq(iext(P_28, X_30, sK2_testcase_premise_fullish_027_Inferred_Property_Characteristics_II_BNODE_l1), true, true, true), true)=true))). % 32.88/20.87 tff(c_16696, 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))). % 32.88/20.87 tff(c_5625, 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))). % 32.88/20.87 tff(c_10576, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdf_List), true, ifeq(iext(P_18, sK2_testcase_premise_fullish_027_Inferred_Property_Characteristics_II_BNODE_l1, Y_21), true, true, true), true)=true))). % 32.88/20.87 tff(c_15067, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdf_List), true, ifeq(iext(P_18, sK3_testcase_premise_fullish_027_Inferred_Property_Characteristics_II_BNODE_l2, Y_21), true, true, true), true)=true))). % 32.88/20.87 tff(c_4661, plain, (![P_47, X_140]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, X_140, uri_rdfs_Resource), true, true, true), true)=true))). % 32.88/20.87 tff(c_3778, 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))). % 32.88/20.87 tff(c_3831, 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))). % 32.88/20.87 tff(c_3701, 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))). % 32.88/20.87 tff(c_3516, 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))). % 32.88/20.87 tff(c_3737, 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))). % 32.88/20.87 tff(c_3894, 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))). % 32.88/20.88 tff(c_4019, 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))). % 32.88/20.88 tff(c_3482, 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))). % 32.88/20.88 tff(c_3979, 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))). % 32.88/20.88 tff(c_15462, 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))). % 32.88/20.88 tff(c_3941, 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))). % 32.88/20.88 tff(c_3740, 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))). % 32.88/20.88 tff(c_3897, 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))). % 32.88/20.88 tff(c_3445, 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))). % 32.88/20.88 tff(c_3564, 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))). % 32.88/20.88 tff(c_3561, 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))). % 32.88/20.88 tff(c_15465, 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))). % 32.88/20.88 tff(c_3658, 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))). % 32.88/20.88 tff(c_3775, 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))). % 32.88/20.88 tff(c_3976, 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))). % 32.88/20.88 tff(c_3698, 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))). % 32.88/20.88 tff(c_3615, 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))). % 32.88/20.88 tff(c_3442, 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))). % 32.88/20.88 tff(c_3519, 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))). % 32.88/20.88 tff(c_3612, 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))). % 32.88/20.88 tff(c_3858, 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))). % 32.88/20.88 tff(c_3855, 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))). % 32.88/20.88 tff(c_3655, 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))). % 32.88/20.88 tff(c_3828, 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))). % 32.88/20.88 tff(c_3479, 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))). % 32.88/20.88 tff(c_4022, 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))). % 32.88/20.88 tff(c_3938, 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))). % 32.88/20.88 tff(c_2078, plain, (![P_96, X_62, Y_99]: (ifeq(iext(uri_rdfs_domain, P_96, uri_rdfs_Resource), true, ifeq(iext(P_96, X_62, Y_99), true, true, true), true)=true))). % 32.88/20.88 tff(c_1704, plain, (![P_92, X_94, X_62]: (ifeq(iext(uri_rdfs_range, P_92, uri_rdfs_Resource), true, ifeq(iext(P_92, X_94, X_62), true, true, true), true)=true))). % 32.88/20.88 tff(c_2627, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdf_type), true, ifeq(iext(P_103, uri_rdf_object, uri_rdf_Property), true, true, true), true)=true))). % 32.88/20.88 tff(c_2519, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdfs_range), true, ifeq(iext(P_103, uri_rdfs_subClassOf, uri_rdfs_Class), true, true, true), true)=true))). % 32.88/20.88 tff(c_39264, 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))). % 32.88/20.88 tff(c_2633, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdfs_domain), true, ifeq(iext(P_103, uri_rdf__3, uri_rdfs_Resource), true, true, true), true)=true))). % 32.88/20.88 tff(c_2645, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdf_type), true, ifeq(iext(P_103, uri_rdf__1, uri_rdfs_ContainerMembershipProperty), true, true, true), true)=true))). % 32.88/20.88 tff(c_2876, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdf_type), true, ifeq(iext(P_103, uri_rdf_subject, uri_rdf_Property), true, true, true), true)=true))). % 32.88/20.88 tff(c_2735, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdfs_subClassOf), true, ifeq(iext(P_103, uri_rdf_Alt, uri_rdfs_Container), true, true, true), true)=true))). % 32.88/20.88 tff(c_2753, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdfs_range), true, ifeq(iext(P_103, uri_rdfs_member, uri_rdfs_Resource), true, true, true), true)=true))). % 32.88/20.88 tff(c_2687, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdfs_domain), true, ifeq(iext(P_103, uri_rdf_subject, uri_rdfs_Statement), true, true, true), true)=true))). % 32.88/20.88 tff(c_2813, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdfs_domain), true, ifeq(iext(P_103, uri_rdfs_member, uri_rdfs_Resource), true, true, true), true)=true))). % 32.88/20.88 tff(c_2591, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdfs_subClassOf), true, ifeq(iext(P_103, uri_rdfs_Datatype, uri_rdfs_Class), true, true, true), true)=true))). % 32.88/20.88 tff(c_2864, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdf_type), true, ifeq(iext(P_103, uri_rdf_first, uri_rdf_Property), true, true, true), true)=true))). % 32.88/20.88 tff(c_2621, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdf_type), true, ifeq(iext(P_103, uri_rdf__1, uri_rdf_Property), true, true, true), true)=true))). % 32.88/20.88 tff(c_2639, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdfs_domain), true, ifeq(iext(P_103, uri_rdfs_comment, uri_rdfs_Resource), true, true, true), true)=true))). % 32.88/20.88 tff(c_2900, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdfs_range), true, ifeq(iext(P_103, uri_rdf_value, uri_rdfs_Resource), true, true, true), true)=true))). % 32.88/20.88 tff(c_2729, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdf_type), true, ifeq(iext(P_103, uri_rdf__2, uri_rdfs_ContainerMembershipProperty), true, true, true), true)=true))). % 32.88/20.88 tff(c_2579, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdfs_domain), true, ifeq(iext(P_103, uri_rdfs_subClassOf, uri_rdfs_Class), true, true, true), true)=true))). % 32.88/20.88 tff(c_2894, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdfs_domain), true, ifeq(iext(P_103, uri_rdfs_range, uri_rdf_Property), true, true, true), true)=true))). % 32.88/20.88 tff(c_2846, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdfs_range), true, ifeq(iext(P_103, uri_rdf__3, uri_rdfs_Resource), true, true, true), true)=true))). % 32.88/20.88 tff(c_2711, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdfs_range), true, ifeq(iext(P_103, uri_rdfs_comment, uri_rdfs_Literal), true, true, true), true)=true))). % 32.88/20.88 tff(c_2525, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdfs_range), true, ifeq(iext(P_103, uri_rdfs_label, uri_rdfs_Literal), true, true, true), true)=true))). % 32.88/20.88 tff(c_2795, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdfs_subClassOf), true, ifeq(iext(P_103, uri_rdfs_ContainerMembershipProperty, uri_rdf_Property), true, true, true), true)=true))). % 32.88/20.88 tff(c_2663, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdfs_domain), true, ifeq(iext(P_103, uri_rdf_type, uri_rdfs_Resource), true, true, true), true)=true))). % 32.88/20.88 tff(c_2699, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdf_type), true, ifeq(iext(P_103, uri_rdf_value, uri_rdf_Property), true, true, true), true)=true))). % 32.88/20.88 tff(c_2834, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdf_type), true, ifeq(iext(P_103, uri_rdf__2, uri_rdf_Property), true, true, true), true)=true))). % 32.88/20.88 tff(c_2681, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdf_type), true, ifeq(iext(P_103, uri_rdf_Property, uri_rdfs_Class), true, true, true), true)=true))). % 32.88/20.88 tff(c_2783, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdfs_domain), true, ifeq(iext(P_103, uri_rdfs_label, uri_rdfs_Resource), true, true, true), true)=true))). % 32.88/20.88 tff(c_2840, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdfs_range), true, ifeq(iext(P_103, uri_rdf_predicate, uri_rdfs_Resource), true, true, true), true)=true))). % 32.88/20.88 tff(c_36134, plain, (![C_791]: (ifeq(iext(uri_rdfs_subClassOf, C_791, uri_rdf_XMLLiteral), true, iext(uri_rdfs_subClassOf, C_791, uri_rdfs_Literal), true)=true))). % 32.88/20.88 tff(c_2852, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdfs_range), true, ifeq(iext(P_103, uri_rdf_first, uri_rdfs_Resource), true, true, true), true)=true))). % 32.88/20.88 tff(c_2675, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdfs_subClassOf), true, ifeq(iext(P_103, uri_rdfs_Seq, uri_rdfs_Container), true, true, true), true)=true))). % 32.88/20.88 tff(c_2723, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdfs_domain), true, ifeq(iext(P_103, uri_rdfs_seeAlso, uri_rdfs_Resource), true, true, true), true)=true))). % 32.88/20.88 tff(c_2882, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdfs_domain), true, ifeq(iext(P_103, uri_rdf_predicate, uri_rdfs_Statement), true, true, true), true)=true))). % 32.88/20.88 tff(c_2543, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdf_type), true, ifeq(iext(P_103, uri_rdf__3, uri_rdfs_ContainerMembershipProperty), true, true, true), true)=true))). % 32.88/20.88 tff(c_2828, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdfs_subPropertyOf), true, ifeq(iext(P_103, uri_rdfs_isDefinedBy, uri_rdfs_seeAlso), true, true, true), true)=true))). % 32.88/20.88 tff(c_2801, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdfs_range), true, ifeq(iext(P_103, uri_rdfs_seeAlso, uri_rdfs_Resource), true, true, true), true)=true))). % 32.88/20.88 tff(c_2537, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdfs_domain), true, ifeq(iext(P_103, uri_rdf_first, uri_rdf_List), true, true, true), true)=true))). % 32.88/20.88 tff(c_2819, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdfs_domain), true, ifeq(iext(P_103, uri_rdf_object, uri_rdfs_Statement), true, true, true), true)=true))). % 32.88/20.88 tff(c_2759, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdfs_subClassOf), true, ifeq(iext(P_103, uri_rdf_Bag, uri_rdfs_Container), true, true, true), true)=true))). % 32.88/20.88 tff(c_2567, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdfs_domain), true, ifeq(iext(P_103, uri_rdf_value, uri_rdfs_Resource), true, true, true), true)=true))). % 32.88/20.88 tff(c_2858, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdfs_range), true, ifeq(iext(P_103, uri_rdfs_range, uri_rdfs_Class), true, true, true), true)=true))). % 32.88/20.88 tff(c_2651, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdfs_range), true, ifeq(iext(P_103, uri_rdfs_subPropertyOf, uri_rdf_Property), true, true, true), true)=true))). % 32.88/20.88 tff(c_2657, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdfs_domain), true, ifeq(iext(P_103, uri_rdfs_subPropertyOf, uri_rdf_Property), true, true, true), true)=true))). % 32.88/20.88 tff(c_2555, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdfs_domain), true, ifeq(iext(P_103, uri_rdf_rest, uri_rdf_List), true, true, true), true)=true))). % 32.88/20.88 tff(c_2585, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdf_type), true, ifeq(iext(P_103, uri_rdf_rest, uri_rdf_Property), true, true, true), true)=true))). % 32.88/20.88 tff(c_34092, plain, (![C_773]: (ifeq(iext(uri_rdfs_subClassOf, C_773, uri_rdfs_Seq), true, iext(uri_rdfs_subClassOf, C_773, uri_rdfs_Container), true)=true))). % 32.88/20.88 tff(c_34041, plain, (![P_771]: (ifeq(iext(uri_rdfs_subPropertyOf, P_771, uri_rdfs_isDefinedBy), true, iext(uri_rdfs_subPropertyOf, P_771, uri_rdfs_seeAlso), true)=true))). % 32.88/20.88 tff(c_2789, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdf_first), true, ifeq(iext(P_103, sK3_testcase_premise_fullish_027_Inferred_Property_Characteristics_II_BNODE_l2, sK1_testcase_premise_fullish_027_Inferred_Property_Characteristics_II_BNODE_v), true, true, true), true)=true))). % 32.88/20.88 tff(c_33855, plain, (![D_768]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_768), true, icext(D_768, uri_rdfs_Resource), true)=true))). % 32.88/20.88 tff(c_33789, plain, (![D_766]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_766), true, icext(D_766, uri_rdfs_domain), true)=true))). % 32.88/20.88 tff(c_33594, plain, (![D_763]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_763), true, icext(D_763, uri_rdfs_seeAlso), true)=true))). % 32.88/20.88 tff(c_2747, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdfs_range), true, ifeq(iext(P_103, uri_rdf__2, uri_rdfs_Resource), true, true, true), true)=true))). % 32.88/20.88 tff(c_33528, plain, (![D_761]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_761), true, icext(D_761, uri_owl_inverseOf), true)=true))). % 32.88/20.88 tff(c_33462, plain, (![D_759]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_759), true, icext(D_759, uri_rdfs_subPropertyOf), true)=true))). % 32.88/20.88 tff(c_33276, plain, (![D_756]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_756), true, icext(D_756, uri_rdfs_subClassOf), true)=true))). % 32.88/20.88 tff(c_2603, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdf_first), true, ifeq(iext(P_103, sK2_testcase_premise_fullish_027_Inferred_Property_Characteristics_II_BNODE_l1, uri_ex_p), true, true, true), true)=true))). % 32.88/20.88 tff(c_33210, plain, (![D_754]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_754), true, icext(D_754, uri_owl_propertyChainAxiom), true)=true))). % 32.88/20.88 tff(c_33144, plain, (![D_752]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_752), true, icext(D_752, uri_rdfs_isDefinedBy), true)=true))). % 32.88/20.88 tff(c_2573, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdf_type), true, ifeq(iext(P_103, uri_rdf_nil, uri_rdf_List), true, true, true), true)=true))). % 32.88/20.88 tff(c_32956, plain, (![D_749]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_749), true, icext(D_749, uri_rdfs_Container), true)=true))). % 32.88/20.88 tff(c_32890, plain, (![D_747]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_747), true, icext(D_747, uri_rdf_Bag), true)=true))). % 32.88/20.88 tff(c_32671, plain, (![D_744]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_744), true, icext(D_744, uri_rdfs_Class), true)=true))). % 32.88/20.88 tff(c_2717, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdfs_domain), true, ifeq(iext(P_103, uri_rdfs_domain, uri_rdf_Property), true, true, true), true)=true))). % 32.88/20.88 tff(c_32605, plain, (![D_742]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_742), true, icext(D_742, uri_rdfs_Seq), true)=true))). % 32.88/20.88 tff(c_32416, plain, (![D_739]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_739), true, icext(D_739, uri_rdfs_Literal), true)=true))). % 32.88/20.88 tff(c_2615, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdfs_range), true, ifeq(iext(P_103, uri_rdfs_domain, uri_rdfs_Class), true, true, true), true)=true))). % 32.88/20.88 tff(c_32350, plain, (![D_737]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_737), true, icext(D_737, uri_rdf_Alt), true)=true))). % 32.88/20.88 tff(c_32284, plain, (![D_735]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_735), true, icext(D_735, uri_rdfs_Datatype), true)=true))). % 32.88/20.88 tff(c_2906, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdf_rest), true, ifeq(iext(P_103, sK3_testcase_premise_fullish_027_Inferred_Property_Characteristics_II_BNODE_l2, uri_rdf_nil), true, true, true), true)=true))). % 32.88/20.89 tff(c_32089, plain, (![D_732]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_732), true, icext(D_732, uri_rdf_XMLLiteral), true)=true))). % 32.88/20.89 tff(c_32023, plain, (![D_730]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_730), true, icext(D_730, uri_rdfs_ContainerMembershipProperty), true)=true))). % 32.88/20.89 tff(c_31835, plain, (![D_727]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_727), true, icext(D_727, uri_rdf_List), true)=true))). % 32.88/20.89 tff(c_2597, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_owl_propertyChainAxiom), true, ifeq(iext(P_103, uri_owl_sameAs, sK2_testcase_premise_fullish_027_Inferred_Property_Characteristics_II_BNODE_l1), true, true, true), true)=true))). % 32.88/20.89 tff(c_31769, plain, (![D_725]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_725), true, icext(D_725, uri_rdfs_comment), true)=true))). % 32.88/20.89 tff(c_31703, plain, (![D_723]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_723), true, icext(D_723, uri_rdfs_label), true)=true))). % 32.88/20.89 tff(c_31517, plain, (![D_720]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_720), true, icext(D_720, uri_rdfs_range), true)=true))). % 32.88/20.89 tff(c_2609, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdf_type), true, ifeq(iext(P_103, uri_rdf__3, uri_rdf_Property), true, true, true), true)=true))). % 32.88/20.89 tff(c_31451, plain, (![D_718]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_List, D_718), true, icext(D_718, sK2_testcase_premise_fullish_027_Inferred_Property_Characteristics_II_BNODE_l1), true)=true))). % 32.88/20.89 tff(c_31385, plain, (![D_716]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_716), true, icext(D_716, uri_rdfs_member), true)=true))). % 32.88/20.89 tff(c_31190, plain, (![D_713]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_713), true, icext(D_713, uri_rdf_predicate), true)=true))). % 32.88/20.89 tff(c_2693, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdfs_range), true, ifeq(iext(P_103, uri_rdf__1, uri_rdfs_Resource), true, true, true), true)=true))). % 32.88/20.89 tff(c_14895, 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))). % 32.88/20.89 tff(c_31086, plain, (![D_709]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_List, D_709), true, icext(D_709, sK3_testcase_premise_fullish_027_Inferred_Property_Characteristics_II_BNODE_l2), true)=true))). % 32.88/20.89 tff(c_30996, plain, (![C_706]: (ifeq(iext(uri_rdfs_subClassOf, C_706, uri_rdf_Bag), true, iext(uri_rdfs_subClassOf, C_706, uri_rdfs_Container), true)=true))). % 32.88/20.89 tff(c_14845, 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))). % 32.88/20.89 tff(c_14751, 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))). % 32.88/20.89 tff(c_17004, 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))). % 32.88/20.89 tff(c_30885, plain, (![D_701]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_701), true, icext(D_701, uri_rdf_subject), true)=true))). % 32.88/20.89 tff(c_30835, plain, (![X_696, Y_697]: (ifeq(iext(uri_rdfs_isDefinedBy, X_696, Y_697), true, iext(uri_rdfs_seeAlso, X_696, Y_697), true)=true))). % 32.88/20.89 tff(c_14614, 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))). % 32.88/20.89 tff(c_30703, plain, (![D_691]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_691), true, icext(D_691, uri_rdf_Property), true)=true))). % 32.88/20.89 tff(c_14685, 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))). % 32.88/20.89 tff(c_30637, plain, (![C_688]: (ifeq(iext(uri_rdfs_subClassOf, C_688, uri_rdfs_ContainerMembershipProperty), true, iext(uri_rdfs_subClassOf, C_688, uri_rdf_Property), true)=true))). % 32.88/20.89 tff(c_14418, 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))). % 32.88/20.89 tff(c_14416, 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))). % 32.88/20.89 tff(c_14331, 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))). % 32.88/20.89 tff(c_13438, 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))). % 32.88/20.89 tff(c_15769, 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))). % 32.88/20.89 tff(c_14264, 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))). % 32.88/20.89 tff(c_13485, 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))). % 32.88/20.89 tff(c_2741, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_owl_inverseOf), true, ifeq(iext(P_103, sK1_testcase_premise_fullish_027_Inferred_Property_Characteristics_II_BNODE_v, uri_ex_p), true, true, true), true)=true))). % 32.88/20.89 tff(c_13389, 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))). % 32.88/20.89 tff(c_13605, 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))). % 32.88/20.89 tff(c_15771, 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))). % 32.88/20.89 tff(c_13268, 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))). % 32.88/20.89 tff(c_15973, 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))). % 32.88/20.89 tff(c_13558, 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))). % 32.88/20.89 tff(c_13315, 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))). % 32.88/20.89 tff(c_2870, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdf_type), true, ifeq(iext(P_103, uri_rdf_type, uri_rdf_Property), true, true, true), true)=true))). % 32.88/20.89 tff(c_14190, 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))). % 32.88/20.89 tff(c_13090, 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))). % 32.88/20.89 tff(c_13192, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, sK2_testcase_premise_fullish_027_Inferred_Property_Characteristics_II_BNODE_l1, uri_rdf_List), true)=true))). % 32.88/20.89 tff(c_15130, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, sK3_testcase_premise_fullish_027_Inferred_Property_Characteristics_II_BNODE_l2, uri_rdf_List), true)=true))). % 32.88/20.89 tff(c_13143, 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))). % 32.88/20.89 tff(c_14077, 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))). % 32.88/20.89 tff(c_13727, 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))). % 32.88/20.89 tff(c_16876, 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))). % 32.88/20.89 tff(c_2549, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdfs_subClassOf), true, ifeq(iext(P_103, uri_rdf_XMLLiteral, uri_rdfs_Literal), true, true, true), true)=true))). % 32.88/20.89 tff(c_7605, 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))). % 32.88/20.89 tff(c_12519, 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))). % 32.88/20.89 tff(c_7054, 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))). % 32.88/20.89 tff(c_11644, 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))). % 32.88/20.89 tff(c_6486, 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))). % 32.88/20.89 tff(c_2669, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdfs_range), true, ifeq(iext(P_103, uri_rdfs_isDefinedBy, uri_rdfs_Resource), true, true, true), true)=true))). % 32.88/20.89 tff(c_7750, 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))). % 32.88/20.89 tff(c_12228, 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))). % 32.88/20.89 tff(c_7748, 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))). % 32.88/20.89 tff(c_4973, 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))). % 32.88/20.89 tff(c_10727, 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))). % 32.88/20.89 tff(c_6359, 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))). % 32.88/20.89 tff(c_12171, 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))). % 32.88/20.89 tff(c_8192, 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))). % 32.88/20.89 tff(c_29239, plain, (![D_639]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_639), true, icext(D_639, uri_rdf_first), true)=true))). % 32.88/20.89 tff(c_4911, 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))). % 32.88/20.89 tff(c_5905, 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))). % 32.88/20.89 tff(c_12681, 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))). % 32.88/20.89 tff(c_7415, 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))). % 32.88/20.89 tff(c_6488, 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))). % 32.88/20.89 tff(c_6199, 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))). % 32.88/20.89 tff(c_5563, 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))). % 32.88/20.89 tff(c_11709, 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))). % 32.88/20.89 tff(c_9688, 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))). % 32.88/20.89 tff(c_2765, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdf_rest), true, ifeq(iext(P_103, sK2_testcase_premise_fullish_027_Inferred_Property_Characteristics_II_BNODE_l1, sK3_testcase_premise_fullish_027_Inferred_Property_Characteristics_II_BNODE_l2), true, true, true), true)=true))). % 32.88/20.89 tff(c_12683, 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))). % 32.88/20.89 tff(c_8787, 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))). % 32.88/20.89 tff(c_28753, plain, (![D_622]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_622), true, icext(D_622, uri_rdf_rest), true)=true))). % 32.88/20.89 tff(c_5323, 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))). % 32.88/20.89 tff(c_12615, 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))). % 32.88/20.89 tff(c_5084, 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))). % 32.88/20.89 tff(c_2561, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdf_type), true, ifeq(iext(P_103, uri_rdf_XMLLiteral, uri_rdfs_Datatype), true, true, true), true)=true))). % 32.88/20.89 tff(c_11899, 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))). % 32.88/20.89 tff(c_6828, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_48), true, iext(Q_48, uri_owl_propertyChainAxiom, uri_owl_propertyChainAxiom), true)=true))). % 32.88/20.89 tff(c_8441, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, uri_owl_propertyChainAxiom, uri_rdf_Property), true)=true))). % 32.88/20.89 tff(c_10327, 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))). % 32.88/20.89 tff(c_7417, 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))). % 32.88/20.89 tff(c_12878, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, uri_owl_inverseOf, uri_rdf_Property), true)=true))). % 32.88/20.89 tff(c_2807, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdfs_range), true, ifeq(iext(P_103, uri_rdf_type, uri_rdfs_Class), true, true, true), true)=true))). % 32.88/20.89 tff(c_11707, 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))). % 32.88/20.89 tff(c_28141, plain, (![D_604]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_604), true, icext(D_604, uri_rdf__1), true)=true))). % 32.88/20.89 tff(c_4741, 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))). % 32.88/20.89 tff(c_2888, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdfs_range), true, ifeq(iext(P_103, uri_rdf_rest, uri_rdf_List), true, true, true), true)=true))). % 32.88/20.89 tff(c_11460, 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))). % 32.88/20.89 tff(c_11643, 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))). % 32.88/20.89 tff(c_27829, plain, (![D_595]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_595), true, icext(D_595, uri_rdf__3), true)=true))). % 32.88/20.89 tff(c_8720, 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))). % 32.88/20.89 tff(c_7224, 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))). % 32.88/20.89 tff(c_2531, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdfs_range), true, ifeq(iext(P_103, uri_rdf_subject, uri_rdfs_Resource), true, true, true), true)=true))). % 32.88/20.89 tff(c_11897, 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))). % 32.88/20.89 tff(c_9190, 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))). % 32.88/20.89 tff(c_9937, 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))). % 32.88/20.89 tff(c_8935, 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))). % 32.88/20.89 tff(c_27456, plain, (![C_583]: (ifeq(iext(uri_rdfs_subClassOf, C_583, uri_rdfs_Datatype), true, iext(uri_rdfs_subClassOf, C_583, uri_rdfs_Class), true)=true))). % 32.88/20.89 tff(c_9750, 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))). % 32.88/20.89 tff(c_11147, 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))). % 32.88/20.89 tff(c_8785, 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))). % 32.88/20.89 tff(c_6884, 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))). % 32.88/20.89 tff(c_5082, 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))). % 32.88/20.89 tff(c_8641, 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))). % 32.88/20.89 tff(c_9417, 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))). % 32.88/20.89 tff(c_2777, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdfs_domain), true, ifeq(iext(P_103, uri_rdfs_isDefinedBy, uri_rdfs_Resource), true, true, true), true)=true))). % 32.88/20.89 tff(c_10422, 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))). % 32.88/20.89 tff(c_4810, 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))). % 32.88/20.89 tff(c_7889, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_48), true, iext(Q_48, uri_owl_inverseOf, uri_owl_inverseOf), true)=true))). % 32.88/20.89 tff(c_12453, 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))). % 32.88/20.90 tff(c_2705, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdfs_domain), true, ifeq(iext(P_103, uri_rdf__1, uri_rdfs_Resource), true, true, true), true)=true))). % 32.88/20.90 tff(c_7222, 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))). % 32.88/20.90 tff(c_10122, 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))). % 32.88/20.90 tff(c_10421, 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))). % 32.88/20.90 tff(c_8137, 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))). % 32.88/20.90 tff(c_9191, 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))). % 32.88/20.90 tff(c_2771, plain, (![P_103]: (ifeq(iext(uri_rdfs_subPropertyOf, P_103, uri_rdfs_domain), true, ifeq(iext(P_103, uri_rdf__2, uri_rdfs_Resource), true, true, true), true)=true))). % 32.88/20.90 tff(c_9282, 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))). % 32.88/20.90 tff(c_7052, 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))). % 32.88/20.90 tff(c_15707, 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))). % 32.88/20.90 tff(c_26449, plain, (![D_551]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_List, D_551), true, icext(D_551, uri_rdf_nil), true)=true))). % 32.88/20.90 tff(c_4681, plain, (![Q_48, X_140]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, X_140, uri_rdfs_Resource), true)=true))). % 32.88/20.90 tff(c_2938, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_104), true, iext(Q_104, uri_rdf_Property, uri_rdfs_Class), true)=true))). % 32.88/20.90 tff(c_2950, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_104), true, iext(Q_104, uri_rdfs_member, uri_rdfs_Resource), true)=true))). % 32.88/20.90 tff(c_2964, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_104), true, iext(Q_104, uri_rdf_predicate, uri_rdfs_Resource), true)=true))). % 32.88/20.90 tff(c_2963, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_104), true, iext(Q_104, uri_rdf__2, uri_rdf_Property), true)=true))). % 32.88/20.90 tff(c_3045, plain, (![E_108]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, E_108), true, iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, E_108), true)=true))). % 32.88/20.90 tff(c_2941, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_104), true, iext(Q_104, uri_rdf_value, uri_rdf_Property), true)=true))). % 32.88/20.90 tff(c_26094, plain, (![D_541]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, D_541), true, icext(D_541, uri_rdf__3), true)=true))). % 32.88/20.90 tff(c_2957, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_104), true, iext(Q_104, uri_rdfs_ContainerMembershipProperty, uri_rdf_Property), true)=true))). % 32.88/20.90 tff(c_2971, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_104), true, iext(Q_104, uri_rdf_predicate, uri_rdfs_Statement), true)=true))). % 32.88/20.90 tff(c_2911, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_104), true, iext(Q_104, uri_rdfs_subClassOf, uri_rdfs_Class), true)=true))). % 32.88/20.90 tff(c_2918, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_104), true, iext(Q_104, uri_rdf_XMLLiteral, uri_rdfs_Datatype), true)=true))). % 32.88/20.90 tff(c_2915, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_104), true, iext(Q_104, uri_rdf__3, uri_rdfs_ContainerMembershipProperty), true)=true))). % 32.88/20.90 tff(c_2951, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_104), true, iext(Q_104, uri_rdf_Bag, uri_rdfs_Container), true)=true))). % 32.88/20.90 tff(c_2939, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_104), true, iext(Q_104, uri_rdf_subject, uri_rdfs_Statement), true)=true))). % 32.88/20.90 tff(c_2969, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_104), true, iext(Q_104, uri_rdf_type, uri_rdf_Property), true)=true))). % 32.88/20.90 tff(c_2923, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_104), true, iext(Q_104, uri_rdfs_Datatype, uri_rdfs_Class), true)=true))). % 32.88/20.90 tff(c_2960, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_104), true, iext(Q_104, uri_rdfs_member, uri_rdfs_Resource), true)=true))). % 32.88/20.90 tff(c_2928, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_104), true, iext(Q_104, uri_rdf__1, uri_rdf_Property), true)=true))). % 32.88/20.90 tff(c_2966, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_104), true, iext(Q_104, uri_rdf_first, uri_rdfs_Resource), true)=true))). % 32.88/20.90 tff(c_2948, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_owl_inverseOf, Q_104), true, iext(Q_104, sK1_testcase_premise_fullish_027_Inferred_Property_Characteristics_II_BNODE_v, uri_ex_p), true)=true))). % 32.88/20.90 tff(c_2970, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_104), true, iext(Q_104, uri_rdf_subject, uri_rdf_Property), true)=true))). % 32.88/20.90 tff(c_2913, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_104), true, iext(Q_104, uri_rdf_subject, uri_rdfs_Resource), true)=true))). % 32.88/20.90 tff(c_3040, plain, (![E_108]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Literal, E_108), true, iext(uri_rdfs_subClassOf, uri_rdf_XMLLiteral, E_108), true)=true))). % 32.88/20.90 tff(c_25730, plain, (![D_523]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_523), true, icext(D_523, uri_rdf__2), true)=true))). % 32.88/20.90 tff(c_2926, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_104), true, iext(Q_104, uri_rdf__3, uri_rdf_Property), true)=true))). % 32.88/20.90 tff(c_2953, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_104), true, iext(Q_104, uri_rdf__2, uri_rdfs_Resource), true)=true))). % 32.88/20.90 tff(c_3042, plain, (![E_108]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Container, E_108), true, iext(uri_rdfs_subClassOf, uri_rdfs_Seq, E_108), true)=true))). % 32.88/20.90 tff(c_2920, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_104), true, iext(Q_104, uri_rdf_nil, uri_rdf_List), true)=true))). % 32.88/20.90 tff(c_3043, plain, (![E_108]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Container, E_108), true, iext(uri_rdfs_subClassOf, uri_rdf_Alt, E_108), true)=true))). % 32.88/20.90 tff(c_2975, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_rest, Q_104), true, iext(Q_104, sK3_testcase_premise_fullish_027_Inferred_Property_Characteristics_II_BNODE_l2, uri_rdf_nil), true)=true))). % 32.88/20.90 tff(c_2912, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_104), true, iext(Q_104, uri_rdfs_label, uri_rdfs_Literal), true)=true))). % 32.88/20.90 tff(c_25510, plain, (![D_514]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, D_514), true, icext(D_514, uri_rdf__2), true)=true))). % 32.88/20.90 tff(c_2959, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_104), true, iext(Q_104, uri_rdf_type, uri_rdfs_Class), true)=true))). % 32.88/20.90 tff(c_2930, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_104), true, iext(Q_104, uri_rdf__3, uri_rdfs_Resource), true)=true))). % 32.88/20.90 tff(c_2961, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_104), true, iext(Q_104, uri_rdf_object, uri_rdfs_Statement), true)=true))). % 32.88/20.90 tff(c_2952, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_rest, Q_104), true, iext(Q_104, sK2_testcase_premise_fullish_027_Inferred_Property_Characteristics_II_BNODE_l1, sK3_testcase_premise_fullish_027_Inferred_Property_Characteristics_II_BNODE_l2), true)=true))). % 32.88/20.90 tff(c_2949, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_104), true, iext(Q_104, uri_rdf__2, uri_rdfs_Resource), true)=true))). % 32.88/20.90 tff(c_2924, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_owl_propertyChainAxiom, Q_104), true, iext(Q_104, uri_owl_sameAs, sK2_testcase_premise_fullish_027_Inferred_Property_Characteristics_II_BNODE_l1), true)=true))). % 32.88/20.90 tff(c_2936, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_104), true, iext(Q_104, uri_rdfs_isDefinedBy, uri_rdfs_Resource), true)=true))). % 32.88/20.90 tff(c_25296, plain, (![D_505]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, D_505), true, icext(D_505, uri_rdf__1), true)=true))). % 32.88/20.90 tff(c_2934, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_104), true, iext(Q_104, uri_rdfs_subPropertyOf, uri_rdf_Property), true)=true))). % 32.88/20.90 tff(c_2962, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_104), true, iext(Q_104, uri_rdfs_isDefinedBy, uri_rdfs_seeAlso), true)=true))). % 32.88/20.90 tff(c_2972, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_104), true, iext(Q_104, uri_rdf_rest, uri_rdf_List), true)=true))). % 32.88/20.90 tff(c_2974, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_104), true, iext(Q_104, uri_rdf_value, uri_rdfs_Resource), true)=true))). % 32.88/20.90 tff(c_2935, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_104), true, iext(Q_104, uri_rdf_type, uri_rdfs_Resource), true)=true))). % 32.88/20.90 tff(c_2944, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_104), true, iext(Q_104, uri_rdfs_domain, uri_rdf_Property), true)=true))). % 32.88/20.90 tff(c_2927, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_104), true, iext(Q_104, uri_rdfs_domain, uri_rdfs_Class), true)=true))). % 32.88/20.90 tff(c_25069, plain, (![D_496]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, D_496), true, icext(D_496, uri_rdf_XMLLiteral), true)=true))). % 32.88/20.90 tff(c_2955, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_104), true, iext(Q_104, uri_rdfs_label, uri_rdfs_Resource), true)=true))). % 32.88/20.90 tff(c_2956, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_first, Q_104), true, iext(Q_104, sK3_testcase_premise_fullish_027_Inferred_Property_Characteristics_II_BNODE_l2, sK1_testcase_premise_fullish_027_Inferred_Property_Characteristics_II_BNODE_v), true)=true))). % 32.88/20.90 tff(c_2925, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_first, Q_104), true, iext(Q_104, sK2_testcase_premise_fullish_027_Inferred_Property_Characteristics_II_BNODE_l1, uri_ex_p), true)=true))). % 32.88/20.90 tff(c_2922, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_104), true, iext(Q_104, uri_rdf_rest, uri_rdf_Property), true)=true))). % 32.88/20.90 tff(c_2931, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_104), true, iext(Q_104, uri_rdfs_comment, uri_rdfs_Resource), true)=true))). % 32.88/20.90 tff(c_2943, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_104), true, iext(Q_104, uri_rdfs_comment, uri_rdfs_Literal), true)=true))). % 32.88/20.90 tff(c_2919, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_104), true, iext(Q_104, uri_rdf_value, uri_rdfs_Resource), true)=true))). % 32.88/20.90 tff(c_24879, plain, (![D_487]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_487), true, icext(D_487, uri_rdf_object), true)=true))). % 32.88/20.90 tff(c_14755, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_predicate), true)=true))). % 32.88/20.90 tff(c_2921, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_104), true, iext(Q_104, uri_rdfs_subClassOf, uri_rdfs_Class), true)=true))). % 32.88/20.90 tff(c_14849, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_label), true)=true))). % 32.88/20.90 tff(c_17007, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_comment), true)=true))). % 32.88/20.90 tff(c_17008, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_comment), true)=true))). % 32.88/20.90 tff(c_24692, plain, (![D_480]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_480), true, icext(D_480, uri_rdf_type), true)=true))). % 32.88/20.90 tff(c_14754, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_predicate), true)=true))). % 32.88/20.90 tff(c_14848, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_label), true)=true))). % 32.88/20.90 tff(c_2954, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_104), true, iext(Q_104, uri_rdfs_isDefinedBy, uri_rdfs_Resource), true)=true))). % 32.88/20.90 tff(c_14688, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_member), true)=true))). % 32.88/20.90 tff(c_14615, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdfs_Resource), true)=true))). % 32.88/20.90 tff(c_24500, plain, (![D_473]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_473), true, icext(D_473, uri_rdfs_Statement), true)=true))). % 32.88/20.90 tff(c_14333, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdf_List), true)=true))). % 32.88/20.90 tff(c_14419, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdf_List), true)=true))). % 32.88/20.90 tff(c_3044, plain, (![E_108]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Container, E_108), true, iext(uri_rdfs_subClassOf, uri_rdf_Bag, E_108), true)=true))). % 32.88/20.90 tff(c_24353, plain, (![D_468]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_468), true, icext(D_468, uri_rdf_value), true)=true))). % 32.88/20.90 tff(c_2945, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_104), true, iext(Q_104, uri_rdfs_seeAlso, uri_rdfs_Resource), true)=true))). % 32.88/20.90 tff(c_15975, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdfs_Statement), true)=true))). % 32.88/20.90 tff(c_2916, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_104), true, iext(Q_104, uri_rdf_XMLLiteral, uri_rdfs_Literal), true)=true))). % 32.88/20.90 tff(c_15974, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdfs_Statement), true)=true))). % 32.88/20.90 tff(c_3041, plain, (![E_108]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, E_108), true, iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, E_108), true)=true))). % 32.88/20.90 tff(c_2937, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_104), true, iext(Q_104, uri_rdfs_Seq, uri_rdfs_Container), true)=true))). % 32.88/20.90 tff(c_24019, plain, (![C_89, X_62]: (ifeq(icext(C_89, X_62), true, true, true)=true))). % 32.88/20.90 tff(c_10329, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdfs_ContainerMembershipProperty), true)=true))). % 32.88/20.90 tff(c_2968, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_104), true, iext(Q_104, uri_rdf_first, uri_rdf_Property), true)=true))). % 32.88/20.90 tff(c_23574, plain, (![D_454, X_455]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Resource, D_454), true, icext(D_454, X_455), true)=true))). % 32.88/20.90 tff(c_8140, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf__2), true)=true))). % 32.88/20.90 tff(c_2914, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_104), true, iext(Q_104, uri_rdf_first, uri_rdf_List), true)=true))). % 32.88/20.90 tff(c_5325, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_seeAlso), true)=true))). % 32.88/20.90 tff(c_10731, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_object), true)=true))). % 32.88/20.90 tff(c_7892, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_owl_inverseOf), true)=true))). % 32.88/20.90 tff(c_23053, plain, (![X_445, Y_446]: (ifeq(iext(uri_rdfs_domain, X_445, Y_446), true, icext(uri_rdf_Property, X_445), true)=true))). % 32.88/20.90 tff(c_7607, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_range), true)=true))). % 32.88/20.90 tff(c_4975, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_subClassOf), true)=true))). % 32.88/20.90 tff(c_6361, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_domain), true)=true))). % 32.88/20.90 tff(c_2973, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_104), true, iext(Q_104, uri_rdfs_range, uri_rdf_Property), true)=true))). % 32.88/20.90 tff(c_8724, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_type), true)=true))). % 32.88/20.90 tff(c_22520, plain, (![X_436, Y_437]: (ifeq(iext(uri_rdfs_subPropertyOf, X_436, Y_437), true, icext(uri_rdf_Property, Y_437), true)=true))). % 32.88/20.90 tff(c_10730, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_object), true)=true))). % 32.88/20.90 tff(c_5085, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdf_Property), true)=true))). % 32.88/20.90 tff(c_2917, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_104), true, iext(Q_104, uri_rdf_rest, uri_rdf_List), true)=true))). % 32.88/20.90 tff(c_11462, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdfs_Seq), true)=true))). % 32.88/20.90 tff(c_12175, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_subject), true)=true))). % 32.88/20.90 tff(c_22367, plain, (![X_427, Y_428]: (ifeq(iext(uri_rdf_predicate, X_427, Y_428), true, icext(uri_rdfs_Statement, X_427), true)=true))). % 32.88/20.90 tff(c_2946, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_104), true, iext(Q_104, uri_rdf__2, uri_rdfs_ContainerMembershipProperty), true)=true))). % 32.88/20.90 tff(c_12521, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdfs_Datatype), true)=true))). % 32.88/20.90 tff(c_22238, plain, (![X_421, Y_422]: (ifeq(iext(uri_rdf_rest, X_421, Y_422), true, icext(uri_rdf_List, X_421), true)=true))). % 32.88/20.90 tff(c_11150, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_subPropertyOf), true)=true))). % 32.88/20.90 tff(c_2942, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_104), true, iext(Q_104, uri_rdf__1, uri_rdfs_Resource), true)=true))). % 32.88/20.90 tff(c_10424, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_member), true)=true))). % 32.88/20.90 tff(c_4743, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdf_XMLLiteral), true)=true))). % 32.88/20.90 tff(c_21728, plain, (![X_413, Y_414]: (ifeq(iext(uri_rdfs_subPropertyOf, X_413, Y_414), true, icext(uri_rdf_Property, X_413), true)=true))). % 32.88/20.90 tff(c_9753, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf__3), true)=true))). % 32.88/20.91 tff(c_8938, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_rest), true)=true))). % 32.88/20.91 tff(c_9692, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf__1), true)=true))). % 32.88/20.91 tff(c_2940, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_104), true, iext(Q_104, uri_rdf__1, uri_rdfs_Resource), true)=true))). % 32.88/20.91 tff(c_21586, plain, (![X_405, Y_406]: (ifeq(iext(uri_rdf_object, X_405, Y_406), true, icext(uri_rdfs_Statement, X_405), true)=true))). % 32.88/20.91 tff(c_6201, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdf_Alt), true)=true))). % 32.88/20.91 tff(c_11645, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf__3), true)=true))). % 32.88/20.91 tff(c_2436, plain, (![R_101]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_seeAlso, R_101), true, iext(uri_rdfs_subPropertyOf, uri_rdfs_isDefinedBy, R_101), true)=true))). % 32.88/20.91 tff(c_10125, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_value), true)=true))). % 32.88/20.91 tff(c_9420, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_first), true)=true))). % 32.88/20.91 tff(c_21429, plain, (![X_396, Y_397]: (ifeq(iext(uri_rdfs_label, X_396, Y_397), true, icext(uri_rdfs_Literal, Y_397), true)=true))). % 32.88/20.91 tff(c_2933, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_104), true, iext(Q_104, uri_rdfs_subPropertyOf, uri_rdf_Property), true)=true))). % 32.88/20.91 tff(c_8723, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_type), true)=true))). % 32.88/20.91 tff(c_9421, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_first), true)=true))). % 32.88/20.91 tff(c_21024, plain, (![X_389, Y_390]: (ifeq(iext(uri_rdfs_range, X_389, Y_390), true, icext(uri_rdfs_Class, Y_390), true)=true))). % 32.88/20.91 tff(c_12619, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_isDefinedBy), true)=true))). % 32.88/20.91 tff(c_2947, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_104), true, iext(Q_104, uri_rdf_Alt, uri_rdfs_Container), true)=true))). % 32.88/20.91 tff(c_12174, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_subject), true)=true))). % 32.88/20.91 tff(c_11151, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_subPropertyOf), true)=true))). % 32.88/20.91 tff(c_20847, plain, (![X_381, Y_382]: (ifeq(iext(uri_rdf_first, X_381, Y_382), true, icext(uri_rdf_List, X_381), true)=true))). % 32.88/20.91 tff(c_10126, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_value), true)=true))). % 32.88/20.91 tff(c_4976, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_subClassOf), true)=true))). % 32.88/20.91 tff(c_9193, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf__1), true)=true))). % 32.88/20.91 tff(c_2958, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_104), true, iext(Q_104, uri_rdfs_seeAlso, uri_rdfs_Resource), true)=true))). % 32.88/20.91 tff(c_20088, plain, (![X_372, Y_373]: (ifeq(iext(uri_rdfs_subClassOf, X_372, Y_373), true, icext(uri_rdfs_Class, X_372), true)=true))). % 32.88/20.91 tff(c_5907, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdf_Bag), true)=true))). % 32.88/20.91 tff(c_6362, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_domain), true)=true))). % 32.88/20.91 tff(c_2965, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_104), true, iext(Q_104, uri_rdf__3, uri_rdfs_Resource), true)=true))). % 32.88/20.91 tff(c_6830, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_owl_propertyChainAxiom), true)=true))). % 32.88/20.91 tff(c_7419, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdfs_Resource), true)=true))). % 32.88/20.91 tff(c_7608, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_range), true)=true))). % 32.88/20.91 tff(c_19594, plain, (![X_362, Y_363]: (ifeq(iext(uri_rdfs_range, X_362, Y_363), true, icext(uri_rdf_Property, X_362), true)=true))). % 32.88/20.91 tff(c_8939, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_rest), true)=true))). % 32.88/20.91 tff(c_7418, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdfs_Literal), true)=true))). % 32.88/20.91 tff(c_4811, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdfs_Container), true)=true))). % 32.88/20.91 tff(c_2929, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_104), true, iext(Q_104, uri_rdf_object, uri_rdf_Property), true)=true))). % 32.88/20.91 tff(c_8139, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf__2), true)=true))). % 32.88/20.91 tff(c_7893, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_owl_inverseOf), true)=true))). % 32.88/20.91 tff(c_4912, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdfs_Class), true)=true))). % 32.88/20.91 tff(c_19385, plain, (![X_351, Y_352]: (ifeq(iext(uri_rdfs_comment, X_351, Y_352), true, icext(uri_rdfs_Literal, Y_352), true)=true))). % 32.88/20.91 tff(c_2932, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_104), true, iext(Q_104, uri_rdf__1, uri_rdfs_ContainerMembershipProperty), true)=true))). % 32.88/20.91 tff(c_6831, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_owl_propertyChainAxiom), true)=true))). % 32.88/20.91 tff(c_19268, plain, (![X_345, Y_346]: (ifeq(iext(uri_rdf_rest, X_345, Y_346), true, icext(uri_rdf_List, Y_346), true)=true))). % 32.88/20.91 tff(c_4683, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_29), true, icext(C_29, uri_rdfs_Resource), true)=true))). % 32.88/20.91 tff(c_2967, plain, (![Q_104]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_104), true, iext(Q_104, uri_rdfs_range, uri_rdfs_Class), true)=true))). % 32.88/20.91 tff(c_4682, plain, (![C_19, X_140]: (ifeq(iext(uri_rdfs_domain, uri_rdf_type, C_19), true, icext(C_19, X_140), true)=true))). % 32.88/20.91 tff(c_2013, plain, (![C_93]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_93), true, icext(C_93, uri_rdfs_seeAlso), true)=true))). % 32.88/20.91 tff(c_2344, plain, (![C_97]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_97), true, icext(C_97, uri_rdfs_subClassOf), true)=true))). % 32.88/20.91 tff(c_2390, plain, (![C_97]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_97), true, icext(C_97, uri_rdf_type), true)=true))). % 32.88/20.91 tff(c_18752, plain, (![X_328, Y_329]: (ifeq(iext(uri_rdf_subject, X_328, Y_329), true, icext(uri_rdfs_Statement, X_328), true)=true))). % 32.88/20.91 tff(c_2336, plain, (![C_97]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_97), true, icext(C_97, uri_rdf_first), true)=true))). % 32.88/20.91 tff(c_2342, plain, (![C_97]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_97), true, icext(C_97, uri_rdf_value), true)=true))). % 32.88/20.91 tff(c_2026, plain, (![C_93]: (ifeq(iext(uri_rdfs_range, uri_rdfs_range, C_93), true, icext(C_93, uri_rdf_List), true)=true))). % 32.88/20.91 tff(c_2348, plain, (![C_97]: (ifeq(iext(uri_rdfs_domain, uri_rdf_first, C_97), true, icext(C_97, sK2_testcase_premise_fullish_027_Inferred_Property_Characteristics_II_BNODE_l1), true)=true))). % 32.88/20.91 tff(c_1967, plain, (![C_93]: (ifeq(iext(uri_rdfs_range, uri_rdfs_domain, C_93), true, icext(C_93, uri_rdfs_Class), true)=true))). % 32.88/20.91 tff(c_2376, plain, (![C_97]: (ifeq(iext(uri_rdfs_domain, uri_owl_inverseOf, C_97), true, icext(C_97, sK1_testcase_premise_fullish_027_Inferred_Property_Characteristics_II_BNODE_v), true)=true))). % 32.88/20.91 tff(c_2354, plain, (![C_97]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_97), true, icext(C_97, uri_rdf__3), true)=true))). % 32.88/20.91 tff(c_2388, plain, (![C_97]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_97), true, icext(C_97, uri_rdfs_ContainerMembershipProperty), true)=true))). % 32.88/20.91 tff(c_2335, plain, (![C_97]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_97), true, icext(C_97, uri_rdf_subject), true)=true))). % 32.88/20.91 tff(c_2398, plain, (![C_97]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_97), true, icext(C_97, uri_rdf_first), true)=true))). % 32.88/20.91 tff(c_2404, plain, (![C_97]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_97), true, icext(C_97, uri_rdf_rest), true)=true))). % 32.88/20.91 tff(c_1971, plain, (![C_93]: (ifeq(iext(uri_rdfs_range, uri_rdf_first, C_93), true, icext(C_93, uri_ex_p), true)=true))). % 32.88/20.91 tff(c_1970, plain, (![C_93]: (ifeq(iext(uri_rdfs_range, uri_owl_propertyChainAxiom, C_93), true, icext(C_93, sK2_testcase_premise_fullish_027_Inferred_Property_Characteristics_II_BNODE_l1), true)=true))). % 32.88/20.91 tff(c_2371, plain, (![C_97]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_97), true, icext(C_97, uri_rdfs_domain), true)=true))). % 32.88/20.91 tff(c_2392, plain, (![C_97]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_97), true, icext(C_97, uri_rdfs_member), true)=true))). % 32.88/20.91 tff(c_2362, plain, (![C_97]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_97), true, icext(C_97, uri_rdfs_isDefinedBy), true)=true))). % 32.88/20.91 tff(c_17914, plain, (![X_305, Y_306]: (ifeq(iext(uri_rdfs_subClassOf, X_305, Y_306), true, icext(uri_rdfs_Class, Y_306), true)=true))). % 32.88/20.91 tff(c_2334, plain, (![C_97]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_97), true, icext(C_97, uri_rdfs_label), true)=true))). % 32.88/20.91 tff(c_2396, plain, (![C_97]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_97), true, icext(C_97, uri_rdf_predicate), true)=true))). % 32.88/20.91 tff(c_2358, plain, (![C_97]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_97), true, icext(C_97, uri_rdfs_subPropertyOf), true)=true))). % 32.88/20.91 tff(c_2382, plain, (![C_97]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_97), true, icext(C_97, uri_rdf__2), true)=true))). % 32.88/20.91 tff(c_2370, plain, (![C_97]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_97), true, icext(C_97, uri_rdfs_comment), true)=true))). % 32.88/20.91 tff(c_2394, plain, (![C_97]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_97), true, icext(C_97, uri_rdfs_isDefinedBy), true)=true))). % 32.88/20.91 tff(c_2350, plain, (![C_97]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_97), true, icext(C_97, uri_rdfs_domain), true)=true))). % 32.88/20.91 tff(c_2333, plain, (![C_97]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_97), true, icext(C_97, uri_rdfs_subClassOf), true)=true))). % 32.88/20.91 tff(c_2012, plain, (![C_93]: (ifeq(iext(uri_rdfs_range, uri_rdfs_domain, C_93), true, icext(C_93, uri_rdfs_Statement), true)=true))). % 32.88/20.91 tff(c_2359, plain, (![C_97]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_97), true, icext(C_97, uri_rdfs_subPropertyOf), true)=true))). % 32.88/20.91 tff(c_1992, plain, (![C_93]: (ifeq(iext(uri_rdfs_range, uri_rdfs_domain, C_93), true, icext(C_93, uri_rdf_Property), true)=true))). % 32.88/20.91 tff(c_17148, plain, (![X_290, Y_291]: (ifeq(iext(uri_rdf_type, X_290, Y_291), true, icext(uri_rdfs_Class, Y_291), true)=true))). % 32.88/20.91 tff(c_2361, plain, (![C_97]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_97), true, icext(C_97, uri_rdf_type), true)=true))). % 32.88/20.91 tff(c_2384, plain, (![C_97]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_97), true, icext(C_97, uri_rdfs_isDefinedBy), true)=true))). % 32.88/20.91 tff(c_1985, plain, (![C_93]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_93), true, icext(C_93, uri_rdfs_Class), true)=true))). % 32.88/20.91 tff(c_16953, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_comment, uri_rdfs_comment)=true)). % 32.88/20.91 tff(c_2346, plain, (![C_97]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_97), true, icext(C_97, uri_rdfs_Datatype), true)=true))). % 32.88/20.91 tff(c_16887, plain, (ip(uri_rdfs_comment)=true)). % 32.88/20.91 tff(c_16834, plain, (iext(uri_rdf_type, uri_rdfs_comment, uri_rdf_Property)=true)). % 32.88/20.91 tff(c_16667, plain, (icext(uri_rdf_Property, uri_rdfs_comment)=true)). % 32.88/20.91 tff(c_2356, plain, (![C_97]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_97), true, icext(C_97, uri_rdfs_comment), true)=true))). % 32.88/20.91 tff(c_2002, plain, (![C_93]: (ifeq(iext(uri_rdfs_range, uri_rdf_rest, C_93), true, icext(C_93, sK3_testcase_premise_fullish_027_Inferred_Property_Characteristics_II_BNODE_l2), true)=true))). % 32.88/20.91 tff(c_2375, plain, (![C_97]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_97), true, icext(C_97, uri_rdf_Alt), true)=true))). % 32.88/20.91 tff(c_2399, plain, (![C_97]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_97), true, icext(C_97, uri_rdfs_range), true)=true))). % 32.88/20.91 tff(c_2387, plain, (![C_97]: (ifeq(iext(uri_rdfs_domain, uri_rdf_first, C_97), true, icext(C_97, sK3_testcase_premise_fullish_027_Inferred_Property_Characteristics_II_BNODE_l2), true)=true))). % 32.88/20.91 tff(c_2369, plain, (![C_97]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_97), true, icext(C_97, uri_rdf__1), true)=true))). % 33.27/20.91 tff(c_15313, plain, (![X_265, Y_266]: (ifeq(iext(uri_rdfs_domain, X_265, Y_266), true, icext(uri_rdfs_Class, Y_266), true)=true))). % 33.27/20.91 tff(c_2365, plain, (![C_97]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_97), true, icext(C_97, uri_rdf_subject), true)=true))). % 33.27/20.91 tff(c_1966, plain, (![C_93]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_93), true, icext(C_93, uri_rdf_List), true)=true))). % 33.27/20.91 tff(c_2377, plain, (![C_97]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_97), true, icext(C_97, uri_rdf__2), true)=true))). % 33.27/20.91 tff(c_1996, plain, (![C_93]: (ifeq(iext(uri_rdfs_range, uri_owl_inverseOf, C_93), true, icext(C_93, uri_ex_p), true)=true))). % 33.27/20.91 tff(c_2347, plain, (![C_97]: (ifeq(iext(uri_rdfs_domain, uri_owl_propertyChainAxiom, C_97), true, icext(C_97, uri_owl_sameAs), true)=true))). % 33.27/20.91 tff(c_14334, plain, (![X_33]: (ifeq(icext(uri_rdf_List, X_33), true, icext(uri_rdf_List, X_33), true)=true))). % 33.27/20.91 tff(c_15976, plain, (![X_33]: (ifeq(icext(uri_rdfs_Statement, X_33), true, icext(uri_rdfs_Statement, X_33), true)=true))). % 33.27/20.91 tff(c_12456, plain, (![X_33]: (ifeq(icext(uri_rdf_Property, X_33), true, icext(uri_rdf_Property, X_33), true)=true))). % 33.27/20.91 tff(c_15920, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Statement, uri_rdfs_Statement)=true)). % 33.27/20.91 tff(c_15718, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Statement, uri_rdfs_Resource)=true)). % 33.27/20.91 tff(c_15671, plain, (iext(uri_rdf_type, uri_rdfs_Statement, uri_rdfs_Class)=true)). % 33.27/20.91 tff(c_15503, plain, (ic(uri_rdfs_Statement)=true)). % 33.27/20.91 tff(c_1978, plain, (![C_93]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_93), true, icext(C_93, uri_rdfs_ContainerMembershipProperty), true)=true))). % 33.27/20.91 tff(c_15434, plain, (icext(uri_rdfs_Class, uri_rdfs_Statement)=true)). % 33.27/20.91 tff(c_11463, plain, (![X_33]: (ifeq(icext(uri_rdfs_Seq, X_33), true, icext(uri_rdfs_Seq, X_33), true)=true))). % 33.27/20.91 tff(c_10330, plain, (![X_33]: (ifeq(icext(uri_rdfs_ContainerMembershipProperty, X_33), true, icext(uri_rdfs_ContainerMembershipProperty, X_33), true)=true))). % 33.27/20.91 tff(c_6202, plain, (![X_33]: (ifeq(icext(uri_rdf_Alt, X_33), true, icext(uri_rdf_Alt, X_33), true)=true))). % 33.27/20.91 tff(c_12522, plain, (![X_33]: (ifeq(icext(uri_rdfs_Datatype, X_33), true, icext(uri_rdfs_Datatype, X_33), true)=true))). % 33.27/20.91 tff(c_4813, plain, (![X_33]: (ifeq(icext(uri_rdfs_Container, X_33), true, icext(uri_rdfs_Container, X_33), true)=true))). % 33.27/20.91 tff(c_15094, plain, (iext(uri_rdf_type, sK3_testcase_premise_fullish_027_Inferred_Property_Characteristics_II_BNODE_l2, uri_rdf_List)=true)). % 33.27/20.91 tff(c_15050, plain, (icext(uri_rdf_List, sK3_testcase_premise_fullish_027_Inferred_Property_Characteristics_II_BNODE_l2)=true)). % 33.27/20.91 tff(c_2407, plain, (![C_97]: (ifeq(iext(uri_rdfs_domain, uri_rdf_rest, C_97), true, icext(C_97, sK3_testcase_premise_fullish_027_Inferred_Property_Characteristics_II_BNODE_l2), true)=true))). % 33.27/20.91 tff(c_8644, plain, (![X_33]: (ifeq(icext(uri_rdfs_Literal, X_33), true, icext(uri_rdfs_Literal, X_33), true)=true))). % 33.27/20.91 tff(c_4744, plain, (![X_33]: (ifeq(icext(uri_rdf_XMLLiteral, X_33), true, icext(uri_rdf_XMLLiteral, X_33), true)=true))). % 33.27/20.91 tff(c_4914, plain, (![X_33]: (ifeq(icext(uri_rdfs_Class, X_33), true, icext(uri_rdfs_Class, X_33), true)=true))). % 33.27/20.91 tff(c_5908, plain, (![X_33]: (ifeq(icext(uri_rdf_Bag, X_33), true, icext(uri_rdf_Bag, X_33), true)=true))). % 33.27/20.91 tff(c_14859, plain, (iext(uri_rdf_type, uri_rdfs_Resource, uri_rdfs_Class)=true)). % 33.27/20.91 tff(c_14765, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_label, uri_rdfs_label)=true)). % 33.27/20.91 tff(c_2366, plain, (![C_97]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_97), true, icext(C_97, uri_rdf__1), true)=true))). % 33.27/20.91 tff(c_14700, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_predicate, uri_rdf_predicate)=true)). % 33.27/20.91 tff(c_14631, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_member, uri_rdfs_member)=true)). % 33.27/20.91 tff(c_14558, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Resource, uri_rdfs_Resource)=true)). % 33.27/20.91 tff(c_14365, plain, (iext(uri_rdfs_subClassOf, uri_rdf_List, uri_rdfs_Resource)=true)). % 33.27/20.91 tff(c_2006, plain, (![C_93]: (ifeq(iext(uri_rdfs_range, uri_rdf_first, C_93), true, icext(C_93, sK1_testcase_premise_fullish_027_Inferred_Property_Characteristics_II_BNODE_v), true)=true))). % 33.27/20.91 tff(c_14278, plain, (iext(uri_rdfs_subClassOf, uri_rdf_List, uri_rdf_List)=true)). % 33.27/20.91 tff(c_14228, plain, (iext(uri_rdf_type, uri_rdf_Bag, uri_rdfs_Class)=true)). % 33.27/20.91 tff(c_2389, plain, (![C_97]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_97), true, icext(C_97, uri_rdfs_seeAlso), true)=true))). % 33.27/20.91 tff(c_14154, plain, (iext(uri_rdf_type, uri_rdfs_Container, uri_rdfs_Class)=true)). % 33.27/20.91 tff(c_14113, plain, (ip(uri_rdf_predicate)=true)). % 33.27/20.91 tff(c_2021, plain, (![C_93]: (ifeq(iext(uri_rdfs_range, uri_rdfs_range, C_93), true, icext(C_93, uri_rdfs_Class), true)=true))). % 33.27/20.91 tff(c_14035, plain, (iext(uri_rdf_type, uri_rdf_predicate, uri_rdf_Property)=true)). % 33.27/20.91 tff(c_13799, plain, (icext(uri_rdf_Property, uri_rdf_predicate)=true)). % 33.27/20.91 tff(c_2403, plain, (![C_97]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_97), true, icext(C_97, uri_rdf_predicate), true)=true))). % 33.27/20.91 tff(c_13738, plain, (ip(uri_rdfs_label)=true)). % 33.27/20.91 tff(c_13685, plain, (iext(uri_rdf_type, uri_rdfs_label, uri_rdf_Property)=true)). % 33.27/20.91 tff(c_13637, plain, (icext(uri_rdf_Property, uri_rdfs_label)=true)). % 33.27/20.91 tff(c_2386, plain, (![C_97]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_97), true, icext(C_97, uri_rdfs_label), true)=true))). % 33.27/20.91 tff(c_13569, plain, (iext(uri_rdf_type, uri_rdfs_Datatype, uri_rdfs_Class)=true)). % 33.27/20.91 tff(c_13522, plain, (iext(uri_rdf_type, uri_rdfs_Literal, uri_rdfs_Class)=true)). % 33.27/20.91 tff(c_1979, plain, (![C_93]: (ifeq(iext(uri_rdfs_range, uri_rdfs_range, C_93), true, icext(C_93, uri_rdf_Property), true)=true))). % 33.27/20.91 tff(c_13449, plain, (iext(uri_rdf_type, uri_rdfs_ContainerMembershipProperty, uri_rdfs_Class)=true)). % 33.27/20.92 tff(c_13402, plain, (iext(uri_rdf_type, uri_rdf_Alt, uri_rdfs_Class)=true)). % 33.27/20.92 tff(c_13328, plain, (iext(uri_rdf_type, uri_rdfs_Seq, uri_rdfs_Class)=true)). % 33.27/20.92 tff(c_1969, plain, (![C_93]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_93), true, icext(C_93, uri_rdfs_Class), true)=true))). % 33.27/20.92 tff(c_13279, plain, (iext(uri_rdf_type, uri_rdfs_Class, uri_rdfs_Class)=true)). % 33.27/20.92 tff(c_13232, plain, (iext(uri_rdf_type, uri_rdf_XMLLiteral, uri_rdfs_Class)=true)). % 33.27/20.92 tff(c_13156, plain, (iext(uri_rdf_type, sK2_testcase_premise_fullish_027_Inferred_Property_Characteristics_II_BNODE_l1, uri_rdf_List)=true)). % 33.27/20.92 tff(c_13101, plain, (iext(uri_rdf_type, uri_rdfs_member, uri_rdf_Property)=true)). % 33.27/20.92 tff(c_13054, plain, (iext(uri_rdf_type, uri_rdf_List, uri_rdfs_Class)=true)). % 33.27/20.92 tff(c_2363, plain, (![C_97]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_97), true, icext(C_97, uri_rdfs_Seq), true)=true))). % 33.27/20.92 tff(c_12890, plain, (icext(uri_rdf_Property, uri_owl_inverseOf)=true)). % 33.27/20.92 tff(c_12836, plain, (iext(uri_rdf_type, uri_owl_inverseOf, uri_rdf_Property)=true)). % 33.27/20.92 tff(c_2397, plain, (![C_97]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_97), true, icext(C_97, uri_rdf__3), true)=true))). % 33.27/20.92 tff(c_12630, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, uri_rdfs_Resource)=true)). % 33.27/20.92 tff(c_12564, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_isDefinedBy, uri_rdfs_isDefinedBy)=true)). % 33.27/20.92 tff(c_12466, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, uri_rdfs_Datatype)=true)). % 33.27/20.92 tff(c_12400, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Property, uri_rdf_Property)=true)). % 33.27/20.92 tff(c_2373, plain, (![C_97]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_97), true, icext(C_97, uri_rdfs_seeAlso), true)=true))). % 33.27/20.92 tff(c_12240, plain, (icext(uri_rdf_Property, uri_rdfs_domain)=true)). % 33.27/20.92 tff(c_12186, plain, (iext(uri_rdf_type, uri_rdfs_domain, uri_rdf_Property)=true)). % 33.27/20.92 tff(c_12095, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_subject, uri_rdf_subject)=true)). % 33.27/20.92 tff(c_3273, plain, (![S_5, O_6]: (ifeq(iext(uri_rdfs_subPropertyOf, S_5, O_6), true, true, true)=true))). % 33.27/20.92 tff(c_11846, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Bag, uri_rdfs_Resource)=true)). % 33.27/20.92 tff(c_2393, plain, (![C_97]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_97), true, icext(C_97, uri_rdf_object), true)=true))). % 33.27/20.92 tff(c_11656, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, uri_rdfs_Resource)=true)). % 33.27/20.92 tff(c_11595, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf__3, uri_rdfs_member)=true)). % 33.27/20.92 tff(c_11407, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Seq, uri_rdfs_Seq)=true)). % 33.27/20.92 tff(c_11093, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf)=true)). % 33.27/20.92 tff(c_10673, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_object, uri_rdf_object)=true)). % 33.27/20.92 tff(c_10561, plain, (icext(uri_rdf_List, sK2_testcase_premise_fullish_027_Inferred_Property_Characteristics_II_BNODE_l1)=true)). % 33.27/20.92 tff(c_2380, plain, (![C_97]: (ifeq(iext(uri_rdfs_domain, uri_rdf_rest, C_97), true, icext(C_97, sK2_testcase_premise_fullish_027_Inferred_Property_Characteristics_II_BNODE_l1), true)=true))). % 33.27/20.92 tff(c_10373, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf__2, uri_rdfs_member)=true)). % 33.27/20.92 tff(c_10274, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, uri_rdfs_ContainerMembershipProperty)=true)). % 33.27/20.92 tff(c_10156, plain, (icext(uri_rdf_Property, uri_rdfs_member)=true)). % 33.27/20.92 tff(c_2378, plain, (![C_97]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_97), true, icext(C_97, uri_rdfs_member), true)=true))). % 33.27/20.92 tff(c_10068, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_value, uri_rdf_value)=true)). % 33.27/20.92 tff(c_9949, plain, (icext(uri_rdf_Property, uri_rdfs_subPropertyOf)=true)). % 33.27/20.92 tff(c_9870, plain, (iext(uri_rdf_type, uri_rdfs_subPropertyOf, uri_rdf_Property)=true)). % 33.27/20.92 tff(c_2005, plain, (![C_93]: (ifeq(iext(uri_rdfs_range, uri_rdfs_domain, C_93), true, icext(C_93, uri_rdfs_Resource), true)=true))). % 33.27/20.92 tff(c_9702, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf__3, uri_rdf__3)=true)). % 33.27/20.92 tff(c_9634, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf__1, uri_rdf__1)=true)). % 33.27/20.92 tff(c_2406, plain, (![C_97]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_97), true, icext(C_97, uri_rdf_value), true)=true))). % 33.27/20.92 tff(c_9363, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_first, uri_rdf_first)=true)). % 33.27/20.92 tff(c_9319, plain, (icext(uri_rdf_Property, uri_rdfs_seeAlso)=true)). % 33.27/20.92 tff(c_1962, plain, (![C_93]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_93), true, icext(C_93, uri_rdfs_Literal), true)=true))). % 33.27/20.92 tff(c_9240, plain, (iext(uri_rdf_type, uri_rdfs_seeAlso, uri_rdf_Property)=true)). % 33.27/20.92 tff(c_9203, plain, (ip(uri_rdfs_member)=true)). % 33.27/20.92 tff(c_9139, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf__1, uri_rdfs_member)=true)). % 33.27/20.92 tff(c_8881, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_rest, uri_rdf_rest)=true)). % 33.27/20.92 tff(c_2379, plain, (![C_97]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_97), true, icext(C_97, uri_rdf_Bag), true)=true))). % 33.27/20.92 tff(c_8734, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Alt, uri_rdfs_Resource)=true)). % 33.27/20.92 tff(c_8666, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_type, uri_rdf_type)=true)). % 33.27/20.92 tff(c_3235, plain, (![S_5, O_6]: (ifeq(iext(uri_owl_inverseOf, S_5, O_6), true, true, true)=true))). % 33.27/20.92 tff(c_8585, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Literal, uri_rdfs_Literal)=true)). % 33.27/20.92 tff(c_8478, plain, (icext(uri_rdf_Property, uri_owl_propertyChainAxiom)=true)). % 33.27/20.92 tff(c_2030, plain, (![C_93]: (ifeq(iext(uri_rdfs_range, uri_rdf_rest, C_93), true, icext(C_93, uri_rdf_nil), true)=true))). % 33.27/20.92 tff(c_8399, plain, (iext(uri_rdf_type, uri_owl_propertyChainAxiom, uri_rdf_Property)=true)). % 33.27/20.92 tff(c_8205, plain, (icext(uri_rdf_Property, uri_rdfs_subClassOf)=true)). % 33.27/20.92 tff(c_8150, plain, (iext(uri_rdf_type, uri_rdfs_subClassOf, uri_rdf_Property)=true)). % 33.27/20.92 tff(c_8086, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf__2, uri_rdf__2)=true)). % 33.27/20.92 tff(c_7838, plain, (iext(uri_rdfs_subPropertyOf, uri_owl_inverseOf, uri_owl_inverseOf)=true)). % 33.27/20.92 tff(c_7697, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Class, uri_rdfs_Resource)=true)). % 33.27/20.92 tff(c_7532, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_range, uri_rdfs_range)=true)). % 33.27/20.92 tff(c_1991, plain, (![C_93]: (ifeq(iext(uri_rdfs_range, uri_rdfs_range, C_93), true, icext(C_93, uri_rdfs_Literal), true)=true))). % 33.27/20.92 tff(c_7364, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Literal, uri_rdfs_Resource)=true)). % 33.27/20.92 tff(c_2007, plain, (![C_93]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_93), true, icext(C_93, uri_rdf_Property), true)=true))). % 33.27/20.92 tff(c_7171, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Container, uri_rdfs_Resource)=true)). % 33.27/20.92 tff(c_7001, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Seq, uri_rdfs_Resource)=true)). % 33.27/20.92 tff(c_2339, plain, (![C_97]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_97), true, icext(C_97, uri_rdf_rest), true)=true))). % 33.27/20.92 tff(c_6896, plain, (icext(uri_rdf_Property, uri_rdfs_isDefinedBy)=true)). % 33.27/20.92 tff(c_6842, plain, (iext(uri_rdf_type, uri_rdfs_isDefinedBy, uri_rdf_Property)=true)). % 33.27/20.92 tff(c_6780, plain, (iext(uri_rdfs_subPropertyOf, uri_owl_propertyChainAxiom, uri_owl_propertyChainAxiom)=true)). % 33.27/20.92 tff(c_1674, plain, (![S_5, O_6]: (ifeq(iext(uri_rdf_rest, S_5, O_6), true, true, true)=true))). % 33.27/20.92 tff(c_2484, plain, (![S_5, O_6]: (ifeq(iext(uri_rdf_object, S_5, O_6), true, true, true)=true))). % 33.27/20.92 tff(c_1972, plain, (![C_93]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_93), true, icext(C_93, uri_rdf_Property), true)=true))). % 33.27/20.92 tff(c_6571, plain, (ic(uri_rdf_List)=true)). % 33.27/20.92 tff(c_6521, plain, (icext(uri_rdfs_Class, uri_rdf_List)=true)). % 33.27/20.92 tff(c_1963, plain, (![C_93]: (ifeq(iext(uri_rdfs_range, uri_rdfs_domain, C_93), true, icext(C_93, uri_rdf_List), true)=true))). % 33.27/20.92 tff(c_6435, plain, (iext(uri_rdfs_subClassOf, uri_rdf_XMLLiteral, uri_rdfs_Resource)=true)). % 33.27/20.92 tff(c_6311, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, uri_rdfs_domain)=true)). % 33.27/20.92 tff(c_1362, plain, (![S_5, O_6]: (ifeq(iext(uri_rdfs_range, S_5, O_6), true, true, true)=true))). % 33.27/20.92 tff(c_1964, plain, (![C_93]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_93), true, icext(C_93, uri_rdfs_Datatype), true)=true))). % 33.27/20.92 tff(c_6146, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Alt, uri_rdf_Alt)=true)). % 33.27/20.92 tff(c_2020, plain, (![C_93]: (ifeq(iext(uri_rdfs_range, uri_rdfs_range, C_93), true, icext(C_93, uri_rdfs_Resource), true)=true))). % 33.27/20.92 tff(c_3152, plain, (![S_5, O_6]: (ifeq(iext(uri_owl_propertyChainAxiom, S_5, O_6), true, true, true)=true))). % 33.27/20.92 tff(c_2049, plain, (![S_5, O_6]: (ifeq(iext(uri_rdfs_domain, S_5, O_6), true, true, true)=true))). % 33.27/20.92 tff(c_2338, plain, (![C_97]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_97), true, icext(C_97, uri_rdf_XMLLiteral), true)=true))). % 33.27/20.92 tff(c_5852, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Bag, uri_rdf_Bag)=true)). % 33.27/20.92 tff(c_2001, plain, (![C_93]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_93), true, icext(C_93, uri_rdfs_Container), true)=true))). % 33.27/20.92 tff(c_5605, plain, (icext(uri_rdf_Property, uri_rdfs_range)=true)). % 33.27/20.92 tff(c_2405, plain, (![C_97]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_97), true, icext(C_97, uri_rdfs_range), true)=true))). % 33.27/20.92 tff(c_5521, plain, (iext(uri_rdf_type, uri_rdfs_range, uri_rdf_Property)=true)). % 33.27/20.92 tff(c_1649, plain, (![X_90]: (ifeq(icext(uri_rdfs_Datatype, X_90), true, icext(uri_rdfs_Class, X_90), true)=true))). % 33.27/20.92 tff(c_1653, plain, (![X_90]: (ifeq(icext(uri_rdfs_ContainerMembershipProperty, X_90), true, icext(uri_rdf_Property, X_90), true)=true))). % 33.27/20.92 tff(c_5275, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_seeAlso, uri_rdfs_seeAlso)=true)). % 33.27/20.92 tff(c_5167, plain, (icext(uri_rdfs_Class, uri_rdfs_Resource)=true)). % 33.27/20.92 tff(c_1652, plain, (![X_90]: (ifeq(icext(uri_rdf_Bag, X_90), true, icext(uri_rdfs_Container, X_90), true)=true))). % 33.27/20.92 tff(c_5096, plain, (ic(uri_rdfs_Resource)=true)). % 33.27/20.92 tff(c_5031, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Property, uri_rdfs_Resource)=true)). % 33.27/20.92 tff(c_1650, plain, (![X_90]: (ifeq(icext(uri_rdfs_Seq, X_90), true, icext(uri_rdfs_Container, X_90), true)=true))). % 33.27/20.92 tff(c_1540, plain, (![S_5, O_6]: (ifeq(iext(uri_rdfs_subClassOf, S_5, O_6), true, true, true)=true))). % 33.27/20.92 tff(c_4925, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, uri_rdfs_subClassOf)=true)). % 33.27/20.92 tff(c_4855, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Class, uri_rdfs_Class)=true)). % 33.27/20.92 tff(c_1648, plain, (![X_90]: (ifeq(icext(uri_rdf_XMLLiteral, X_90), true, icext(uri_rdfs_Literal, X_90), true)=true))). % 33.27/20.92 tff(c_4761, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Container, uri_rdfs_Container)=true)). % 33.27/20.92 tff(c_1651, plain, (![X_90]: (ifeq(icext(uri_rdf_Alt, X_90), true, icext(uri_rdfs_Container, X_90), true)=true))). % 33.27/20.92 tff(c_4692, plain, (iext(uri_rdfs_subClassOf, uri_rdf_XMLLiteral, uri_rdf_XMLLiteral)=true)). % 33.27/20.92 tff(c_4641, plain, (![X_139]: (iext(uri_rdf_type, X_139, uri_rdfs_Resource)=true))). % 33.27/20.92 tff(c_2360, plain, (![X_98, Y_99]: (ifeq(iext(uri_rdf_type, X_98, Y_99), true, true, true)=true))). % 33.27/20.92 tff(c_2017, plain, (![X_94, Y_95]: (ifeq(iext(uri_rdf__3, X_94, Y_95), true, true, true)=true))). % 33.27/20.92 tff(c_1958, plain, (![X_94, Y_95]: (ifeq(iext(uri_rdf_subject, X_94, Y_95), true, true, true)=true))). % 33.27/20.92 tff(c_2355, plain, (![X_98, Y_99]: (ifeq(iext(uri_rdfs_comment, X_98, Y_99), true, true, true)=true))). % 33.27/20.92 tff(c_2368, plain, (![X_98, Y_99]: (ifeq(iext(uri_rdf__1, X_98, Y_99), true, true, true)=true))). % 33.27/20.92 tff(c_2015, plain, (![X_94, Y_95]: (ifeq(iext(uri_rdf_predicate, X_94, Y_95), true, true, true)=true))). % 33.27/20.92 tff(c_2385, plain, (![X_98, Y_99]: (ifeq(iext(uri_rdfs_label, X_98, Y_99), true, true, true)=true))). % 33.27/20.92 tff(c_1982, plain, (![X_94, Y_95]: (ifeq(iext(uri_rdfs_isDefinedBy, X_94, Y_95), true, true, true)=true))). % 33.27/20.92 tff(c_2372, plain, (![X_98, Y_99]: (ifeq(iext(uri_rdfs_seeAlso, X_98, Y_99), true, true, true)=true))). % 33.27/20.92 tff(c_2019, plain, (![X_94, Y_95]: (ifeq(iext(uri_rdf_first, X_94, Y_95), true, true, true)=true))). % 33.27/20.92 tff(c_2341, plain, (![X_98, Y_99]: (ifeq(iext(uri_rdf_value, X_98, Y_99), true, true, true)=true))). % 33.27/20.92 tff(c_4438, plain, (icext(uri_rdfs_Class, uri_rdfs_Container)=true)). % 33.27/20.92 tff(c_4394, plain, (icext(uri_rdfs_Class, uri_rdfs_ContainerMembershipProperty)=true)). % 33.27/20.92 tff(c_4341, plain, (icext(uri_rdfs_Class, uri_rdf_XMLLiteral)=true)). % 33.27/20.92 tff(c_1999, plain, (![X_94, Y_95]: (ifeq(iext(uri_rdfs_member, X_94, Y_95), true, true, true)=true))). % 33.27/20.92 tff(c_4298, plain, (icext(uri_rdfs_Class, uri_rdf_Bag)=true)). % 33.27/20.92 tff(c_4242, plain, (icext(uri_rdfs_Class, uri_rdfs_Class)=true)). % 33.27/20.92 tff(c_4198, plain, (icext(uri_rdfs_Class, uri_rdfs_Seq)=true)). % 33.27/20.92 tff(c_4151, plain, (icext(uri_rdfs_Class, uri_rdfs_Literal)=true)). % 33.27/20.92 tff(c_2381, plain, (![X_98, Y_99]: (ifeq(iext(uri_rdf__2, X_98, Y_99), true, true, true)=true))). % 33.27/20.92 tff(c_4097, plain, (icext(uri_rdfs_Class, uri_rdf_Alt)=true)). % 33.27/20.92 tff(c_4054, plain, (icext(uri_rdfs_Class, uri_rdfs_Datatype)=true)). % 33.27/20.92 tff(c_4005, plain, (icext(uri_rdfs_Class, uri_rdf_Property)=true)). % 33.27/20.92 tff(c_3964, plain, (icext(uri_rdfs_ContainerMembershipProperty, uri_rdf__3)=true)). % 33.27/20.92 tff(c_3923, plain, (icext(uri_rdf_Property, uri_rdf_value)=true)). % 33.27/20.92 tff(c_3880, plain, (icext(uri_rdfs_ContainerMembershipProperty, uri_rdf__1)=true)). % 33.27/20.92 tff(c_3814, plain, (icext(uri_rdf_Property, uri_rdf_rest)=true)). % 33.27/20.92 tff(c_3804, plain, (icext(uri_rdf_Property, uri_rdf__3)=true)). % 33.27/20.92 tff(c_3763, plain, (icext(uri_rdf_Property, uri_rdf_subject)=true)). % 33.27/20.92 tff(c_3722, plain, (icext(uri_rdf_Property, uri_rdf_object)=true)). % 33.27/20.92 tff(c_3684, plain, (icext(uri_rdf_Property, uri_rdf_first)=true)). % 33.27/20.92 tff(c_3641, plain, (icext(uri_rdfs_Datatype, uri_rdf_XMLLiteral)=true)). % 33.27/20.92 tff(c_3598, plain, (icext(uri_rdfs_ContainerMembershipProperty, uri_rdf__2)=true)). % 33.27/20.92 tff(c_3549, plain, (icext(uri_rdf_List, uri_rdf_nil)=true)). % 33.27/20.92 tff(c_3504, plain, (icext(uri_rdf_Property, uri_rdf__2)=true)). % 33.27/20.92 tff(c_3467, plain, (icext(uri_rdf_Property, uri_rdf__1)=true)). % 33.27/20.92 tff(c_3430, plain, (icext(uri_rdf_Property, uri_rdf_type)=true)). % 33.27/20.92 tff(c_3381, plain, (ic(uri_rdfs_Seq)=true)). % 33.27/20.92 tff(c_3337, plain, (ip(uri_rdf__2)=true)). % 33.27/20.92 tff(c_3295, plain, (ic(uri_rdfs_Class)=true)). % 33.27/20.92 tff(c_3258, plain, (ip(uri_rdfs_subPropertyOf)=true)). % 33.27/20.92 tff(c_3220, plain, (ip(uri_owl_inverseOf)=true)). % 33.27/20.92 tff(c_3175, plain, (ic(uri_rdf_XMLLiteral)=true)). % 33.27/20.92 tff(c_3137, plain, (ip(uri_owl_propertyChainAxiom)=true)). % 33.27/20.92 tff(c_3093, plain, (ip(uri_rdf__1)=true)). % 33.27/20.92 tff(c_3050, plain, (ic(uri_rdf_Property)=true)). % 33.27/20.92 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.27/20.92 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.27/20.92 tff(c_2469, plain, (ip(uri_rdf_object)=true)). % 33.27/20.92 tff(c_2417, plain, (ip(uri_rdf_first)=true)). % 33.27/20.92 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.27/20.92 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.27/20.92 tff(c_2034, plain, (ip(uri_rdfs_domain)=true)). % 33.27/20.92 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.27/20.92 tff(c_1657, plain, (ip(uri_rdf_rest)=true)). % 33.27/20.92 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.27/20.92 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.27/20.92 tff(c_1525, plain, (ip(uri_rdfs_subClassOf)=true)). % 33.27/20.92 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.27/20.92 tff(c_1431, plain, (ip(uri_rdf__3)=true)). % 33.27/20.92 tff(c_1382, plain, (ip(uri_rdf_value)=true)). % 33.27/20.92 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.27/20.92 tff(c_1340, plain, (ip(uri_rdfs_range)=true)). % 33.27/20.92 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.27/20.92 tff(c_1303, plain, (ip(uri_rdf_subject)=true)). % 33.27/20.92 tff(c_30, plain, (![P_10]: (ifeq(iext(uri_rdf_type, P_10, uri_rdf_Property), true, ip(P_10), true)=true))). % 33.27/20.92 tff(c_1215, plain, (ip(uri_rdf_type)=true)). % 33.27/20.92 tff(c_156, plain, (![C_39]: (ifeq(ic(C_39), true, iext(uri_rdfs_subClassOf, C_39, C_39), true)=true))). % 33.27/20.92 tff(c_1150, plain, (ic(uri_rdfs_Container)=true)). % 33.27/20.92 tff(c_1118, plain, (ip(uri_rdfs_seeAlso)=true)). % 33.27/20.92 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.27/20.92 tff(c_865, plain, (ic(uri_rdfs_Datatype)=true)). % 33.27/20.92 tff(c_162, plain, (![P_43, Q_44]: (ifeq(iext(uri_rdfs_subPropertyOf, P_43, Q_44), true, ip(Q_44), true)=true))). % 33.27/20.92 tff(c_812, plain, (ic(uri_rdfs_Literal)=true)). % 33.27/20.92 tff(c_745, plain, (ic(uri_rdf_Bag)=true)). % 33.27/20.92 tff(c_150, plain, (![C_35, D_36]: (ifeq(iext(uri_rdfs_subClassOf, C_35, D_36), true, ic(D_36), true)=true))). % 33.27/20.92 tff(c_702, plain, (ic(uri_rdf_Alt)=true)). % 33.27/20.92 tff(c_170, plain, (![P_51]: (ifeq(ip(P_51), true, iext(uri_rdfs_subPropertyOf, P_51, P_51), true)=true))). % 33.27/20.92 tff(c_58, plain, (![C_15]: (ifeq(ic(C_15), true, iext(uri_rdfs_subClassOf, C_15, uri_rdfs_Resource), true)=true))). % 33.27/20.92 tff(c_654, plain, (ic(uri_rdfs_ContainerMembershipProperty)=true)). % 33.27/20.92 tff(c_152, plain, (![C_37, D_38]: (ifeq(iext(uri_rdfs_subClassOf, C_37, D_38), true, ic(C_37), true)=true))). % 33.27/20.92 tff(c_556, plain, (ip(uri_rdfs_isDefinedBy)=true)). % 33.27/20.92 tff(c_28, plain, (![P_9]: (ifeq(ip(P_9), true, iext(uri_rdf_type, P_9, uri_rdf_Property), true)=true))). % 33.27/20.93 tff(c_164, plain, (![P_45, Q_46]: (ifeq(iext(uri_rdfs_subPropertyOf, P_45, Q_46), true, ip(P_45), true)=true))). % 33.27/20.93 tff(c_124, plain, (![X_27]: (ifeq(lv(X_27), true, icext(uri_rdfs_Literal, X_27), true)=true))). % 33.27/20.93 tff(c_114, plain, (![X_22]: (ifeq(ic(X_22), true, icext(uri_rdfs_Class, X_22), true)=true))). % 33.27/20.93 tff(c_122, plain, (![X_26]: (ifeq(icext(uri_rdfs_Literal, X_26), true, lv(X_26), true)=true))). % 33.27/20.93 tff(c_502, plain, (![X_62]: (icext(uri_rdfs_Resource, X_62)=true))). % 33.27/20.93 tff(c_116, plain, (![X_23]: (ifeq(icext(uri_rdfs_Class, X_23), true, ic(X_23), true)=true))). % 33.27/20.93 tff(c_197, plain, (![X_8]: (ifeq(lv(X_8), true, true, true)=true))). % 33.27/20.93 tff(c_2, plain, (![A_1, B_2, C_3]: (ifeq(A_1, A_1, B_2, C_3)=B_2))). % 33.27/20.93 tff(c_154, plain, (iext(uri_rdfs_range, uri_rdfs_subClassOf, uri_rdfs_Class)=true)). % 33.27/20.93 tff(c_48, plain, (iext(uri_rdfs_range, uri_rdfs_label, uri_rdfs_Literal)=true)). % 33.27/20.93 tff(c_144, plain, (iext(uri_rdfs_range, uri_rdf_subject, uri_rdfs_Resource)=true)). % 33.27/20.93 tff(c_60, plain, (iext(uri_rdfs_domain, uri_rdf_first, uri_rdf_List)=true)). % 33.27/20.93 tff(c_96, plain, (iext(uri_rdf_type, uri_rdf__3, uri_rdfs_ContainerMembershipProperty)=true)). % 33.27/20.93 tff(c_100, plain, (iext(uri_rdfs_subClassOf, uri_rdf_XMLLiteral, uri_rdfs_Literal)=true)). % 33.27/20.93 tff(c_64, plain, (iext(uri_rdfs_domain, uri_rdf_rest, uri_rdf_List)=true)). % 33.27/20.93 tff(c_102, plain, (iext(uri_rdf_type, uri_rdf_XMLLiteral, uri_rdfs_Datatype)=true)). % 33.27/20.93 tff(c_178, plain, (iext(uri_rdfs_domain, uri_rdf_value, uri_rdfs_Resource)=true)). % 33.27/20.93 tff(c_12, plain, (iext(uri_rdf_type, uri_rdf_nil, uri_rdf_List)=true)). % 33.27/20.93 tff(c_146, plain, (iext(uri_rdfs_domain, uri_rdfs_subClassOf, uri_rdfs_Class)=true)). % 33.27/20.93 tff(c_14, plain, (iext(uri_rdf_type, uri_rdf_rest, uri_rdf_Property)=true)). % 33.27/20.93 tff(c_106, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, uri_rdfs_Class)=true)). % 33.27/20.93 tff(c_184, plain, (iext(uri_owl_propertyChainAxiom, uri_owl_sameAs, sK2_testcase_premise_fullish_027_Inferred_Property_Characteristics_II_BNODE_l1)=true)). % 33.27/20.93 tff(c_190, plain, (iext(uri_rdf_first, sK2_testcase_premise_fullish_027_Inferred_Property_Characteristics_II_BNODE_l1, uri_ex_p)=true)). % 33.27/20.93 tff(c_20, plain, (iext(uri_rdf_type, uri_rdf__3, uri_rdf_Property)=true)). % 33.27/20.93 tff(c_112, plain, (iext(uri_rdfs_range, uri_rdfs_domain, uri_rdfs_Class)=true)). % 33.27/20.93 tff(c_16, plain, (iext(uri_rdf_type, uri_rdf__1, uri_rdf_Property)=true)). % 33.27/20.93 tff(c_22, plain, (iext(uri_rdf_type, uri_rdf_object, uri_rdf_Property)=true)). % 33.27/20.93 tff(c_84, plain, (iext(uri_rdfs_domain, uri_rdf__3, uri_rdfs_Resource)=true)). % 33.27/20.93 tff(c_36, plain, (iext(uri_rdfs_domain, uri_rdfs_comment, uri_rdfs_Resource)=true)). % 33.27/20.93 tff(c_92, plain, (iext(uri_rdf_type, uri_rdf__1, uri_rdfs_ContainerMembershipProperty)=true)). % 33.27/20.93 tff(c_168, plain, (iext(uri_rdfs_range, uri_rdfs_subPropertyOf, uri_rdf_Property)=true)). % 33.27/20.93 tff(c_160, plain, (iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, uri_rdf_Property)=true)). % 33.27/20.93 tff(c_174, plain, (iext(uri_rdfs_domain, uri_rdf_type, uri_rdfs_Resource)=true)). % 33.27/20.93 tff(c_42, plain, (iext(uri_rdfs_range, uri_rdfs_isDefinedBy, uri_rdfs_Resource)=true)). % 33.27/20.93 tff(c_98, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Seq, uri_rdfs_Container)=true)). % 33.27/20.93 tff(c_126, plain, (iext(uri_rdf_type, uri_rdf_Property, uri_rdfs_Class)=true)). % 33.27/20.93 tff(c_142, plain, (iext(uri_rdfs_domain, uri_rdf_subject, uri_rdfs_Statement)=true)). % 33.27/20.93 tff(c_86, plain, (iext(uri_rdfs_range, uri_rdf__1, uri_rdfs_Resource)=true)). % 33.27/20.93 tff(c_24, plain, (iext(uri_rdf_type, uri_rdf_value, uri_rdf_Property)=true)). % 33.27/20.93 tff(c_80, plain, (iext(uri_rdfs_domain, uri_rdf__1, uri_rdfs_Resource)=true)). % 33.27/20.93 tff(c_38, plain, (iext(uri_rdfs_range, uri_rdfs_comment, uri_rdfs_Literal)=true)). % 33.27/20.93 tff(c_108, plain, (iext(uri_rdfs_domain, uri_rdfs_domain, uri_rdf_Property)=true)). % 33.27/20.93 tff(c_50, plain, (iext(uri_rdfs_domain, uri_rdfs_seeAlso, uri_rdfs_Resource)=true)). % 33.27/20.93 tff(c_94, plain, (iext(uri_rdf_type, uri_rdf__2, uri_rdfs_ContainerMembershipProperty)=true)). % 33.27/20.93 tff(c_68, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Alt, uri_rdfs_Container)=true)). % 33.27/20.93 tff(c_182, plain, (iext(uri_owl_inverseOf, sK1_testcase_premise_fullish_027_Inferred_Property_Characteristics_II_BNODE_v, uri_ex_p)=true)). % 33.27/20.93 tff(c_88, plain, (iext(uri_rdfs_range, uri_rdf__2, uri_rdfs_Resource)=true)). % 33.27/20.93 tff(c_78, plain, (iext(uri_rdfs_range, uri_rdfs_member, uri_rdfs_Resource)=true)). % 33.27/20.93 tff(c_70, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Bag, uri_rdfs_Container)=true)). % 33.27/20.93 tff(c_186, plain, (iext(uri_rdf_rest, sK2_testcase_premise_fullish_027_Inferred_Property_Characteristics_II_BNODE_l1, sK3_testcase_premise_fullish_027_Inferred_Property_Characteristics_II_BNODE_l2)=true)). % 33.27/20.93 tff(c_82, plain, (iext(uri_rdfs_domain, uri_rdf__2, uri_rdfs_Resource)=true)). % 33.27/20.93 tff(c_40, plain, (iext(uri_rdfs_domain, uri_rdfs_isDefinedBy, uri_rdfs_Resource)=true)). % 33.27/20.93 tff(c_46, plain, (iext(uri_rdfs_domain, uri_rdfs_label, uri_rdfs_Resource)=true)). % 33.27/20.93 tff(c_192, plain, (iext(uri_rdf_first, sK3_testcase_premise_fullish_027_Inferred_Property_Characteristics_II_BNODE_l2, sK1_testcase_premise_fullish_027_Inferred_Property_Characteristics_II_BNODE_v)=true)). % 33.27/20.93 tff(c_74, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, uri_rdf_Property)=true)). % 33.27/20.93 tff(c_52, plain, (iext(uri_rdfs_range, uri_rdfs_seeAlso, uri_rdfs_Resource)=true)). % 33.27/20.93 tff(c_176, plain, (iext(uri_rdfs_range, uri_rdf_type, uri_rdfs_Class)=true)). % 33.27/20.93 tff(c_76, plain, (iext(uri_rdfs_domain, uri_rdfs_member, uri_rdfs_Resource)=true)). % 33.27/20.93 tff(c_134, plain, (iext(uri_rdfs_domain, uri_rdf_object, uri_rdfs_Statement)=true)). % 33.27/20.93 tff(c_44, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_isDefinedBy, uri_rdfs_seeAlso)=true)). % 33.27/20.93 tff(c_18, plain, (iext(uri_rdf_type, uri_rdf__2, uri_rdf_Property)=true)). % 33.27/20.93 tff(c_140, plain, (iext(uri_rdfs_range, uri_rdf_predicate, uri_rdfs_Resource)=true)). % 33.27/20.93 tff(c_90, plain, (iext(uri_rdfs_range, uri_rdf__3, uri_rdfs_Resource)=true)). % 33.27/20.93 tff(c_62, plain, (iext(uri_rdfs_range, uri_rdf_first, uri_rdfs_Resource)=true)). % 33.27/20.93 tff(c_132, plain, (iext(uri_rdfs_range, uri_rdfs_range, uri_rdfs_Class)=true)). % 33.27/20.93 tff(c_10, plain, (iext(uri_rdf_type, uri_rdf_first, uri_rdf_Property)=true)). % 33.27/20.93 tff(c_34, plain, (iext(uri_rdf_type, uri_rdf_type, uri_rdf_Property)=true)). % 33.27/20.93 tff(c_26, plain, (iext(uri_rdf_type, uri_rdf_subject, uri_rdf_Property)=true)). % 33.27/20.93 tff(c_138, plain, (iext(uri_rdfs_domain, uri_rdf_predicate, uri_rdfs_Statement)=true)). % 33.27/20.93 tff(c_66, plain, (iext(uri_rdfs_range, uri_rdf_rest, uri_rdf_List)=true)). % 33.27/20.93 tff(c_128, plain, (iext(uri_rdfs_domain, uri_rdfs_range, uri_rdf_Property)=true)). % 33.27/20.93 tff(c_180, plain, (iext(uri_rdfs_range, uri_rdf_value, uri_rdfs_Resource)=true)). % 33.27/20.93 tff(c_188, plain, (iext(uri_rdf_rest, sK3_testcase_premise_fullish_027_Inferred_Property_Characteristics_II_BNODE_l2, uri_rdf_nil)=true)). % 33.27/20.93 tff(c_194, plain, (iext(uri_rdf_type, uri_ex_p, uri_owl_InverseFunctionalProperty)!=true)). % 33.27/20.93 tff(c_6, plain, (![X_7]: (ir(X_7)=true))). % 33.27/20.93 % SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 33.27/20.93 %------------------------------------------------------------------------------