%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : SWB010-10 : TPTP v9.0.0. Released v7.3.0. % Transfm : none % Format : tptp:raw % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % Computer : n010.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:48 PM UTC 2025 % Result : Satisfiable 37.73s 25.71s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.13 % Problem : SWB010-10 : TPTP v9.0.0. Released v7.3.0. % 0.11/0.14 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % 0.13/0.35 % Computer : n010.cluster.edu % 0.13/0.35 % Model : x86_64 x86_64 % 0.13/0.35 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.35 % Memory : 8042.1875MB % 0.13/0.35 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.35 % CPULimit : 300 % 0.13/0.35 % WCLimit : 300 % 0.13/0.35 % DateTime : Wed Apr 9 00:54:48 EDT 2025 % 0.13/0.35 % CPUTime : % 37.73/25.70 % 37.73/25.71 % SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 37.73/25.71 % 37.73/25.71 % SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 37.73/25.73 %$ tuple > 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_targetIndividual > uri_owl_sourceIndividual > uri_owl_oneOf > uri_owl_onProperty > uri_owl_complementOf > uri_owl_assertionProperty > uri_owl_allValuesFrom > uri_owl_ObjectProperty > uri_owl_NegativePropertyAssertion > uri_ex_s > uri_ex_p > uri_ex_o > true > sK4_testcase_premise_fullish_010_Negative_Property_Assertions_BNODE_x2 > sK3_testcase_premise_fullish_010_Negative_Property_Assertions_BNODE_x1 > sK2_testcase_premise_fullish_010_Negative_Property_Assertions_BNODE_x4 > sK1_testcase_premise_fullish_010_Negative_Property_Assertions_BNODE_x3 % 37.73/25.73 % 37.73/25.73 %Foreground sorts: % 37.73/25.73 % 37.73/25.73 % 37.73/25.73 %Background operators: % 37.73/25.73 % 37.73/25.73 % 37.73/25.73 %Foreground operators: % 37.73/25.73 tff(uri_rdfs_Datatype, type, uri_rdfs_Datatype: $i). % 37.73/25.73 tff(uri_owl_complementOf, type, uri_owl_complementOf: $i). % 37.73/25.73 tff(sK3_testcase_premise_fullish_010_Negative_Property_Assertions_BNODE_x1, type, sK3_testcase_premise_fullish_010_Negative_Property_Assertions_BNODE_x1: $i). % 37.73/25.73 tff(uri_rdfs_ContainerMembershipProperty, type, uri_rdfs_ContainerMembershipProperty: $i). % 37.73/25.73 tff(uri_owl_oneOf, type, uri_owl_oneOf: $i). % 37.73/25.73 tff(uri_rdfs_Resource, type, uri_rdfs_Resource: $i). % 37.73/25.73 tff(uri_rdf_Property, type, uri_rdf_Property: $i). % 37.73/25.73 tff(uri_rdf_subject, type, uri_rdf_subject: $i). % 37.73/25.73 tff(uri_owl_NegativePropertyAssertion, type, uri_owl_NegativePropertyAssertion: $i). % 37.73/25.73 tff(uri_rdf_type, type, uri_rdf_type: $i). % 37.73/25.73 tff(uri_owl_onProperty, type, uri_owl_onProperty: $i). % 37.73/25.73 tff(uri_rdfs_subPropertyOf, type, uri_rdfs_subPropertyOf: $i). % 37.73/25.73 tff(uri_rdfs_seeAlso, type, uri_rdfs_seeAlso: $i). % 37.73/25.73 tff(icext, type, icext: ($i * $i) > $i). % 37.73/25.73 tff(uri_rdfs_range, type, uri_rdfs_range: $i). % 37.73/25.73 tff(uri_rdf_XMLLiteral, type, uri_rdf_XMLLiteral: $i). % 37.73/25.73 tff(uri_owl_assertionProperty, type, uri_owl_assertionProperty: $i). % 37.73/25.73 tff(uri_rdf_List, type, uri_rdf_List: $i). % 37.73/25.73 tff(uri_ex_s, type, uri_ex_s: $i). % 37.73/25.73 tff(uri_rdf_first, type, uri_rdf_first: $i). % 37.73/25.73 tff(uri_rdf_predicate, type, uri_rdf_predicate: $i). % 37.73/25.73 tff(ir, type, ir: $i > $i). % 37.73/25.73 tff(lv, type, lv: $i > $i). % 37.73/25.73 tff(uri_rdf__3, type, uri_rdf__3: $i). % 37.73/25.73 tff(uri_rdf_value, type, uri_rdf_value: $i). % 37.73/25.73 tff(ic, type, ic: $i > $i). % 37.73/25.73 tff(uri_rdfs_Statement, type, uri_rdfs_Statement: $i). % 37.73/25.73 tff(uri_ex_p, type, uri_ex_p: $i). % 37.73/25.73 tff(uri_rdf__1, type, uri_rdf__1: $i). % 37.73/25.73 tff(iext, type, iext: ($i * $i * $i) > $i). % 37.73/25.73 tff(uri_rdf_rest, type, uri_rdf_rest: $i). % 37.73/25.73 tff(uri_rdfs_label, type, uri_rdfs_label: $i). % 37.73/25.73 tff(uri_rdfs_Container, type, uri_rdfs_Container: $i). % 37.73/25.73 tff(uri_owl_allValuesFrom, type, uri_owl_allValuesFrom: $i). % 37.73/25.73 tff(uri_owl_ObjectProperty, type, uri_owl_ObjectProperty: $i). % 37.73/25.73 tff(uri_rdfs_subClassOf, type, uri_rdfs_subClassOf: $i). % 37.73/25.73 tff(sK1_testcase_premise_fullish_010_Negative_Property_Assertions_BNODE_x3, type, sK1_testcase_premise_fullish_010_Negative_Property_Assertions_BNODE_x3: $i). % 37.73/25.73 tff(uri_owl_sourceIndividual, type, uri_owl_sourceIndividual: $i). % 37.73/25.73 tff(uri_rdf_object, type, uri_rdf_object: $i). % 37.73/25.73 tff(ip, type, ip: $i > $i). % 37.73/25.73 tff(uri_rdfs_Class, type, uri_rdfs_Class: $i). % 37.73/25.73 tff(uri_rdfs_Seq, type, uri_rdfs_Seq: $i). % 37.73/25.73 tff(sK2_testcase_premise_fullish_010_Negative_Property_Assertions_BNODE_x4, type, sK2_testcase_premise_fullish_010_Negative_Property_Assertions_BNODE_x4: $i). % 37.73/25.73 tff(uri_rdfs_member, type, uri_rdfs_member: $i). % 37.73/25.73 tff(uri_rdf_Bag, type, uri_rdf_Bag: $i). % 37.73/25.73 tff(uri_rdf__2, type, uri_rdf__2: $i). % 37.73/25.73 tff(uri_rdfs_comment, type, uri_rdfs_comment: $i). % 37.73/25.73 tff(uri_rdfs_Literal, type, uri_rdfs_Literal: $i). % 37.73/25.73 tff(true, type, true: $i). % 37.73/25.73 tff(uri_owl_targetIndividual, type, uri_owl_targetIndividual: $i). % 37.73/25.73 tff(uri_rdf_Alt, type, uri_rdf_Alt: $i). % 37.73/25.73 tff(uri_rdf_nil, type, uri_rdf_nil: $i). % 37.73/25.73 tff(uri_ex_o, type, uri_ex_o: $i). % 37.73/25.73 tff(tuple, type, tuple: ($i * $i * $i * $i) > $i). % 37.73/25.73 tff(sK4_testcase_premise_fullish_010_Negative_Property_Assertions_BNODE_x2, type, sK4_testcase_premise_fullish_010_Negative_Property_Assertions_BNODE_x2: $i). % 37.73/25.73 tff(uri_rdfs_isDefinedBy, type, uri_rdfs_isDefinedBy: $i). % 37.73/25.73 tff(uri_rdfs_domain, type, uri_rdfs_domain: $i). % 37.73/25.73 tff(ifeq, type, ifeq: ($i * $i * $i * $i) > $i). % 37.73/25.73 % 37.73/25.73 %Saturated clause set: % 37.73/25.73 tff(c_15106, 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))). % 37.73/25.73 tff(c_14641, 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))). % 37.73/25.73 tff(c_14638, 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))). % 37.73/25.73 tff(c_78810, plain, (![X_1306, Y_1307]: (ifeq(iext(uri_rdfs_comment, X_1306, Y_1307), true, iext(uri_rdfs_comment, X_1306, Y_1307), true)=true))). % 37.73/25.73 tff(c_78783, plain, (![X_1302, Y_1303]: (ifeq(iext(uri_rdfs_label, X_1302, Y_1303), true, iext(uri_rdfs_label, X_1302, Y_1303), true)=true))). % 37.73/25.73 tff(c_78756, plain, (![X_1298, Y_1299]: (ifeq(iext(uri_rdf_predicate, X_1298, Y_1299), true, iext(uri_rdf_predicate, X_1298, Y_1299), true)=true))). % 37.73/25.73 tff(c_15044, 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))). % 37.73/25.73 tff(c_14954, 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))). % 37.73/25.73 tff(c_16220, 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))). % 37.73/25.73 tff(c_78336, plain, (![X_1291, Y_1292]: (ifeq(iext(uri_rdfs_member, X_1291, Y_1292), true, iext(uri_rdfs_member, X_1291, Y_1292), true)=true))). % 37.73/25.73 tff(c_5090, 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))). % 37.73/25.73 tff(c_14883, 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))). % 37.73/25.73 tff(c_14584, 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))). % 37.73/25.73 tff(c_5093, 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))). % 37.73/25.73 tff(c_14818, 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))). % 37.73/25.73 tff(c_14332, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subClassOf), true, ifeq(iext(P_47, sK3_testcase_premise_fullish_010_Negative_Property_Assertions_BNODE_x1, uri_rdfs_Resource), true, true, true), true)=true))). % 37.73/25.73 tff(c_77228, plain, (![C_1281]: (ifeq(iext(uri_rdfs_subClassOf, C_1281, uri_rdf_List), true, iext(uri_rdfs_subClassOf, C_1281, uri_rdfs_Resource), true)=true))). % 37.73/25.73 tff(c_13066, 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))). % 37.73/25.73 tff(c_76937, plain, (![C_1278]: (ifeq(iext(uri_rdfs_subClassOf, C_1278, uri_rdfs_Statement), true, iext(uri_rdfs_subClassOf, C_1278, uri_rdfs_Resource), true)=true))). % 37.73/25.73 tff(c_14266, 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))). % 37.73/25.73 tff(c_76646, plain, (![C_1275]: (ifeq(iext(uri_rdfs_subClassOf, C_1275, sK3_testcase_premise_fullish_010_Negative_Property_Assertions_BNODE_x1), true, iext(uri_rdfs_subClassOf, C_1275, uri_rdfs_Resource), true)=true))). % 37.73/25.73 tff(c_76491, plain, (![C_1273]: (ifeq(iext(uri_rdfs_subClassOf, C_1273, uri_owl_ObjectProperty), true, iext(uri_rdfs_subClassOf, C_1273, uri_rdfs_Resource), true)=true))). % 37.73/25.73 tff(c_13737, 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))). % 37.73/25.73 tff(c_14174, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subClassOf), true, ifeq(iext(P_47, uri_owl_ObjectProperty, uri_owl_ObjectProperty), true, true, true), true)=true))). % 37.73/25.73 tff(c_13515, 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))). % 37.73/25.73 tff(c_13581, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subClassOf), true, ifeq(iext(P_47, uri_owl_ObjectProperty, uri_rdfs_Resource), true, true, true), true)=true))). % 37.73/25.73 tff(c_14108, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subClassOf), true, ifeq(iext(P_47, sK3_testcase_premise_fullish_010_Negative_Property_Assertions_BNODE_x1, sK3_testcase_premise_fullish_010_Negative_Property_Assertions_BNODE_x1), true, true, true), true)=true))). % 37.73/25.73 tff(c_8313, 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))). % 37.73/25.73 tff(c_12771, 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))). % 37.73/25.74 tff(c_9041, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdf_Property), true, ifeq(iext(P_28, X_30, uri_owl_complementOf), true, true, true), true)=true))). % 37.73/25.74 tff(c_6880, 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))). % 37.73/25.74 tff(c_9038, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdf_Property), true, ifeq(iext(P_18, uri_owl_complementOf, Y_21), true, true, true), true)=true))). % 37.73/25.74 tff(c_7209, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdf_Property), true, ifeq(iext(P_18, uri_owl_onProperty, Y_21), true, true, true), true)=true))). % 37.73/25.74 tff(c_10085, 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))). % 37.73/25.74 tff(c_9483, 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))). % 37.73/25.74 tff(c_12524, 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))). % 37.73/25.74 tff(c_12724, 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))). % 37.73/25.74 tff(c_9480, 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))). % 37.73/25.74 tff(c_6698, 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))). % 37.73/25.74 tff(c_8476, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdf_Property), true, ifeq(iext(P_18, uri_owl_oneOf, Y_21), true, true, true), true)=true))). % 37.73/25.74 tff(c_11829, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdf_Property), true, ifeq(iext(P_18, uri_rdfs_isDefinedBy, Y_21), true, true, true), true)=true))). % 37.73/25.74 tff(c_8479, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdf_Property), true, ifeq(iext(P_28, X_30, uri_owl_oneOf), true, true, true), true)=true))). % 37.73/25.74 tff(c_12650, 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))). % 37.73/25.74 tff(c_12890, 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))). % 37.73/25.74 tff(c_7212, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdf_Property), true, ifeq(iext(P_28, X_30, uri_owl_onProperty), true, true, true), true)=true))). % 37.73/25.74 tff(c_10530, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdf_Property), true, ifeq(iext(P_28, X_30, uri_owl_allValuesFrom), true, true, true), true)=true))). % 37.73/25.74 tff(c_12938, 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))). % 37.73/25.74 tff(c_6877, 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))). % 37.73/25.74 tff(c_12986, 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))). % 37.73/25.74 tff(c_11832, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdf_Property), true, ifeq(iext(P_28, X_30, uri_rdfs_isDefinedBy), true, true, true), true)=true))). % 37.73/25.74 tff(c_8310, 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))). % 37.73/25.74 tff(c_12843, 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))). % 37.73/25.74 tff(c_6701, 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))). % 37.73/25.74 tff(c_12602, 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))). % 37.73/25.74 tff(c_10527, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdf_Property), true, ifeq(iext(P_18, uri_owl_allValuesFrom, Y_21), true, true, true), true)=true))). % 37.73/25.74 tff(c_10088, 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))). % 37.73/25.74 tff(c_12426, 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))). % 37.73/25.74 tff(c_12474, 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))). % 37.73/25.74 tff(c_14052, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, sK3_testcase_premise_fullish_010_Negative_Property_Assertions_BNODE_x1, uri_rdfs_Class), true, true, true), true)=true))). % 37.73/25.74 tff(c_13355, 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))). % 37.73/25.74 tff(c_16122, 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))). % 37.73/25.74 tff(c_12255, 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))). % 37.73/25.74 tff(c_12379, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, uri_owl_ObjectProperty, uri_rdfs_Class), true, true, true), true)=true))). % 37.73/25.74 tff(c_15274, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, sK2_testcase_premise_fullish_010_Negative_Property_Assertions_BNODE_x4, uri_rdf_List), true, true, true), true)=true))). % 37.73/25.74 tff(c_7438, 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))). % 37.73/25.74 tff(c_8073, 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))). % 37.73/25.74 tff(c_11746, 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))). % 37.73/25.74 tff(c_4608, 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))). % 37.73/25.74 tff(c_8654, 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))). % 37.73/25.74 tff(c_11461, 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))). % 37.73/25.74 tff(c_69813, plain, (![C_1202]: (ifeq(iext(uri_rdfs_subClassOf, C_1202, uri_rdfs_Literal), true, iext(uri_rdfs_subClassOf, C_1202, uri_rdfs_Resource), true)=true))). % 37.73/25.74 tff(c_4360, 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))). % 37.73/25.74 tff(c_12115, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subPropertyOf), true, ifeq(iext(P_47, uri_owl_oneOf, uri_owl_oneOf), true, true, true), true)=true))). % 37.73/25.74 tff(c_4662, 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))). % 37.73/25.74 tff(c_4510, 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))). % 37.73/25.74 tff(c_69091, plain, (![C_1193]: (ifeq(iext(uri_rdfs_subClassOf, C_1193, uri_rdfs_Seq), true, iext(uri_rdfs_subClassOf, C_1193, uri_rdfs_Resource), true)=true))). % 37.73/25.74 tff(c_69024, plain, (![P_1191]: (ifeq(iext(uri_rdfs_subPropertyOf, P_1191, uri_rdf__2), true, iext(uri_rdfs_subPropertyOf, P_1191, uri_rdfs_member), true)=true))). % 37.73/25.74 tff(c_68869, plain, (![C_1189]: (ifeq(iext(uri_rdfs_subClassOf, C_1189, uri_rdfs_ContainerMembershipProperty), true, iext(uri_rdfs_subClassOf, C_1189, uri_rdfs_Resource), true)=true))). % 37.73/25.74 tff(c_4659, 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))). % 37.73/25.74 tff(c_7629, 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))). % 37.73/25.74 tff(c_10785, 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))). % 37.73/25.74 tff(c_68302, plain, (![C_1183]: (ifeq(iext(uri_rdfs_subClassOf, C_1183, uri_rdfs_Datatype), true, iext(uri_rdfs_subClassOf, C_1183, uri_rdfs_Resource), true)=true))). % 37.73/25.74 tff(c_68259, plain, (![X_1179, Y_1180]: (ifeq(iext(uri_owl_complementOf, X_1179, Y_1180), true, iext(uri_owl_complementOf, X_1179, Y_1180), true)=true))). % 37.73/25.74 tff(c_68154, plain, (![X_1174, Y_1175]: (ifeq(iext(uri_rdfs_isDefinedBy, X_1174, Y_1175), true, iext(uri_rdfs_isDefinedBy, X_1174, Y_1175), true)=true))). % 37.73/25.74 tff(c_68077, plain, (![C_1173]: (ifeq(iext(uri_rdfs_subClassOf, C_1173, uri_rdf_Bag), true, iext(uri_rdfs_subClassOf, C_1173, uri_rdfs_Resource), true)=true))). % 37.73/25.74 tff(c_11143, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subPropertyOf), true, ifeq(iext(P_47, uri_owl_onProperty, uri_owl_onProperty), true, true, true), true)=true))). % 37.73/25.75 tff(c_67920, plain, (![X_1168, Y_1169]: (ifeq(iext(uri_rdf__1, X_1168, Y_1169), true, iext(uri_rdf__1, X_1168, Y_1169), true)=true))). % 37.73/25.75 tff(c_8002, 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))). % 37.73/25.75 tff(c_7378, 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))). % 37.73/25.75 tff(c_11305, 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))). % 37.73/25.75 tff(c_6644, 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))). % 37.73/25.75 tff(c_9304, 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))). % 37.73/25.75 tff(c_67100, plain, (![C_1161]: (ifeq(iext(uri_rdfs_subClassOf, C_1161, uri_rdf_XMLLiteral), true, iext(uri_rdfs_subClassOf, C_1161, uri_rdfs_Resource), true)=true))). % 37.73/25.75 tff(c_67073, plain, (![X_1157, Y_1158]: (ifeq(iext(uri_rdf__3, X_1157, Y_1158), true, iext(uri_rdf__3, X_1157, Y_1158), true)=true))). % 37.73/25.75 tff(c_8596, 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))). % 37.73/25.75 tff(c_66773, plain, (![C_1154]: (ifeq(iext(uri_rdfs_subClassOf, C_1154, uri_rdf_Property), true, iext(uri_rdfs_subClassOf, C_1154, uri_rdfs_Resource), true)=true))). % 37.73/25.75 tff(c_4363, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdfs_Class), true, ifeq(iext(P_28, X_30, uri_rdf_Bag), true, true, true), true)=true))). % 37.73/25.75 tff(c_4415, 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))). % 37.73/25.75 tff(c_66326, plain, (![X_1145, Y_1146]: (ifeq(iext(uri_rdf_value, X_1145, Y_1146), true, iext(uri_rdf_value, X_1145, Y_1146), true)=true))). % 37.73/25.75 tff(c_5808, 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))). % 37.73/25.75 tff(c_10384, 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))). % 37.73/25.75 tff(c_66128, plain, (![P_1142]: (ifeq(iext(uri_rdfs_subPropertyOf, P_1142, uri_rdf__1), true, iext(uri_rdfs_subPropertyOf, P_1142, uri_rdfs_member), true)=true))). % 37.73/25.75 tff(c_6390, 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))). % 37.73/25.75 tff(c_65965, plain, (![X_1137, Y_1138]: (ifeq(iext(uri_rdf__3, X_1137, Y_1138), true, iext(uri_rdfs_member, X_1137, Y_1138), true)=true))). % 37.73/25.75 tff(c_6823, 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))). % 37.73/25.75 tff(c_65768, plain, (![P_1134]: (ifeq(iext(uri_rdfs_subPropertyOf, P_1134, uri_rdf__3), true, iext(uri_rdfs_subPropertyOf, P_1134, uri_rdfs_member), true)=true))). % 37.73/25.75 tff(c_8422, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, uri_owl_oneOf, uri_rdf_Property), true, true, true), true)=true))). % 37.73/25.75 tff(c_65611, plain, (![X_1129, Y_1130]: (ifeq(iext(uri_rdf__2, X_1129, Y_1130), true, iext(uri_rdf__2, X_1129, Y_1130), true)=true))). % 37.73/25.75 tff(c_4611, 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))). % 37.73/25.75 tff(c_64846, plain, (![X_1123, Y_1124]: (ifeq(iext(uri_rdfs_subPropertyOf, X_1123, Y_1124), true, iext(uri_rdfs_subPropertyOf, X_1123, Y_1124), true)=true))). % 37.73/25.75 tff(c_8922, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subPropertyOf), true, ifeq(iext(P_47, uri_owl_complementOf, uri_owl_complementOf), true, true, true), true)=true))). % 37.73/25.75 tff(c_4316, 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))). % 37.73/25.75 tff(c_64529, plain, (![X_1114, Y_1115]: (ifeq(iext(uri_rdf_subject, X_1114, Y_1115), true, iext(uri_rdf_subject, X_1114, Y_1115), true)=true))). % 37.73/25.75 tff(c_64516, plain, (![X_1112, Y_1113]: (ifeq(iext(uri_rdf__1, X_1112, Y_1113), true, iext(uri_rdfs_member, X_1112, Y_1113), true)=true))). % 37.73/25.75 tff(c_9736, 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))). % 37.73/25.75 tff(c_7155, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, uri_owl_onProperty, uri_rdf_Property), true, true, true), true)=true))). % 37.73/25.75 tff(c_4513, 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))). % 37.73/25.75 tff(c_10448, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, uri_owl_allValuesFrom, uri_rdf_Property), true, true, true), true)=true))). % 37.73/25.75 tff(c_11975, 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))). % 37.73/25.75 tff(c_12182, 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))). % 37.73/25.75 tff(c_8984, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, uri_owl_complementOf, uri_rdf_Property), true, true, true), true)=true))). % 37.73/25.75 tff(c_11688, 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))). % 37.73/25.75 tff(c_62141, plain, (![X_1095, Y_1096]: (ifeq(iext(uri_rdfs_subClassOf, X_1095, Y_1096), true, iext(uri_rdfs_subClassOf, X_1095, Y_1096), true)=true))). % 37.73/25.75 tff(c_8832, 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))). % 37.73/25.75 tff(c_7570, 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))). % 37.73/25.75 tff(c_4568, 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))). % 37.73/25.75 tff(c_61249, plain, (![C_1087]: (ifeq(iext(uri_rdfs_subClassOf, C_1087, uri_rdfs_Container), true, iext(uri_rdfs_subClassOf, C_1087, uri_rdfs_Resource), true)=true))). % 37.73/25.75 tff(c_9807, 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))). % 37.73/25.75 tff(c_5872, 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))). % 37.73/25.75 tff(c_8742, 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))). % 37.73/25.75 tff(c_5142, 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))). % 37.73/25.75 tff(c_4418, 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))). % 37.73/25.75 tff(c_5360, 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))). % 37.73/25.75 tff(c_60402, plain, (![X_1076, Y_1077]: (ifeq(iext(uri_rdf_rest, X_1076, Y_1077), true, iext(uri_rdf_rest, X_1076, Y_1077), true)=true))). % 37.73/25.75 tff(c_11617, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subPropertyOf), true, ifeq(iext(P_47, uri_owl_allValuesFrom, uri_owl_allValuesFrom), true, true, true), true)=true))). % 37.73/25.75 tff(c_59617, plain, (![X_1069, Y_1070]: (ifeq(iext(uri_rdfs_domain, X_1069, Y_1070), true, iext(uri_rdfs_domain, X_1069, Y_1070), true)=true))). % 37.73/25.75 tff(c_5716, 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))). % 37.73/25.75 tff(c_4464, 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))). % 37.73/25.75 tff(c_9873, 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))). % 37.73/25.75 tff(c_4313, 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))). % 37.73/25.75 tff(c_57845, plain, (![X_1051, Y_1052]: (ifeq(iext(uri_rdfs_seeAlso, X_1051, Y_1052), true, iext(uri_rdfs_seeAlso, X_1051, Y_1052), true)=true))). % 37.73/25.75 tff(c_57801, plain, (![X_1047, Y_1048]: (ifeq(iext(uri_owl_oneOf, X_1047, Y_1048), true, iext(uri_owl_oneOf, X_1047, Y_1048), true)=true))). % 37.73/25.75 tff(c_9236, 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))). % 37.73/25.75 tff(c_4266, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdfs_Class), true, ifeq(iext(P_28, X_30, uri_rdfs_Literal), true, true, true), true)=true))). % 37.73/25.75 tff(c_5599, 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))). % 37.73/25.75 tff(c_57344, plain, (![X_1039, Y_1040]: (ifeq(iext(uri_owl_allValuesFrom, X_1039, Y_1040), true, iext(uri_owl_allValuesFrom, X_1039, Y_1040), true)=true))). % 37.73/25.75 tff(c_10655, 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))). % 37.73/25.75 tff(c_55753, plain, (![C_1028]: (ifeq(iext(uri_rdfs_subClassOf, C_1028, uri_rdfs_Class), true, iext(uri_rdfs_subClassOf, C_1028, uri_rdfs_Resource), true)=true))). % 37.73/25.75 tff(c_11052, 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))). % 37.73/25.75 tff(c_54932, plain, (![X_1019, Y_1020]: (ifeq(iext(uri_rdf_object, X_1019, Y_1020), true, iext(uri_rdf_object, X_1019, Y_1020), true)=true))). % 37.73/25.76 tff(c_4461, 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))). % 37.73/25.76 tff(c_54423, plain, (![X_1011, Y_1012]: (ifeq(iext(uri_owl_onProperty, X_1011, Y_1012), true, iext(uri_owl_onProperty, X_1011, Y_1012), true)=true))). % 37.73/25.76 tff(c_53644, plain, (![X_1007, Y_1008]: (ifeq(iext(uri_rdf_type, X_1007, Y_1008), true, iext(uri_rdf_type, X_1007, Y_1008), true)=true))). % 37.73/25.76 tff(c_53488, plain, (![C_1005]: (ifeq(iext(uri_rdfs_subClassOf, C_1005, uri_rdf_Alt), true, iext(uri_rdfs_subClassOf, C_1005, uri_rdfs_Resource), true)=true))). % 37.73/25.76 tff(c_53462, plain, (![X_1001, Y_1002]: (ifeq(iext(uri_rdf__2, X_1001, Y_1002), true, iext(uri_rdfs_member, X_1001, Y_1002), true)=true))). % 37.73/25.76 tff(c_5959, 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))). % 37.73/25.76 tff(c_4959, 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))). % 37.73/25.76 tff(c_9364, 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))). % 37.73/25.76 tff(c_9581, 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))). % 37.73/25.76 tff(c_11208, 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))). % 37.73/25.76 tff(c_52212, plain, (![X_988, Y_989]: (ifeq(iext(uri_rdf_first, X_988, Y_989), true, iext(uri_rdf_first, X_988, Y_989), true)=true))). % 37.73/25.76 tff(c_8256, 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))). % 37.73/25.76 tff(c_4565, 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))). % 37.73/25.76 tff(c_10031, 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))). % 37.73/25.76 tff(c_9426, 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))). % 37.73/25.76 tff(c_4263, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdfs_Class), true, ifeq(iext(P_18, uri_rdfs_Literal, Y_21), true, true, true), true)=true))). % 37.73/25.76 tff(c_50981, plain, (![X_975, Y_976]: (ifeq(iext(uri_rdfs_range, X_975, Y_976), true, iext(uri_rdfs_range, X_975, Y_976), true)=true))). % 37.73/25.76 tff(c_6763, 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))). % 37.98/25.76 tff(c_5513, 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))). % 37.98/25.76 tff(c_15949, 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))). % 37.98/25.76 tff(c_7887, 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))). % 37.98/25.76 tff(c_13126, 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))). % 37.98/25.76 tff(c_10928, 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))). % 37.98/25.76 tff(c_7764, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdfs_Class), true, ifeq(iext(P_28, X_30, uri_owl_ObjectProperty), true, true, true), true)=true))). % 37.98/25.76 tff(c_15232, 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_010_Negative_Property_Assertions_BNODE_x4), true, true, true), true)=true))). % 37.98/25.76 tff(c_13823, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdfs_Class), true, ifeq(iext(P_28, X_30, sK3_testcase_premise_fullish_010_Negative_Property_Assertions_BNODE_x1), true, true, true), true)=true))). % 37.98/25.76 tff(c_15229, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdf_List), true, ifeq(iext(P_18, sK2_testcase_premise_fullish_010_Negative_Property_Assertions_BNODE_x4, Y_21), true, true, true), true)=true))). % 37.98/25.76 tff(c_4859, plain, (![P_47, X_141]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, X_141, uri_rdfs_Resource), true, true, true), true)=true))). % 37.98/25.76 tff(c_13129, 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))). % 37.98/25.76 tff(c_13820, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdfs_Class), true, ifeq(iext(P_18, sK3_testcase_premise_fullish_010_Negative_Property_Assertions_BNODE_x1, Y_21), true, true, true), true)=true))). % 37.98/25.76 tff(c_10155, 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))). % 37.98/25.76 tff(c_7761, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdfs_Class), true, ifeq(iext(P_18, uri_owl_ObjectProperty, Y_21), true, true, true), true)=true))). % 37.98/25.76 tff(c_15952, 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))). % 37.98/25.76 tff(c_10152, 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))). % 37.98/25.76 tff(c_7890, 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))). % 37.98/25.76 tff(c_10931, 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))). % 37.98/25.76 tff(c_4024, 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))). % 37.98/25.76 tff(c_3780, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, sK3_testcase_premise_fullish_010_Negative_Property_Assertions_BNODE_x1), true, ifeq(iext(P_28, X_30, uri_ex_s), true, true, true), true)=true))). % 37.98/25.76 tff(c_3657, 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))). % 37.98/25.76 tff(c_3701, 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))). % 37.98/25.76 tff(c_4223, 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))). % 37.98/25.76 tff(c_4064, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_owl_ObjectProperty), true, ifeq(iext(P_28, X_30, uri_ex_p), true, true, true), true)=true))). % 37.98/25.76 tff(c_3777, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, sK3_testcase_premise_fullish_010_Negative_Property_Assertions_BNODE_x1), true, ifeq(iext(P_18, uri_ex_s, Y_21), true, true, true), true)=true))). % 37.98/25.76 tff(c_4107, 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))). % 37.98/25.76 tff(c_3738, 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))). % 37.98/25.76 tff(c_4226, 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))). % 37.98/25.76 tff(c_3549, 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))). % 37.98/25.76 tff(c_3989, 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))). % 37.98/25.76 tff(c_3654, 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))). % 37.98/25.76 tff(c_3939, 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))). % 37.98/25.76 tff(c_3590, 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))). % 37.98/25.76 tff(c_4146, 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))). % 37.98/25.76 tff(c_4021, 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))). % 37.98/25.76 tff(c_3819, 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))). % 37.98/25.76 tff(c_4143, 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))). % 37.98/25.76 tff(c_4180, 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))). % 37.98/25.76 tff(c_3741, 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))). % 37.98/25.76 tff(c_4104, 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))). % 37.98/25.76 tff(c_3900, 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))). % 37.98/25.76 tff(c_3936, 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))). % 37.98/25.76 tff(c_3593, 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))). % 37.98/25.76 tff(c_3816, 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))). % 37.98/25.76 tff(c_4061, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_owl_ObjectProperty), true, ifeq(iext(P_18, uri_ex_p, Y_21), true, true, true), true)=true))). % 37.98/25.76 tff(c_3868, 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))). % 37.98/25.76 tff(c_3698, 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))). % 37.98/25.76 tff(c_3552, 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))). % 37.98/25.76 tff(c_4183, 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))). % 37.98/25.76 tff(c_3897, 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))). % 37.98/25.76 tff(c_3986, 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))). % 37.98/25.76 tff(c_3871, 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))). % 37.98/25.76 tff(c_2071, plain, (![P_97, X_63, Y_100]: (ifeq(iext(uri_rdfs_domain, P_97, uri_rdfs_Resource), true, ifeq(iext(P_97, X_63, Y_100), true, true, true), true)=true))). % 37.98/25.76 tff(c_1712, plain, (![P_93, X_95, X_63]: (ifeq(iext(uri_rdfs_range, P_93, uri_rdfs_Resource), true, ifeq(iext(P_93, X_95, X_63), true, true, true), true)=true))). % 37.98/25.76 tff(c_2858, plain, (![P_104]: (ifeq(iext(uri_rdfs_subPropertyOf, P_104, uri_rdf_type), true, ifeq(iext(P_104, uri_rdf_type, uri_rdf_Property), true, true, true), true)=true))). % 37.98/25.77 tff(c_2519, plain, (![P_104]: (ifeq(iext(uri_rdfs_subPropertyOf, P_104, uri_rdf_type), true, ifeq(iext(P_104, uri_ex_p, uri_owl_ObjectProperty), true, true, true), true)=true))). % 37.98/25.77 tff(c_2708, plain, (![P_104]: (ifeq(iext(uri_rdfs_subPropertyOf, P_104, uri_rdfs_domain), true, ifeq(iext(P_104, uri_rdf__2, uri_rdfs_Resource), true, true, true), true)=true))). % 37.98/25.77 tff(c_2549, plain, (![P_104]: (ifeq(iext(uri_rdfs_subPropertyOf, P_104, uri_rdf_type), true, ifeq(iext(P_104, uri_rdf_nil, uri_rdf_List), true, true, true), true)=true))). % 37.98/25.77 tff(c_2567, plain, (![P_104]: (ifeq(iext(uri_rdfs_subPropertyOf, P_104, uri_rdfs_domain), true, ifeq(iext(P_104, uri_rdfs_seeAlso, uri_rdfs_Resource), true, true, true), true)=true))). % 37.98/25.77 tff(c_2774, plain, (![P_104]: (ifeq(iext(uri_rdfs_subPropertyOf, P_104, uri_rdfs_domain), true, ifeq(iext(P_104, uri_rdfs_member, uri_rdfs_Resource), true, true, true), true)=true))). % 37.98/25.77 tff(c_2834, plain, (![P_104]: (ifeq(iext(uri_rdfs_subPropertyOf, P_104, uri_rdfs_range), true, ifeq(iext(P_104, uri_rdf_rest, uri_rdf_List), true, true, true), true)=true))). % 37.98/25.77 tff(c_2687, plain, (![P_104]: (ifeq(iext(uri_rdfs_subPropertyOf, P_104, uri_rdfs_domain), true, ifeq(iext(P_104, uri_rdfs_comment, uri_rdfs_Resource), true, true, true), true)=true))). % 37.98/25.77 tff(c_2693, plain, (![P_104]: (ifeq(iext(uri_rdfs_subPropertyOf, P_104, uri_rdfs_range), true, ifeq(iext(P_104, uri_rdfs_domain, uri_rdfs_Class), true, true, true), true)=true))). % 37.98/25.77 tff(c_2507, plain, (![P_104]: (ifeq(iext(uri_rdfs_subPropertyOf, P_104, uri_rdfs_range), true, ifeq(iext(P_104, uri_rdfs_seeAlso, uri_rdfs_Resource), true, true, true), true)=true))). % 37.98/25.77 tff(c_2876, plain, (![P_104]: (ifeq(iext(uri_rdfs_subPropertyOf, P_104, uri_rdfs_range), true, ifeq(iext(P_104, uri_rdf_predicate, uri_rdfs_Resource), true, true, true), true)=true))). % 37.98/25.77 tff(c_2840, plain, (![P_104]: (ifeq(iext(uri_rdfs_subPropertyOf, P_104, uri_rdf_type), true, ifeq(iext(P_104, uri_rdf_rest, uri_rdf_Property), true, true, true), true)=true))). % 37.98/25.77 tff(c_2627, plain, (![P_104]: (ifeq(iext(uri_rdfs_subPropertyOf, P_104, uri_rdf_type), true, ifeq(iext(P_104, uri_rdf_XMLLiteral, uri_rdfs_Datatype), true, true, true), true)=true))). % 37.98/25.77 tff(c_39642, plain, (![C_848]: (ifeq(iext(uri_rdfs_subClassOf, C_848, uri_rdf_Alt), true, iext(uri_rdfs_subClassOf, C_848, uri_rdfs_Container), true)=true))). % 37.98/25.77 tff(c_39591, plain, (![C_846]: (ifeq(iext(uri_rdfs_subClassOf, C_846, uri_rdfs_Datatype), true, iext(uri_rdfs_subClassOf, C_846, uri_rdfs_Class), true)=true))). % 37.98/25.77 tff(c_2573, plain, (![P_104]: (ifeq(iext(uri_rdfs_subPropertyOf, P_104, uri_rdf_type), true, ifeq(iext(P_104, uri_rdf__1, uri_rdf_Property), true, true, true), true)=true))). % 37.98/25.77 tff(c_2561, plain, (![P_104]: (ifeq(iext(uri_rdfs_subPropertyOf, P_104, uri_rdf_type), true, ifeq(iext(P_104, uri_rdf_object, uri_rdf_Property), true, true, true), true)=true))). % 37.98/25.77 tff(c_2609, plain, (![P_104]: (ifeq(iext(uri_rdfs_subPropertyOf, P_104, uri_rdfs_domain), true, ifeq(iext(P_104, uri_rdfs_subPropertyOf, uri_rdf_Property), true, true, true), true)=true))). % 37.98/25.77 tff(c_2798, plain, (![P_104]: (ifeq(iext(uri_rdfs_subPropertyOf, P_104, uri_rdf_rest), true, ifeq(iext(P_104, sK2_testcase_premise_fullish_010_Negative_Property_Assertions_BNODE_x4, uri_rdf_nil), true, true, true), true)=true))). % 37.98/25.77 tff(c_2852, plain, (![P_104]: (ifeq(iext(uri_rdfs_subPropertyOf, P_104, uri_rdfs_domain), true, ifeq(iext(P_104, uri_rdf_predicate, uri_rdfs_Statement), true, true, true), true)=true))). % 37.98/25.77 tff(c_2633, plain, (![P_104]: (ifeq(iext(uri_rdfs_subPropertyOf, P_104, uri_rdfs_subClassOf), true, ifeq(iext(P_104, uri_rdfs_Seq, uri_rdfs_Container), true, true, true), true)=true))). % 37.98/25.77 tff(c_2555, plain, (![P_104]: (ifeq(iext(uri_rdfs_subPropertyOf, P_104, uri_rdfs_subClassOf), true, ifeq(iext(P_104, uri_rdf_XMLLiteral, uri_rdfs_Literal), true, true, true), true)=true))). % 37.98/25.77 tff(c_2615, plain, (![P_104]: (ifeq(iext(uri_rdfs_subPropertyOf, P_104, uri_rdfs_range), true, ifeq(iext(P_104, uri_rdf_type, uri_rdfs_Class), true, true, true), true)=true))). % 37.98/25.77 tff(c_2768, plain, (![P_104]: (ifeq(iext(uri_rdfs_subPropertyOf, P_104, uri_rdfs_range), true, ifeq(iext(P_104, uri_rdfs_label, uri_rdfs_Literal), true, true, true), true)=true))). % 37.98/25.77 tff(c_2810, plain, (![P_104]: (ifeq(iext(uri_rdfs_subPropertyOf, P_104, uri_rdf_first), true, ifeq(iext(P_104, sK2_testcase_premise_fullish_010_Negative_Property_Assertions_BNODE_x4, uri_ex_o), true, true, true), true)=true))). % 37.98/25.77 tff(c_2702, plain, (![P_104]: (ifeq(iext(uri_rdfs_subPropertyOf, P_104, uri_rdfs_subPropertyOf), true, ifeq(iext(P_104, uri_rdfs_isDefinedBy, uri_rdfs_seeAlso), true, true, true), true)=true))). % 37.98/25.77 tff(c_2738, plain, (![P_104]: (ifeq(iext(uri_rdfs_subPropertyOf, P_104, uri_rdfs_domain), true, ifeq(iext(P_104, uri_rdf__1, uri_rdfs_Resource), true, true, true), true)=true))). % 37.98/25.77 tff(c_2726, plain, (![P_104]: (ifeq(iext(uri_rdfs_subPropertyOf, P_104, uri_rdfs_range), true, ifeq(iext(P_104, uri_rdf__3, uri_rdfs_Resource), true, true, true), true)=true))). % 37.98/25.77 tff(c_37823, plain, (![C_831]: (ifeq(iext(uri_rdfs_subClassOf, C_831, uri_rdf_XMLLiteral), true, iext(uri_rdfs_subClassOf, C_831, uri_rdfs_Literal), true)=true))). % 37.98/25.77 tff(c_37772, plain, (![P_829]: (ifeq(iext(uri_rdfs_subPropertyOf, P_829, uri_rdfs_isDefinedBy), true, iext(uri_rdfs_subPropertyOf, P_829, uri_rdfs_seeAlso), true)=true))). % 37.98/25.77 tff(c_37721, plain, (![C_827]: (ifeq(iext(uri_rdfs_subClassOf, C_827, uri_rdfs_ContainerMembershipProperty), true, iext(uri_rdfs_subClassOf, C_827, uri_rdf_Property), true)=true))). % 37.98/25.77 tff(c_2543, plain, (![P_104]: (ifeq(iext(uri_rdfs_subPropertyOf, P_104, uri_rdf_type), true, ifeq(iext(P_104, uri_rdf__2, uri_rdf_Property), true, true, true), true)=true))). % 37.98/25.77 tff(c_2732, plain, (![P_104]: (ifeq(iext(uri_rdfs_subPropertyOf, P_104, uri_rdf_type), true, ifeq(iext(P_104, uri_rdf_subject, uri_rdf_Property), true, true, true), true)=true))). % 37.98/25.77 tff(c_2675, plain, (![P_104]: (ifeq(iext(uri_rdfs_subPropertyOf, P_104, uri_rdfs_domain), true, ifeq(iext(P_104, uri_rdf_type, uri_rdfs_Resource), true, true, true), true)=true))). % 37.98/25.77 tff(c_2525, plain, (![P_104]: (ifeq(iext(uri_rdfs_subPropertyOf, P_104, uri_rdf_type), true, ifeq(iext(P_104, uri_rdf_first, uri_rdf_Property), true, true, true), true)=true))). % 37.98/25.77 tff(c_2762, plain, (![P_104]: (ifeq(iext(uri_rdfs_subPropertyOf, P_104, uri_rdfs_domain), true, ifeq(iext(P_104, uri_rdfs_label, uri_rdfs_Resource), true, true, true), true)=true))). % 37.98/25.77 tff(c_2621, plain, (![P_104]: (ifeq(iext(uri_rdfs_subPropertyOf, P_104, uri_owl_oneOf), true, ifeq(iext(P_104, sK1_testcase_premise_fullish_010_Negative_Property_Assertions_BNODE_x3, sK2_testcase_premise_fullish_010_Negative_Property_Assertions_BNODE_x4), true, true, true), true)=true))). % 37.98/25.77 tff(c_2828, plain, (![P_104]: (ifeq(iext(uri_rdfs_subPropertyOf, P_104, uri_rdfs_domain), true, ifeq(iext(P_104, uri_rdfs_subClassOf, uri_rdfs_Class), true, true, true), true)=true))). % 37.98/25.77 tff(c_2714, plain, (![P_104]: (ifeq(iext(uri_rdfs_subPropertyOf, P_104, uri_rdf_type), true, ifeq(iext(P_104, uri_rdf_Property, uri_rdfs_Class), true, true, true), true)=true))). % 37.98/25.77 tff(c_2513, plain, (![P_104]: (ifeq(iext(uri_rdfs_subPropertyOf, P_104, uri_owl_allValuesFrom), true, ifeq(iext(P_104, sK3_testcase_premise_fullish_010_Negative_Property_Assertions_BNODE_x1, sK4_testcase_premise_fullish_010_Negative_Property_Assertions_BNODE_x2), true, true, true), true)=true))). % 37.98/25.77 tff(c_2603, plain, (![P_104]: (ifeq(iext(uri_rdfs_subPropertyOf, P_104, uri_rdfs_range), true, ifeq(iext(P_104, uri_rdfs_range, uri_rdfs_Class), true, true, true), true)=true))). % 37.98/25.77 tff(c_2744, plain, (![P_104]: (ifeq(iext(uri_rdfs_subPropertyOf, P_104, uri_rdfs_range), true, ifeq(iext(P_104, uri_rdf_subject, uri_rdfs_Resource), true, true, true), true)=true))). % 37.98/25.77 tff(c_2864, plain, (![P_104]: (ifeq(iext(uri_rdfs_subPropertyOf, P_104, uri_rdfs_subClassOf), true, ifeq(iext(P_104, uri_rdf_Alt, uri_rdfs_Container), true, true, true), true)=true))). % 37.98/25.77 tff(c_2894, plain, (![P_104]: (ifeq(iext(uri_rdfs_subPropertyOf, P_104, uri_rdfs_range), true, ifeq(iext(P_104, uri_rdfs_subPropertyOf, uri_rdf_Property), true, true, true), true)=true))). % 37.98/25.77 tff(c_2822, plain, (![P_104]: (ifeq(iext(uri_rdfs_subPropertyOf, P_104, uri_rdfs_domain), true, ifeq(iext(P_104, uri_rdf_subject, uri_rdfs_Statement), true, true, true), true)=true))). % 37.98/25.77 tff(c_2645, plain, (![P_104]: (ifeq(iext(uri_rdfs_subPropertyOf, P_104, uri_rdfs_range), true, ifeq(iext(P_104, uri_rdf__1, uri_rdfs_Resource), true, true, true), true)=true))). % 37.98/25.77 tff(c_2537, plain, (![P_104]: (ifeq(iext(uri_rdfs_subPropertyOf, P_104, uri_rdfs_domain), true, ifeq(iext(P_104, uri_rdf_value, uri_rdfs_Resource), true, true, true), true)=true))). % 37.98/25.77 tff(c_2804, plain, (![P_104]: (ifeq(iext(uri_rdfs_subPropertyOf, P_104, uri_rdfs_domain), true, ifeq(iext(P_104, uri_rdfs_domain, uri_rdf_Property), true, true, true), true)=true))). % 37.98/25.77 tff(c_35394, plain, (![D_808]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_808), true, icext(D_808, uri_rdfs_member), true)=true))). % 37.98/25.77 tff(c_35327, plain, (![D_806]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_806), true, icext(D_806, uri_rdfs_Resource), true)=true))). % 37.98/25.77 tff(c_35121, plain, (![D_803]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_803), true, icext(D_803, uri_rdfs_domain), true)=true))). % 37.98/25.77 tff(c_2657, plain, (![P_104]: (ifeq(iext(uri_rdfs_subPropertyOf, P_104, uri_rdfs_range), true, ifeq(iext(P_104, uri_rdfs_isDefinedBy, uri_rdfs_Resource), true, true, true), true)=true))). % 37.98/25.77 tff(c_35053, plain, (![D_801]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_801), true, icext(D_801, uri_rdfs_subPropertyOf), true)=true))). % 37.98/25.77 tff(c_34987, plain, (![D_799]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_799), true, icext(D_799, uri_rdfs_subClassOf), true)=true))). % 37.98/25.77 tff(c_2651, plain, (![P_104]: (ifeq(iext(uri_rdfs_subPropertyOf, P_104, uri_rdf_type), true, ifeq(iext(P_104, uri_rdf__3, uri_rdf_Property), true, true, true), true)=true))). % 37.98/25.77 tff(c_34791, plain, (![D_796]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_796), true, icext(D_796, uri_owl_complementOf), true)=true))). % 37.98/25.77 tff(c_34725, plain, (![D_794]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_794), true, icext(D_794, uri_owl_onProperty), true)=true))). % 37.98/25.77 tff(c_34659, plain, (![D_792]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_792), true, icext(D_792, uri_rdfs_seeAlso), true)=true))). % 37.98/25.77 tff(c_2888, plain, (![P_104]: (ifeq(iext(uri_rdfs_subPropertyOf, P_104, uri_rdfs_domain), true, ifeq(iext(P_104, uri_rdf_object, uri_rdfs_Statement), true, true, true), true)=true))). % 37.98/25.77 tff(c_34463, plain, (![D_789]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_789), true, icext(D_789, uri_owl_oneOf), true)=true))). % 37.98/25.77 tff(c_34397, plain, (![D_787]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_787), true, icext(D_787, uri_owl_allValuesFrom), true)=true))). % 37.98/25.77 tff(c_34329, plain, (![C_785]: (ifeq(iext(uri_rdfs_subClassOf, C_785, uri_rdf_Bag), true, iext(uri_rdfs_subClassOf, C_785, uri_rdfs_Container), true)=true))). % 37.98/25.77 tff(c_34264, plain, (![D_783]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_783), true, icext(D_783, uri_rdfs_range), true)=true))). % 37.98/25.77 tff(c_34198, plain, (![D_781]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_781), true, icext(D_781, uri_rdfs_isDefinedBy), true)=true))). % 37.98/25.77 tff(c_34131, plain, (![D_779]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_779), true, icext(D_779, uri_rdfs_Container), true)=true))). % 37.98/25.77 tff(c_2531, plain, (![P_104]: (ifeq(iext(uri_rdfs_subPropertyOf, P_104, uri_rdfs_range), true, ifeq(iext(P_104, uri_rdfs_subClassOf, uri_rdfs_Class), true, true, true), true)=true))). % 37.98/25.77 tff(c_33931, plain, (![D_776]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_776), true, icext(D_776, uri_rdf_Bag), true)=true))). % 37.98/25.77 tff(c_33837, plain, (![D_774]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_774), true, icext(D_774, uri_rdfs_Class), true)=true))). % 37.98/25.77 tff(c_33771, plain, (![D_772]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_772), true, icext(D_772, uri_rdfs_Datatype), true)=true))). % 37.98/25.77 tff(c_2585, plain, (![P_104]: (ifeq(iext(uri_rdfs_subPropertyOf, P_104, uri_rdf_type), true, ifeq(iext(P_104, uri_rdf__3, uri_rdfs_ContainerMembershipProperty), true, true, true), true)=true))). % 37.98/25.77 tff(c_33572, plain, (![D_769]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_769), true, icext(D_769, uri_rdfs_ContainerMembershipProperty), true)=true))). % 37.98/25.77 tff(c_33495, plain, (![D_767]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_767), true, icext(D_767, uri_rdf_XMLLiteral), true)=true))). % 37.98/25.77 tff(c_33428, plain, (![D_765]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_765), true, icext(D_765, uri_rdfs_Seq), true)=true))). % 37.98/25.77 tff(c_2900, plain, (![P_104]: (ifeq(iext(uri_rdfs_subPropertyOf, P_104, uri_owl_complementOf), true, ifeq(iext(P_104, sK4_testcase_premise_fullish_010_Negative_Property_Assertions_BNODE_x2, sK1_testcase_premise_fullish_010_Negative_Property_Assertions_BNODE_x3), true, true, true), true)=true))). % 37.98/25.77 tff(c_33230, plain, (![D_762]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_762), true, icext(D_762, uri_rdfs_Literal), true)=true))). % 37.98/25.77 tff(c_33164, plain, (![D_760]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_760), true, icext(D_760, uri_rdf_Alt), true)=true))). % 37.98/25.77 tff(c_33097, plain, (![D_758]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_758), true, icext(D_758, sK3_testcase_premise_fullish_010_Negative_Property_Assertions_BNODE_x1), true)=true))). % 37.98/25.77 tff(c_2597, plain, (![P_104]: (ifeq(iext(uri_rdfs_subPropertyOf, P_104, uri_rdfs_domain), true, ifeq(iext(P_104, uri_rdf_first, uri_rdf_List), true, true, true), true)=true))). % 37.98/25.77 tff(c_32901, plain, (![D_755]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_755), true, icext(D_755, uri_owl_ObjectProperty), true)=true))). % 37.98/25.77 tff(c_32835, plain, (![D_753]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_753), true, icext(D_753, uri_rdfs_label), true)=true))). % 37.98/25.77 tff(c_32769, plain, (![D_751]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_751), true, icext(D_751, uri_rdfs_comment), true)=true))). % 37.98/25.77 tff(c_2786, plain, (![P_104]: (ifeq(iext(uri_rdfs_subPropertyOf, P_104, uri_rdfs_range), true, ifeq(iext(P_104, uri_rdf_value, uri_rdfs_Resource), true, true, true), true)=true))). % 37.98/25.77 tff(c_32564, plain, (![D_748]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_List, D_748), true, icext(D_748, sK2_testcase_premise_fullish_010_Negative_Property_Assertions_BNODE_x4), true)=true))). % 37.98/25.77 tff(c_32498, plain, (![D_746]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_746), true, icext(D_746, uri_rdf_predicate), true)=true))). % 37.98/25.77 tff(c_32301, plain, (![D_743]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_743), true, icext(D_743, uri_rdfs_Statement), true)=true))). % 37.98/25.77 tff(c_2669, plain, (![P_104]: (ifeq(iext(uri_rdfs_subPropertyOf, P_104, uri_rdf_type), true, ifeq(iext(P_104, uri_rdf__2, uri_rdfs_ContainerMembershipProperty), true, true, true), true)=true))). % 37.98/25.77 tff(c_15125, 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))). % 37.98/25.77 tff(c_32197, plain, (![D_739]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_739), true, icext(D_739, uri_rdf_List), true)=true))). % 37.98/25.77 tff(c_14985, 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))). % 37.98/25.77 tff(c_15075, 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))). % 37.98/25.77 tff(c_16251, 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))). % 37.98/25.77 tff(c_14917, 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))). % 37.98/25.77 tff(c_14848, 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))). % 37.98/25.77 tff(c_14609, 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))). % 37.98/25.77 tff(c_14293, 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))). % 37.98/25.77 tff(c_2792, plain, (![P_104]: (ifeq(iext(uri_rdfs_subPropertyOf, P_104, uri_rdfs_subClassOf), true, ifeq(iext(P_104, uri_rdfs_ContainerMembershipProperty, uri_rdf_Property), true, true, true), true)=true))). % 37.98/25.77 tff(c_13093, 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))). % 37.98/25.77 tff(c_14359, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_48), true, iext(Q_48, sK3_testcase_premise_fullish_010_Negative_Property_Assertions_BNODE_x1, uri_rdfs_Resource), true)=true))). % 37.98/25.77 tff(c_13606, plain, (![E_41]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Resource, E_41), true, iext(uri_rdfs_subClassOf, uri_owl_ObjectProperty, E_41), true)=true))). % 37.98/25.78 tff(c_13091, 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))). % 37.98/25.78 tff(c_14201, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_48), true, iext(Q_48, uri_owl_ObjectProperty, uri_owl_ObjectProperty), true)=true))). % 37.98/25.78 tff(c_2906, plain, (![P_104]: (ifeq(iext(uri_rdfs_subPropertyOf, P_104, uri_rdf_type), true, ifeq(iext(P_104, uri_ex_s, sK3_testcase_premise_fullish_010_Negative_Property_Assertions_BNODE_x1), true, true, true), true)=true))). % 37.98/25.78 tff(c_13608, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_48), true, iext(Q_48, uri_owl_ObjectProperty, uri_rdfs_Resource), true)=true))). % 37.98/25.78 tff(c_14135, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_48), true, iext(Q_48, sK3_testcase_premise_fullish_010_Negative_Property_Assertions_BNODE_x1, sK3_testcase_premise_fullish_010_Negative_Property_Assertions_BNODE_x1), true)=true))). % 37.98/25.78 tff(c_14357, plain, (![E_41]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Resource, E_41), true, iext(uri_rdfs_subClassOf, sK3_testcase_premise_fullish_010_Negative_Property_Assertions_BNODE_x1, E_41), true)=true))). % 37.98/25.78 tff(c_31421, plain, (![D_713]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_713), true, icext(D_713, uri_rdf_object), true)=true))). % 37.98/25.78 tff(c_13764, 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))). % 37.98/25.78 tff(c_14291, 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))). % 37.98/25.78 tff(c_2639, plain, (![P_104]: (ifeq(iext(uri_rdfs_subPropertyOf, P_104, uri_rdf_type), true, ifeq(iext(P_104, uri_rdf__1, uri_rdfs_ContainerMembershipProperty), true, true, true), true)=true))). % 37.98/25.78 tff(c_13542, 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))). % 37.98/25.78 tff(c_12957, 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))). % 37.98/25.78 tff(c_12862, 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))). % 37.98/25.78 tff(c_12669, 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))). % 37.98/25.78 tff(c_12790, 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))). % 37.98/25.78 tff(c_13005, 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))). % 37.98/25.78 tff(c_31108, plain, (![X_699, Y_700]: (ifeq(iext(uri_rdfs_isDefinedBy, X_699, Y_700), true, iext(uri_rdfs_seeAlso, X_699, Y_700), true)=true))). % 37.98/25.78 tff(c_12621, 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))). % 37.98/25.78 tff(c_12743, 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))). % 37.98/25.78 tff(c_12543, 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))). % 37.98/25.78 tff(c_12909, 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))). % 37.98/25.78 tff(c_12280, 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))). % 37.98/25.78 tff(c_12445, 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))). % 37.98/25.78 tff(c_14071, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, sK3_testcase_premise_fullish_010_Negative_Property_Assertions_BNODE_x1, uri_rdfs_Class), true)=true))). % 37.98/25.78 tff(c_12398, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, uri_owl_ObjectProperty, uri_rdfs_Class), true)=true))). % 37.98/25.78 tff(c_2780, plain, (![P_104]: (ifeq(iext(uri_rdfs_subPropertyOf, P_104, uri_rdfs_domain), true, ifeq(iext(P_104, uri_rdf__3, uri_rdfs_Resource), true, true, true), true)=true))). % 37.98/25.78 tff(c_12493, 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))). % 37.98/25.78 tff(c_13380, 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))). % 37.98/25.78 tff(c_15293, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, sK2_testcase_premise_fullish_010_Negative_Property_Assertions_BNODE_x4, uri_rdf_List), true)=true))). % 37.98/25.78 tff(c_16147, 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))). % 37.98/25.78 tff(c_5839, 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))). % 37.98/25.78 tff(c_8863, 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))). % 37.98/25.78 tff(c_11648, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_48), true, iext(Q_48, uri_owl_allValuesFrom, uri_owl_allValuesFrom), true)=true))). % 37.98/25.78 tff(c_2750, plain, (![P_104]: (ifeq(iext(uri_rdfs_subPropertyOf, P_104, uri_rdfs_domain), true, ifeq(iext(P_104, uri_rdfs_isDefinedBy, uri_rdfs_Resource), true, true, true), true)=true))). % 37.98/25.78 tff(c_8621, 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))). % 37.98/25.78 tff(c_12002, 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))). % 37.98/25.78 tff(c_8447, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, uri_owl_oneOf, uri_rdf_Property), true)=true))). % 37.98/25.78 tff(c_10473, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, uri_owl_allValuesFrom, uri_rdf_Property), true)=true))). % 37.98/25.78 tff(c_4984, 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))). % 37.98/25.78 tff(c_2591, plain, (![P_104]: (ifeq(iext(uri_rdfs_subPropertyOf, P_104, uri_rdfs_domain), true, ifeq(iext(P_104, uri_rdf_rest, uri_rdf_List), true, true, true), true)=true))). % 37.98/25.78 tff(c_10810, 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))). % 37.98/25.78 tff(c_8098, 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))). % 37.98/25.78 tff(c_5624, 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))). % 37.98/25.78 tff(c_30081, plain, (![D_667]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, D_667), true, icext(D_667, uri_rdf__3), true)=true))). % 37.98/25.78 tff(c_10682, 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))). % 37.98/25.78 tff(c_29994, plain, (![C_664]: (ifeq(iext(uri_rdfs_subClassOf, C_664, uri_rdfs_Seq), true, iext(uri_rdfs_subClassOf, C_664, uri_rdfs_Container), true)=true))). % 37.98/25.78 tff(c_9451, 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))). % 37.98/25.78 tff(c_10812, 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))). % 37.98/25.78 tff(c_6848, 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))). % 37.98/25.78 tff(c_8281, 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))). % 37.98/25.78 tff(c_8033, 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))). % 37.98/25.78 tff(c_2720, plain, (![P_104]: (ifeq(iext(uri_rdfs_subPropertyOf, P_104, uri_rdfs_range), true, ifeq(iext(P_104, uri_rdf__2, uri_rdfs_Resource), true, true, true), true)=true))). % 37.98/25.78 tff(c_11771, 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))). % 37.98/25.78 tff(c_29514, plain, (![D_650]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, D_650), true, icext(D_650, uri_rdf_XMLLiteral), true)=true))). % 37.98/25.78 tff(c_5542, 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))). % 37.98/25.78 tff(c_11488, 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))). % 37.98/25.78 tff(c_11486, 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))). % 37.98/25.78 tff(c_2870, plain, (![P_104]: (ifeq(iext(uri_rdfs_subPropertyOf, P_104, uri_rdfs_subClassOf), true, ifeq(iext(P_104, uri_rdfs_Datatype, uri_rdfs_Class), true, true, true), true)=true))). % 37.98/25.78 tff(c_10680, 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))). % 37.98/25.78 tff(c_9009, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, uri_owl_complementOf, uri_rdf_Property), true)=true))). % 37.98/25.78 tff(c_6414, 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))). % 37.98/25.78 tff(c_29199, plain, (![D_641]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_641), true, icext(D_641, uri_rdf_subject), true)=true))). % 37.98/25.78 tff(c_11239, 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))). % 37.98/25.78 tff(c_2816, plain, (![P_104]: (ifeq(iext(uri_rdfs_subPropertyOf, P_104, uri_rdfs_range), true, ifeq(iext(P_104, uri_rdfs_member, uri_rdfs_Resource), true, true, true), true)=true))). % 37.98/25.78 tff(c_7470, 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))). % 37.98/25.78 tff(c_7595, 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))). % 37.98/25.78 tff(c_11083, 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))). % 37.98/25.78 tff(c_28884, plain, (![D_632]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_632), true, icext(D_632, uri_rdf_first), true)=true))). % 37.98/25.78 tff(c_4983, 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))). % 37.98/25.78 tff(c_5742, 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))). % 37.98/25.78 tff(c_5390, 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))). % 37.98/25.78 tff(c_2846, plain, (![P_104]: (ifeq(iext(uri_rdfs_subPropertyOf, P_104, uri_rdfs_range), true, ifeq(iext(P_104, uri_rdfs_comment, uri_rdfs_Literal), true, true, true), true)=true))). % 37.98/25.78 tff(c_7660, 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))). % 37.98/25.78 tff(c_10416, 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))). % 37.98/25.78 tff(c_28574, plain, (![D_623]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_623), true, icext(D_623, uri_rdf__2), true)=true))). % 37.98/25.78 tff(c_9264, 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))). % 37.98/25.78 tff(c_2579, plain, (![P_104]: (ifeq(iext(uri_rdfs_subPropertyOf, P_104, uri_owl_onProperty), true, ifeq(iext(P_104, sK3_testcase_premise_fullish_010_Negative_Property_Assertions_BNODE_x1, uri_ex_p), true, true, true), true)=true))). % 37.98/25.78 tff(c_11332, 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))). % 37.98/25.78 tff(c_28227, plain, (![D_614]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_614), true, icext(D_614, uri_rdf_rest), true)=true))). % 37.98/25.78 tff(c_8620, 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))). % 37.98/25.78 tff(c_11330, 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))). % 37.98/25.78 tff(c_8773, 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))). % 37.98/25.78 tff(c_28018, plain, (![D_606]: (ifeq(iext(uri_rdfs_subClassOf, uri_owl_ObjectProperty, D_606), true, icext(D_606, uri_ex_p), true)=true))). % 37.98/25.78 tff(c_7405, 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))). % 37.98/25.78 tff(c_8953, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_48), true, iext(Q_48, uri_owl_complementOf, uri_owl_complementOf), true)=true))). % 37.98/25.78 tff(c_2681, plain, (![P_104]: (ifeq(iext(uri_rdfs_subPropertyOf, P_104, uri_rdfs_range), true, ifeq(iext(P_104, uri_rdf_first, uri_rdfs_Resource), true, true, true), true)=true))). % 37.98/25.78 tff(c_10056, 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))). % 37.98/25.78 tff(c_6669, 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))). % 37.98/25.78 tff(c_9834, 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))). % 37.98/25.78 tff(c_27707, plain, (![D_597]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_597), true, icext(D_597, uri_rdf_type), true)=true))). % 37.98/25.78 tff(c_11174, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_48), true, iext(Q_48, uri_owl_onProperty, uri_owl_onProperty), true)=true))). % 37.98/25.78 tff(c_9900, 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))). % 37.98/25.78 tff(c_2882, plain, (![P_104]: (ifeq(iext(uri_rdfs_subPropertyOf, P_104, uri_rdfs_subClassOf), true, ifeq(iext(P_104, uri_rdf_Bag, uri_rdfs_Container), true, true, true), true)=true))). % 37.98/25.78 tff(c_7180, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, uri_owl_onProperty, uri_rdf_Property), true)=true))). % 37.98/25.78 tff(c_10415, 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))). % 37.98/25.78 tff(c_9330, 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))). % 37.98/25.78 tff(c_5989, 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))). % 37.98/25.78 tff(c_9395, 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))). % 37.98/25.78 tff(c_12146, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_48), true, iext(Q_48, uri_owl_oneOf, uri_owl_oneOf), true)=true))). % 37.98/25.78 tff(c_6793, 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))). % 37.98/25.78 tff(c_5173, 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))). % 37.98/25.78 tff(c_8100, 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))). % 37.98/25.78 tff(c_5903, 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))). % 37.98/25.78 tff(c_9607, 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))). % 37.98/25.78 tff(c_12213, 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))). % 37.98/25.78 tff(c_2756, plain, (![P_104]: (ifeq(iext(uri_rdfs_subPropertyOf, P_104, uri_rdf_type), true, ifeq(iext(P_104, uri_rdf_value, uri_rdf_Property), true, true, true), true)=true))). % 37.98/25.78 tff(c_8774, 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))). % 37.98/25.78 tff(c_12000, 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))). % 37.98/25.78 tff(c_6415, 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))). % 37.98/25.78 tff(c_26957, plain, (![D_571]: (ifeq(iext(uri_rdfs_subClassOf, sK3_testcase_premise_fullish_010_Negative_Property_Assertions_BNODE_x1, D_571), true, icext(D_571, uri_ex_s), true)=true))). % 37.98/25.78 tff(c_9898, 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))). % 37.98/25.78 tff(c_11715, 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))). % 37.98/25.78 tff(c_2663, plain, (![P_104]: (ifeq(iext(uri_rdfs_subPropertyOf, P_104, uri_rdfs_domain), true, ifeq(iext(P_104, uri_rdfs_range, uri_rdf_Property), true, true, true), true)=true))). % 37.98/25.78 tff(c_8685, 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))). % 37.98/25.78 tff(c_7469, 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))). % 37.98/25.79 tff(c_9767, 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))). % 37.98/25.79 tff(c_4879, plain, (![Q_48, X_141]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, X_141, uri_rdfs_Resource), true)=true))). % 37.98/25.79 tff(c_3079, plain, (![E_109]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Container, E_109), true, iext(uri_rdfs_subClassOf, uri_rdf_Bag, E_109), true)=true))). % 37.98/25.79 tff(c_2965, plain, (![Q_105]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_105), true, iext(Q_105, uri_rdf_rest, uri_rdf_List), true)=true))). % 37.98/25.79 tff(c_2951, plain, (![Q_105]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_105), true, iext(Q_105, uri_rdfs_isDefinedBy, uri_rdfs_Resource), true)=true))). % 37.98/25.79 tff(c_2976, plain, (![Q_105]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_owl_complementOf, Q_105), true, iext(Q_105, sK4_testcase_premise_fullish_010_Negative_Property_Assertions_BNODE_x2, sK1_testcase_premise_fullish_010_Negative_Property_Assertions_BNODE_x3), true)=true))). % 37.98/25.79 tff(c_2967, plain, (![Q_105]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_105), true, iext(Q_105, uri_rdfs_comment, uri_rdfs_Literal), true)=true))). % 38.12/25.79 tff(c_26300, plain, (![D_552]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_552), true, icext(D_552, uri_rdf_value), true)=true))). % 38.12/25.79 tff(c_2949, plain, (![Q_105]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_105), true, iext(Q_105, uri_rdf__1, uri_rdfs_Resource), true)=true))). % 38.12/25.79 tff(c_2966, plain, (![Q_105]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_105), true, iext(Q_105, uri_rdf_rest, uri_rdf_Property), true)=true))). % 38.12/25.79 tff(c_2942, plain, (![Q_105]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_105), true, iext(Q_105, uri_rdfs_domain, uri_rdfs_Class), true)=true))). % 38.12/25.79 tff(c_2933, plain, (![Q_105]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_105), true, iext(Q_105, uri_rdf__1, uri_rdfs_ContainerMembershipProperty), true)=true))). % 38.12/25.79 tff(c_2946, plain, (![Q_105]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_105), true, iext(Q_105, uri_rdf__2, uri_rdfs_Resource), true)=true))). % 38.12/25.79 tff(c_2971, plain, (![Q_105]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_105), true, iext(Q_105, uri_rdfs_Datatype, uri_rdfs_Class), true)=true))). % 38.12/25.79 tff(c_2921, plain, (![Q_105]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_105), true, iext(Q_105, uri_rdfs_seeAlso, uri_rdfs_Resource), true)=true))). % 38.12/25.79 tff(c_26098, plain, (![D_543]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_List, D_543), true, icext(D_543, uri_rdf_nil), true)=true))). % 38.12/25.79 tff(c_2937, plain, (![Q_105]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_105), true, iext(Q_105, uri_rdfs_range, uri_rdf_Property), true)=true))). % 38.12/25.79 tff(c_2977, plain, (![Q_105]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_105), true, iext(Q_105, uri_ex_s, sK3_testcase_premise_fullish_010_Negative_Property_Assertions_BNODE_x1), true)=true))). % 38.12/25.79 tff(c_2939, plain, (![Q_105]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_105), true, iext(Q_105, uri_rdf_type, uri_rdfs_Resource), true)=true))). % 38.12/25.79 tff(c_3075, plain, (![E_109]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Container, E_109), true, iext(uri_rdfs_subClassOf, uri_rdfs_Seq, E_109), true)=true))). % 38.12/25.79 tff(c_2918, plain, (![Q_105]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_105), true, iext(Q_105, uri_rdf_nil, uri_rdf_List), true)=true))). % 38.12/25.79 tff(c_2932, plain, (![Q_105]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_105), true, iext(Q_105, uri_rdfs_Seq, uri_rdfs_Container), true)=true))). % 38.12/25.79 tff(c_2462, plain, (![R_102]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_seeAlso, R_102), true, iext(uri_rdfs_subPropertyOf, uri_rdfs_isDefinedBy, R_102), true)=true))). % 38.12/25.79 tff(c_2922, plain, (![Q_105]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_105), true, iext(Q_105, uri_rdf__1, uri_rdf_Property), true)=true))). % 38.12/25.79 tff(c_2938, plain, (![Q_105]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_105), true, iext(Q_105, uri_rdf__2, uri_rdfs_ContainerMembershipProperty), true)=true))). % 38.12/25.79 tff(c_2961, plain, (![Q_105]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_first, Q_105), true, iext(Q_105, sK2_testcase_premise_fullish_010_Negative_Property_Assertions_BNODE_x4, uri_ex_o), true)=true))). % 38.12/25.79 tff(c_2973, plain, (![Q_105]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_105), true, iext(Q_105, uri_rdf_Bag, uri_rdfs_Container), true)=true))). % 38.12/25.79 tff(c_2954, plain, (![Q_105]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_105), true, iext(Q_105, uri_rdfs_label, uri_rdfs_Literal), true)=true))). % 38.12/25.79 tff(c_2924, plain, (![Q_105]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_105), true, iext(Q_105, uri_rdf__3, uri_rdfs_ContainerMembershipProperty), true)=true))). % 38.12/25.79 tff(c_2934, plain, (![Q_105]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_105), true, iext(Q_105, uri_rdf__1, uri_rdfs_Resource), true)=true))). % 38.12/25.79 tff(c_2926, plain, (![Q_105]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_105), true, iext(Q_105, uri_rdf_first, uri_rdf_List), true)=true))). % 38.12/25.79 tff(c_2919, plain, (![Q_105]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_105), true, iext(Q_105, uri_rdf_XMLLiteral, uri_rdfs_Literal), true)=true))). % 38.12/25.79 tff(c_2944, plain, (![Q_105]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_105), true, iext(Q_105, uri_rdf__2, uri_rdfs_Resource), true)=true))). % 38.12/25.79 tff(c_2920, plain, (![Q_105]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_105), true, iext(Q_105, uri_rdf_object, uri_rdf_Property), true)=true))). % 38.12/25.79 tff(c_3077, plain, (![E_109]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Container, E_109), true, iext(uri_rdfs_subClassOf, uri_rdf_Alt, E_109), true)=true))). % 38.12/25.79 tff(c_2935, plain, (![Q_105]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_105), true, iext(Q_105, uri_rdf__3, uri_rdf_Property), true)=true))). % 38.12/25.79 tff(c_2916, plain, (![Q_105]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_105), true, iext(Q_105, uri_rdf_value, uri_rdfs_Resource), true)=true))). % 38.12/25.79 tff(c_2974, plain, (![Q_105]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_105), true, iext(Q_105, uri_rdf_object, uri_rdfs_Statement), true)=true))). % 38.12/25.79 tff(c_2968, plain, (![Q_105]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_105), true, iext(Q_105, uri_rdf_predicate, uri_rdfs_Statement), true)=true))). % 38.12/25.79 tff(c_2925, plain, (![Q_105]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_105), true, iext(Q_105, uri_rdf_rest, uri_rdf_List), true)=true))). % 38.12/25.79 tff(c_2927, plain, (![Q_105]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_105), true, iext(Q_105, uri_rdfs_range, uri_rdfs_Class), true)=true))). % 38.12/25.79 tff(c_25577, plain, (![D_516]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_516), true, icext(D_516, uri_rdf_Property), true)=true))). % 38.12/25.79 tff(c_2952, plain, (![Q_105]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_105), true, iext(Q_105, uri_rdf_value, uri_rdf_Property), true)=true))). % 38.12/25.79 tff(c_2948, plain, (![Q_105]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_105), true, iext(Q_105, uri_rdf_subject, uri_rdf_Property), true)=true))). % 38.12/25.79 tff(c_2970, plain, (![Q_105]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_105), true, iext(Q_105, uri_rdf_Alt, uri_rdfs_Container), true)=true))). % 38.12/25.79 tff(c_2958, plain, (![Q_105]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_105), true, iext(Q_105, uri_rdfs_ContainerMembershipProperty, uri_rdf_Property), true)=true))). % 38.12/25.79 tff(c_2936, plain, (![Q_105]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_105), true, iext(Q_105, uri_rdfs_isDefinedBy, uri_rdfs_Resource), true)=true))). % 38.12/25.79 tff(c_2943, plain, (![Q_105]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_105), true, iext(Q_105, uri_rdfs_isDefinedBy, uri_rdfs_seeAlso), true)=true))). % 38.12/25.79 tff(c_2912, plain, (![Q_105]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_owl_allValuesFrom, Q_105), true, iext(Q_105, sK3_testcase_premise_fullish_010_Negative_Property_Assertions_BNODE_x1, sK4_testcase_premise_fullish_010_Negative_Property_Assertions_BNODE_x2), true)=true))). % 38.12/25.79 tff(c_25381, plain, (![D_507]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, D_507), true, icext(D_507, uri_rdf__1), true)=true))). % 38.12/25.79 tff(c_2930, plain, (![Q_105]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_owl_oneOf, Q_105), true, iext(Q_105, sK1_testcase_premise_fullish_010_Negative_Property_Assertions_BNODE_x3, sK2_testcase_premise_fullish_010_Negative_Property_Assertions_BNODE_x4), true)=true))). % 38.12/25.79 tff(c_3078, plain, (![E_109]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, E_109), true, iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, E_109), true)=true))). % 38.12/25.79 tff(c_2975, plain, (![Q_105]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_105), true, iext(Q_105, uri_rdfs_subPropertyOf, uri_rdf_Property), true)=true))). % 38.12/25.79 tff(c_2953, plain, (![Q_105]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_105), true, iext(Q_105, uri_rdfs_label, uri_rdfs_Resource), true)=true))). % 38.12/25.79 tff(c_2972, plain, (![Q_105]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_105), true, iext(Q_105, uri_rdf_predicate, uri_rdfs_Resource), true)=true))). % 38.12/25.79 tff(c_2940, plain, (![Q_105]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_105), true, iext(Q_105, uri_rdf_first, uri_rdfs_Resource), true)=true))). % 38.12/25.79 tff(c_2947, plain, (![Q_105]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_105), true, iext(Q_105, uri_rdf__3, uri_rdfs_Resource), true)=true))). % 38.12/25.79 tff(c_14989, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_label), true)=true))). % 38.12/25.79 tff(c_16255, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_comment), true)=true))). % 38.12/25.79 tff(c_16254, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_comment), true)=true))). % 38.12/25.79 tff(c_14988, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_label), true)=true))). % 38.12/25.79 tff(c_2915, plain, (![Q_105]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_105), true, iext(Q_105, uri_rdfs_subClassOf, uri_rdfs_Class), true)=true))). % 38.12/25.79 tff(c_15078, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_predicate), true)=true))). % 38.12/25.79 tff(c_15079, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_predicate), true)=true))). % 38.12/25.79 tff(c_24986, plain, (![D_491]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_491), true, icext(D_491, uri_rdf__3), true)=true))). % 38.12/25.79 tff(c_14849, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdfs_Resource), true)=true))). % 38.12/25.79 tff(c_14920, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_member), true)=true))). % 38.12/25.79 tff(c_2928, plain, (![Q_105]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_105), true, iext(Q_105, uri_rdfs_subPropertyOf, uri_rdf_Property), true)=true))). % 38.12/25.79 tff(c_13544, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdfs_Statement), true)=true))). % 38.12/25.79 tff(c_14360, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, sK3_testcase_premise_fullish_010_Negative_Property_Assertions_BNODE_x1), true)=true))). % 38.12/25.79 tff(c_2964, plain, (![Q_105]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_105), true, iext(Q_105, uri_rdfs_subClassOf, uri_rdfs_Class), true)=true))). % 38.12/25.79 tff(c_14137, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, sK3_testcase_premise_fullish_010_Negative_Property_Assertions_BNODE_x1), true)=true))). % 38.12/25.79 tff(c_13766, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdf_List), true)=true))). % 38.12/25.79 tff(c_14202, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_owl_ObjectProperty), true)=true))). % 38.12/25.79 tff(c_13094, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdf_List), true)=true))). % 38.12/25.79 tff(c_14203, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_owl_ObjectProperty), true)=true))). % 38.12/25.79 tff(c_14294, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdfs_Statement), true)=true))). % 38.12/25.79 tff(c_2955, plain, (![Q_105]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_105), true, iext(Q_105, uri_rdfs_member, uri_rdfs_Resource), true)=true))). % 38.12/25.79 tff(c_3074, plain, (![E_109]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Literal, E_109), true, iext(uri_rdfs_subClassOf, uri_rdf_XMLLiteral, E_109), true)=true))). % 38.12/25.79 tff(c_24546, plain, (![D_475]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_475), true, icext(D_475, uri_rdf__1), true)=true))). % 38.12/25.79 tff(c_2963, plain, (![Q_105]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_105), true, iext(Q_105, uri_rdf_subject, uri_rdfs_Statement), true)=true))). % 38.12/25.79 tff(c_9770, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_rest), true)=true))). % 38.12/25.79 tff(c_5744, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdfs_Datatype), true)=true))). % 38.12/25.79 tff(c_9398, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_first), true)=true))). % 38.12/25.79 tff(c_2969, plain, (![Q_105]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_105), true, iext(Q_105, uri_rdf_type, uri_rdf_Property), true)=true))). % 38.12/25.79 tff(c_24337, plain, (![D_468]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, D_468), true, icext(D_468, uri_rdf__2), true)=true))). % 38.12/25.79 tff(c_5991, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_type), true)=true))). % 38.12/25.79 tff(c_5906, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_value), true)=true))). % 38.12/25.79 tff(c_2957, plain, (![Q_105]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_105), true, iext(Q_105, uri_rdf_value, uri_rdfs_Resource), true)=true))). % 38.12/25.79 tff(c_7663, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_domain), true)=true))). % 38.12/25.79 tff(c_9399, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_first), true)=true))). % 38.12/25.79 tff(c_23766, plain, (![D_459, X_460]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Resource, D_459), true, icext(D_459, X_460), true)=true))). % 38.12/25.79 tff(c_2923, plain, (![Q_105]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_owl_onProperty, Q_105), true, iext(Q_105, sK3_testcase_premise_fullish_010_Negative_Property_Assertions_BNODE_x1, uri_ex_p), true)=true))). % 38.12/25.79 tff(c_8867, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_isDefinedBy), true)=true))). % 38.12/25.79 tff(c_9265, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdf_Property), true)=true))). % 38.12/25.79 tff(c_23511, plain, (![C_90, X_63]: (ifeq(icext(C_90, X_63), true, true, true)=true))). % 38.12/25.79 tff(c_8037, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_subject), true)=true))). % 38.12/25.79 tff(c_2941, plain, (![Q_105]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_105), true, iext(Q_105, uri_rdfs_comment, uri_rdfs_Resource), true)=true))). % 38.12/25.79 tff(c_7664, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_domain), true)=true))). % 38.12/25.79 tff(c_23070, plain, (![X_447, Y_448]: (ifeq(iext(uri_rdfs_range, X_447, Y_448), true, icext(uri_rdf_Property, X_447), true)=true))). % 38.12/25.79 tff(c_8036, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_subject), true)=true))). % 38.12/25.79 tff(c_8956, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_owl_complementOf), true)=true))). % 38.12/25.79 tff(c_2931, plain, (![Q_105]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_105), true, iext(Q_105, uri_rdf_XMLLiteral, uri_rdfs_Datatype), true)=true))). % 38.12/25.79 tff(c_22969, plain, (![X_440, Y_441]: (ifeq(iext(uri_rdfs_label, X_440, Y_441), true, icext(uri_rdfs_Literal, Y_441), true)=true))). % 38.12/25.79 tff(c_9836, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdfs_ContainerMembershipProperty), true)=true))). % 38.12/25.79 tff(c_2962, plain, (![Q_105]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_105), true, iext(Q_105, uri_rdfs_member, uri_rdfs_Resource), true)=true))). % 38.12/25.79 tff(c_9332, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdf_Alt), true)=true))). % 38.12/25.79 tff(c_22310, plain, (![X_432, Y_433]: (ifeq(iext(uri_rdfs_subClassOf, X_432, Y_433), true, icext(uri_rdfs_Class, Y_433), true)=true))). % 38.12/25.79 tff(c_5907, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_value), true)=true))). % 38.12/25.79 tff(c_11652, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_owl_allValuesFrom), true)=true))). % 38.12/25.79 tff(c_2959, plain, (![Q_105]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_rest, Q_105), true, iext(Q_105, sK2_testcase_premise_fullish_010_Negative_Property_Assertions_BNODE_x4, uri_rdf_nil), true)=true))). % 38.12/25.79 tff(c_5841, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_subPropertyOf), true)=true))). % 38.12/25.79 tff(c_21761, plain, (![X_424, Y_425]: (ifeq(iext(uri_rdfs_subPropertyOf, X_424, Y_425), true, icext(uri_rdf_Property, X_424), true)=true))). % 38.12/25.79 tff(c_8776, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf__3), true)=true))). % 38.12/25.79 tff(c_2945, plain, (![Q_105]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_105), true, iext(Q_105, uri_rdf_Property, uri_rdfs_Class), true)=true))). % 38.12/25.79 tff(c_21172, plain, (![X_418, Y_419]: (ifeq(iext(uri_rdf_type, X_418, Y_419), true, icext(uri_rdfs_Class, Y_419), true)=true))). % 38.12/25.79 tff(c_2913, plain, (![Q_105]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_105), true, iext(Q_105, uri_ex_p, uri_owl_ObjectProperty), true)=true))). % 38.12/25.79 tff(c_8689, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf__1), true)=true))). % 38.12/25.80 tff(c_8622, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdfs_Container), true)=true))). % 38.12/25.80 tff(c_20695, plain, (![X_411, Y_412]: (ifeq(iext(uri_rdfs_domain, X_411, Y_412), true, icext(uri_rdf_Property, X_411), true)=true))). % 38.12/25.80 tff(c_10418, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf__2), true)=true))). % 38.12/25.80 tff(c_7472, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf__1), true)=true))). % 38.12/25.80 tff(c_2917, plain, (![Q_105]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_105), true, iext(Q_105, uri_rdf__2, uri_rdf_Property), true)=true))). % 38.12/25.80 tff(c_5393, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_object), true)=true))). % 38.12/25.80 tff(c_12216, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_range), true)=true))). % 38.12/25.80 tff(c_20538, plain, (![X_402, Y_403]: (ifeq(iext(uri_rdf_predicate, X_402, Y_403), true, icext(uri_rdfs_Statement, X_402), true)=true))). % 38.12/25.80 tff(c_5392, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_object), true)=true))). % 38.12/25.80 tff(c_9771, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_rest), true)=true))). % 38.12/25.80 tff(c_2956, plain, (![Q_105]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_105), true, iext(Q_105, uri_rdf__3, uri_rdfs_Resource), true)=true))). % 38.12/25.80 tff(c_20116, plain, (![X_395, Y_396]: (ifeq(iext(uri_rdfs_range, X_395, Y_396), true, icext(uri_rdfs_Class, Y_396), true)=true))). % 38.12/25.80 tff(c_5842, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_subPropertyOf), true)=true))). % 38.12/25.80 tff(c_2929, plain, (![Q_105]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_105), true, iext(Q_105, uri_rdf_type, uri_rdfs_Class), true)=true))). % 38.12/25.80 tff(c_8101, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdfs_Class), true)=true))). % 38.12/25.80 tff(c_11178, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_owl_onProperty), true)=true))). % 38.12/25.80 tff(c_11177, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_owl_onProperty), true)=true))). % 38.12/25.80 tff(c_19955, plain, (![X_386, Y_387]: (ifeq(iext(uri_rdf_subject, X_386, Y_387), true, icext(uri_rdfs_Statement, X_386), true)=true))). % 38.12/25.80 tff(c_5992, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_type), true)=true))). % 38.12/25.80 tff(c_8957, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_owl_complementOf), true)=true))). % 38.12/25.80 tff(c_11243, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_subClassOf), true)=true))). % 38.12/25.80 tff(c_2911, plain, (![Q_105]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_105), true, iext(Q_105, uri_rdfs_seeAlso, uri_rdfs_Resource), true)=true))). % 38.12/25.80 tff(c_19180, plain, (![X_377, Y_378]: (ifeq(iext(uri_rdfs_subClassOf, X_377, Y_378), true, icext(uri_rdfs_Class, X_377), true)=true))). % 38.12/25.80 tff(c_7473, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_member), true)=true))). % 38.12/25.80 tff(c_3076, plain, (![E_109]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, E_109), true, iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, E_109), true)=true))). % 38.12/25.80 tff(c_5543, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdfs_Literal), true)=true))). % 38.12/25.80 tff(c_5626, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdf_Bag), true)=true))). % 38.12/25.80 tff(c_18643, plain, (![X_369, Y_370]: (ifeq(iext(uri_rdfs_subPropertyOf, X_369, Y_370), true, icext(uri_rdf_Property, Y_370), true)=true))). % 38.12/25.80 tff(c_11717, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdfs_Seq), true)=true))). % 38.12/25.80 tff(c_7597, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdf_XMLLiteral), true)=true))). % 38.12/25.80 tff(c_11242, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_subClassOf), true)=true))). % 38.12/25.80 tff(c_2960, plain, (![Q_105]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_105), true, iext(Q_105, uri_rdfs_domain, uri_rdf_Property), true)=true))). % 38.12/25.80 tff(c_12150, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_owl_oneOf), true)=true))). % 38.12/25.80 tff(c_12217, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_range), true)=true))). % 38.12/25.80 tff(c_18428, plain, (![X_359, Y_360]: (ifeq(iext(uri_rdf_first, X_359, Y_360), true, icext(uri_rdf_List, X_359), true)=true))). % 38.12/25.80 tff(c_6796, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf__3), true)=true))). % 38.12/25.80 tff(c_11651, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_owl_allValuesFrom), true)=true))). % 38.12/25.80 tff(c_2914, plain, (![Q_105]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_105), true, iext(Q_105, uri_rdf_first, uri_rdf_Property), true)=true))). % 38.12/25.80 tff(c_12149, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_owl_oneOf), true)=true))). % 38.12/25.80 tff(c_11334, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdfs_Resource), true)=true))). % 38.12/25.80 tff(c_18239, plain, (![X_350, Y_351]: (ifeq(iext(uri_rdf_rest, X_350, Y_351), true, icext(uri_rdf_List, Y_351), true)=true))). % 38.12/25.80 tff(c_11087, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf__2), true)=true))). % 38.12/25.80 tff(c_5176, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_seeAlso), true)=true))). % 38.12/25.80 tff(c_4880, plain, (![C_19, X_141]: (ifeq(iext(uri_rdfs_domain, uri_rdf_type, C_19), true, icext(C_19, X_141), true)=true))). % 38.12/25.80 tff(c_2950, plain, (![Q_105]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_105), true, iext(Q_105, uri_rdf_subject, uri_rdfs_Resource), true)=true))). % 38.12/25.80 tff(c_4881, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_29), true, icext(C_29, uri_rdfs_Resource), true)=true))). % 38.12/25.80 tff(c_17551, plain, (![X_338, Y_339]: (ifeq(iext(uri_rdfs_domain, X_338, Y_339), true, icext(uri_rdfs_Class, Y_339), true)=true))). % 38.12/25.80 tff(c_2348, plain, (![C_98]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_98), true, icext(C_98, uri_rdf_rest), true)=true))). % 38.12/25.80 tff(c_2350, plain, (![C_98]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_98), true, icext(C_98, uri_rdfs_range), true)=true))). % 38.12/25.80 tff(c_2379, plain, (![C_98]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_98), true, icext(C_98, uri_rdfs_isDefinedBy), true)=true))). % 38.12/25.80 tff(c_2044, plain, (![C_94]: (ifeq(iext(uri_rdfs_range, uri_rdfs_range, C_94), true, icext(C_94, uri_rdf_Property), true)=true))). % 38.12/25.80 tff(c_2385, plain, (![C_98]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_98), true, icext(C_98, uri_rdfs_member), true)=true))). % 38.12/25.80 tff(c_2402, plain, (![C_98]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_98), true, icext(C_98, uri_rdfs_Datatype), true)=true))). % 38.12/25.80 tff(c_2352, plain, (![C_98]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_98), true, icext(C_98, uri_rdf_type), true)=true))). % 38.12/25.80 tff(c_2025, plain, (![C_94]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_94), true, icext(C_94, uri_rdf_Property), true)=true))). % 38.12/25.80 tff(c_2336, plain, (![C_98]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_98), true, icext(C_98, uri_rdfs_subClassOf), true)=true))). % 38.12/25.80 tff(c_2360, plain, (![C_98]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_98), true, icext(C_98, uri_rdfs_range), true)=true))). % 38.12/25.80 tff(c_2406, plain, (![C_98]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_98), true, icext(C_98, uri_rdfs_subPropertyOf), true)=true))). % 38.12/25.80 tff(c_2383, plain, (![C_98]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_98), true, icext(C_98, uri_rdfs_label), true)=true))). % 38.12/25.80 tff(c_2355, plain, (![C_98]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_98), true, icext(C_98, uri_rdfs_Seq), true)=true))). % 38.12/25.80 tff(c_17061, plain, (![X_316, Y_317]: (ifeq(iext(uri_rdf_object, X_316, Y_317), true, icext(uri_rdfs_Statement, X_316), true)=true))). % 38.12/25.80 tff(c_2368, plain, (![C_98]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_98), true, icext(C_98, uri_rdfs_isDefinedBy), true)=true))). % 38.12/25.80 tff(c_2344, plain, (![C_98]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_98), true, icext(C_98, uri_rdfs_seeAlso), true)=true))). % 38.12/25.80 tff(c_2332, plain, (![C_98]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_98), true, icext(C_98, uri_rdfs_seeAlso), true)=true))). % 38.12/25.80 tff(c_2032, plain, (![C_94]: (ifeq(iext(uri_rdfs_range, uri_rdfs_domain, C_94), true, icext(C_94, uri_rdfs_Class), true)=true))). % 38.12/25.80 tff(c_2039, plain, (![C_94]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_94), true, icext(C_94, uri_rdfs_Class), true)=true))). % 38.12/25.80 tff(c_2377, plain, (![C_98]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_98), true, icext(C_98, uri_rdf_subject), true)=true))). % 38.12/25.80 tff(c_2389, plain, (![C_98]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_98), true, icext(C_98, uri_rdfs_ContainerMembershipProperty), true)=true))). % 38.12/25.80 tff(c_2341, plain, (![C_98]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_98), true, icext(C_98, uri_rdf_XMLLiteral), true)=true))). % 38.12/25.80 tff(c_2026, plain, (![C_94]: (ifeq(iext(uri_rdfs_range, uri_rdf_rest, C_94), true, icext(C_94, uri_rdf_nil), true)=true))). % 38.12/25.80 tff(c_2373, plain, (![C_98]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_98), true, icext(C_98, uri_rdf__3), true)=true))). % 38.12/25.80 tff(c_2006, plain, (![C_94]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_94), true, icext(C_94, uri_rdfs_seeAlso), true)=true))). % 38.12/25.80 tff(c_2045, plain, (![C_94]: (ifeq(iext(uri_rdfs_range, uri_owl_complementOf, C_94), true, icext(C_94, sK1_testcase_premise_fullish_010_Negative_Property_Assertions_BNODE_x3), true)=true))). % 38.12/25.80 tff(c_2395, plain, (![C_98]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_98), true, icext(C_98, uri_rdfs_subClassOf), true)=true))). % 38.12/25.80 tff(c_2405, plain, (![C_98]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_98), true, icext(C_98, uri_rdf_object), true)=true))). % 38.12/25.80 tff(c_2357, plain, (![C_98]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_98), true, icext(C_98, uri_rdf__1), true)=true))). % 38.12/25.80 tff(c_16628, plain, (![X_297, Y_298]: (ifeq(iext(uri_rdf_rest, X_297, Y_298), true, icext(uri_rdf_List, X_297), true)=true))). % 38.12/25.80 tff(c_1979, plain, (![C_94]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_94), true, icext(C_94, uri_rdfs_Literal), true)=true))). % 38.12/25.80 tff(c_2353, plain, (![C_98]: (ifeq(iext(uri_rdfs_domain, uri_owl_oneOf, C_98), true, icext(C_98, sK1_testcase_premise_fullish_010_Negative_Property_Assertions_BNODE_x3), true)=true))). % 38.12/25.80 tff(c_2366, plain, (![C_98]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_98), true, icext(C_98, uri_rdfs_comment), true)=true))). % 38.12/25.80 tff(c_2346, plain, (![C_98]: (ifeq(iext(uri_rdfs_domain, uri_owl_onProperty, C_98), true, icext(C_98, sK3_testcase_premise_fullish_010_Negative_Property_Assertions_BNODE_x1), true)=true))). % 38.12/25.80 tff(c_2394, plain, (![C_98]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_98), true, icext(C_98, uri_rdf_subject), true)=true))). % 38.12/25.80 tff(c_2359, plain, (![C_98]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_98), true, icext(C_98, uri_rdfs_isDefinedBy), true)=true))). % 38.12/25.80 tff(c_2363, plain, (![C_98]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_98), true, icext(C_98, uri_rdf_type), true)=true))). % 38.12/25.80 tff(c_2399, plain, (![C_98]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_98), true, icext(C_98, uri_rdf_predicate), true)=true))). % 38.12/25.80 tff(c_2033, plain, (![C_94]: (ifeq(iext(uri_rdfs_range, uri_rdfs_range, C_94), true, icext(C_94, uri_rdf_List), true)=true))). % 38.12/25.80 tff(c_2407, plain, (![C_98]: (ifeq(iext(uri_rdfs_domain, uri_owl_complementOf, C_98), true, icext(C_98, sK4_testcase_premise_fullish_010_Negative_Property_Assertions_BNODE_x2), true)=true))). % 38.12/25.80 tff(c_15621, plain, (![X_271, Y_272]: (ifeq(iext(uri_rdfs_comment, X_271, Y_272), true, icext(uri_rdfs_Literal, Y_272), true)=true))). % 38.12/25.80 tff(c_2391, plain, (![C_98]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_98), true, icext(C_98, uri_rdfs_domain), true)=true))). % 38.12/25.80 tff(c_2338, plain, (![C_98]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_98), true, icext(C_98, uri_rdf_value), true)=true))). % 38.12/25.80 tff(c_2387, plain, (![C_98]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_98), true, icext(C_98, uri_rdf__3), true)=true))). % 38.12/25.80 tff(c_16200, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_comment, uri_rdfs_comment)=true)). % 38.12/25.80 tff(c_16159, plain, (ip(uri_rdfs_comment)=true)). % 38.12/25.80 tff(c_16105, plain, (iext(uri_rdf_type, uri_rdfs_comment, uri_rdf_Property)=true)). % 38.12/25.80 tff(c_15923, plain, (icext(uri_rdf_Property, uri_rdfs_comment)=true)). % 38.12/25.80 tff(c_2398, plain, (![C_98]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_98), true, icext(C_98, uri_rdfs_comment), true)=true))). % 38.12/25.80 tff(c_2392, plain, (![C_98]: (ifeq(iext(uri_rdfs_domain, uri_rdf_first, C_98), true, icext(C_98, sK2_testcase_premise_fullish_010_Negative_Property_Assertions_BNODE_x4), true)=true))). % 38.12/25.80 tff(c_14204, plain, (![X_33]: (ifeq(icext(uri_owl_ObjectProperty, X_33), true, icext(uri_owl_ObjectProperty, X_33), true)=true))). % 38.12/25.80 tff(c_14138, plain, (![X_33]: (ifeq(icext(sK3_testcase_premise_fullish_010_Negative_Property_Assertions_BNODE_x1, X_33), true, icext(sK3_testcase_premise_fullish_010_Negative_Property_Assertions_BNODE_x1, X_33), true)=true))). % 38.12/25.80 tff(c_13767, plain, (![X_33]: (ifeq(icext(uri_rdf_List, X_33), true, icext(uri_rdf_List, X_33), true)=true))). % 38.12/25.80 tff(c_13545, plain, (![X_33]: (ifeq(icext(uri_rdfs_Statement, X_33), true, icext(uri_rdfs_Statement, X_33), true)=true))). % 38.12/25.80 tff(c_9610, plain, (![X_33]: (ifeq(icext(uri_rdfs_Container, X_33), true, icext(uri_rdfs_Container, X_33), true)=true))). % 38.12/25.80 tff(c_9267, plain, (![X_33]: (ifeq(icext(uri_rdf_Property, X_33), true, icext(uri_rdf_Property, X_33), true)=true))). % 38.12/25.80 tff(c_7408, plain, (![X_33]: (ifeq(icext(uri_rdfs_Class, X_33), true, icext(uri_rdfs_Class, X_33), true)=true))). % 38.12/25.80 tff(c_9333, plain, (![X_33]: (ifeq(icext(uri_rdf_Alt, X_33), true, icext(uri_rdf_Alt, X_33), true)=true))). % 38.12/25.80 tff(c_11718, plain, (![X_33]: (ifeq(icext(uri_rdfs_Seq, X_33), true, icext(uri_rdfs_Seq, X_33), true)=true))). % 38.12/25.80 tff(c_2370, plain, (![C_98]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_98), true, icext(C_98, uri_rdf__2), true)=true))). % 38.12/25.80 tff(c_5627, plain, (![X_33]: (ifeq(icext(uri_rdf_Bag, X_33), true, icext(uri_rdf_Bag, X_33), true)=true))). % 38.12/25.80 tff(c_5545, plain, (![X_33]: (ifeq(icext(uri_rdfs_Literal, X_33), true, icext(uri_rdfs_Literal, X_33), true)=true))). % 38.12/25.80 tff(c_15257, plain, (iext(uri_rdf_type, sK2_testcase_premise_fullish_010_Negative_Property_Assertions_BNODE_x4, uri_rdf_List)=true)). % 38.12/25.80 tff(c_15209, plain, (icext(uri_rdf_List, sK2_testcase_premise_fullish_010_Negative_Property_Assertions_BNODE_x4)=true)). % 38.12/25.80 tff(c_2390, plain, (![C_98]: (ifeq(iext(uri_rdfs_domain, uri_rdf_rest, C_98), true, icext(C_98, sK2_testcase_premise_fullish_010_Negative_Property_Assertions_BNODE_x4), true)=true))). % 38.12/25.80 tff(c_9837, plain, (![X_33]: (ifeq(icext(uri_rdfs_ContainerMembershipProperty, X_33), true, icext(uri_rdfs_ContainerMembershipProperty, X_33), true)=true))). % 38.12/25.80 tff(c_7598, plain, (![X_33]: (ifeq(icext(uri_rdf_XMLLiteral, X_33), true, icext(uri_rdf_XMLLiteral, X_33), true)=true))). % 38.12/25.80 tff(c_5745, plain, (![X_33]: (ifeq(icext(uri_rdfs_Datatype, X_33), true, icext(uri_rdfs_Datatype, X_33), true)=true))). % 38.12/25.80 tff(c_15089, plain, (iext(uri_rdf_type, uri_rdfs_Resource, uri_rdfs_Class)=true)). % 38.12/25.80 tff(c_15024, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_predicate, uri_rdf_predicate)=true)). % 38.12/25.80 tff(c_2393, plain, (![C_98]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_98), true, icext(C_98, uri_rdfs_member), true)=true))). % 38.12/25.80 tff(c_14934, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_label, uri_rdfs_label)=true)). % 38.12/25.80 tff(c_14863, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_member, uri_rdfs_member)=true)). % 38.12/25.80 tff(c_14792, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Resource, uri_rdfs_Resource)=true)). % 38.12/25.80 tff(c_14621, plain, (icext(uri_rdf_Property, uri_rdfs_member)=true)). % 38.12/25.80 tff(c_14567, plain, (iext(uri_rdf_type, uri_rdfs_member, uri_rdf_Property)=true)). % 38.12/25.80 tff(c_14306, plain, (iext(uri_rdfs_subClassOf, sK3_testcase_premise_fullish_010_Negative_Property_Assertions_BNODE_x1, uri_rdfs_Resource)=true)). % 38.12/25.80 tff(c_14240, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Statement, uri_rdfs_Resource)=true)). % 38.12/25.80 tff(c_2401, plain, (![C_98]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_98), true, icext(C_98, uri_rdf_Alt), true)=true))). % 38.12/25.80 tff(c_14148, plain, (iext(uri_rdfs_subClassOf, uri_owl_ObjectProperty, uri_owl_ObjectProperty)=true)). % 38.12/25.80 tff(c_14082, plain, (iext(uri_rdfs_subClassOf, sK3_testcase_premise_fullish_010_Negative_Property_Assertions_BNODE_x1, sK3_testcase_premise_fullish_010_Negative_Property_Assertions_BNODE_x1)=true)). % 38.12/25.80 tff(c_14010, plain, (iext(uri_rdf_type, sK3_testcase_premise_fullish_010_Negative_Property_Assertions_BNODE_x1, uri_rdfs_Class)=true)). % 38.12/25.80 tff(c_2388, plain, (![C_98]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_98), true, icext(C_98, uri_rdf_value), true)=true))). % 38.12/25.80 tff(c_13859, plain, (ic(sK3_testcase_premise_fullish_010_Negative_Property_Assertions_BNODE_x1)=true)). % 38.12/25.80 tff(c_13797, plain, (icext(uri_rdfs_Class, sK3_testcase_premise_fullish_010_Negative_Property_Assertions_BNODE_x1)=true)). % 38.12/25.80 tff(c_2046, plain, (![C_94]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_94), true, icext(C_94, sK3_testcase_premise_fullish_010_Negative_Property_Assertions_BNODE_x1), true)=true))). % 38.12/25.80 tff(c_13711, plain, (iext(uri_rdfs_subClassOf, uri_rdf_List, uri_rdf_List)=true)). % 38.12/25.80 tff(c_13555, plain, (iext(uri_rdfs_subClassOf, uri_owl_ObjectProperty, uri_rdfs_Resource)=true)). % 38.12/25.80 tff(c_13464, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Statement, uri_rdfs_Statement)=true)). % 38.12/25.80 tff(c_1991, plain, (![C_94]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_94), true, icext(C_94, uri_rdfs_Datatype), true)=true))). % 38.12/25.80 tff(c_13420, plain, (ip(uri_rdfs_label)=true)). % 38.12/25.80 tff(c_13338, plain, (iext(uri_rdf_type, uri_rdfs_label, uri_rdf_Property)=true)). % 38.12/25.80 tff(c_13106, plain, (icext(uri_rdf_Property, uri_rdfs_label)=true)). % 38.12/25.80 tff(c_13020, plain, (iext(uri_rdfs_subClassOf, uri_rdf_List, uri_rdfs_Resource)=true)). % 38.12/25.80 tff(c_2382, plain, (![C_98]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_98), true, icext(C_98, uri_rdfs_label), true)=true))). % 38.12/25.80 tff(c_12969, plain, (iext(uri_rdf_type, uri_rdfs_Literal, uri_rdfs_Class)=true)). % 38.12/25.80 tff(c_12921, plain, (iext(uri_rdf_type, uri_rdf_Alt, uri_rdfs_Class)=true)). % 38.12/25.80 tff(c_12873, plain, (iext(uri_rdf_type, uri_rdf_Bag, uri_rdfs_Class)=true)). % 38.12/25.80 tff(c_12826, plain, (iext(uri_rdf_type, uri_rdfs_Container, uri_rdfs_Class)=true)). % 38.12/25.80 tff(c_2404, plain, (![C_98]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_98), true, icext(C_98, uri_rdf_Bag), true)=true))). % 38.12/25.80 tff(c_12754, plain, (iext(uri_rdf_type, uri_rdfs_ContainerMembershipProperty, uri_rdfs_Class)=true)). % 38.12/25.80 tff(c_12707, plain, (iext(uri_rdf_type, uri_rdfs_Class, uri_rdfs_Class)=true)). % 38.12/25.80 tff(c_2351, plain, (![C_98]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_98), true, icext(C_98, uri_rdfs_subPropertyOf), true)=true))). % 38.12/25.80 tff(c_12633, plain, (iext(uri_rdf_type, uri_rdfs_Seq, uri_rdfs_Class)=true)). % 38.12/25.80 tff(c_12585, plain, (iext(uri_rdf_type, uri_rdf_XMLLiteral, uri_rdfs_Class)=true)). % 38.12/25.80 tff(c_12507, plain, (iext(uri_rdf_type, uri_rdfs_Datatype, uri_rdfs_Class)=true)). % 38.12/25.80 tff(c_12457, plain, (iext(uri_rdf_type, uri_rdf_List, uri_rdfs_Class)=true)). % 38.12/25.80 tff(c_12409, plain, (iext(uri_rdf_type, uri_rdfs_Statement, uri_rdfs_Class)=true)). % 38.12/25.80 tff(c_12362, plain, (iext(uri_rdf_type, uri_owl_ObjectProperty, uri_rdfs_Class)=true)). % 38.12/25.80 tff(c_12320, plain, (ip(uri_rdf_predicate)=true)). % 38.12/25.80 tff(c_1985, plain, (![C_94]: (ifeq(iext(uri_rdfs_range, uri_rdfs_domain, C_94), true, icext(C_94, uri_rdf_List), true)=true))). % 38.12/25.80 tff(c_12238, plain, (iext(uri_rdf_type, uri_rdf_predicate, uri_rdf_Property)=true)). % 38.12/25.80 tff(c_3405, plain, (![S_5, O_6]: (ifeq(iext(uri_owl_onProperty, S_5, O_6), true, true, true)=true))). % 38.12/25.80 tff(c_12162, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_range, uri_rdfs_range)=true)). % 38.12/25.80 tff(c_12095, plain, (iext(uri_rdfs_subPropertyOf, uri_owl_oneOf, uri_owl_oneOf)=true)). % 38.12/25.80 tff(c_11949, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Bag, uri_rdfs_Resource)=true)). % 38.12/25.81 tff(c_11812, plain, (icext(uri_rdf_Property, uri_rdfs_isDefinedBy)=true)). % 38.12/25.81 tff(c_2376, plain, (![C_98]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_98), true, icext(C_98, uri_rdf__1), true)=true))). % 38.12/25.81 tff(c_11729, plain, (iext(uri_rdf_type, uri_rdfs_isDefinedBy, uri_rdf_Property)=true)). % 38.12/25.81 tff(c_11662, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Seq, uri_rdfs_Seq)=true)). % 38.12/25.81 tff(c_11597, plain, (iext(uri_rdfs_subPropertyOf, uri_owl_allValuesFrom, uri_owl_allValuesFrom)=true)). % 38.12/25.81 tff(c_1999, plain, (![C_94]: (ifeq(iext(uri_rdfs_range, uri_rdfs_domain, C_94), true, icext(C_94, uri_rdf_Property), true)=true))). % 38.12/25.81 tff(c_11435, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Seq, uri_rdfs_Resource)=true)). % 38.12/25.81 tff(c_11279, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, uri_rdfs_Resource)=true)). % 38.12/25.81 tff(c_1984, plain, (![C_94]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_94), true, icext(C_94, uri_rdfs_ContainerMembershipProperty), true)=true))). % 38.12/25.81 tff(c_11188, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, uri_rdfs_subClassOf)=true)). % 38.12/25.81 tff(c_11123, plain, (iext(uri_rdfs_subPropertyOf, uri_owl_onProperty, uri_owl_onProperty)=true)). % 38.12/25.81 tff(c_2364, plain, (![C_98]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_98), true, icext(C_98, uri_rdf_first), true)=true))). % 38.12/25.81 tff(c_11032, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf__2, uri_rdf__2)=true)). % 38.12/25.81 tff(c_10908, plain, (icext(uri_rdf_Property, uri_rdf_predicate)=true)). % 38.12/25.81 tff(c_2403, plain, (![C_98]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_98), true, icext(C_98, uri_rdf_predicate), true)=true))). % 38.12/25.81 tff(c_10759, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Alt, uri_rdfs_Resource)=true)). % 38.12/25.81 tff(c_10629, plain, (iext(uri_rdfs_subClassOf, uri_rdf_XMLLiteral, uri_rdfs_Resource)=true)). % 38.12/25.81 tff(c_2333, plain, (![C_98]: (ifeq(iext(uri_rdfs_domain, uri_owl_allValuesFrom, C_98), true, icext(C_98, sK3_testcase_premise_fullish_010_Negative_Property_Assertions_BNODE_x1), true)=true))). % 38.12/25.81 tff(c_10510, plain, (icext(uri_rdf_Property, uri_owl_allValuesFrom)=true)). % 38.12/25.81 tff(c_1992, plain, (![C_94]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_94), true, icext(C_94, uri_rdfs_Container), true)=true))). % 38.12/25.81 tff(c_10431, plain, (iext(uri_rdf_type, uri_owl_allValuesFrom, uri_rdf_Property)=true)). % 38.12/25.81 tff(c_10364, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf__2, uri_rdfs_member)=true)). % 38.12/25.81 tff(c_2349, plain, (![C_98]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_98), true, icext(C_98, uri_rdf_first), true)=true))). % 38.12/25.81 tff(c_10186, plain, (ic(uri_rdf_List)=true)). % 38.12/25.81 tff(c_10132, plain, (icext(uri_rdfs_Class, uri_rdf_List)=true)). % 38.12/25.81 tff(c_1978, plain, (![C_94]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_94), true, icext(C_94, uri_rdf_List), true)=true))). % 38.12/25.81 tff(c_10068, plain, (icext(uri_rdf_Property, uri_rdfs_range)=true)). % 38.12/25.81 tff(c_10014, plain, (iext(uri_rdf_type, uri_rdfs_range, uri_rdf_Property)=true)). % 38.12/25.81 tff(c_3288, plain, (![S_5, O_6]: (ifeq(iext(uri_owl_oneOf, S_5, O_6), true, true, true)=true))). % 38.12/25.81 tff(c_2008, plain, (![C_94]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_94), true, icext(C_94, uri_rdfs_Class), true)=true))). % 38.12/25.81 tff(c_9847, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, uri_rdfs_Resource)=true)). % 38.12/25.81 tff(c_9781, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, uri_rdfs_ContainerMembershipProperty)=true)). % 38.12/25.81 tff(c_9716, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_rest, uri_rdf_rest)=true)). % 38.12/25.81 tff(c_1983, plain, (![C_94]: (ifeq(iext(uri_rdfs_range, uri_owl_onProperty, C_94), true, icext(C_94, uri_ex_p), true)=true))). % 38.12/25.81 tff(c_919, plain, (![S_5, O_6]: (ifeq(iext(uri_rdfs_subClassOf, S_5, O_6), true, true, true)=true))). % 38.12/25.81 tff(c_9555, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Container, uri_rdfs_Container)=true)). % 38.12/25.81 tff(c_9463, plain, (icext(uri_rdf_Property, uri_rdfs_subPropertyOf)=true)). % 38.12/25.81 tff(c_9409, plain, (iext(uri_rdf_type, uri_rdfs_subPropertyOf, uri_rdf_Property)=true)). % 38.12/25.81 tff(c_9344, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_first, uri_rdf_first)=true)). % 38.12/25.81 tff(c_9278, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Alt, uri_rdf_Alt)=true)). % 38.12/25.81 tff(c_9208, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Property, uri_rdf_Property)=true)). % 38.12/25.81 tff(c_9021, plain, (icext(uri_rdf_Property, uri_owl_complementOf)=true)). % 38.12/25.81 tff(c_8967, plain, (iext(uri_rdf_type, uri_owl_complementOf, uri_rdf_Property)=true)). % 38.12/25.81 tff(c_8881, plain, (iext(uri_rdfs_subPropertyOf, uri_owl_complementOf, uri_owl_complementOf)=true)). % 38.12/25.81 tff(c_2028, plain, (![C_94]: (ifeq(iext(uri_rdfs_range, uri_rdf_first, C_94), true, icext(C_94, uri_ex_o), true)=true))). % 38.12/25.81 tff(c_8812, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_isDefinedBy, uri_rdfs_isDefinedBy)=true)). % 38.12/25.81 tff(c_1982, plain, (![C_94]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_94), true, icext(C_94, uri_rdf_Property), true)=true))). % 38.12/25.81 tff(c_8722, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf__3, uri_rdfs_member)=true)). % 38.12/25.81 tff(c_8634, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf__1, uri_rdf__1)=true)). % 38.12/25.81 tff(c_8572, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Container, uri_rdfs_Resource)=true)). % 38.12/25.81 tff(c_2020, plain, (![C_94]: (ifeq(iext(uri_rdfs_range, uri_rdfs_range, C_94), true, icext(C_94, uri_rdfs_Literal), true)=true))). % 38.12/25.81 tff(c_8459, plain, (icext(uri_rdf_Property, uri_owl_oneOf)=true)). % 38.12/25.81 tff(c_8405, plain, (iext(uri_rdf_type, uri_owl_oneOf, uri_rdf_Property)=true)). % 38.12/25.81 tff(c_8293, plain, (icext(uri_rdf_Property, uri_rdfs_subClassOf)=true)). % 38.12/25.81 tff(c_8239, plain, (iext(uri_rdf_type, uri_rdfs_subClassOf, uri_rdf_Property)=true)). % 38.12/25.81 tff(c_1514, plain, (![S_5, O_6]: (ifeq(iext(uri_owl_complementOf, S_5, O_6), true, true, true)=true))). % 38.12/25.81 tff(c_8047, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Class, uri_rdfs_Resource)=true)). % 38.12/25.81 tff(c_7965, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_subject, uri_rdf_subject)=true)). % 38.12/25.81 tff(c_1990, plain, (![C_94]: (ifeq(iext(uri_rdfs_range, uri_owl_oneOf, C_94), true, icext(C_94, sK2_testcase_premise_fullish_010_Negative_Property_Assertions_BNODE_x4), true)=true))). % 38.12/25.81 tff(c_7922, plain, (ic(uri_rdfs_Statement)=true)). % 38.12/25.81 tff(c_7869, plain, (icext(uri_rdfs_Class, uri_rdfs_Statement)=true)). % 38.12/25.81 tff(c_2036, plain, (![C_94]: (ifeq(iext(uri_rdfs_range, uri_rdfs_domain, C_94), true, icext(C_94, uri_rdfs_Statement), true)=true))). % 38.12/25.81 tff(c_1694, plain, (![S_5, O_6]: (ifeq(iext(uri_owl_allValuesFrom, S_5, O_6), true, true, true)=true))). % 38.12/25.81 tff(c_7796, plain, (ic(uri_owl_ObjectProperty)=true)). % 38.12/25.81 tff(c_7743, plain, (icext(uri_rdfs_Class, uri_owl_ObjectProperty)=true)). % 38.12/25.81 tff(c_1973, plain, (![C_94]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_94), true, icext(C_94, uri_owl_ObjectProperty), true)=true))). % 38.12/25.81 tff(c_3171, plain, (![S_5, O_6]: (ifeq(iext(uri_rdf_rest, S_5, O_6), true, true, true)=true))). % 38.12/25.81 tff(c_7609, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, uri_rdfs_domain)=true)). % 38.12/25.81 tff(c_7546, plain, (iext(uri_rdfs_subClassOf, uri_rdf_XMLLiteral, uri_rdf_XMLLiteral)=true)). % 38.12/25.81 tff(c_2010, plain, (![C_94]: (ifeq(iext(uri_rdfs_range, uri_rdfs_range, C_94), true, icext(C_94, uri_rdfs_Resource), true)=true))). % 38.12/25.81 tff(c_7482, plain, (ip(uri_rdfs_member)=true)). % 38.12/25.81 tff(c_7418, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf__1, uri_rdfs_member)=true)). % 38.12/25.81 tff(c_7352, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Class, uri_rdfs_Class)=true)). % 38.12/25.81 tff(c_2367, plain, (![C_98]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_98), true, icext(C_98, uri_rdfs_domain), true)=true))). % 38.12/25.81 tff(c_7192, plain, (icext(uri_rdf_Property, uri_owl_onProperty)=true)). % 38.12/25.81 tff(c_7113, plain, (iext(uri_rdf_type, uri_owl_onProperty, uri_rdf_Property)=true)). % 38.12/25.81 tff(c_2396, plain, (![C_98]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_98), true, icext(C_98, uri_rdf_rest), true)=true))). % 38.12/25.81 tff(c_1335, plain, (![S_5, O_6]: (ifeq(iext(uri_rdfs_subPropertyOf, S_5, O_6), true, true, true)=true))). % 38.12/25.81 tff(c_2372, plain, (![C_98]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_98), true, icext(C_98, uri_rdf__2), true)=true))). % 38.12/25.81 tff(c_6860, plain, (icext(uri_rdf_Property, uri_rdfs_seeAlso)=true)). % 38.12/25.81 tff(c_6806, plain, (iext(uri_rdf_type, uri_rdfs_seeAlso, uri_rdf_Property)=true)). % 38.12/25.81 tff(c_6745, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf__3, uri_rdf__3)=true)). % 38.12/25.81 tff(c_1972, plain, (![C_94]: (ifeq(iext(uri_rdfs_range, uri_owl_allValuesFrom, C_94), true, icext(C_94, sK4_testcase_premise_fullish_010_Negative_Property_Assertions_BNODE_x2), true)=true))). % 38.12/25.81 tff(c_6681, plain, (icext(uri_rdf_Property, uri_rdfs_domain)=true)). % 38.12/25.81 tff(c_6627, plain, (iext(uri_rdf_type, uri_rdfs_domain, uri_rdf_Property)=true)). % 38.12/25.81 tff(c_647, plain, (![S_71, O_72]: (ifeq(iext(uri_rdf_object, S_71, O_72), true, true, true)=true))). % 38.12/25.81 tff(c_2004, plain, (![C_94]: (ifeq(iext(uri_rdfs_range, uri_rdfs_domain, C_94), true, icext(C_94, uri_rdfs_Resource), true)=true))). % 38.12/25.81 tff(c_1076, plain, (![S_5, O_6]: (ifeq(iext(uri_rdfs_range, S_5, O_6), true, true, true)=true))). % 38.12/25.81 tff(c_6366, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Literal, uri_rdfs_Resource)=true)). % 38.12/25.81 tff(c_1252, plain, (![S_5, O_6]: (ifeq(iext(uri_rdfs_domain, S_5, O_6), true, true, true)=true))). % 38.12/25.81 tff(c_5917, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_type, uri_rdf_type)=true)). % 38.12/25.81 tff(c_1987, plain, (![C_94]: (ifeq(iext(uri_rdfs_range, uri_rdfs_range, C_94), true, icext(C_94, uri_rdfs_Class), true)=true))). % 38.12/25.81 tff(c_5852, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_value, uri_rdf_value)=true)). % 38.12/25.81 tff(c_5788, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf)=true)). % 38.12/25.81 tff(c_5690, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, uri_rdfs_Datatype)=true)). % 38.12/25.81 tff(c_5575, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Bag, uri_rdf_Bag)=true)). % 38.12/25.81 tff(c_1663, plain, (![X_91]: (ifeq(icext(uri_rdf_Alt, X_91), true, icext(uri_rdfs_Container, X_91), true)=true))). % 38.12/25.81 tff(c_5487, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Literal, uri_rdfs_Literal)=true)). % 38.12/25.81 tff(c_1662, plain, (![X_91]: (ifeq(icext(uri_rdfs_ContainerMembershipProperty, X_91), true, icext(uri_rdf_Property, X_91), true)=true))). % 38.12/25.81 tff(c_5342, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_object, uri_rdf_object)=true)). % 38.12/25.81 tff(c_1660, plain, (![X_91]: (ifeq(icext(uri_rdf_XMLLiteral, X_91), true, icext(uri_rdfs_Literal, X_91), true)=true))). % 38.12/25.81 tff(c_1664, plain, (![X_91]: (ifeq(icext(uri_rdfs_Datatype, X_91), true, icext(uri_rdfs_Class, X_91), true)=true))). % 38.12/25.81 tff(c_5122, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_seeAlso, uri_rdfs_seeAlso)=true)). % 38.12/25.81 tff(c_5076, plain, (icext(uri_rdfs_Class, uri_rdfs_Resource)=true)). % 38.12/25.81 tff(c_1665, plain, (![X_91]: (ifeq(icext(uri_rdf_Bag, X_91), true, icext(uri_rdfs_Container, X_91), true)=true))). % 38.12/25.81 tff(c_4996, plain, (ic(uri_rdfs_Resource)=true)). % 38.12/25.81 tff(c_4935, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Property, uri_rdfs_Resource)=true)). % 38.12/25.81 tff(c_1661, plain, (![X_91]: (ifeq(icext(uri_rdfs_Seq, X_91), true, icext(uri_rdfs_Container, X_91), true)=true))). % 38.12/25.81 tff(c_4839, plain, (![X_140]: (iext(uri_rdf_type, X_140, uri_rdfs_Resource)=true))). % 38.12/25.81 tff(c_1994, plain, (![X_95, Y_96]: (ifeq(iext(uri_rdf__1, X_95, Y_96), true, true, true)=true))). % 38.12/25.81 tff(c_2337, plain, (![X_99, Y_100]: (ifeq(iext(uri_rdf_value, X_99, Y_100), true, true, true)=true))). % 38.12/25.81 tff(c_2029, plain, (![X_95, Y_96]: (ifeq(iext(uri_rdfs_member, X_95, Y_96), true, true, true)=true))). % 38.12/25.81 tff(c_2365, plain, (![X_99, Y_100]: (ifeq(iext(uri_rdfs_comment, X_99, Y_100), true, true, true)=true))). % 38.12/25.81 tff(c_2362, plain, (![X_99, Y_100]: (ifeq(iext(uri_rdf_type, X_99, Y_100), true, true, true)=true))). % 38.12/25.81 tff(c_2369, plain, (![X_99, Y_100]: (ifeq(iext(uri_rdf__2, X_99, Y_100), true, true, true)=true))). % 38.12/25.81 tff(c_2343, plain, (![X_99, Y_100]: (ifeq(iext(uri_rdfs_seeAlso, X_99, Y_100), true, true, true)=true))). % 38.12/25.81 tff(c_2040, plain, (![X_95, Y_96]: (ifeq(iext(uri_rdf_predicate, X_95, Y_96), true, true, true)=true))). % 38.12/25.81 tff(c_2381, plain, (![X_99, Y_100]: (ifeq(iext(uri_rdfs_label, X_99, Y_100), true, true, true)=true))). % 38.12/25.81 tff(c_4640, plain, (icext(uri_rdfs_Class, uri_rdf_Alt)=true)). % 38.12/25.81 tff(c_2011, plain, (![X_95, Y_96]: (ifeq(iext(uri_rdf__3, X_95, Y_96), true, true, true)=true))). % 38.12/25.81 tff(c_4596, plain, (icext(uri_rdfs_Class, uri_rdf_XMLLiteral)=true)). % 38.12/25.81 tff(c_4551, plain, (icext(uri_rdfs_Class, uri_rdfs_Class)=true)). % 38.12/25.81 tff(c_2002, plain, (![X_95, Y_96]: (ifeq(iext(uri_rdf_first, X_95, Y_96), true, true, true)=true))). % 38.12/25.81 tff(c_4496, plain, (icext(uri_rdfs_Class, uri_rdfs_Seq)=true)). % 38.12/25.81 tff(c_4447, plain, (icext(uri_rdfs_Class, uri_rdfs_Container)=true)). % 38.12/25.81 tff(c_4396, plain, (icext(uri_rdfs_Class, uri_rdfs_ContainerMembershipProperty)=true)). % 38.12/25.81 tff(c_2378, plain, (![X_99, Y_100]: (ifeq(iext(uri_rdfs_isDefinedBy, X_99, Y_100), true, true, true)=true))). % 38.12/25.81 tff(c_4348, plain, (icext(uri_rdfs_Class, uri_rdf_Bag)=true)). % 38.12/25.81 tff(c_4294, plain, (icext(uri_rdfs_Class, uri_rdfs_Datatype)=true)). % 38.12/25.81 tff(c_2015, plain, (![X_95, Y_96]: (ifeq(iext(uri_rdf_subject, X_95, Y_96), true, true, true)=true))). % 38.12/25.81 tff(c_4251, plain, (icext(uri_rdfs_Class, uri_rdfs_Literal)=true)). % 38.12/25.81 tff(c_4209, plain, (icext(uri_rdfs_ContainerMembershipProperty, uri_rdf__3)=true)). % 38.12/25.81 tff(c_4168, plain, (icext(uri_rdf_Property, uri_rdf_value)=true)). % 38.12/25.81 tff(c_4129, plain, (icext(uri_rdf_Property, uri_rdf_rest)=true)). % 38.12/25.81 tff(c_4090, plain, (icext(uri_rdf_Property, uri_rdf_type)=true)). % 38.12/25.81 tff(c_4047, plain, (icext(uri_owl_ObjectProperty, uri_ex_p)=true)). % 38.12/25.81 tff(c_3972, plain, (icext(uri_rdf_Property, uri_rdf_first)=true)). % 38.12/25.81 tff(c_3962, plain, (icext(uri_rdfs_Class, uri_rdf_Property)=true)). % 38.12/25.81 tff(c_3922, plain, (icext(uri_rdf_Property, uri_rdf__3)=true)). % 38.12/25.81 tff(c_3856, plain, (icext(uri_rdf_Property, uri_rdf__2)=true)). % 38.12/25.81 tff(c_3846, plain, (icext(uri_rdf_Property, uri_rdf__1)=true)). % 38.12/25.81 tff(c_3802, plain, (icext(uri_rdf_Property, uri_rdf_object)=true)). % 38.12/25.81 tff(c_3762, plain, (icext(sK3_testcase_premise_fullish_010_Negative_Property_Assertions_BNODE_x1, uri_ex_s)=true)). % 38.12/25.81 tff(c_3726, plain, (icext(uri_rdf_List, uri_rdf_nil)=true)). % 38.12/25.81 tff(c_3686, plain, (icext(uri_rdfs_ContainerMembershipProperty, uri_rdf__2)=true)). % 38.12/25.81 tff(c_3640, plain, (icext(uri_rdfs_ContainerMembershipProperty, uri_rdf__1)=true)). % 38.12/25.81 tff(c_3578, plain, (icext(uri_rdfs_Datatype, uri_rdf_XMLLiteral)=true)). % 38.12/25.81 tff(c_3537, plain, (icext(uri_rdf_Property, uri_rdf_subject)=true)). % 38.12/25.81 tff(c_3493, plain, (ip(uri_rdf__2)=true)). % 38.12/25.81 tff(c_3458, plain, (ic(uri_rdfs_Seq)=true)). % 38.12/25.81 tff(c_3422, plain, (ic(uri_rdf_Alt)=true)). % 38.12/25.81 tff(c_3381, plain, (ip(uri_owl_onProperty)=true)). % 38.12/25.81 tff(c_3337, plain, (ic(uri_rdfs_ContainerMembershipProperty)=true)). % 38.12/25.81 tff(c_3299, plain, (ic(uri_rdf_XMLLiteral)=true)). % 38.12/25.81 tff(c_3264, plain, (ip(uri_owl_oneOf)=true)). % 38.12/25.81 tff(c_3224, plain, (ip(uri_rdf__1)=true)). % 38.12/25.81 tff(c_3184, plain, (ic(uri_rdfs_Datatype)=true)). % 38.12/25.81 tff(c_3147, plain, (ip(uri_rdf_rest)=true)). % 38.12/25.81 tff(c_3092, plain, (ip(uri_rdfs_seeAlso)=true)). % 38.12/25.81 tff(c_198, plain, (![BNODE_z_55]: (tuple(iext(uri_owl_sourceIndividual, BNODE_z_55, uri_ex_s), iext(uri_rdf_type, BNODE_z_55, uri_owl_NegativePropertyAssertion), iext(uri_owl_assertionProperty, BNODE_z_55, uri_ex_p), iext(uri_owl_targetIndividual, BNODE_z_55, uri_ex_o))!=tuple(true, true, true, true)))). % 38.12/25.81 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))). % 38.12/25.81 tff(c_2982, plain, (ic(uri_rdf_Property)=true)). % 38.12/25.81 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))). % 38.12/25.81 tff(c_2439, plain, (ic(uri_rdfs_Container)=true)). % 38.12/25.81 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))). % 38.12/25.81 tff(c_2054, plain, (ip(uri_rdf__3)=true)). % 38.12/25.81 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))). % 38.12/25.81 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))). % 38.12/25.81 tff(c_1670, plain, (ip(uri_owl_allValuesFrom)=true)). % 38.12/25.81 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))). % 38.12/25.81 tff(c_1587, plain, (ic(uri_rdfs_Literal)=true)). % 38.12/25.81 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))). % 38.12/25.81 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))). % 38.12/25.81 tff(c_1490, plain, (ip(uri_owl_complementOf)=true)). % 38.12/25.81 tff(c_1442, plain, (ip(uri_rdf_subject)=true)). % 38.12/25.81 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))). % 38.12/25.81 tff(c_1346, plain, (ip(uri_rdfs_isDefinedBy)=true)). % 38.12/25.81 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))). % 38.12/25.81 tff(c_1311, plain, (ip(uri_rdfs_subPropertyOf)=true)). % 38.12/25.81 tff(c_164, plain, (![P_45, Q_46]: (ifeq(iext(uri_rdfs_subPropertyOf, P_45, Q_46), true, ip(P_45), true)=true))). % 38.12/25.81 tff(c_1231, plain, (ip(uri_rdfs_domain)=true)). % 38.12/25.81 tff(c_156, plain, (![C_39]: (ifeq(ic(C_39), true, iext(uri_rdfs_subClassOf, C_39, C_39), true)=true))). % 38.12/25.81 tff(c_1178, plain, (ic(uri_rdfs_Class)=true)). % 38.12/25.81 tff(c_150, plain, (![C_35, D_36]: (ifeq(iext(uri_rdfs_subClassOf, C_35, D_36), true, ic(D_36), true)=true))). % 38.12/25.81 tff(c_1112, plain, (ic(uri_rdf_Bag)=true)). % 38.12/25.81 tff(c_152, plain, (![C_37, D_38]: (ifeq(iext(uri_rdfs_subClassOf, C_37, D_38), true, ic(C_37), true)=true))). % 38.12/25.81 tff(c_1055, plain, (ip(uri_rdfs_range)=true)). % 38.12/25.81 tff(c_1019, plain, (ip(uri_rdf_value)=true)). % 38.12/25.81 tff(c_162, plain, (![P_43, Q_44]: (ifeq(iext(uri_rdfs_subPropertyOf, P_43, Q_44), true, ip(Q_44), true)=true))). % 38.12/25.81 tff(c_28, plain, (![P_9]: (ifeq(ip(P_9), true, iext(uri_rdf_type, P_9, uri_rdf_Property), true)=true))). % 38.12/25.81 tff(c_904, plain, (ip(uri_rdfs_subClassOf)=true)). % 38.12/25.81 tff(c_170, plain, (![P_51]: (ifeq(ip(P_51), true, iext(uri_rdfs_subPropertyOf, P_51, P_51), true)=true))). % 38.12/25.81 tff(c_864, plain, (ip(uri_rdf_type)=true)). % 38.12/25.81 tff(c_4, plain, (![P_4, S_5, O_6]: (ifeq(iext(P_4, S_5, O_6), true, ip(P_4), true)=true))). % 38.12/25.81 tff(c_620, plain, (ip(uri_rdf_object)=true)). % 38.12/25.81 tff(c_599, plain, (ip(uri_rdf_first)=true)). % 38.12/25.81 tff(c_30, plain, (![P_10]: (ifeq(iext(uri_rdf_type, P_10, uri_rdf_Property), true, ip(P_10), true)=true))). % 38.12/25.81 tff(c_58, plain, (![C_15]: (ifeq(ic(C_15), true, iext(uri_rdfs_subClassOf, C_15, uri_rdfs_Resource), true)=true))). % 38.12/25.81 tff(c_114, plain, (![X_22]: (ifeq(ic(X_22), true, icext(uri_rdfs_Class, X_22), true)=true))). % 38.12/25.81 tff(c_116, plain, (![X_23]: (ifeq(icext(uri_rdfs_Class, X_23), true, ic(X_23), true)=true))). % 38.12/25.81 tff(c_122, plain, (![X_26]: (ifeq(icext(uri_rdfs_Literal, X_26), true, lv(X_26), true)=true))). % 38.12/25.82 tff(c_514, plain, (![X_63]: (icext(uri_rdfs_Resource, X_63)=true))). % 38.12/25.82 tff(c_201, plain, (![X_8]: (ifeq(lv(X_8), true, true, true)=true))). % 38.12/25.82 tff(c_124, plain, (![X_27]: (ifeq(lv(X_27), true, icext(uri_rdfs_Literal, X_27), true)=true))). % 38.12/25.82 tff(c_2, plain, (![A_1, B_2, C_3]: (ifeq(A_1, A_1, B_2, C_3)=B_2))). % 38.12/25.82 tff(c_52, plain, (iext(uri_rdfs_range, uri_rdfs_seeAlso, uri_rdfs_Resource)=true)). % 38.12/25.82 tff(c_186, plain, (iext(uri_owl_allValuesFrom, sK3_testcase_premise_fullish_010_Negative_Property_Assertions_BNODE_x1, sK4_testcase_premise_fullish_010_Negative_Property_Assertions_BNODE_x2)=true)). % 38.12/25.82 tff(c_194, plain, (iext(uri_rdf_type, uri_ex_p, uri_owl_ObjectProperty)=true)). % 38.12/25.82 tff(c_10, plain, (iext(uri_rdf_type, uri_rdf_first, uri_rdf_Property)=true)). % 38.12/25.82 tff(c_154, plain, (iext(uri_rdfs_range, uri_rdfs_subClassOf, uri_rdfs_Class)=true)). % 38.12/25.82 tff(c_178, plain, (iext(uri_rdfs_domain, uri_rdf_value, uri_rdfs_Resource)=true)). % 38.12/25.82 tff(c_18, plain, (iext(uri_rdf_type, uri_rdf__2, uri_rdf_Property)=true)). % 38.12/25.82 tff(c_12, plain, (iext(uri_rdf_type, uri_rdf_nil, uri_rdf_List)=true)). % 38.12/25.82 tff(c_100, plain, (iext(uri_rdfs_subClassOf, uri_rdf_XMLLiteral, uri_rdfs_Literal)=true)). % 38.12/25.82 tff(c_22, plain, (iext(uri_rdf_type, uri_rdf_object, uri_rdf_Property)=true)). % 38.12/25.82 tff(c_50, plain, (iext(uri_rdfs_domain, uri_rdfs_seeAlso, uri_rdfs_Resource)=true)). % 38.12/25.82 tff(c_16, plain, (iext(uri_rdf_type, uri_rdf__1, uri_rdf_Property)=true)). % 38.12/25.82 tff(c_188, plain, (iext(uri_owl_onProperty, sK3_testcase_premise_fullish_010_Negative_Property_Assertions_BNODE_x1, uri_ex_p)=true)). % 38.12/25.82 tff(c_96, plain, (iext(uri_rdf_type, uri_rdf__3, uri_rdfs_ContainerMembershipProperty)=true)). % 38.12/25.82 tff(c_64, plain, (iext(uri_rdfs_domain, uri_rdf_rest, uri_rdf_List)=true)). % 38.12/25.82 tff(c_60, plain, (iext(uri_rdfs_domain, uri_rdf_first, uri_rdf_List)=true)). % 38.12/25.82 tff(c_132, plain, (iext(uri_rdfs_range, uri_rdfs_range, uri_rdfs_Class)=true)). % 38.12/25.82 tff(c_160, plain, (iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, uri_rdf_Property)=true)). % 38.12/25.82 tff(c_176, plain, (iext(uri_rdfs_range, uri_rdf_type, uri_rdfs_Class)=true)). % 38.12/25.82 tff(c_182, plain, (iext(uri_owl_oneOf, sK1_testcase_premise_fullish_010_Negative_Property_Assertions_BNODE_x3, sK2_testcase_premise_fullish_010_Negative_Property_Assertions_BNODE_x4)=true)). % 38.12/25.82 tff(c_102, plain, (iext(uri_rdf_type, uri_rdf_XMLLiteral, uri_rdfs_Datatype)=true)). % 38.12/25.82 tff(c_98, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Seq, uri_rdfs_Container)=true)). % 38.12/25.82 tff(c_92, plain, (iext(uri_rdf_type, uri_rdf__1, uri_rdfs_ContainerMembershipProperty)=true)). % 38.12/25.82 tff(c_86, plain, (iext(uri_rdfs_range, uri_rdf__1, uri_rdfs_Resource)=true)). % 38.12/25.82 tff(c_20, plain, (iext(uri_rdf_type, uri_rdf__3, uri_rdf_Property)=true)). % 38.12/25.82 tff(c_42, plain, (iext(uri_rdfs_range, uri_rdfs_isDefinedBy, uri_rdfs_Resource)=true)). % 38.12/25.82 tff(c_128, plain, (iext(uri_rdfs_domain, uri_rdfs_range, uri_rdf_Property)=true)). % 38.12/25.82 tff(c_94, plain, (iext(uri_rdf_type, uri_rdf__2, uri_rdfs_ContainerMembershipProperty)=true)). % 38.12/25.82 tff(c_174, plain, (iext(uri_rdfs_domain, uri_rdf_type, uri_rdfs_Resource)=true)). % 38.12/25.82 tff(c_62, plain, (iext(uri_rdfs_range, uri_rdf_first, uri_rdfs_Resource)=true)). % 38.12/25.82 tff(c_36, plain, (iext(uri_rdfs_domain, uri_rdfs_comment, uri_rdfs_Resource)=true)). % 38.12/25.82 tff(c_112, plain, (iext(uri_rdfs_range, uri_rdfs_domain, uri_rdfs_Class)=true)). % 38.12/25.82 tff(c_44, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_isDefinedBy, uri_rdfs_seeAlso)=true)). % 38.12/25.82 tff(c_82, plain, (iext(uri_rdfs_domain, uri_rdf__2, uri_rdfs_Resource)=true)). % 38.12/25.82 tff(c_126, plain, (iext(uri_rdf_type, uri_rdf_Property, uri_rdfs_Class)=true)). % 38.12/25.82 tff(c_88, plain, (iext(uri_rdfs_range, uri_rdf__2, uri_rdfs_Resource)=true)). % 38.12/25.82 tff(c_90, plain, (iext(uri_rdfs_range, uri_rdf__3, uri_rdfs_Resource)=true)). % 38.12/25.82 tff(c_26, plain, (iext(uri_rdf_type, uri_rdf_subject, uri_rdf_Property)=true)). % 38.12/25.82 tff(c_80, plain, (iext(uri_rdfs_domain, uri_rdf__1, uri_rdfs_Resource)=true)). % 38.12/25.82 tff(c_144, plain, (iext(uri_rdfs_range, uri_rdf_subject, uri_rdfs_Resource)=true)). % 38.12/25.82 tff(c_40, plain, (iext(uri_rdfs_domain, uri_rdfs_isDefinedBy, uri_rdfs_Resource)=true)). % 38.12/25.82 tff(c_24, plain, (iext(uri_rdf_type, uri_rdf_value, uri_rdf_Property)=true)). % 38.12/25.82 tff(c_46, plain, (iext(uri_rdfs_domain, uri_rdfs_label, uri_rdfs_Resource)=true)). % 38.12/25.82 tff(c_48, plain, (iext(uri_rdfs_range, uri_rdfs_label, uri_rdfs_Literal)=true)). % 38.12/25.82 tff(c_76, plain, (iext(uri_rdfs_domain, uri_rdfs_member, uri_rdfs_Resource)=true)). % 38.12/25.82 tff(c_84, plain, (iext(uri_rdfs_domain, uri_rdf__3, uri_rdfs_Resource)=true)). % 38.12/25.82 tff(c_180, plain, (iext(uri_rdfs_range, uri_rdf_value, uri_rdfs_Resource)=true)). % 38.12/25.82 tff(c_74, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, uri_rdf_Property)=true)). % 38.12/25.82 tff(c_190, plain, (iext(uri_rdf_rest, sK2_testcase_premise_fullish_010_Negative_Property_Assertions_BNODE_x4, uri_rdf_nil)=true)). % 38.12/25.82 tff(c_108, plain, (iext(uri_rdfs_domain, uri_rdfs_domain, uri_rdf_Property)=true)). % 38.12/25.82 tff(c_192, plain, (iext(uri_rdf_first, sK2_testcase_premise_fullish_010_Negative_Property_Assertions_BNODE_x4, uri_ex_o)=true)). % 38.12/25.82 tff(c_78, plain, (iext(uri_rdfs_range, uri_rdfs_member, uri_rdfs_Resource)=true)). % 38.12/25.82 tff(c_142, plain, (iext(uri_rdfs_domain, uri_rdf_subject, uri_rdfs_Statement)=true)). % 38.12/25.82 tff(c_146, plain, (iext(uri_rdfs_domain, uri_rdfs_subClassOf, uri_rdfs_Class)=true)). % 38.12/25.82 tff(c_66, plain, (iext(uri_rdfs_range, uri_rdf_rest, uri_rdf_List)=true)). % 38.12/25.82 tff(c_14, plain, (iext(uri_rdf_type, uri_rdf_rest, uri_rdf_Property)=true)). % 38.12/25.82 tff(c_38, plain, (iext(uri_rdfs_range, uri_rdfs_comment, uri_rdfs_Literal)=true)). % 38.12/25.82 tff(c_138, plain, (iext(uri_rdfs_domain, uri_rdf_predicate, uri_rdfs_Statement)=true)). % 38.12/25.82 tff(c_34, plain, (iext(uri_rdf_type, uri_rdf_type, uri_rdf_Property)=true)). % 38.12/25.82 tff(c_68, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Alt, uri_rdfs_Container)=true)). % 38.12/25.82 tff(c_106, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, uri_rdfs_Class)=true)). % 38.12/25.82 tff(c_140, plain, (iext(uri_rdfs_range, uri_rdf_predicate, uri_rdfs_Resource)=true)). % 38.12/25.82 tff(c_70, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Bag, uri_rdfs_Container)=true)). % 38.12/25.82 tff(c_134, plain, (iext(uri_rdfs_domain, uri_rdf_object, uri_rdfs_Statement)=true)). % 38.12/25.82 tff(c_168, plain, (iext(uri_rdfs_range, uri_rdfs_subPropertyOf, uri_rdf_Property)=true)). % 38.12/25.82 tff(c_184, plain, (iext(uri_owl_complementOf, sK4_testcase_premise_fullish_010_Negative_Property_Assertions_BNODE_x2, sK1_testcase_premise_fullish_010_Negative_Property_Assertions_BNODE_x3)=true)). % 38.12/25.82 tff(c_196, plain, (iext(uri_rdf_type, uri_ex_s, sK3_testcase_premise_fullish_010_Negative_Property_Assertions_BNODE_x1)=true)). % 38.12/25.82 tff(c_6, plain, (![X_7]: (ir(X_7)=true))). % 38.12/25.82 % SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 38.12/25.82 %------------------------------------------------------------------------------