%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : SWB012-10 : TPTP v9.0.0. Released v7.5.0. % Transfm : none % Format : tptp:raw % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % Computer : 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:49 PM UTC 2025 % Result : Satisfiable 37.32s 25.75s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.07/0.12 % Problem : SWB012-10 : TPTP v9.0.0. Released v7.5.0. % 0.07/0.13 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % 0.13/0.34 % Computer : n010.cluster.edu % 0.13/0.34 % Model : x86_64 x86_64 % 0.13/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.34 % Memory : 8042.1875MB % 0.13/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.34 % CPULimit : 300 % 0.13/0.34 % WCLimit : 300 % 0.13/0.34 % DateTime : Wed Apr 9 00:56:03 EDT 2025 % 0.13/0.34 % CPUTime : % 37.32/25.74 % 37.32/25.75 % SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 37.32/25.75 % 37.32/25.75 % SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 37.32/25.77 %$ ifeq > iext > tuple > icext > #nlpp > lv > literal_plain > ir > ip > ic > uri_rdfs_subPropertyOf > uri_rdfs_subClassOf > uri_rdfs_seeAlso > uri_rdfs_range > uri_rdfs_member > uri_rdfs_label > uri_rdfs_isDefinedBy > uri_rdfs_domain > uri_rdfs_comment > uri_rdfs_Statement > uri_rdfs_Seq > uri_rdfs_Resource > uri_rdfs_Literal > uri_rdfs_Datatype > uri_rdfs_ContainerMembershipProperty > uri_rdfs_Container > uri_rdfs_Class > uri_rdf_value > uri_rdf_type > uri_rdf_subject > uri_rdf_rest > uri_rdf_predicate > uri_rdf_object > uri_rdf_nil > uri_rdf_first > uri_rdf__3 > uri_rdf__2 > uri_rdf__1 > uri_rdf_XMLLiteral > uri_rdf_Property > uri_rdf_List > uri_rdf_Bag > uri_rdf_Alt > uri_owl_onProperty > uri_owl_intersectionOf > uri_owl_hasValue > uri_owl_Restriction > uri_owl_FunctionalProperty > uri_owl_DatatypeProperty > uri_owl_Class > uri_foaf_Person > uri_ex_name > uri_ex_alice > uri_ex_PersonAttribute > true > sK4_testcase_premise_fullish_012_Template_Class_BNODE_l2 > sK3_testcase_premise_fullish_012_Template_Class_BNODE_l1 > sK2_testcase_premise_fullish_012_Template_Class_BNODE_r > sK1_testcase_premise_fullish_012_Template_Class_BNODE_l3 > dat_str_alice % 37.32/25.77 % 37.32/25.77 %Foreground sorts: % 37.32/25.77 % 37.32/25.77 % 37.32/25.77 %Background operators: % 37.32/25.77 % 37.32/25.77 % 37.32/25.77 %Foreground operators: % 37.32/25.77 tff(uri_rdfs_Datatype, type, uri_rdfs_Datatype: $i). % 37.32/25.77 tff(uri_rdfs_ContainerMembershipProperty, type, uri_rdfs_ContainerMembershipProperty: $i). % 37.32/25.77 tff(uri_rdfs_Resource, type, uri_rdfs_Resource: $i). % 37.32/25.77 tff(uri_rdf_Property, type, uri_rdf_Property: $i). % 37.32/25.77 tff(uri_rdf_subject, type, uri_rdf_subject: $i). % 37.32/25.77 tff(uri_rdf_type, type, uri_rdf_type: $i). % 37.32/25.77 tff(uri_owl_onProperty, type, uri_owl_onProperty: $i). % 37.32/25.77 tff(uri_rdfs_subPropertyOf, type, uri_rdfs_subPropertyOf: $i). % 37.32/25.77 tff(uri_rdfs_seeAlso, type, uri_rdfs_seeAlso: $i). % 37.32/25.77 tff(icext, type, icext: ($i * $i) > $i). % 37.32/25.77 tff(uri_rdfs_range, type, uri_rdfs_range: $i). % 37.32/25.77 tff(uri_rdf_XMLLiteral, type, uri_rdf_XMLLiteral: $i). % 37.32/25.77 tff(uri_rdf_List, type, uri_rdf_List: $i). % 37.32/25.77 tff(uri_rdf_first, type, uri_rdf_first: $i). % 37.32/25.77 tff(uri_rdf_predicate, type, uri_rdf_predicate: $i). % 37.32/25.77 tff(uri_owl_intersectionOf, type, uri_owl_intersectionOf: $i). % 37.32/25.77 tff(tuple, type, tuple: ($i * $i) > $i). % 37.32/25.77 tff(ir, type, ir: $i > $i). % 37.32/25.77 tff(lv, type, lv: $i > $i). % 37.32/25.77 tff(sK1_testcase_premise_fullish_012_Template_Class_BNODE_l3, type, sK1_testcase_premise_fullish_012_Template_Class_BNODE_l3: $i). % 37.32/25.77 tff(uri_owl_hasValue, type, uri_owl_hasValue: $i). % 37.32/25.77 tff(uri_rdf__3, type, uri_rdf__3: $i). % 37.32/25.77 tff(uri_rdf_value, type, uri_rdf_value: $i). % 37.32/25.77 tff(uri_owl_FunctionalProperty, type, uri_owl_FunctionalProperty: $i). % 37.32/25.77 tff(ic, type, ic: $i > $i). % 37.32/25.77 tff(uri_rdfs_Statement, type, uri_rdfs_Statement: $i). % 37.32/25.77 tff(uri_rdf__1, type, uri_rdf__1: $i). % 37.32/25.77 tff(uri_foaf_Person, type, uri_foaf_Person: $i). % 37.32/25.77 tff(iext, type, iext: ($i * $i * $i) > $i). % 37.32/25.77 tff(uri_ex_PersonAttribute, type, uri_ex_PersonAttribute: $i). % 37.32/25.77 tff(dat_str_alice, type, dat_str_alice: $i). % 37.32/25.77 tff(uri_owl_Restriction, type, uri_owl_Restriction: $i). % 37.32/25.77 tff(uri_ex_alice, type, uri_ex_alice: $i). % 37.32/25.77 tff(uri_rdf_rest, type, uri_rdf_rest: $i). % 37.32/25.77 tff(uri_rdfs_label, type, uri_rdfs_label: $i). % 37.32/25.77 tff(uri_rdfs_Container, type, uri_rdfs_Container: $i). % 37.32/25.77 tff(uri_rdfs_subClassOf, type, uri_rdfs_subClassOf: $i). % 37.32/25.77 tff(uri_rdf_object, type, uri_rdf_object: $i). % 37.32/25.77 tff(uri_ex_name, type, uri_ex_name: $i). % 37.32/25.77 tff(ip, type, ip: $i > $i). % 37.32/25.77 tff(uri_rdfs_Class, type, uri_rdfs_Class: $i). % 37.32/25.77 tff(uri_rdfs_Seq, type, uri_rdfs_Seq: $i). % 37.32/25.77 tff(uri_owl_Class, type, uri_owl_Class: $i). % 37.32/25.77 tff(uri_owl_DatatypeProperty, type, uri_owl_DatatypeProperty: $i). % 37.32/25.77 tff(sK3_testcase_premise_fullish_012_Template_Class_BNODE_l1, type, sK3_testcase_premise_fullish_012_Template_Class_BNODE_l1: $i). % 37.32/25.77 tff(uri_rdfs_member, type, uri_rdfs_member: $i). % 37.32/25.77 tff(uri_rdf_Bag, type, uri_rdf_Bag: $i). % 37.32/25.77 tff(uri_rdf__2, type, uri_rdf__2: $i). % 37.32/25.77 tff(uri_rdfs_comment, type, uri_rdfs_comment: $i). % 37.32/25.77 tff(uri_rdfs_Literal, type, uri_rdfs_Literal: $i). % 37.32/25.77 tff(true, type, true: $i). % 37.32/25.77 tff(uri_rdf_Alt, type, uri_rdf_Alt: $i). % 37.32/25.77 tff(uri_rdf_nil, type, uri_rdf_nil: $i). % 37.32/25.77 tff(literal_plain, type, literal_plain: $i > $i). % 37.32/25.77 tff(sK2_testcase_premise_fullish_012_Template_Class_BNODE_r, type, sK2_testcase_premise_fullish_012_Template_Class_BNODE_r: $i). % 37.32/25.77 tff(uri_rdfs_isDefinedBy, type, uri_rdfs_isDefinedBy: $i). % 37.32/25.77 tff(uri_rdfs_domain, type, uri_rdfs_domain: $i). % 37.32/25.77 tff(sK4_testcase_premise_fullish_012_Template_Class_BNODE_l2, type, sK4_testcase_premise_fullish_012_Template_Class_BNODE_l2: $i). % 37.32/25.77 tff(ifeq, type, ifeq: ($i * $i * $i * $i) > $i). % 37.32/25.77 % 37.32/25.77 %Saturated clause set: % 37.32/25.77 tff(c_14741, 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.32/25.77 tff(c_14738, 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.32/25.77 tff(c_15068, 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.32/25.77 tff(c_80893, plain, (![X_1333, Y_1334]: (ifeq(iext(uri_rdfs_comment, X_1333, Y_1334), true, iext(uri_rdfs_comment, X_1333, Y_1334), true)=true))). % 37.32/25.77 tff(c_14978, 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.32/25.77 tff(c_80735, plain, (![X_1328, Y_1329]: (ifeq(iext(uri_rdfs_label, X_1328, Y_1329), true, iext(uri_rdfs_label, X_1328, Y_1329), true)=true))). % 37.32/25.77 tff(c_14913, 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.32/25.77 tff(c_80578, plain, (![X_1323, Y_1324]: (ifeq(iext(uri_rdf_predicate, X_1323, Y_1324), true, iext(uri_rdf_predicate, X_1323, Y_1324), true)=true))). % 37.32/25.77 tff(c_14667, 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.32/25.77 tff(c_80418, plain, (![X_1318, Y_1319]: (ifeq(iext(uri_rdfs_member, X_1318, Y_1319), true, iext(uri_rdfs_member, X_1318, Y_1319), true)=true))). % 37.32/25.77 tff(c_14610, 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.32/25.77 tff(c_80125, plain, (![C_1315]: (ifeq(iext(uri_rdfs_subClassOf, C_1315, uri_owl_Class), true, iext(uri_rdfs_subClassOf, C_1315, uri_rdfs_Resource), true)=true))). % 37.32/25.77 tff(c_14316, 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.32/25.77 tff(c_17192, 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.32/25.77 tff(c_79691, plain, (![C_1311]: (ifeq(iext(uri_rdfs_subClassOf, C_1311, uri_ex_PersonAttribute), true, iext(uri_rdfs_subClassOf, C_1311, uri_rdfs_Resource), true)=true))). % 37.32/25.77 tff(c_13735, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subClassOf), true, ifeq(iext(P_47, uri_owl_Restriction, uri_rdfs_Resource), true, true, true), true)=true))). % 37.32/25.77 tff(c_16849, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subClassOf), true, ifeq(iext(P_47, uri_ex_PersonAttribute, uri_ex_PersonAttribute), true, true, true), true)=true))). % 37.32/25.77 tff(c_13947, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subClassOf), true, ifeq(iext(P_47, uri_owl_Class, uri_owl_Class), true, true, true), true)=true))). % 37.32/25.77 tff(c_14013, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subClassOf), true, ifeq(iext(P_47, uri_owl_Class, uri_rdfs_Resource), true, true, true), true)=true))). % 37.32/25.77 tff(c_78996, plain, (![C_1305]: (ifeq(iext(uri_rdfs_subClassOf, C_1305, uri_rdfs_Statement), true, iext(uri_rdfs_subClassOf, C_1305, uri_rdfs_Resource), true)=true))). % 37.32/25.77 tff(c_17466, 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.32/25.77 tff(c_16940, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subClassOf), true, ifeq(iext(P_47, uri_ex_PersonAttribute, uri_rdfs_Resource), true, true, true), true)=true))). % 37.32/25.77 tff(c_14532, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subClassOf), true, ifeq(iext(P_47, uri_owl_Restriction, uri_owl_Restriction), true, true, true), true)=true))). % 37.32/25.77 tff(c_13663, 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.32/25.77 tff(c_78218, plain, (![C_1298]: (ifeq(iext(uri_rdfs_subClassOf, C_1298, uri_owl_Restriction), true, iext(uri_rdfs_subClassOf, C_1298, uri_rdfs_Resource), true)=true))). % 37.32/25.77 tff(c_78137, plain, (![C_1297]: (ifeq(iext(uri_rdfs_subClassOf, C_1297, uri_rdf_List), true, iext(uri_rdfs_subClassOf, C_1297, uri_rdfs_Resource), true)=true))). % 37.32/25.77 tff(c_14250, 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.32/25.77 tff(c_6564, 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.32/25.77 tff(c_11893, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdf_Property), true, ifeq(iext(P_18, uri_ex_name, Y_21), true, true, true), true)=true))). % 37.32/25.77 tff(c_11896, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdf_Property), true, ifeq(iext(P_28, X_30, uri_ex_name), true, true, true), true)=true))). % 37.32/25.77 tff(c_7103, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdf_Property), true, ifeq(iext(P_18, uri_owl_hasValue, Y_21), true, true, true), true)=true))). % 37.32/25.77 tff(c_8440, 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.32/25.78 tff(c_7397, 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.32/25.78 tff(c_13539, 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.32/25.78 tff(c_10893, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdf_Property), true, ifeq(iext(P_28, X_30, uri_owl_intersectionOf), true, true, true), true)=true))). % 37.32/25.78 tff(c_13176, 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.32/25.78 tff(c_5340, 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.32/25.78 tff(c_5337, 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.32/25.78 tff(c_10890, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdf_Property), true, ifeq(iext(P_18, uri_owl_intersectionOf, Y_21), true, true, true), true)=true))). % 37.32/25.78 tff(c_13271, 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.32/25.78 tff(c_13369, 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.32/25.78 tff(c_5560, 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.32/25.78 tff(c_13445, 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.32/25.78 tff(c_13492, 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.32/25.78 tff(c_6561, 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.32/25.78 tff(c_8437, 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.32/25.78 tff(c_13319, 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.32/25.78 tff(c_7106, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdf_Property), true, ifeq(iext(P_28, X_30, uri_owl_hasValue), true, true, true), true)=true))). % 37.32/25.78 tff(c_13223, 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.32/25.78 tff(c_13616, 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.32/25.78 tff(c_5563, 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.32/25.78 tff(c_7400, 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.32/25.78 tff(c_12548, 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.32/25.78 tff(c_12667, 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.32/25.78 tff(c_12977, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, sK3_testcase_premise_fullish_012_Template_Class_BNODE_l1, uri_rdf_List), true, true, true), true)=true))). % 37.32/25.78 tff(c_12930, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, uri_owl_Class, uri_rdfs_Class), true, true, true), true)=true))). % 37.32/25.78 tff(c_16755, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, uri_ex_PersonAttribute, uri_rdfs_Class), true, true, true), true)=true))). % 37.32/25.78 tff(c_12787, 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.32/25.78 tff(c_12835, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, uri_owl_Restriction, uri_rdfs_Class), true, true, true), true)=true))). % 37.32/25.78 tff(c_12882, 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.32/25.78 tff(c_16802, 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.32/25.78 tff(c_13024, 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.32/25.78 tff(c_7178, 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.32/25.78 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.32/25.78 tff(c_15524, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, sK1_testcase_premise_fullish_012_Template_Class_BNODE_l3, uri_rdf_List), true, true, true), true)=true))). % 37.32/25.78 tff(c_4771, 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.32/25.78 tff(c_10628, 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.32/25.78 tff(c_9322, 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.32/25.78 tff(c_6964, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, uri_owl_hasValue, uri_rdf_Property), true, true, true), true)=true))). % 37.32/25.78 tff(c_5223, 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.32/25.78 tff(c_72150, plain, (![X_1231, Y_1232]: (ifeq(iext(uri_owl_hasValue, X_1231, Y_1232), true, iext(uri_owl_hasValue, X_1231, Y_1232), true)=true))). % 37.32/25.78 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.32/25.78 tff(c_11049, 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.32/25.78 tff(c_8206, 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.32/25.78 tff(c_71720, plain, (![X_1223, Y_1224]: (ifeq(iext(uri_rdf_object, X_1223, Y_1224), true, iext(uri_rdf_object, X_1223, Y_1224), true)=true))). % 37.32/25.78 tff(c_71259, plain, (![X_1218, Y_1219]: (ifeq(iext(uri_rdfs_domain, X_1218, Y_1219), true, iext(uri_rdfs_domain, X_1218, Y_1219), true)=true))). % 37.32/25.78 tff(c_7640, 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.32/25.78 tff(c_6235, 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.32/25.78 tff(c_5506, 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.32/25.78 tff(c_11770, 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.32/25.78 tff(c_4519, 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.32/25.78 tff(c_70543, plain, (![C_1211]: (ifeq(iext(uri_rdfs_subClassOf, C_1211, uri_rdfs_Literal), true, iext(uri_rdfs_subClassOf, C_1211, uri_rdfs_Resource), true)=true))). % 37.32/25.78 tff(c_70372, plain, (![C_1209]: (ifeq(iext(uri_rdfs_subClassOf, C_1209, uri_rdfs_Class), true, iext(uri_rdfs_subClassOf, C_1209, uri_rdfs_Resource), true)=true))). % 37.32/25.78 tff(c_4768, 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.32/25.78 tff(c_70062, plain, (![C_1205]: (ifeq(iext(uri_rdfs_subClassOf, C_1205, uri_rdfs_ContainerMembershipProperty), true, iext(uri_rdfs_subClassOf, C_1205, uri_rdfs_Resource), true)=true))). % 37.32/25.78 tff(c_7719, 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.32/25.78 tff(c_5765, 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.32/25.78 tff(c_8034, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subPropertyOf), true, ifeq(iext(P_47, uri_owl_intersectionOf, uri_owl_intersectionOf), true, true, true), true)=true))). % 37.32/25.78 tff(c_69640, plain, (![X_1198, Y_1199]: (ifeq(iext(uri_rdf__3, X_1198, Y_1199), true, iext(uri_rdfs_member, X_1198, Y_1199), true)=true))). % 37.32/25.78 tff(c_69613, plain, (![X_1194, Y_1195]: (ifeq(iext(uri_rdf_subject, X_1194, Y_1195), true, iext(uri_rdf_subject, X_1194, Y_1195), true)=true))). % 37.32/25.78 tff(c_4823, 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.32/25.78 tff(c_69432, plain, (![X_1188, Y_1189]: (ifeq(iext(uri_rdfs_isDefinedBy, X_1188, Y_1189), true, iext(uri_rdfs_isDefinedBy, X_1188, Y_1189), true)=true))). % 37.32/25.78 tff(c_12387, 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.32/25.78 tff(c_5276, 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.32/25.78 tff(c_8276, 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.32/25.79 tff(c_68322, plain, (![X_1181, Y_1182]: (ifeq(iext(uri_rdfs_subClassOf, X_1181, Y_1182), true, iext(uri_rdfs_subClassOf, X_1181, Y_1182), true)=true))). % 37.32/25.79 tff(c_4720, 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.32/25.79 tff(c_7956, 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.32/25.79 tff(c_4619, 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.32/25.79 tff(c_4563, 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.32/25.79 tff(c_67580, plain, (![C_1172]: (ifeq(iext(uri_rdfs_subClassOf, C_1172, uri_rdfs_Datatype), true, iext(uri_rdfs_subClassOf, C_1172, uri_rdfs_Resource), true)=true))). % 37.32/25.79 tff(c_9404, 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.32/25.79 tff(c_9811, 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.32/25.79 tff(c_12495, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subPropertyOf), true, ifeq(iext(P_47, uri_owl_hasValue, uri_owl_hasValue), true, true, true), true)=true))). % 37.32/25.79 tff(c_9878, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subPropertyOf), true, ifeq(iext(P_47, uri_ex_name, uri_ex_name), true, true, true), true)=true))). % 37.32/25.79 tff(c_8676, 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.32/25.79 tff(c_66762, plain, (![C_1165]: (ifeq(iext(uri_rdfs_subClassOf, C_1165, uri_rdf_Alt), true, iext(uri_rdfs_subClassOf, C_1165, uri_rdfs_Resource), true)=true))). % 37.32/25.79 tff(c_4717, 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.32/25.79 tff(c_5997, 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.32/25.79 tff(c_66457, plain, (![X_1158, Y_1159]: (ifeq(iext(uri_rdf__2, X_1158, Y_1159), true, iext(uri_rdf__2, X_1158, Y_1159), true)=true))). % 37.32/25.79 tff(c_7575, 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.32/25.79 tff(c_9029, 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.32/25.79 tff(c_9470, 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.32/25.79 tff(c_4469, 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.32/25.79 tff(c_4522, 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.32/25.79 tff(c_65713, plain, (![X_1147, Y_1148]: (ifeq(iext(uri_owl_onProperty, X_1147, Y_1148), true, iext(uri_owl_onProperty, X_1147, Y_1148), true)=true))). % 37.32/25.79 tff(c_5391, 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.32/25.79 tff(c_65420, plain, (![C_1144]: (ifeq(iext(uri_rdfs_subClassOf, C_1144, uri_rdfs_Seq), true, iext(uri_rdfs_subClassOf, C_1144, uri_rdfs_Resource), true)=true))). % 37.32/25.79 tff(c_6874, 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.32/25.79 tff(c_65214, plain, (![X_1139, Y_1140]: (ifeq(iext(uri_rdf_first, X_1139, Y_1140), true, iext(uri_rdf_first, X_1139, Y_1140), true)=true))). % 37.32/25.79 tff(c_10395, 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.32/25.79 tff(c_64766, plain, (![X_1132, Y_1133]: (ifeq(iext(uri_rdf_value, X_1132, Y_1133), true, iext(uri_rdf_value, X_1132, Y_1133), true)=true))). % 37.32/25.79 tff(c_11142, 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.32/25.79 tff(c_11411, 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.32/25.79 tff(c_4820, 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.32/25.79 tff(c_7797, 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.32/25.79 tff(c_64200, plain, (![X_1123, Y_1124]: (ifeq(iext(uri_rdf__3, X_1123, Y_1124), true, iext(uri_rdf__3, X_1123, Y_1124), true)=true))). % 37.32/25.79 tff(c_5687, 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.32/25.79 tff(c_63905, plain, (![C_1120]: (ifeq(iext(uri_rdfs_subClassOf, C_1120, uri_rdf_XMLLiteral), true, iext(uri_rdfs_subClassOf, C_1120, uri_rdfs_Resource), true)=true))). % 37.32/25.79 tff(c_10016, 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.32/25.79 tff(c_63489, plain, (![X_1113, Y_1114]: (ifeq(iext(uri_ex_name, X_1113, Y_1114), true, iext(uri_ex_name, X_1113, Y_1114), true)=true))). % 37.32/25.79 tff(c_63421, plain, (![P_1111]: (ifeq(iext(uri_rdfs_subPropertyOf, P_1111, uri_rdf__1), true, iext(uri_rdfs_subPropertyOf, P_1111, uri_rdfs_member), true)=true))). % 37.32/25.79 tff(c_63395, plain, (![X_1107, Y_1108]: (ifeq(iext(uri_rdfs_seeAlso, X_1107, Y_1108), true, iext(uri_rdfs_seeAlso, X_1107, Y_1108), true)=true))). % 37.32/25.79 tff(c_12031, 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.32/25.79 tff(c_15477, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, sK4_testcase_premise_fullish_012_Template_Class_BNODE_l2, uri_rdf_List), true, true, true), true)=true))). % 37.32/25.79 tff(c_10218, 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.32/25.79 tff(c_62571, plain, (![C_1100]: (ifeq(iext(uri_rdfs_subClassOf, C_1100, uri_rdfs_Container), true, iext(uri_rdfs_subClassOf, C_1100, uri_rdfs_Resource), true)=true))). % 37.32/25.79 tff(c_7315, 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.32/25.79 tff(c_62397, plain, (![X_1095, Y_1096]: (ifeq(iext(uri_owl_intersectionOf, X_1095, Y_1096), true, iext(uri_owl_intersectionOf, X_1095, Y_1096), true)=true))). % 37.32/25.79 tff(c_9944, 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.32/25.79 tff(c_62104, plain, (![C_1092]: (ifeq(iext(uri_rdfs_subClassOf, C_1092, uri_rdf_Bag), true, iext(uri_rdfs_subClassOf, C_1092, uri_rdfs_Resource), true)=true))). % 37.32/25.79 tff(c_6082, 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.32/25.79 tff(c_4616, 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.32/25.79 tff(c_61718, plain, (![X_1084, Y_1085]: (ifeq(iext(uri_rdf_rest, X_1084, Y_1085), true, iext(uri_rdf_rest, X_1084, Y_1085), true)=true))). % 37.32/25.79 tff(c_61685, plain, (![P_1083]: (ifeq(iext(uri_rdfs_subPropertyOf, P_1083, uri_rdf__2), true, iext(uri_rdfs_subPropertyOf, P_1083, uri_rdfs_member), true)=true))). % 37.32/25.79 tff(c_5944, 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.32/25.79 tff(c_9242, 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.32/25.79 tff(c_8380, 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.32/25.79 tff(c_7510, 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.32/25.79 tff(c_61098, plain, (![P_1077]: (ifeq(iext(uri_rdfs_subPropertyOf, P_1077, uri_rdf__3), true, iext(uri_rdfs_subPropertyOf, P_1077, uri_rdfs_member), true)=true))). % 37.32/25.79 tff(c_4472, 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.32/25.79 tff(c_8976, 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.32/25.79 tff(c_12307, 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.32/25.79 tff(c_59653, plain, (![X_1066, Y_1067]: (ifeq(iext(uri_rdfs_subPropertyOf, X_1066, Y_1067), true, iext(uri_rdfs_subPropertyOf, X_1066, Y_1067), true)=true))). % 37.32/25.79 tff(c_6729, 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.32/25.79 tff(c_12097, 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.32/25.79 tff(c_59242, plain, (![X_1059, Y_1060]: (ifeq(iext(uri_rdf__1, X_1059, Y_1060), true, iext(uri_rdf__1, X_1059, Y_1060), true)=true))). % 37.32/25.79 tff(c_11836, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, uri_ex_name, uri_rdf_Property), true, true, true), true)=true))). % 37.32/25.79 tff(c_4425, 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.32/25.79 tff(c_58600, plain, (![X_1050, Y_1051]: (ifeq(iext(uri_rdf__1, X_1050, Y_1051), true, iext(uri_rdfs_member, X_1050, Y_1051), true)=true))). % 37.32/25.79 tff(c_58429, plain, (![C_1048]: (ifeq(iext(uri_rdfs_subClassOf, C_1048, uri_rdf_Property), true, iext(uri_rdfs_subClassOf, C_1048, uri_rdfs_Resource), true)=true))). % 37.32/25.79 tff(c_57517, plain, (![X_1038, Y_1039]: (ifeq(iext(uri_rdf__2, X_1038, Y_1039), true, iext(uri_rdfs_member, X_1038, Y_1039), true)=true))). % 37.32/25.79 tff(c_8729, 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.32/25.79 tff(c_57064, plain, (![X_1033, Y_1034]: (ifeq(iext(uri_rdfs_range, X_1033, Y_1034), true, iext(uri_rdfs_range, X_1033, Y_1034), true)=true))). % 37.32/25.79 tff(c_10690, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, uri_owl_intersectionOf, uri_rdf_Property), true, true, true), true)=true))). % 37.32/25.79 tff(c_9123, 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.32/25.79 tff(c_55961, plain, (![X_1027, Y_1028]: (ifeq(iext(uri_rdf_type, X_1027, Y_1028), true, iext(uri_rdf_type, X_1027, Y_1028), true)=true))). % 37.32/25.79 tff(c_4566, 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.32/25.79 tff(c_4422, 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.32/25.79 tff(c_11490, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdfs_Class), true, ifeq(iext(P_28, X_30, uri_owl_Class), true, true, true), true)=true))). % 37.32/25.79 tff(c_6407, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdfs_Class), true, ifeq(iext(P_28, X_30, uri_owl_Restriction), true, true, true), true)=true))). % 37.32/25.79 tff(c_6152, 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.32/25.79 tff(c_16276, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdfs_Class), true, ifeq(iext(P_28, X_30, uri_ex_PersonAttribute), true, true, true), true)=true))). % 37.32/25.79 tff(c_5001, plain, (![P_47, X_132]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, X_132, uri_rdfs_Resource), true, true, true), true)=true))). % 37.32/25.79 tff(c_8501, 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.32/25.80 tff(c_6292, 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.32/25.80 tff(c_8809, 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.32/25.80 tff(c_10764, 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.32/25.80 tff(c_6149, 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.32/25.80 tff(c_8806, 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.32/25.80 tff(c_7034, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdf_List), true, ifeq(iext(P_18, sK3_testcase_premise_fullish_012_Template_Class_BNODE_l1, Y_21), true, true, true), true)=true))). % 37.32/25.80 tff(c_6289, 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.32/25.80 tff(c_6645, 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.32/25.80 tff(c_8504, 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.32/25.80 tff(c_11487, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdfs_Class), true, ifeq(iext(P_18, uri_owl_Class, Y_21), true, true, true), true)=true))). % 37.32/25.80 tff(c_8117, 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.32/25.80 tff(c_6404, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdfs_Class), true, ifeq(iext(P_18, uri_owl_Restriction, Y_21), true, true, true), true)=true))). % 37.32/25.80 tff(c_16404, 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.32/25.80 tff(c_8114, 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.32/25.80 tff(c_6648, 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.32/25.80 tff(c_16401, 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.32/25.80 tff(c_16273, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdfs_Class), true, ifeq(iext(P_18, uri_ex_PersonAttribute, Y_21), true, true, true), true)=true))). % 37.32/25.80 tff(c_10767, 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.32/25.80 tff(c_7037, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdf_List), true, ifeq(iext(P_28, X_30, sK3_testcase_premise_fullish_012_Template_Class_BNODE_l1), true, true, true), true)=true))). % 37.32/25.80 tff(c_3880, 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.32/25.80 tff(c_4048, 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.32/25.80 tff(c_4003, 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.32/25.80 tff(c_3801, 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.32/25.80 tff(c_4098, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_ex_PersonAttribute), true, ifeq(iext(P_28, X_30, uri_ex_name), true, true, true), true)=true))). % 37.32/25.80 tff(c_3838, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_owl_Class), true, ifeq(iext(P_18, uri_foaf_Person, Y_21), true, true, true), true)=true))). % 37.32/25.80 tff(c_4254, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_owl_Restriction), true, ifeq(iext(P_28, X_30, sK2_testcase_premise_fullish_012_Template_Class_BNODE_r), true, true, true), true)=true))). % 37.32/25.80 tff(c_3777, 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.32/25.80 tff(c_3921, 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.32/25.80 tff(c_4332, 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.32/25.80 tff(c_4124, 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.32/25.80 tff(c_3721, 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.32/25.80 tff(c_4335, 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.32/25.80 tff(c_4006, 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.32/25.80 tff(c_3841, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_owl_Class), true, ifeq(iext(P_28, X_30, uri_foaf_Person), true, true, true), true)=true))). % 37.32/25.80 tff(c_4215, 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.32/25.80 tff(c_4379, 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.32/25.80 tff(c_15176, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdf_List), true, ifeq(iext(P_28, X_30, sK1_testcase_premise_fullish_012_Template_Class_BNODE_l3), true, true, true), true)=true))). % 37.32/25.80 tff(c_4127, 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.32/25.80 tff(c_3958, 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.32/25.80 tff(c_3774, 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.32/25.80 tff(c_3683, 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.32/25.80 tff(c_4095, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_ex_PersonAttribute), true, ifeq(iext(P_18, uri_ex_name, Y_21), true, true, true), true)=true))). % 37.32/25.80 tff(c_3918, 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.32/25.80 tff(c_4170, 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.32/25.80 tff(c_4382, 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.32/25.80 tff(c_3883, 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.32/25.80 tff(c_4051, 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.32/25.80 tff(c_4212, 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.32/25.80 tff(c_15142, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdf_List), true, ifeq(iext(P_18, sK4_testcase_premise_fullish_012_Template_Class_BNODE_l2, Y_21), true, true, true), true)=true))). % 37.32/25.80 tff(c_3724, 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.32/25.80 tff(c_4251, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_owl_Restriction), true, ifeq(iext(P_18, sK2_testcase_premise_fullish_012_Template_Class_BNODE_r, Y_21), true, true, true), true)=true))). % 37.32/25.80 tff(c_3961, 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.32/25.80 tff(c_4294, 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.32/25.80 tff(c_4291, 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.32/25.80 tff(c_3804, 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.32/25.80 tff(c_3680, 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.32/25.80 tff(c_4167, 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.32/25.80 tff(c_15173, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdf_List), true, ifeq(iext(P_18, sK1_testcase_premise_fullish_012_Template_Class_BNODE_l3, Y_21), true, true, true), true)=true))). % 37.32/25.80 tff(c_15145, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdf_List), true, ifeq(iext(P_28, X_30, sK4_testcase_premise_fullish_012_Template_Class_BNODE_l2), true, true, true), true)=true))). % 37.32/25.80 tff(c_2163, plain, (![P_95, X_60, Y_98]: (ifeq(iext(uri_rdfs_domain, P_95, uri_rdfs_Resource), true, ifeq(iext(P_95, X_60, Y_98), true, true, true), true)=true))). % 37.32/25.80 tff(c_2672, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_ex_name), true, ifeq(iext(P_102, uri_ex_alice, literal_plain(dat_str_alice)), true, true, true), true)=true))). % 37.32/25.80 tff(c_1793, plain, (![P_91, X_93, X_60]: (ifeq(iext(uri_rdfs_range, P_91, uri_rdfs_Resource), true, ifeq(iext(P_91, X_93, X_60), true, true, true), true)=true))). % 37.32/25.80 tff(c_2792, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdf_type), true, ifeq(iext(P_102, uri_rdf_first, uri_rdf_Property), true, true, true), true)=true))). % 37.32/25.80 tff(c_2684, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdf_type), true, ifeq(iext(P_102, uri_rdf_type, uri_rdf_Property), true, true, true), true)=true))). % 37.32/25.80 tff(c_2981, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdf_first), true, ifeq(iext(P_102, sK3_testcase_premise_fullish_012_Template_Class_BNODE_l1, uri_owl_DatatypeProperty), true, true, true), true)=true))). % 37.32/25.80 tff(c_2921, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_domain), true, ifeq(iext(P_102, uri_rdfs_label, uri_rdfs_Resource), true, true, true), true)=true))). % 37.32/25.80 tff(c_2939, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdf_type), true, ifeq(iext(P_102, uri_rdf_object, uri_rdf_Property), true, true, true), true)=true))). % 37.32/25.80 tff(c_3089, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_domain), true, ifeq(iext(P_102, uri_rdf_value, uri_rdfs_Resource), true, true, true), true)=true))). % 37.32/25.80 tff(c_2756, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdf_type), true, ifeq(iext(P_102, uri_foaf_Person, uri_owl_Class), true, true, true), true)=true))). % 37.32/25.80 tff(c_43198, plain, (![X_873, Y_874]: (ifeq(iext(uri_rdfs_isDefinedBy, X_873, Y_874), true, iext(uri_rdfs_seeAlso, X_873, Y_874), true)=true))). % 37.32/25.80 tff(c_2834, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdf_rest), true, ifeq(iext(P_102, sK4_testcase_premise_fullish_012_Template_Class_BNODE_l2, sK1_testcase_premise_fullish_012_Template_Class_BNODE_l3), true, true, true), true)=true))). % 37.32/25.80 tff(c_2828, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_domain), true, ifeq(iext(P_102, uri_rdfs_seeAlso, uri_rdfs_Resource), true, true, true), true)=true))). % 37.32/25.80 tff(c_2987, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_range), true, ifeq(iext(P_102, uri_rdfs_comment, uri_rdfs_Literal), true, true, true), true)=true))). % 37.32/25.80 tff(c_2798, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_range), true, ifeq(iext(P_102, uri_rdf_predicate, uri_rdfs_Resource), true, true, true), true)=true))). % 37.32/25.80 tff(c_3041, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_domain), true, ifeq(iext(P_102, uri_rdf_predicate, uri_rdfs_Statement), true, true, true), true)=true))). % 37.32/25.80 tff(c_2951, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdf_type), true, ifeq(iext(P_102, uri_rdf_XMLLiteral, uri_rdfs_Datatype), true, true, true), true)=true))). % 37.32/25.80 tff(c_42334, plain, (![C_865]: (ifeq(iext(uri_rdfs_subClassOf, C_865, uri_rdf_Alt), true, iext(uri_rdfs_subClassOf, C_865, uri_rdfs_Container), true)=true))). % 37.32/25.80 tff(c_2840, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_owl_intersectionOf), true, ifeq(iext(P_102, uri_ex_PersonAttribute, sK3_testcase_premise_fullish_012_Template_Class_BNODE_l1), true, true, true), true)=true))). % 37.32/25.80 tff(c_2678, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_domain), true, ifeq(iext(P_102, uri_rdf__3, uri_rdfs_Resource), true, true, true), true)=true))). % 37.32/25.80 tff(c_41998, plain, (![C_861]: (ifeq(iext(uri_rdfs_subClassOf, C_861, uri_rdf_Bag), true, iext(uri_rdfs_subClassOf, C_861, uri_rdfs_Container), true)=true))). % 37.32/25.80 tff(c_2999, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_subClassOf), true, ifeq(iext(P_102, uri_rdf_Bag, uri_rdfs_Container), true, true, true), true)=true))). % 37.32/25.80 tff(c_2708, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdf_type), true, ifeq(iext(P_102, uri_rdf__2, uri_rdf_Property), true, true, true), true)=true))). % 37.32/25.80 tff(c_2762, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_domain), true, ifeq(iext(P_102, uri_rdfs_domain, uri_rdf_Property), true, true, true), true)=true))). % 37.32/25.80 tff(c_2858, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_subClassOf), true, ifeq(iext(P_102, uri_rdf_Alt, uri_rdfs_Container), true, true, true), true)=true))). % 37.32/25.80 tff(c_3011, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_domain), true, ifeq(iext(P_102, uri_rdf__2, uri_rdfs_Resource), true, true, true), true)=true))). % 37.32/25.80 tff(c_3077, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_domain), true, ifeq(iext(P_102, uri_rdf__1, uri_rdfs_Resource), true, true, true), true)=true))). % 37.32/25.80 tff(c_41145, plain, (![P_853]: (ifeq(iext(uri_rdfs_subPropertyOf, P_853, uri_rdfs_isDefinedBy), true, iext(uri_rdfs_subPropertyOf, P_853, uri_rdfs_seeAlso), true)=true))). % 37.32/25.81 tff(c_2744, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdf_type), true, ifeq(iext(P_102, uri_rdf__3, uri_rdf_Property), true, true, true), true)=true))). % 37.32/25.81 tff(c_3053, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdf_type), true, ifeq(iext(P_102, uri_rdf_nil, uri_rdf_List), true, true, true), true)=true))). % 37.32/25.81 tff(c_2714, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_range), true, ifeq(iext(P_102, uri_rdf_type, uri_rdfs_Class), true, true, true), true)=true))). % 37.32/25.81 tff(c_2915, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdf_type), true, ifeq(iext(P_102, uri_rdf__3, uri_rdfs_ContainerMembershipProperty), true, true, true), true)=true))). % 37.32/25.81 tff(c_40574, plain, (![C_847]: (ifeq(iext(uri_rdfs_subClassOf, C_847, uri_rdfs_Datatype), true, iext(uri_rdfs_subClassOf, C_847, uri_rdfs_Class), true)=true))). % 37.32/25.81 tff(c_3083, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_domain), true, ifeq(iext(P_102, uri_rdfs_subClassOf, uri_rdfs_Class), true, true, true), true)=true))). % 37.32/25.81 tff(c_3047, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_domain), true, ifeq(iext(P_102, uri_rdfs_comment, uri_rdfs_Resource), true, true, true), true)=true))). % 37.32/25.81 tff(c_2909, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_range), true, ifeq(iext(P_102, uri_rdfs_range, uri_rdfs_Class), true, true, true), true)=true))). % 37.32/25.81 tff(c_3029, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_domain), true, ifeq(iext(P_102, uri_rdfs_member, uri_rdfs_Resource), true, true, true), true)=true))). % 37.32/25.81 tff(c_2876, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_subClassOf), true, ifeq(iext(P_102, uri_rdfs_Datatype, uri_rdfs_Class), true, true, true), true)=true))). % 37.32/25.81 tff(c_2690, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_domain), true, ifeq(iext(P_102, uri_rdf_subject, uri_rdfs_Statement), true, true, true), true)=true))). % 37.32/25.81 tff(c_2993, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdf_type), true, ifeq(iext(P_102, uri_rdf_value, uri_rdf_Property), true, true, true), true)=true))). % 37.32/25.81 tff(c_39575, plain, (![C_838]: (ifeq(iext(uri_rdfs_subClassOf, C_838, uri_rdfs_Seq), true, iext(uri_rdfs_subClassOf, C_838, uri_rdfs_Container), true)=true))). % 37.32/25.81 tff(c_3017, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_range), true, ifeq(iext(P_102, uri_rdf__1, uri_rdfs_Resource), true, true, true), true)=true))). % 37.32/25.81 tff(c_2702, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_range), true, ifeq(iext(P_102, uri_rdf_rest, uri_rdf_List), true, true, true), true)=true))). % 37.32/25.81 tff(c_2780, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_domain), true, ifeq(iext(P_102, uri_rdfs_range, uri_rdf_Property), true, true, true), true)=true))). % 37.32/25.81 tff(c_3059, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_range), true, ifeq(iext(P_102, uri_rdfs_member, uri_rdfs_Resource), true, true, true), true)=true))). % 37.32/25.81 tff(c_2804, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdf_type), true, ifeq(iext(P_102, uri_rdf__2, uri_rdfs_ContainerMembershipProperty), true, true, true), true)=true))). % 37.32/25.81 tff(c_2726, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_range), true, ifeq(iext(P_102, uri_rdf_subject, uri_rdfs_Resource), true, true, true), true)=true))). % 37.32/25.81 tff(c_2927, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_domain), true, ifeq(iext(P_102, uri_rdf_type, uri_rdfs_Resource), true, true, true), true)=true))). % 37.32/25.81 tff(c_2750, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_range), true, ifeq(iext(P_102, uri_rdfs_subPropertyOf, uri_rdf_Property), true, true, true), true)=true))). % 37.32/25.81 tff(c_2864, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_range), true, ifeq(iext(P_102, uri_rdfs_subClassOf, uri_rdfs_Class), true, true, true), true)=true))). % 37.32/25.81 tff(c_2816, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_domain), true, ifeq(iext(P_102, uri_rdf_object, uri_rdfs_Statement), true, true, true), true)=true))). % 37.32/25.81 tff(c_38030, plain, (![D_825]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_825), true, icext(D_825, uri_rdfs_member), true)=true))). % 37.32/25.81 tff(c_2810, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdf_type), true, ifeq(iext(P_102, uri_rdf_rest, uri_rdf_Property), true, true, true), true)=true))). % 37.32/25.81 tff(c_37963, plain, (![D_823]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_823), true, icext(D_823, uri_rdfs_range), true)=true))). % 37.32/25.81 tff(c_37897, plain, (![D_821]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_821), true, icext(D_821, uri_owl_intersectionOf), true)=true))). % 37.32/25.81 tff(c_2903, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdf_rest), true, ifeq(iext(P_102, sK1_testcase_premise_fullish_012_Template_Class_BNODE_l3, uri_rdf_nil), true, true, true), true)=true))). % 37.32/25.81 tff(c_37701, plain, (![D_818]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_818), true, icext(D_818, uri_owl_hasValue), true)=true))). % 37.32/25.81 tff(c_37635, plain, (![D_816]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_816), true, icext(D_816, uri_rdfs_domain), true)=true))). % 37.32/25.81 tff(c_37561, plain, (![D_814]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_814), true, icext(D_814, uri_ex_name), true)=true))). % 37.32/25.81 tff(c_2696, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdf_type), true, ifeq(iext(P_102, uri_rdf__1, uri_rdf_Property), true, true, true), true)=true))). % 37.32/25.81 tff(c_37365, plain, (![D_811]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_811), true, icext(D_811, uri_owl_onProperty), true)=true))). % 37.32/25.81 tff(c_37299, plain, (![D_809]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_809), true, icext(D_809, uri_rdfs_isDefinedBy), true)=true))). % 37.32/25.81 tff(c_37233, plain, (![D_807]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_807), true, icext(D_807, uri_rdfs_subClassOf), true)=true))). % 37.32/25.81 tff(c_2846, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdf_type), true, ifeq(iext(P_102, uri_rdf_subject, uri_rdf_Property), true, true, true), true)=true))). % 37.32/25.81 tff(c_37035, plain, (![D_804]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_804), true, icext(D_804, uri_rdfs_Container), true)=true))). % 37.32/25.81 tff(c_36941, plain, (![D_802]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_802), true, icext(D_802, uri_rdfs_Class), true)=true))). % 37.32/25.81 tff(c_3023, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_subClassOf), true, ifeq(iext(P_102, uri_rdf_XMLLiteral, uri_rdfs_Literal), true, true, true), true)=true))). % 37.32/25.81 tff(c_36744, plain, (![D_799]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_799), true, icext(D_799, uri_rdfs_Seq), true)=true))). % 37.32/25.81 tff(c_36670, plain, (![D_797]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_797), true, icext(D_797, uri_rdf_XMLLiteral), true)=true))). % 37.32/25.81 tff(c_36604, plain, (![D_795]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_795), true, icext(D_795, uri_rdfs_ContainerMembershipProperty), true)=true))). % 37.32/25.81 tff(c_2957, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_range), true, ifeq(iext(P_102, uri_rdf__3, uri_rdfs_Resource), true, true, true), true)=true))). % 37.32/25.81 tff(c_36399, plain, (![D_792]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_792), true, icext(D_792, uri_rdf_Bag), true)=true))). % 37.32/25.81 tff(c_36333, plain, (![D_790]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_790), true, icext(D_790, uri_rdfs_Literal), true)=true))). % 37.32/25.81 tff(c_36135, plain, (![D_787]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_787), true, icext(D_787, uri_rdfs_Datatype), true)=true))). % 37.32/25.81 tff(c_3005, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_range), true, ifeq(iext(P_102, uri_rdfs_label, uri_rdfs_Literal), true, true, true), true)=true))). % 37.32/25.81 tff(c_36068, plain, (![D_785]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_785), true, icext(D_785, uri_rdf_Alt), true)=true))). % 37.32/25.81 tff(c_2720, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdf_type), true, ifeq(iext(P_102, uri_ex_name, uri_ex_PersonAttribute), true, true, true), true)=true))). % 37.32/25.81 tff(c_35869, plain, (![D_782]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_782), true, icext(D_782, uri_owl_Class), true)=true))). % 37.32/25.81 tff(c_35803, plain, (![D_780]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_780), true, icext(D_780, uri_rdfs_Resource), true)=true))). % 37.32/25.81 tff(c_35737, plain, (![D_778]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_778), true, icext(D_778, uri_rdfs_subPropertyOf), true)=true))). % 37.32/25.81 tff(c_2822, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdf_rest), true, ifeq(iext(P_102, sK3_testcase_premise_fullish_012_Template_Class_BNODE_l1, sK4_testcase_premise_fullish_012_Template_Class_BNODE_l2), true, true, true), true)=true))). % 37.32/25.81 tff(c_35541, plain, (![D_775]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_775), true, icext(D_775, uri_owl_Restriction), true)=true))). % 37.32/25.81 tff(c_35475, plain, (![D_773]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_773), true, icext(D_773, uri_rdfs_Statement), true)=true))). % 37.32/25.81 tff(c_35409, plain, (![D_771]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_771), true, icext(D_771, uri_rdfs_seeAlso), true)=true))). % 37.32/25.81 tff(c_2945, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_range), true, ifeq(iext(P_102, uri_rdfs_isDefinedBy, uri_rdfs_Resource), true, true, true), true)=true))). % 37.32/25.81 tff(c_35204, plain, (![D_768]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_768), true, icext(D_768, uri_ex_PersonAttribute), true)=true))). % 37.32/25.81 tff(c_35138, plain, (![D_766]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_766), true, icext(D_766, uri_rdf_List), true)=true))). % 37.32/25.81 tff(c_35051, plain, (![C_763]: (ifeq(iext(uri_rdfs_subClassOf, C_763, uri_rdfs_ContainerMembershipProperty), true, iext(uri_rdfs_subClassOf, C_763, uri_rdf_Property), true)=true))). % 37.32/25.81 tff(c_35021, plain, (![D_762]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_762), true, icext(D_762, uri_rdf_predicate), true)=true))). % 37.32/25.81 tff(c_34955, plain, (![D_760]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_List, D_760), true, icext(D_760, sK3_testcase_premise_fullish_012_Template_Class_BNODE_l1), true)=true))). % 37.32/25.81 tff(c_34889, plain, (![D_758]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_758), true, icext(D_758, uri_rdfs_label), true)=true))). % 37.32/25.81 tff(c_15002, 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.32/25.81 tff(c_2774, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_range), true, ifeq(iext(P_102, uri_rdfs_domain, uri_rdfs_Class), true, true, true), true)=true))). % 37.32/25.81 tff(c_14937, 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.32/25.81 tff(c_15092, 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.32/25.81 tff(c_34602, plain, (![D_750]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_750), true, icext(D_750, uri_rdfs_comment), true)=true))). % 37.32/25.81 tff(c_14692, 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.32/25.81 tff(c_14637, 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.32/25.81 tff(c_14284, 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.32/25.81 tff(c_13770, plain, (![E_41]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Resource, E_41), true, iext(uri_rdfs_subClassOf, uri_owl_Restriction, E_41), true)=true))). % 37.32/25.81 tff(c_13769, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_48), true, iext(Q_48, uri_owl_Restriction, uri_rdfs_Resource), true)=true))). % 37.32/25.81 tff(c_14350, 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.32/25.81 tff(c_14047, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_48), true, iext(Q_48, uri_owl_Class, uri_rdfs_Resource), true)=true))). % 37.32/25.81 tff(c_13981, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_48), true, iext(Q_48, uri_owl_Class, uri_owl_Class), true)=true))). % 37.32/25.81 tff(c_2882, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_range), true, ifeq(iext(P_102, uri_rdfs_seeAlso, uri_rdfs_Resource), true, true, true), true)=true))). % 37.32/25.81 tff(c_14351, 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.32/25.81 tff(c_13700, 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.32/25.81 tff(c_16975, plain, (![E_41]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Resource, E_41), true, iext(uri_rdfs_subClassOf, uri_ex_PersonAttribute, E_41), true)=true))). % 37.32/25.81 tff(c_16883, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_48), true, iext(Q_48, uri_ex_PersonAttribute, uri_ex_PersonAttribute), true)=true))). % 37.32/25.81 tff(c_3065, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_domain), true, ifeq(iext(P_102, uri_rdfs_isDefinedBy, uri_rdfs_Resource), true, true, true), true)=true))). % 37.32/25.81 tff(c_17227, 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.32/25.81 tff(c_17226, 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.32/25.81 tff(c_14566, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_48), true, iext(Q_48, uri_owl_Restriction, uri_owl_Restriction), true)=true))). % 37.32/25.81 tff(c_16974, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_48), true, iext(Q_48, uri_ex_PersonAttribute, uri_rdfs_Resource), true)=true))). % 37.32/25.81 tff(c_14048, plain, (![E_41]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Resource, E_41), true, iext(uri_rdfs_subClassOf, uri_owl_Class, E_41), true)=true))). % 37.32/25.81 tff(c_17500, 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.32/25.81 tff(c_13338, 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.32/25.81 tff(c_2933, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_range), true, ifeq(iext(P_102, uri_rdf_first, uri_rdfs_Resource), true, true, true), true)=true))). % 37.32/25.81 tff(c_13558, 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.32/25.81 tff(c_13464, 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.32/25.81 tff(c_13635, 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.32/25.81 tff(c_13388, 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.32/25.81 tff(c_13242, 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.32/25.81 tff(c_13195, 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.32/25.81 tff(c_13511, 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.32/25.81 tff(c_13290, 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.32/25.81 tff(c_3071, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_range), true, ifeq(iext(P_102, uri_rdf__2, uri_rdfs_Resource), true, true, true), true)=true))). % 37.32/25.81 tff(c_12901, 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.32/25.81 tff(c_12996, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, sK3_testcase_premise_fullish_012_Template_Class_BNODE_l1, uri_rdf_List), true)=true))). % 37.32/25.81 tff(c_12854, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, uri_owl_Restriction, uri_rdfs_Class), true)=true))). % 37.32/25.81 tff(c_13049, 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.32/25.81 tff(c_12806, 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.32/25.81 tff(c_12949, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, uri_owl_Class, uri_rdfs_Class), true)=true))). % 37.32/25.81 tff(c_33216, plain, (![C_703]: (ifeq(iext(uri_rdfs_subClassOf, C_703, uri_rdf_XMLLiteral), true, iext(uri_rdfs_subClassOf, C_703, uri_rdfs_Literal), true)=true))). % 37.32/25.81 tff(c_16774, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, uri_ex_PersonAttribute, uri_rdfs_Class), true)=true))). % 37.32/25.82 tff(c_12573, 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.32/25.82 tff(c_16821, 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.32/25.82 tff(c_33089, plain, (![D_698]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, D_698), true, icext(D_698, uri_rdf__1), true)=true))). % 37.32/25.82 tff(c_12692, 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.32/25.82 tff(c_3035, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdf_type), true, ifeq(iext(P_102, uri_rdf_Property, uri_rdfs_Class), true, true, true), true)=true))). % 37.32/25.82 tff(c_6031, 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.32/25.82 tff(c_11176, 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.32/25.82 tff(c_32750, plain, (![D_689]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_List, D_689), true, icext(D_689, uri_rdf_nil), true)=true))). % 37.32/25.82 tff(c_11073, 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.32/25.82 tff(c_2969, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_domain), true, ifeq(iext(P_102, uri_rdfs_subPropertyOf, uri_rdf_Property), true, true, true), true)=true))). % 37.32/25.82 tff(c_11435, 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.32/25.82 tff(c_6989, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, uri_owl_hasValue, uri_rdf_Property), true)=true))). % 37.32/25.82 tff(c_7664, 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.32/25.82 tff(c_7599, 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.32/25.82 tff(c_6763, 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.32/25.82 tff(c_3101, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdf_type), true, ifeq(iext(P_102, sK2_testcase_premise_fullish_012_Template_Class_BNODE_r, uri_owl_Restriction), true, true, true), true)=true))). % 37.32/25.82 tff(c_11177, 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.32/25.82 tff(c_9145, 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.32/25.82 tff(c_32112, plain, (![D_671]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_List, D_671), true, icext(D_671, sK4_testcase_premise_fullish_012_Template_Class_BNODE_l2), true)=true))). % 37.32/25.82 tff(c_5721, 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.32/25.82 tff(c_2786, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_subClassOf), true, ifeq(iext(P_102, uri_rdfs_Seq, uri_rdfs_Container), true, true, true), true)=true))). % 37.32/25.82 tff(c_8058, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_48), true, iext(Q_48, uri_owl_intersectionOf, uri_owl_intersectionOf), true)=true))). % 37.32/25.82 tff(c_11071, 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.32/25.82 tff(c_9276, 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.32/25.82 tff(c_6116, 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.32/25.82 tff(c_10253, 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.32/25.82 tff(c_5301, 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.32/25.82 tff(c_6764, 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.32/25.82 tff(c_2975, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_owl_hasValue), true, ifeq(iext(P_102, sK2_testcase_premise_fullish_012_Template_Class_BNODE_r, uri_foaf_Person), true, true, true), true)=true))). % 37.32/25.82 tff(c_9504, 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.32/25.82 tff(c_31466, plain, (![D_653]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_653), true, icext(D_653, uri_rdf_value), true)=true))). % 37.32/25.82 tff(c_12341, 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.32/25.82 tff(c_2732, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_subClassOf), true, ifeq(iext(P_102, uri_rdfs_ContainerMembershipProperty, uri_rdf_Property), true, true, true), true)=true))). % 37.32/25.82 tff(c_10652, 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.32/25.82 tff(c_12411, 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.32/25.82 tff(c_31140, plain, (![D_644]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_644), true, icext(D_644, uri_rdf_first), true)=true))). % 37.32/25.82 tff(c_15543, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, sK1_testcase_premise_fullish_012_Template_Class_BNODE_l3, uri_rdf_List), true)=true))). % 37.32/25.82 tff(c_11804, 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.32/25.82 tff(c_2897, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_subPropertyOf), true, ifeq(iext(P_102, uri_rdfs_isDefinedBy, uri_rdfs_seeAlso), true, true, true), true)=true))). % 37.69/25.82 tff(c_5415, 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.69/25.82 tff(c_7212, 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.69/25.82 tff(c_9346, 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.69/25.82 tff(c_30803, plain, (![D_635]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_635), true, icext(D_635, uri_rdf__2), true)=true))). % 37.69/25.82 tff(c_7821, 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.69/25.82 tff(c_9439, 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.69/25.82 tff(c_9054, 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.69/25.82 tff(c_3095, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdf_first), true, ifeq(iext(P_102, sK1_testcase_premise_fullish_012_Template_Class_BNODE_l3, sK2_testcase_premise_fullish_012_Template_Class_BNODE_r), true, true, true), true)=true))). % 37.69/25.82 tff(c_9438, 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.69/25.82 tff(c_8243, 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.69/25.82 tff(c_7754, 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.69/25.82 tff(c_30492, plain, (![D_626]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_626), true, icext(D_626, uri_rdf__3), true)=true))). % 37.69/25.82 tff(c_5968, 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.69/25.82 tff(c_9000, 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.69/25.82 tff(c_2870, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdf_first), true, ifeq(iext(P_102, sK4_testcase_premise_fullish_012_Template_Class_BNODE_l2, uri_owl_FunctionalProperty), true, true, true), true)=true))). % 37.69/25.82 tff(c_9902, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_48), true, iext(Q_48, uri_ex_name, uri_ex_name), true)=true))). % 37.69/25.82 tff(c_8700, 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.69/25.82 tff(c_8405, 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.69/25.82 tff(c_9505, 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.69/25.82 tff(c_2963, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_owl_onProperty), true, ifeq(iext(P_102, sK2_testcase_premise_fullish_012_Template_Class_BNODE_r, uri_rdfs_domain), true, true, true), true)=true))). % 37.69/25.82 tff(c_10051, 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.69/25.82 tff(c_10050, 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.69/25.82 tff(c_12132, 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.69/25.82 tff(c_7753, 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.69/25.82 tff(c_5531, 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.69/25.82 tff(c_11861, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, uri_ex_name, uri_rdf_Property), true)=true))). % 37.69/25.82 tff(c_5789, 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.69/25.82 tff(c_2738, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_range), true, ifeq(iext(P_102, uri_rdf_value, uri_rdfs_Resource), true, true, true), true)=true))). % 37.69/25.82 tff(c_6260, 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.69/25.82 tff(c_9968, 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.69/25.82 tff(c_9835, 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.69/25.82 tff(c_29585, plain, (![D_599]: (ifeq(iext(uri_rdfs_subClassOf, uri_owl_Restriction, D_599), true, icext(D_599, sK2_testcase_premise_fullish_012_Template_Class_BNODE_r), true)=true))). % 37.69/25.82 tff(c_11433, 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.69/25.82 tff(c_2852, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdf_type), true, ifeq(iext(P_102, uri_rdf__1, uri_rdfs_ContainerMembershipProperty), true, true, true), true)=true))). % 37.69/25.82 tff(c_8754, 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.69/25.82 tff(c_7534, 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.69/25.82 tff(c_29255, plain, (![D_590]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_List, D_590), true, icext(D_590, sK1_testcase_premise_fullish_012_Template_Class_BNODE_l3), true)=true))). % 37.69/25.82 tff(c_8310, 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.69/25.82 tff(c_15496, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, sK4_testcase_premise_fullish_012_Template_Class_BNODE_l2, uri_rdf_List), true)=true))). % 37.69/25.82 tff(c_2768, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_domain), true, ifeq(iext(P_102, uri_rdf_first, uri_rdf_List), true, true, true), true)=true))). % 37.69/25.82 tff(c_10429, 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.69/25.82 tff(c_12065, 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.69/25.82 tff(c_28948, plain, (![D_581]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_581), true, icext(D_581, uri_rdf_Property), true)=true))). % 37.69/25.82 tff(c_6898, 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.69/25.82 tff(c_7990, 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.69/25.82 tff(c_10430, 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.69/25.82 tff(c_2888, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_domain), true, ifeq(iext(P_102, uri_rdf_rest, uri_rdf_List), true, true, true), true)=true))). % 37.69/25.82 tff(c_7213, 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.69/25.82 tff(c_12131, 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.69/25.82 tff(c_9147, 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.69/25.82 tff(c_28637, plain, (![D_572]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_572), true, icext(D_572, uri_rdf_type), true)=true))). % 37.69/25.82 tff(c_10715, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, uri_owl_intersectionOf, uri_rdf_Property), true)=true))). % 37.69/25.82 tff(c_10252, 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.69/25.82 tff(c_7340, 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.69/25.82 tff(c_3104, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_ex_name, Q_103), true, iext(Q_103, uri_ex_alice, literal_plain(dat_str_alice)), true)=true))). % 37.69/25.82 tff(c_12519, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_48), true, iext(Q_48, uri_owl_hasValue, uri_owl_hasValue), true)=true))). % 37.69/25.82 tff(c_5247, 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.69/25.82 tff(c_5021, plain, (![Q_48, X_132]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, X_132, uri_rdfs_Resource), true)=true))). % 37.69/25.82 tff(c_3163, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_103), true, iext(Q_103, uri_rdfs_member, uri_rdfs_Resource), true)=true))). % 37.69/25.82 tff(c_3115, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_103), true, iext(Q_103, uri_rdf_value, uri_rdfs_Resource), true)=true))). % 37.69/25.82 tff(c_3166, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_103), true, iext(Q_103, uri_rdfs_comment, uri_rdfs_Resource), true)=true))). % 37.69/25.82 tff(c_3129, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_rest, Q_103), true, iext(Q_103, sK3_testcase_premise_fullish_012_Template_Class_BNODE_l1, sK4_testcase_premise_fullish_012_Template_Class_BNODE_l2), true)=true))). % 37.69/25.82 tff(c_3160, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_103), true, iext(Q_103, uri_rdf__2, uri_rdfs_Resource), true)=true))). % 37.69/25.82 tff(c_3109, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_103), true, iext(Q_103, uri_rdf_rest, uri_rdf_List), true)=true))). % 37.69/25.82 tff(c_3141, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_103), true, iext(Q_103, uri_rdfs_isDefinedBy, uri_rdfs_seeAlso), true)=true))). % 37.69/25.82 tff(c_3116, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_103), true, iext(Q_103, uri_rdf__3, uri_rdf_Property), true)=true))). % 37.69/25.82 tff(c_3156, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_103), true, iext(Q_103, uri_rdfs_comment, uri_rdfs_Literal), true)=true))). % 37.69/25.82 tff(c_3126, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_103), true, iext(Q_103, uri_rdf__2, uri_rdfs_ContainerMembershipProperty), true)=true))). % 37.69/25.82 tff(c_3131, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_rest, Q_103), true, iext(Q_103, sK4_testcase_premise_fullish_012_Template_Class_BNODE_l2, sK1_testcase_premise_fullish_012_Template_Class_BNODE_l3), true)=true))). % 37.69/25.82 tff(c_3140, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_103), true, iext(Q_103, uri_rdf_rest, uri_rdf_List), true)=true))). % 37.69/25.82 tff(c_3112, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_103), true, iext(Q_103, uri_ex_name, uri_ex_PersonAttribute), true)=true))). % 37.69/25.82 tff(c_3169, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_103), true, iext(Q_103, uri_rdfs_isDefinedBy, uri_rdfs_Resource), true)=true))). % 37.69/25.82 tff(c_3119, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_103), true, iext(Q_103, uri_rdfs_domain, uri_rdf_Property), true)=true))). % 37.69/25.82 tff(c_3147, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_103), true, iext(Q_103, uri_rdf_first, uri_rdfs_Resource), true)=true))). % 37.69/25.82 tff(c_3157, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_103), true, iext(Q_103, uri_rdf_value, uri_rdf_Property), true)=true))). % 37.69/25.82 tff(c_3167, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_103), true, iext(Q_103, uri_rdf_nil, uri_rdf_List), true)=true))). % 37.69/25.82 tff(c_3105, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_103), true, iext(Q_103, uri_rdf__3, uri_rdfs_Resource), true)=true))). % 37.69/25.82 tff(c_3162, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_103), true, iext(Q_103, uri_rdf_XMLLiteral, uri_rdfs_Literal), true)=true))). % 37.69/25.82 tff(c_3106, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_103), true, iext(Q_103, uri_rdf_type, uri_rdf_Property), true)=true))). % 37.69/25.83 tff(c_3122, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_103), true, iext(Q_103, uri_rdfs_range, uri_rdf_Property), true)=true))). % 37.69/25.83 tff(c_3134, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_103), true, iext(Q_103, uri_rdf__1, uri_rdfs_ContainerMembershipProperty), true)=true))). % 37.69/25.83 tff(c_3118, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_103), true, iext(Q_103, uri_foaf_Person, uri_owl_Class), true)=true))). % 37.69/25.83 tff(c_3128, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_103), true, iext(Q_103, uri_rdf_object, uri_rdfs_Statement), true)=true))). % 37.69/25.83 tff(c_3132, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_owl_intersectionOf, Q_103), true, iext(Q_103, uri_ex_PersonAttribute, sK3_testcase_premise_fullish_012_Template_Class_BNODE_l1), true)=true))). % 37.69/25.83 tff(c_3150, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_103), true, iext(Q_103, uri_rdf_XMLLiteral, uri_rdfs_Datatype), true)=true))). % 37.69/25.83 tff(c_27800, plain, (![D_535]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_535), true, icext(D_535, uri_rdf__1), true)=true))). % 37.69/25.83 tff(c_3148, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_103), true, iext(Q_103, uri_rdf_object, uri_rdf_Property), true)=true))). % 37.69/25.83 tff(c_2618, plain, (![E_100]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Container, E_100), true, iext(uri_rdfs_subClassOf, uri_rdfs_Seq, E_100), true)=true))). % 37.69/25.83 tff(c_2620, plain, (![E_100]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, E_100), true, iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, E_100), true)=true))). % 37.69/25.83 tff(c_3170, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_103), true, iext(Q_103, uri_rdf__2, uri_rdfs_Resource), true)=true))). % 37.69/25.83 tff(c_3164, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_103), true, iext(Q_103, uri_rdf_Property, uri_rdfs_Class), true)=true))). % 37.69/25.83 tff(c_3138, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_103), true, iext(Q_103, uri_rdfs_Datatype, uri_rdfs_Class), true)=true))). % 37.69/25.83 tff(c_3125, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_103), true, iext(Q_103, uri_rdf_predicate, uri_rdfs_Resource), true)=true))). % 37.69/25.83 tff(c_3121, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_103), true, iext(Q_103, uri_rdfs_domain, uri_rdfs_Class), true)=true))). % 37.69/25.83 tff(c_3168, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_103), true, iext(Q_103, uri_rdfs_member, uri_rdfs_Resource), true)=true))). % 37.69/25.83 tff(c_3165, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_103), true, iext(Q_103, uri_rdf_predicate, uri_rdfs_Statement), true)=true))). % 37.69/25.83 tff(c_3203, plain, (![R_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_seeAlso, R_107), true, iext(uri_rdfs_subPropertyOf, uri_rdfs_isDefinedBy, R_107), true)=true))). % 37.69/25.83 tff(c_3158, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_103), true, iext(Q_103, uri_rdf_Bag, uri_rdfs_Container), true)=true))). % 37.69/25.83 tff(c_3172, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_103), true, iext(Q_103, uri_rdfs_subClassOf, uri_rdfs_Class), true)=true))). % 37.69/25.83 tff(c_3173, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_103), true, iext(Q_103, uri_rdf_value, uri_rdfs_Resource), true)=true))). % 37.69/25.83 tff(c_3154, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_owl_hasValue, Q_103), true, iext(Q_103, sK2_testcase_premise_fullish_012_Template_Class_BNODE_r, uri_foaf_Person), true)=true))). % 37.69/25.83 tff(c_3120, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_103), true, iext(Q_103, uri_rdf_first, uri_rdf_List), true)=true))). % 37.69/25.83 tff(c_27425, plain, (![D_517]: (ifeq(iext(uri_rdfs_subClassOf, uri_owl_Class, D_517), true, icext(D_517, uri_foaf_Person), true)=true))). % 37.69/25.83 tff(c_3145, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_103), true, iext(Q_103, uri_rdfs_label, uri_rdfs_Resource), true)=true))). % 37.69/25.83 tff(c_3137, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_first, Q_103), true, iext(Q_103, sK4_testcase_premise_fullish_012_Template_Class_BNODE_l2, uri_owl_FunctionalProperty), true)=true))). % 37.69/25.83 tff(c_3155, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_first, Q_103), true, iext(Q_103, sK3_testcase_premise_fullish_012_Template_Class_BNODE_l1, uri_owl_DatatypeProperty), true)=true))). % 37.69/25.83 tff(c_3113, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_103), true, iext(Q_103, uri_rdf_subject, uri_rdfs_Resource), true)=true))). % 37.69/25.83 tff(c_3136, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_103), true, iext(Q_103, uri_rdfs_subClassOf, uri_rdfs_Class), true)=true))). % 37.69/25.83 tff(c_3146, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_103), true, iext(Q_103, uri_rdf_type, uri_rdfs_Resource), true)=true))). % 37.69/25.83 tff(c_3175, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_103), true, iext(Q_103, sK2_testcase_premise_fullish_012_Template_Class_BNODE_r, uri_owl_Restriction), true)=true))). % 37.69/25.83 tff(c_27219, plain, (![D_508]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, D_508), true, icext(D_508, uri_rdf__2), true)=true))). % 37.69/25.83 tff(c_3133, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_103), true, iext(Q_103, uri_rdf_subject, uri_rdf_Property), true)=true))). % 37.69/25.83 tff(c_3153, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_103), true, iext(Q_103, uri_rdfs_subPropertyOf, uri_rdf_Property), true)=true))). % 37.69/25.83 tff(c_14939, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_label), true)=true))). % 37.69/25.83 tff(c_3159, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_103), true, iext(Q_103, uri_rdfs_label, uri_rdfs_Literal), true)=true))). % 37.69/25.83 tff(c_14938, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_label), true)=true))). % 37.69/25.83 tff(c_15093, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_predicate), true)=true))). % 37.69/25.83 tff(c_15094, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_predicate), true)=true))). % 37.69/25.83 tff(c_26984, plain, (![D_499]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, D_499), true, icext(D_499, uri_rdf__3), true)=true))). % 37.69/25.83 tff(c_15003, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_comment), true)=true))). % 37.69/25.83 tff(c_15004, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_comment), true)=true))). % 37.69/25.83 tff(c_14638, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_member), true)=true))). % 37.69/25.83 tff(c_3108, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_103), true, iext(Q_103, uri_rdf__1, uri_rdf_Property), true)=true))). % 37.69/25.83 tff(c_14288, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdf_List), true)=true))). % 37.69/25.83 tff(c_13985, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_owl_Class), true)=true))). % 37.69/25.83 tff(c_3143, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_103), true, iext(Q_103, uri_rdfs_range, uri_rdfs_Class), true)=true))). % 37.69/25.83 tff(c_13703, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdfs_Resource), true)=true))). % 37.69/25.83 tff(c_13772, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_owl_Restriction), true)=true))). % 37.69/25.83 tff(c_14570, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_owl_Restriction), true)=true))). % 37.69/25.83 tff(c_3135, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_103), true, iext(Q_103, uri_rdf_Alt, uri_rdfs_Container), true)=true))). % 37.69/25.83 tff(c_16977, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_ex_PersonAttribute), true)=true))). % 37.69/25.83 tff(c_14353, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdf_List), true)=true))). % 37.69/25.83 tff(c_26599, plain, (![D_484]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_484), true, icext(D_484, uri_rdf_rest), true)=true))). % 37.69/25.83 tff(c_17504, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdfs_Statement), true)=true))). % 37.69/25.83 tff(c_13984, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_owl_Class), true)=true))). % 37.69/25.83 tff(c_3144, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_103), true, iext(Q_103, uri_rdf__3, uri_rdfs_ContainerMembershipProperty), true)=true))). % 37.69/25.83 tff(c_17229, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdfs_Statement), true)=true))). % 37.69/25.83 tff(c_16887, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_ex_PersonAttribute), true)=true))). % 37.69/25.83 tff(c_26416, plain, (![D_477]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_477), true, icext(D_477, uri_rdf_object), true)=true))). % 37.69/25.83 tff(c_2066, plain, (![C_92]: (ifeq(iext(uri_rdfs_range, uri_ex_name, C_92), true, icext(C_92, literal_plain(dat_str_alice)), true)=true))). % 37.69/25.83 tff(c_3114, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_103), true, iext(Q_103, uri_rdfs_ContainerMembershipProperty, uri_rdf_Property), true)=true))). % 37.69/25.83 tff(c_26287, plain, (![D_473]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, D_473), true, icext(D_473, uri_rdf_XMLLiteral), true)=true))). % 37.69/25.83 tff(c_3151, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_103), true, iext(Q_103, uri_rdf__3, uri_rdfs_Resource), true)=true))). % 37.69/25.83 tff(c_26191, plain, (![D_470]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_470), true, icext(D_470, uri_rdf_subject), true)=true))). % 37.69/25.83 tff(c_3139, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_103), true, iext(Q_103, uri_rdfs_seeAlso, uri_rdfs_Resource), true)=true))). % 37.69/25.83 tff(c_3123, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_103), true, iext(Q_103, uri_rdfs_Seq, uri_rdfs_Container), true)=true))). % 37.69/25.83 tff(c_26063, plain, (![D_466]: (ifeq(iext(uri_rdfs_subClassOf, uri_ex_PersonAttribute, D_466), true, icext(D_466, uri_ex_name), true)=true))). % 37.69/25.83 tff(c_9836, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_object), true)=true))). % 37.69/25.83 tff(c_3130, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_103), true, iext(Q_103, uri_rdfs_seeAlso, uri_rdfs_Resource), true)=true))). % 37.69/25.83 tff(c_5725, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdf_Bag), true)=true))). % 37.69/25.83 tff(c_9348, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf__2), true)=true))). % 37.69/25.83 tff(c_10654, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf__3), true)=true))). % 37.69/25.83 tff(c_3152, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_owl_onProperty, Q_103), true, iext(Q_103, sK2_testcase_premise_fullish_012_Template_Class_BNODE_r, uri_rdfs_domain), true)=true))). % 37.69/25.83 tff(c_8702, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_owl_onProperty), true)=true))). % 37.69/25.83 tff(c_5248, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_seeAlso), true)=true))). % 37.69/25.83 tff(c_11074, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf__1), true)=true))). % 37.69/25.83 tff(c_25352, plain, (![D_453, X_454]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Resource, D_453), true, icext(D_453, X_454), true)=true))). % 37.69/25.83 tff(c_7600, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_type), true)=true))). % 37.69/25.83 tff(c_3107, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_103), true, iext(Q_103, uri_rdf_subject, uri_rdfs_Statement), true)=true))). % 37.69/25.83 tff(c_5416, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_subPropertyOf), true)=true))). % 37.69/25.83 tff(c_25064, plain, (![C_88, X_60]: (ifeq(icext(C_88, X_60), true, true, true)=true))). % 37.69/25.83 tff(c_3110, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_103), true, iext(Q_103, uri_rdf__2, uri_rdf_Property), true)=true))). % 37.69/25.83 tff(c_25016, plain, (![X_443, Y_444]: (ifeq(iext(uri_rdf_subject, X_443, Y_444), true, icext(uri_rdfs_Statement, X_443), true)=true))). % 37.69/25.83 tff(c_8060, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_owl_intersectionOf), true)=true))). % 37.69/25.83 tff(c_7536, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_subject), true)=true))). % 37.69/25.83 tff(c_3149, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_103), true, iext(Q_103, uri_rdfs_isDefinedBy, uri_rdfs_Resource), true)=true))). % 37.69/25.83 tff(c_24602, plain, (![X_436, Y_437]: (ifeq(iext(uri_rdfs_domain, X_436, Y_437), true, icext(uri_rdfs_Class, Y_437), true)=true))). % 37.69/25.83 tff(c_9280, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdfs_Datatype), true)=true))). % 37.69/25.83 tff(c_2622, plain, (![E_100]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Literal, E_100), true, iext(uri_rdfs_subClassOf, uri_rdf_XMLLiteral, E_100), true)=true))). % 37.69/25.83 tff(c_8701, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_owl_onProperty), true)=true))). % 37.69/25.83 tff(c_24149, plain, (![X_429, Y_430]: (ifeq(iext(uri_rdfs_range, X_429, Y_430), true, icext(uri_rdf_Property, X_429), true)=true))). % 37.69/25.83 tff(c_12069, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdf_Alt), true)=true))). % 37.69/25.83 tff(c_12520, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_owl_hasValue), true)=true))). % 37.69/25.83 tff(c_3117, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_103), true, iext(Q_103, uri_rdfs_subPropertyOf, uri_rdf_Property), true)=true))). % 37.69/25.83 tff(c_7535, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_subject), true)=true))). % 37.69/25.83 tff(c_23435, plain, (![X_420, Y_421]: (ifeq(iext(uri_rdfs_subClassOf, X_420, Y_421), true, icext(uri_rdfs_Class, Y_421), true)=true))). % 37.69/25.83 tff(c_5790, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_range), true)=true))). % 37.69/25.83 tff(c_7822, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_first), true)=true))). % 37.69/25.83 tff(c_3127, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_103), true, iext(Q_103, uri_rdf_rest, uri_rdf_Property), true)=true))). % 37.69/25.83 tff(c_9002, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_subClassOf), true)=true))). % 37.69/25.83 tff(c_22938, plain, (![X_412, Y_413]: (ifeq(iext(uri_rdfs_domain, X_412, Y_413), true, icext(uri_rdf_Property, X_412), true)=true))). % 37.69/25.83 tff(c_7823, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_first), true)=true))). % 37.69/25.83 tff(c_2617, plain, (![E_100]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, E_100), true, iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, E_100), true)=true))). % 37.69/25.83 tff(c_9001, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_subClassOf), true)=true))). % 37.69/25.83 tff(c_7994, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdfs_Seq), true)=true))). % 37.69/25.83 tff(c_22745, plain, (![X_404, Y_405]: (ifeq(iext(uri_rdf_first, X_404, Y_405), true, icext(uri_rdf_List, X_404), true)=true))). % 37.69/25.83 tff(c_9507, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdfs_Literal), true)=true))). % 37.69/25.83 tff(c_11436, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf__2), true)=true))). % 37.69/25.83 tff(c_3161, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_103), true, iext(Q_103, uri_rdf__1, uri_rdfs_Resource), true)=true))). % 37.69/25.83 tff(c_6035, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdf_XMLLiteral), true)=true))). % 37.69/25.83 tff(c_11807, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdfs_Class), true)=true))). % 37.69/25.83 tff(c_5969, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_domain), true)=true))). % 37.69/25.83 tff(c_22555, plain, (![X_394, Y_395]: (ifeq(iext(uri_rdf_object, X_394, Y_395), true, icext(uri_rdfs_Statement, X_394), true)=true))). % 37.69/25.83 tff(c_7665, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_rest), true)=true))). % 37.69/25.83 tff(c_8059, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_owl_intersectionOf), true)=true))). % 37.69/25.83 tff(c_10653, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf__3), true)=true))). % 37.69/25.83 tff(c_3142, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_rest, Q_103), true, iext(Q_103, sK1_testcase_premise_fullish_012_Template_Class_BNODE_l3, uri_rdf_nil), true)=true))). % 37.69/25.83 tff(c_9904, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_ex_name), true)=true))). % 37.69/25.83 tff(c_21986, plain, (![X_385, Y_386]: (ifeq(iext(uri_rdfs_subPropertyOf, X_385, Y_386), true, icext(uri_rdf_Property, X_385), true)=true))). % 37.69/25.83 tff(c_2621, plain, (![E_100]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Container, E_100), true, iext(uri_rdfs_subClassOf, uri_rdf_Bag, E_100), true)=true))). % 37.69/25.83 tff(c_9970, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf__1), true)=true))). % 37.69/25.83 tff(c_5417, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_subPropertyOf), true)=true))). % 37.69/25.83 tff(c_21865, plain, (![X_378, Y_379]: (ifeq(iext(uri_rdfs_comment, X_378, Y_379), true, icext(uri_rdfs_Literal, Y_379), true)=true))). % 37.69/25.83 tff(c_8314, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdfs_ContainerMembershipProperty), true)=true))). % 37.69/25.83 tff(c_6900, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_isDefinedBy), true)=true))). % 37.69/25.83 tff(c_9837, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_object), true)=true))). % 37.69/25.83 tff(c_2619, plain, (![E_100]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Container, E_100), true, iext(uri_rdfs_subClassOf, uri_rdf_Alt, E_100), true)=true))). % 37.69/25.83 tff(c_7601, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_type), true)=true))). % 37.69/25.83 tff(c_12412, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_value), true)=true))). % 37.69/25.83 tff(c_21360, plain, (![X_368, Y_369]: (ifeq(iext(uri_rdfs_range, X_368, Y_369), true, icext(uri_rdfs_Class, Y_369), true)=true))). % 37.69/25.83 tff(c_5970, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_domain), true)=true))). % 37.69/25.83 tff(c_9903, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_ex_name), true)=true))). % 37.69/25.83 tff(c_3111, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_103), true, iext(Q_103, uri_rdf_type, uri_rdfs_Class), true)=true))). % 37.69/25.83 tff(c_6119, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdfs_Container), true)=true))). % 37.69/25.83 tff(c_12135, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdfs_Resource), true)=true))). % 37.69/25.83 tff(c_20659, plain, (![X_359, Y_360]: (ifeq(iext(uri_rdf_type, X_359, Y_360), true, icext(uri_rdfs_Class, Y_360), true)=true))). % 37.69/25.84 tff(c_11437, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_member), true)=true))). % 37.69/25.84 tff(c_12413, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_value), true)=true))). % 37.69/25.84 tff(c_5791, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_range), true)=true))). % 37.69/25.84 tff(c_3171, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_103), true, iext(Q_103, uri_rdf__1, uri_rdfs_Resource), true)=true))). % 37.69/25.84 tff(c_7666, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_rest), true)=true))). % 37.69/25.84 tff(c_19764, plain, (![X_349, Y_350]: (ifeq(iext(uri_rdfs_subClassOf, X_349, Y_350), true, icext(uri_rdfs_Class, X_349), true)=true))). % 37.69/25.84 tff(c_3174, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_first, Q_103), true, iext(Q_103, sK1_testcase_premise_fullish_012_Template_Class_BNODE_l3, sK2_testcase_premise_fullish_012_Template_Class_BNODE_r), true)=true))). % 37.69/25.84 tff(c_12521, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_owl_hasValue), true)=true))). % 37.69/25.84 tff(c_11179, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdf_Property), true)=true))). % 37.69/25.84 tff(c_19663, plain, (![X_342, Y_343]: (ifeq(iext(uri_rdf_predicate, X_342, Y_343), true, icext(uri_rdfs_Statement, X_342), true)=true))). % 37.69/25.84 tff(c_5022, plain, (![C_19, X_132]: (ifeq(iext(uri_rdfs_domain, uri_rdf_type, C_19), true, icext(C_19, X_132), true)=true))). % 37.69/25.84 tff(c_5023, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_29), true, icext(C_29, uri_rdfs_Resource), true)=true))). % 37.69/25.84 tff(c_3124, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_103), true, iext(Q_103, uri_rdf_first, uri_rdf_Property), true)=true))). % 37.69/25.84 tff(c_2124, plain, (![C_92]: (ifeq(iext(uri_rdfs_range, uri_rdf_first, C_92), true, icext(C_92, uri_owl_DatatypeProperty), true)=true))). % 37.69/25.84 tff(c_2458, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_96), true, icext(C_96, uri_rdfs_range), true)=true))). % 37.69/25.84 tff(c_2081, plain, (![C_92]: (ifeq(iext(uri_rdfs_range, uri_rdfs_range, C_92), true, icext(C_92, uri_rdf_Property), true)=true))). % 37.69/25.84 tff(c_2118, plain, (![C_92]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_92), true, icext(C_92, uri_rdfs_Datatype), true)=true))). % 37.69/25.84 tff(c_2510, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_96), true, icext(C_96, uri_rdfs_member), true)=true))). % 37.69/25.84 tff(c_18815, plain, (![X_323, Y_324]: (ifeq(iext(uri_rdfs_subPropertyOf, X_323, Y_324), true, icext(uri_rdf_Property, Y_324), true)=true))). % 37.69/25.84 tff(c_2450, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_96), true, icext(C_96, uri_rdfs_ContainerMembershipProperty), true)=true))). % 37.69/25.84 tff(c_2483, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_96), true, icext(C_96, uri_rdfs_label), true)=true))). % 37.69/25.84 tff(c_2468, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdf_rest, C_96), true, icext(C_96, sK4_testcase_premise_fullish_012_Template_Class_BNODE_l2), true)=true))). % 37.69/25.84 tff(c_2515, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_96), true, icext(C_96, uri_rdf__1), true)=true))). % 37.69/25.84 tff(c_2488, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_96), true, icext(C_96, uri_rdfs_isDefinedBy), true)=true))). % 37.69/25.84 tff(c_2472, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_96), true, icext(C_96, uri_rdf_Alt), true)=true))). % 37.69/25.84 tff(c_2107, plain, (![C_92]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_92), true, icext(C_92, uri_rdfs_seeAlso), true)=true))). % 37.69/25.84 tff(c_2457, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_96), true, icext(C_96, uri_rdfs_domain), true)=true))). % 37.69/25.84 tff(c_2447, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_96), true, icext(C_96, uri_rdf_type), true)=true))). % 37.69/25.84 tff(c_2096, plain, (![C_92]: (ifeq(iext(uri_rdfs_range, uri_rdf_rest, C_92), true, icext(C_92, sK1_testcase_premise_fullish_012_Template_Class_BNODE_l3), true)=true))). % 37.69/25.84 tff(c_2134, plain, (![C_92]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_92), true, icext(C_92, uri_rdfs_Class), true)=true))). % 37.69/25.84 tff(c_2500, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_96), true, icext(C_96, uri_rdf__2), true)=true))). % 37.69/25.84 tff(c_2123, plain, (![C_92]: (ifeq(iext(uri_rdfs_range, uri_owl_hasValue, C_92), true, icext(C_92, uri_foaf_Person), true)=true))). % 37.69/25.84 tff(c_2518, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_96), true, icext(C_96, uri_rdf_value), true)=true))). % 37.69/25.84 tff(c_2501, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_96), true, icext(C_96, uri_rdf__1), true)=true))). % 37.69/25.84 tff(c_18141, plain, (![X_300, Y_301]: (ifeq(iext(uri_rdfs_label, X_300, Y_301), true, icext(uri_rdfs_Literal, Y_301), true)=true))). % 37.69/25.84 tff(c_2132, plain, (![C_92]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_92), true, icext(C_92, uri_rdfs_Literal), true)=true))). % 37.69/25.84 tff(c_2449, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_96), true, icext(C_96, uri_rdf_subject), true)=true))). % 37.69/25.84 tff(c_2108, plain, (![C_92]: (ifeq(iext(uri_rdfs_range, uri_rdf_rest, C_92), true, icext(C_92, uri_rdf_nil), true)=true))). % 37.69/25.84 tff(c_2506, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_96), true, icext(C_96, uri_rdf_predicate), true)=true))). % 37.69/25.84 tff(c_2497, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_96), true, icext(C_96, uri_rdf_Bag), true)=true))). % 37.69/25.84 tff(c_2519, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdf_first, C_96), true, icext(C_96, sK1_testcase_premise_fullish_012_Template_Class_BNODE_l3), true)=true))). % 37.69/25.84 tff(c_2479, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdf_rest, C_96), true, icext(C_96, sK1_testcase_premise_fullish_012_Template_Class_BNODE_l3), true)=true))). % 37.69/25.84 tff(c_2439, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_ex_name, C_96), true, icext(C_96, uri_ex_alice), true)=true))). % 37.69/25.84 tff(c_2473, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_96), true, icext(C_96, uri_rdfs_subClassOf), true)=true))). % 37.69/25.84 tff(c_2146, plain, (![C_92]: (ifeq(iext(uri_rdfs_range, uri_rdf_first, C_92), true, icext(C_92, sK2_testcase_premise_fullish_012_Template_Class_BNODE_r), true)=true))). % 37.69/25.84 tff(c_2094, plain, (![C_92]: (ifeq(iext(uri_rdfs_range, uri_rdf_rest, C_92), true, icext(C_92, sK4_testcase_premise_fullish_012_Template_Class_BNODE_l2), true)=true))). % 37.69/25.84 tff(c_2512, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_96), true, icext(C_96, uri_rdfs_isDefinedBy), true)=true))). % 37.69/25.84 tff(c_2083, plain, (![C_92]: (ifeq(iext(uri_rdfs_range, uri_rdfs_domain, C_92), true, icext(C_92, uri_rdf_Property), true)=true))). % 37.69/25.84 tff(c_2465, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdf_rest, C_96), true, icext(C_96, sK3_testcase_premise_fullish_012_Template_Class_BNODE_l1), true)=true))). % 37.69/25.84 tff(c_2102, plain, (![C_92]: (ifeq(iext(uri_rdfs_range, uri_rdf_first, C_92), true, icext(C_92, uri_owl_FunctionalProperty), true)=true))). % 37.69/25.84 tff(c_2084, plain, (![C_92]: (ifeq(iext(uri_rdfs_range, uri_rdfs_domain, C_92), true, icext(C_92, uri_rdf_List), true)=true))). % 37.69/25.84 tff(c_2121, plain, (![C_92]: (ifeq(iext(uri_rdfs_range, uri_owl_onProperty, C_92), true, icext(C_92, uri_rdfs_domain), true)=true))). % 37.69/25.84 tff(c_17537, plain, (![X_274, Y_275]: (ifeq(iext(uri_rdf_rest, X_274, Y_275), true, icext(uri_rdf_List, Y_275), true)=true))). % 37.69/25.84 tff(c_2492, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_96), true, icext(C_96, uri_rdfs_subPropertyOf), true)=true))). % 37.69/25.84 tff(c_2490, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_96), true, icext(C_96, uri_rdf__3), true)=true))). % 37.69/25.84 tff(c_2508, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_96), true, icext(C_96, uri_rdfs_comment), true)=true))). % 37.69/25.84 tff(c_2486, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_96), true, icext(C_96, uri_rdf_first), true)=true))). % 37.69/25.84 tff(c_2099, plain, (![C_92]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_92), true, icext(C_92, uri_rdfs_ContainerMembershipProperty), true)=true))). % 37.69/25.84 tff(c_17505, plain, (![X_33]: (ifeq(icext(uri_rdfs_Statement, X_33), true, icext(uri_rdfs_Statement, X_33), true)=true))). % 37.69/25.84 tff(c_16888, plain, (![X_33]: (ifeq(icext(uri_ex_PersonAttribute, X_33), true, icext(uri_ex_PersonAttribute, X_33), true)=true))). % 37.69/25.84 tff(c_17449, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Statement, uri_rdfs_Statement)=true)). % 37.69/25.84 tff(c_2476, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_96), true, icext(C_96, uri_rdfs_seeAlso), true)=true))). % 37.69/25.84 tff(c_17175, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Statement, uri_rdfs_Resource)=true)). % 37.69/25.84 tff(c_16923, plain, (iext(uri_rdfs_subClassOf, uri_ex_PersonAttribute, uri_rdfs_Resource)=true)). % 37.69/25.84 tff(c_2464, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_96), true, icext(C_96, uri_rdf_object), true)=true))). % 37.69/25.84 tff(c_16832, plain, (iext(uri_rdfs_subClassOf, uri_ex_PersonAttribute, uri_ex_PersonAttribute)=true)). % 37.69/25.84 tff(c_16785, plain, (iext(uri_rdf_type, uri_rdfs_Statement, uri_rdfs_Class)=true)). % 37.69/25.84 tff(c_16738, plain, (iext(uri_rdf_type, uri_ex_PersonAttribute, uri_rdfs_Class)=true)). % 37.69/25.84 tff(c_16437, plain, (ic(uri_rdfs_Statement)=true)). % 37.69/25.84 tff(c_16375, plain, (icext(uri_rdfs_Class, uri_rdfs_Statement)=true)). % 37.69/25.84 tff(c_2135, plain, (![C_92]: (ifeq(iext(uri_rdfs_range, uri_rdfs_domain, C_92), true, icext(C_92, uri_rdfs_Statement), true)=true))). % 37.69/25.84 tff(c_16314, plain, (ic(uri_ex_PersonAttribute)=true)). % 37.69/25.84 tff(c_16244, plain, (icext(uri_rdfs_Class, uri_ex_PersonAttribute)=true)). % 37.69/25.84 tff(c_2074, plain, (![C_92]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_92), true, icext(C_92, uri_ex_PersonAttribute), true)=true))). % 37.69/25.84 tff(c_2475, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_96), true, icext(C_96, uri_rdfs_Datatype), true)=true))). % 37.69/25.84 tff(c_2474, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdf_first, C_96), true, icext(C_96, sK4_testcase_premise_fullish_012_Template_Class_BNODE_l2), true)=true))). % 37.69/25.84 tff(c_2097, plain, (![C_92]: (ifeq(iext(uri_rdfs_range, uri_owl_intersectionOf, C_92), true, icext(C_92, sK3_testcase_premise_fullish_012_Template_Class_BNODE_l1), true)=true))). % 37.69/25.84 tff(c_2443, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_96), true, icext(C_96, uri_rdf_subject), true)=true))). % 37.69/25.84 tff(c_2480, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_96), true, icext(C_96, uri_rdfs_range), true)=true))). % 37.69/25.84 tff(c_2459, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_96), true, icext(C_96, uri_rdfs_Seq), true)=true))). % 37.69/25.84 tff(c_13986, plain, (![X_33]: (ifeq(icext(uri_owl_Class, X_33), true, icext(uri_owl_Class, X_33), true)=true))). % 37.69/25.84 tff(c_14289, plain, (![X_33]: (ifeq(icext(uri_rdf_List, X_33), true, icext(uri_rdf_List, X_33), true)=true))). % 37.69/25.84 tff(c_14571, plain, (![X_33]: (ifeq(icext(uri_owl_Restriction, X_33), true, icext(uri_owl_Restriction, X_33), true)=true))). % 37.69/25.84 tff(c_8248, plain, (![X_33]: (ifeq(icext(uri_rdfs_Literal, X_33), true, icext(uri_rdfs_Literal, X_33), true)=true))). % 37.69/25.84 tff(c_8315, plain, (![X_33]: (ifeq(icext(uri_rdfs_ContainerMembershipProperty, X_33), true, icext(uri_rdfs_ContainerMembershipProperty, X_33), true)=true))). % 37.69/25.84 tff(c_11809, plain, (![X_33]: (ifeq(icext(uri_rdfs_Class, X_33), true, icext(uri_rdfs_Class, X_33), true)=true))). % 37.69/25.84 tff(c_15117, plain, (![X_239, Y_240]: (ifeq(iext(uri_rdf_rest, X_239, Y_240), true, icext(uri_rdf_List, X_239), true)=true))). % 37.69/25.84 tff(c_9281, plain, (![X_33]: (ifeq(icext(uri_rdfs_Datatype, X_33), true, icext(uri_rdfs_Datatype, X_33), true)=true))). % 37.69/25.84 tff(c_6121, plain, (![X_33]: (ifeq(icext(uri_rdfs_Container, X_33), true, icext(uri_rdfs_Container, X_33), true)=true))). % 37.69/25.84 tff(c_7995, plain, (![X_33]: (ifeq(icext(uri_rdfs_Seq, X_33), true, icext(uri_rdfs_Seq, X_33), true)=true))). % 37.69/25.84 tff(c_5726, plain, (![X_33]: (ifeq(icext(uri_rdf_Bag, X_33), true, icext(uri_rdf_Bag, X_33), true)=true))). % 37.69/25.84 tff(c_12346, plain, (![X_33]: (ifeq(icext(uri_rdf_Property, X_33), true, icext(uri_rdf_Property, X_33), true)=true))). % 37.69/25.84 tff(c_6036, plain, (![X_33]: (ifeq(icext(uri_rdf_XMLLiteral, X_33), true, icext(uri_rdf_XMLLiteral, X_33), true)=true))). % 37.69/25.84 tff(c_12070, plain, (![X_33]: (ifeq(icext(uri_rdf_Alt, X_33), true, icext(uri_rdf_Alt, X_33), true)=true))). % 37.69/25.84 tff(c_15507, plain, (iext(uri_rdf_type, sK1_testcase_premise_fullish_012_Template_Class_BNODE_l3, uri_rdf_List)=true)). % 37.69/25.84 tff(c_15435, plain, (iext(uri_rdf_type, sK4_testcase_premise_fullish_012_Template_Class_BNODE_l2, uri_rdf_List)=true)). % 37.69/25.84 tff(c_2504, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_96), true, icext(C_96, uri_rdfs_member), true)=true))). % 37.69/25.84 tff(c_15133, plain, (icext(uri_rdf_List, sK1_testcase_premise_fullish_012_Template_Class_BNODE_l3)=true)). % 37.69/25.84 tff(c_15132, plain, (icext(uri_rdf_List, sK4_testcase_premise_fullish_012_Template_Class_BNODE_l2)=true)). % 37.69/25.84 tff(c_15039, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_predicate, uri_rdf_predicate)=true)). % 37.69/25.84 tff(c_2456, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_96), true, icext(C_96, uri_rdf_first), true)=true))). % 37.69/25.84 tff(c_14949, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_comment, uri_rdfs_comment)=true)). % 37.69/25.84 tff(c_14884, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_label, uri_rdfs_label)=true)). % 37.69/25.84 tff(c_14704, plain, (icext(uri_rdf_Property, uri_rdfs_member)=true)). % 37.69/25.84 tff(c_2469, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_owl_intersectionOf, C_96), true, icext(C_96, uri_ex_PersonAttribute), true)=true))). % 37.69/25.84 tff(c_14650, plain, (iext(uri_rdf_type, uri_rdfs_member, uri_rdf_Property)=true)). % 37.69/25.84 tff(c_14581, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_member, uri_rdfs_member)=true)). % 37.69/25.84 tff(c_14514, plain, (iext(uri_rdfs_subClassOf, uri_owl_Restriction, uri_owl_Restriction)=true)). % 37.69/25.84 tff(c_14299, plain, (iext(uri_rdfs_subClassOf, uri_rdf_List, uri_rdfs_Resource)=true)). % 37.69/25.84 tff(c_14233, plain, (iext(uri_rdfs_subClassOf, uri_rdf_List, uri_rdf_List)=true)). % 37.69/25.84 tff(c_13996, plain, (iext(uri_rdfs_subClassOf, uri_owl_Class, uri_rdfs_Resource)=true)). % 37.69/25.84 tff(c_13930, plain, (iext(uri_rdfs_subClassOf, uri_owl_Class, uri_owl_Class)=true)). % 37.69/25.84 tff(c_13717, plain, (iext(uri_rdfs_subClassOf, uri_owl_Restriction, uri_rdfs_Resource)=true)). % 37.69/25.84 tff(c_13646, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Resource, uri_rdfs_Resource)=true)). % 37.69/25.84 tff(c_13599, plain, (iext(uri_rdf_type, uri_rdf_Bag, uri_rdfs_Class)=true)). % 37.69/25.84 tff(c_2441, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_96), true, icext(C_96, uri_rdf__3), true)=true))). % 37.69/25.84 tff(c_13522, plain, (iext(uri_rdf_type, uri_rdf_XMLLiteral, uri_rdfs_Class)=true)). % 37.69/25.84 tff(c_13475, plain, (iext(uri_rdf_type, uri_rdfs_Literal, uri_rdfs_Class)=true)). % 37.69/25.84 tff(c_13428, plain, (iext(uri_rdf_type, uri_rdfs_Seq, uri_rdfs_Class)=true)). % 37.69/25.84 tff(c_2513, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_96), true, icext(C_96, uri_rdf__2), true)=true))). % 37.69/25.84 tff(c_13352, plain, (iext(uri_rdf_type, uri_rdfs_Container, uri_rdfs_Class)=true)). % 37.69/25.84 tff(c_13302, plain, (iext(uri_rdf_type, uri_rdf_Alt, uri_rdfs_Class)=true)). % 37.69/25.84 tff(c_13254, plain, (iext(uri_rdf_type, uri_rdfs_Class, uri_rdfs_Class)=true)). % 37.69/25.84 tff(c_13206, plain, (iext(uri_rdf_type, uri_rdfs_ContainerMembershipProperty, uri_rdfs_Class)=true)). % 37.69/25.84 tff(c_13134, plain, (iext(uri_rdf_type, uri_rdfs_Datatype, uri_rdfs_Class)=true)). % 37.69/25.84 tff(c_2485, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_96), true, icext(C_96, uri_rdf_type), true)=true))). % 37.69/25.84 tff(c_13089, plain, (ip(uri_rdfs_label)=true)). % 37.69/25.84 tff(c_2455, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_96), true, icext(C_96, uri_rdfs_domain), true)=true))). % 37.69/25.84 tff(c_13007, plain, (iext(uri_rdf_type, uri_rdfs_label, uri_rdf_Property)=true)). % 37.69/25.84 tff(c_12960, plain, (iext(uri_rdf_type, sK3_testcase_premise_fullish_012_Template_Class_BNODE_l1, uri_rdf_List)=true)). % 37.69/25.84 tff(c_12913, plain, (iext(uri_rdf_type, uri_owl_Class, uri_rdfs_Class)=true)). % 37.69/25.84 tff(c_12865, plain, (iext(uri_rdf_type, uri_rdf_List, uri_rdfs_Class)=true)). % 37.69/25.84 tff(c_12818, plain, (iext(uri_rdf_type, uri_owl_Restriction, uri_rdfs_Class)=true)). % 37.69/25.84 tff(c_12745, plain, (iext(uri_rdf_type, uri_rdfs_Resource, uri_rdfs_Class)=true)). % 37.69/25.84 tff(c_2516, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_96), true, icext(C_96, uri_rdfs_subClassOf), true)=true))). % 37.69/25.84 tff(c_12703, plain, (ip(uri_rdfs_comment)=true)). % 37.69/25.84 tff(c_12650, plain, (iext(uri_rdf_type, uri_rdfs_comment, uri_rdf_Property)=true)). % 37.69/25.84 tff(c_12584, plain, (ip(uri_rdf_predicate)=true)). % 37.69/25.84 tff(c_12531, plain, (iext(uri_rdf_type, uri_rdf_predicate, uri_rdf_Property)=true)). % 37.69/25.84 tff(c_12465, plain, (iext(uri_rdfs_subPropertyOf, uri_owl_hasValue, uri_owl_hasValue)=true)). % 37.69/25.84 tff(c_1500, plain, (![S_5, O_6]: (ifeq(iext(uri_owl_onProperty, S_5, O_6), true, true, true)=true))). % 37.69/25.84 tff(c_2144, plain, (![C_92]: (ifeq(iext(uri_rdfs_range, uri_rdfs_domain, C_92), true, icext(C_92, uri_rdfs_Class), true)=true))). % 37.69/25.84 tff(c_12358, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_value, uri_rdf_value)=true)). % 37.69/25.84 tff(c_12290, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Property, uri_rdf_Property)=true)). % 37.69/25.84 tff(c_12080, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Container, uri_rdfs_Resource)=true)). % 37.69/25.84 tff(c_12014, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Alt, uri_rdf_Alt)=true)). % 37.69/25.84 tff(c_11873, plain, (icext(uri_rdf_Property, uri_ex_name)=true)). % 37.69/25.84 tff(c_11819, plain, (iext(uri_rdf_type, uri_ex_name, uri_rdf_Property)=true)). % 37.69/25.84 tff(c_11753, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Class, uri_rdfs_Class)=true)). % 37.69/25.84 tff(c_2502, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_96), true, icext(C_96, uri_rdf_XMLLiteral), true)=true))). % 37.69/25.84 tff(c_1142, plain, (![S_5, O_6]: (ifeq(iext(uri_rdfs_domain, S_5, O_6), true, true, true)=true))). % 37.69/25.84 tff(c_11525, plain, (ic(uri_owl_Class)=true)). % 37.69/25.84 tff(c_11467, plain, (icext(uri_rdfs_Class, uri_owl_Class)=true)). % 37.69/25.84 tff(c_2082, plain, (![C_92]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_92), true, icext(C_92, uri_owl_Class), true)=true))). % 37.69/25.84 tff(c_11382, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf__2, uri_rdfs_member)=true)). % 37.69/25.84 tff(c_11125, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Property, uri_rdfs_Resource)=true)). % 37.69/25.84 tff(c_2077, plain, (![C_92]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_92), true, icext(C_92, uri_rdf_Property), true)=true))). % 37.69/25.84 tff(c_3470, plain, (![S_5, O_6]: (ifeq(iext(uri_owl_hasValue, S_5, O_6), true, true, true)=true))). % 37.69/25.84 tff(c_11020, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf__1, uri_rdfs_member)=true)). % 37.69/25.84 tff(c_2100, plain, (![C_92]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_92), true, icext(C_92, uri_rdfs_Container), true)=true))). % 37.69/25.84 tff(c_10873, plain, (icext(uri_rdf_Property, uri_owl_intersectionOf)=true)). % 37.69/25.84 tff(c_10746, plain, (icext(uri_rdf_Property, uri_rdfs_label)=true)). % 37.69/25.84 tff(c_2498, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_96), true, icext(C_96, uri_rdfs_label), true)=true))). % 37.69/25.84 tff(c_10673, plain, (iext(uri_rdf_type, uri_owl_intersectionOf, uri_rdf_Property)=true)). % 37.69/25.84 tff(c_3314, plain, (![S_5, O_6]: (ifeq(iext(uri_rdf_object, S_5, O_6), true, true, true)=true))). % 37.69/25.84 tff(c_10599, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf__3, uri_rdf__3)=true)). % 37.69/25.84 tff(c_2478, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_96), true, icext(C_96, uri_rdfs_isDefinedBy), true)=true))). % 37.69/25.84 tff(c_10378, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, uri_rdfs_Resource)=true)). % 37.69/25.84 tff(c_10201, plain, (iext(uri_rdfs_subClassOf, uri_rdf_XMLLiteral, uri_rdfs_Resource)=true)). % 37.69/25.84 tff(c_2139, plain, (![C_92]: (ifeq(iext(uri_rdfs_range, uri_rdfs_range, C_92), true, icext(C_92, uri_rdfs_Resource), true)=true))). % 37.69/25.84 tff(c_9999, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Alt, uri_rdfs_Resource)=true)). % 37.69/25.84 tff(c_1171, plain, (![S_5, O_6]: (ifeq(iext(uri_rdf_rest, S_5, O_6), true, true, true)=true))). % 37.69/25.84 tff(c_9914, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf__1, uri_rdf__1)=true)). % 37.69/25.84 tff(c_9849, plain, (iext(uri_rdfs_subPropertyOf, uri_ex_name, uri_ex_name)=true)). % 37.69/25.84 tff(c_9782, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_object, uri_rdf_object)=true)). % 37.69/25.84 tff(c_9453, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Literal, uri_rdfs_Resource)=true)). % 37.69/25.84 tff(c_9387, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Class, uri_rdfs_Resource)=true)). % 37.69/25.84 tff(c_9293, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf__2, uri_rdf__2)=true)). % 37.69/25.84 tff(c_9225, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, uri_rdfs_Datatype)=true)). % 37.69/25.84 tff(c_2071, plain, (![C_92]: (ifeq(iext(uri_rdfs_range, uri_rdfs_range, C_92), true, icext(C_92, uri_rdf_List), true)=true))). % 37.69/25.84 tff(c_9158, plain, (ip(uri_rdfs_member)=true)). % 37.69/25.84 tff(c_9094, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf__3, uri_rdfs_member)=true)). % 37.69/25.84 tff(c_2493, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_owl_hasValue, C_96), true, icext(C_96, sK2_testcase_premise_fullish_012_Template_Class_BNODE_r), true)=true))). % 37.69/25.84 tff(c_9012, plain, (iext(uri_rdf_type, uri_rdfs_seeAlso, uri_rdf_Property)=true)). % 37.69/25.84 tff(c_8922, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, uri_rdfs_subClassOf)=true)). % 37.69/25.84 tff(c_2115, plain, (![C_92]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_92), true, icext(C_92, uri_rdf_Property), true)=true))). % 37.69/25.84 tff(c_8843, plain, (ic(uri_rdf_List)=true)). % 37.69/25.84 tff(c_8788, plain, (icext(uri_rdfs_Class, uri_rdf_List)=true)). % 37.69/25.84 tff(c_2137, plain, (![C_92]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_92), true, icext(C_92, uri_rdf_List), true)=true))). % 37.69/25.84 tff(c_8712, plain, (iext(uri_rdf_type, uri_rdfs_subPropertyOf, uri_rdf_Property)=true)). % 37.69/25.84 tff(c_8647, plain, (iext(uri_rdfs_subPropertyOf, uri_owl_onProperty, uri_owl_onProperty)=true)). % 37.69/25.84 tff(c_2477, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_96), true, icext(C_96, uri_rdf_rest), true)=true))). % 37.69/25.84 tff(c_3506, plain, (![S_5, O_6]: (ifeq(iext(uri_owl_intersectionOf, S_5, O_6), true, true, true)=true))). % 37.69/25.85 tff(c_8483, plain, (icext(uri_rdf_Property, uri_rdfs_subPropertyOf)=true)). % 37.69/25.85 tff(c_2453, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_96), true, icext(C_96, uri_rdfs_subPropertyOf), true)=true))). % 37.69/25.85 tff(c_8420, plain, (icext(uri_rdf_Property, uri_rdfs_subClassOf)=true)). % 37.69/25.85 tff(c_8363, plain, (iext(uri_rdf_type, uri_rdfs_subClassOf, uri_rdf_Property)=true)). % 37.69/25.85 tff(c_2125, plain, (![C_92]: (ifeq(iext(uri_rdfs_range, uri_rdfs_range, C_92), true, icext(C_92, uri_rdfs_Literal), true)=true))). % 37.69/25.85 tff(c_1535, plain, (![S_5, O_6]: (ifeq(iext(uri_ex_name, S_5, O_6), true, true, true)=true))). % 37.69/25.85 tff(c_8259, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, uri_rdfs_ContainerMembershipProperty)=true)). % 37.69/25.85 tff(c_8189, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Literal, uri_rdfs_Literal)=true)). % 37.69/25.85 tff(c_8096, plain, (icext(uri_rdf_Property, uri_rdfs_comment)=true)). % 37.69/25.85 tff(c_2495, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_96), true, icext(C_96, uri_rdfs_comment), true)=true))). % 37.69/25.85 tff(c_8005, plain, (iext(uri_rdfs_subPropertyOf, uri_owl_intersectionOf, uri_owl_intersectionOf)=true)). % 37.69/25.85 tff(c_7939, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Seq, uri_rdfs_Seq)=true)). % 37.69/25.85 tff(c_2085, plain, (![C_92]: (ifeq(iext(uri_rdfs_range, uri_rdfs_range, C_92), true, icext(C_92, uri_rdfs_Class), true)=true))). % 37.69/25.85 tff(c_7768, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_first, uri_rdf_first)=true)). % 37.69/25.85 tff(c_7702, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Seq, uri_rdfs_Resource)=true)). % 37.69/25.85 tff(c_7611, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_rest, uri_rdf_rest)=true)). % 37.69/25.85 tff(c_7546, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_type, uri_rdf_type)=true)). % 37.69/25.85 tff(c_7456, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_subject, uri_rdf_subject)=true)). % 37.69/25.85 tff(c_2445, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_96), true, icext(C_96, uri_rdf_rest), true)=true))). % 37.69/25.85 tff(c_7380, plain, (icext(uri_rdf_Property, uri_owl_onProperty)=true)). % 37.69/25.85 tff(c_2103, plain, (![C_92]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_92), true, icext(C_92, uri_rdfs_Class), true)=true))). % 37.69/25.85 tff(c_7298, plain, (iext(uri_rdf_type, uri_owl_onProperty, uri_rdf_Property)=true)). % 37.69/25.85 tff(c_7161, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Bag, uri_rdfs_Resource)=true)). % 37.69/25.85 tff(c_7086, plain, (icext(uri_rdf_Property, uri_owl_hasValue)=true)). % 37.69/25.85 tff(c_7019, plain, (icext(uri_rdf_List, sK3_testcase_premise_fullish_012_Template_Class_BNODE_l1)=true)). % 37.69/25.85 tff(c_2494, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdf_first, C_96), true, icext(C_96, sK3_testcase_premise_fullish_012_Template_Class_BNODE_l1), true)=true))). % 37.69/25.85 tff(c_6947, plain, (iext(uri_rdf_type, uri_owl_hasValue, uri_rdf_Property)=true)). % 37.69/25.85 tff(c_6845, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_isDefinedBy, uri_rdfs_isDefinedBy)=true)). % 37.69/25.85 tff(c_6693, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, uri_rdfs_Resource)=true)). % 37.69/25.85 tff(c_2491, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_owl_onProperty, C_96), true, icext(C_96, sK2_testcase_premise_fullish_012_Template_Class_BNODE_r), true)=true))). % 37.69/25.85 tff(c_6627, plain, (icext(uri_rdf_Property, uri_rdf_predicate)=true)). % 37.69/25.85 tff(c_2461, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_96), true, icext(C_96, uri_rdf_predicate), true)=true))). % 37.69/25.85 tff(c_6544, plain, (icext(uri_rdf_Property, uri_rdfs_isDefinedBy)=true)). % 37.69/25.85 tff(c_6440, plain, (ic(uri_owl_Restriction)=true)). % 37.69/25.85 tff(c_6386, plain, (icext(uri_rdfs_Class, uri_owl_Restriction)=true)). % 37.69/25.85 tff(c_2147, plain, (![C_92]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_92), true, icext(C_92, uri_owl_Restriction), true)=true))). % 37.69/25.85 tff(c_6325, plain, (ic(uri_rdfs_Resource)=true)). % 37.69/25.85 tff(c_6271, plain, (icext(uri_rdfs_Class, uri_rdfs_Resource)=true)). % 37.69/25.85 tff(c_6198, plain, (iext(uri_rdf_type, uri_rdfs_isDefinedBy, uri_rdf_Property)=true)). % 37.69/25.85 tff(c_2140, plain, (![C_92]: (ifeq(iext(uri_rdfs_range, uri_rdfs_domain, C_92), true, icext(C_92, uri_rdfs_Resource), true)=true))). % 37.69/25.85 tff(c_6131, plain, (icext(uri_rdf_Property, uri_rdfs_seeAlso)=true)). % 37.69/25.85 tff(c_6046, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Container, uri_rdfs_Container)=true)). % 37.69/25.85 tff(c_2467, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_96), true, icext(C_96, uri_rdfs_seeAlso), true)=true))). % 37.69/25.85 tff(c_5980, plain, (iext(uri_rdfs_subClassOf, uri_rdf_XMLLiteral, uri_rdf_XMLLiteral)=true)). % 37.69/25.85 tff(c_5915, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, uri_rdfs_domain)=true)). % 37.69/25.85 tff(c_2451, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_96), true, icext(C_96, uri_rdf_value), true)=true))). % 37.69/25.85 tff(c_1770, plain, (![X_89]: (ifeq(icext(uri_rdfs_ContainerMembershipProperty, X_89), true, icext(uri_rdf_Property, X_89), true)=true))). % 37.69/25.85 tff(c_5736, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_range, uri_rdfs_range)=true)). % 37.69/25.85 tff(c_5670, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Bag, uri_rdf_Bag)=true)). % 37.69/25.85 tff(c_1323, plain, (![S_5, O_6]: (ifeq(iext(uri_rdfs_range, S_5, O_6), true, true, true)=true))). % 37.69/25.85 tff(c_1772, plain, (![X_89]: (ifeq(icext(uri_rdf_Alt, X_89), true, icext(uri_rdfs_Container, X_89), true)=true))). % 37.69/25.85 tff(c_5546, plain, (icext(uri_rdf_Property, uri_rdfs_range)=true)). % 37.69/25.85 tff(c_5489, plain, (iext(uri_rdf_type, uri_rdfs_range, uri_rdf_Property)=true)). % 37.69/25.85 tff(c_1691, plain, (![S_5, O_6]: (ifeq(iext(uri_rdfs_subClassOf, S_5, O_6), true, true, true)=true))). % 37.69/25.85 tff(c_1771, plain, (![X_89]: (ifeq(icext(uri_rdfs_Seq, X_89), true, icext(uri_rdfs_Container, X_89), true)=true))). % 37.69/25.85 tff(c_5362, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf)=true)). % 37.69/25.85 tff(c_5323, plain, (icext(uri_rdf_Property, uri_rdfs_domain)=true)). % 37.69/25.85 tff(c_1775, plain, (![X_89]: (ifeq(icext(uri_rdf_XMLLiteral, X_89), true, icext(uri_rdfs_Literal, X_89), true)=true))). % 37.69/25.85 tff(c_5259, plain, (iext(uri_rdf_type, uri_rdfs_domain, uri_rdf_Property)=true)). % 37.69/25.85 tff(c_5194, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_seeAlso, uri_rdfs_seeAlso)=true)). % 37.69/25.85 tff(c_1774, plain, (![X_89]: (ifeq(icext(uri_rdf_Bag, X_89), true, icext(uri_rdfs_Container, X_89), true)=true))). % 37.69/25.85 tff(c_1773, plain, (![X_89]: (ifeq(icext(uri_rdfs_Datatype, X_89), true, icext(uri_rdfs_Class, X_89), true)=true))). % 37.69/25.85 tff(c_2545, plain, (![S_5, O_6]: (ifeq(iext(uri_rdfs_subPropertyOf, S_5, O_6), true, true, true)=true))). % 37.69/25.85 tff(c_2119, plain, (![X_93, Y_94]: (ifeq(iext(uri_rdf__3, X_93, Y_94), true, true, true)=true))). % 37.69/25.85 tff(c_2075, plain, (![X_93, Y_94]: (ifeq(iext(uri_rdf_subject, X_93, Y_94), true, true, true)=true))). % 37.69/25.85 tff(c_2507, plain, (![X_97, Y_98]: (ifeq(iext(uri_rdfs_comment, X_97, Y_98), true, true, true)=true))). % 37.69/25.85 tff(c_4981, plain, (![X_131]: (iext(uri_rdf_type, X_131, uri_rdfs_Resource)=true))). % 37.69/25.85 tff(c_2116, plain, (![X_93, Y_94]: (ifeq(iext(uri_rdfs_isDefinedBy, X_93, Y_94), true, true, true)=true))). % 37.69/25.85 tff(c_2113, plain, (![X_93, Y_94]: (ifeq(iext(uri_rdf_first, X_93, Y_94), true, true, true)=true))). % 37.69/25.85 tff(c_2514, plain, (![X_97, Y_98]: (ifeq(iext(uri_rdf__1, X_97, Y_98), true, true, true)=true))). % 37.69/25.85 tff(c_2104, plain, (![X_93, Y_94]: (ifeq(iext(uri_rdfs_seeAlso, X_93, Y_94), true, true, true)=true))). % 37.69/25.85 tff(c_2484, plain, (![X_97, Y_98]: (ifeq(iext(uri_rdf_type, X_97, Y_98), true, true, true)=true))). % 37.69/25.85 tff(c_2503, plain, (![X_97, Y_98]: (ifeq(iext(uri_rdfs_member, X_97, Y_98), true, true, true)=true))). % 37.69/25.85 tff(c_4799, plain, (icext(uri_rdfs_Class, uri_rdfs_Literal)=true)). % 37.69/25.85 tff(c_2089, plain, (![X_93, Y_94]: (ifeq(iext(uri_rdf_predicate, X_93, Y_94), true, true, true)=true))). % 37.69/25.85 tff(c_4754, plain, (icext(uri_rdfs_Class, uri_rdfs_Seq)=true)). % 37.69/25.85 tff(c_4696, plain, (icext(uri_rdfs_Class, uri_rdfs_Datatype)=true)). % 37.69/25.85 tff(c_2499, plain, (![X_97, Y_98]: (ifeq(iext(uri_rdf__2, X_97, Y_98), true, true, true)=true))). % 37.69/25.85 tff(c_4647, plain, (icext(uri_rdfs_Class, uri_rdf_Alt)=true)). % 37.69/25.85 tff(c_4595, plain, (icext(uri_rdfs_Class, uri_rdfs_ContainerMembershipProperty)=true)). % 37.69/25.85 tff(c_2078, plain, (![X_93, Y_94]: (ifeq(iext(uri_rdf_value, X_93, Y_94), true, true, true)=true))). % 37.69/25.85 tff(c_4551, plain, (icext(uri_rdfs_Class, uri_rdf_Bag)=true)). % 37.69/25.85 tff(c_4507, plain, (icext(uri_rdfs_Class, uri_rdfs_Container)=true)). % 37.69/25.85 tff(c_2482, plain, (![X_97, Y_98]: (ifeq(iext(uri_rdfs_label, X_97, Y_98), true, true, true)=true))). % 37.69/25.85 tff(c_4457, plain, (icext(uri_rdfs_Class, uri_rdf_XMLLiteral)=true)). % 37.69/25.85 tff(c_4410, plain, (icext(uri_rdfs_Class, uri_rdfs_Class)=true)). % 37.69/25.85 tff(c_4365, plain, (icext(uri_rdf_Property, uri_rdf_object)=true)). % 37.69/25.85 tff(c_4318, plain, (icext(uri_rdfs_ContainerMembershipProperty, uri_rdf__2)=true)). % 37.69/25.85 tff(c_4277, plain, (icext(uri_rdf_Property, uri_rdf__3)=true)). % 37.69/25.85 tff(c_4237, plain, (icext(uri_owl_Restriction, sK2_testcase_premise_fullish_012_Template_Class_BNODE_r)=true)). % 37.69/25.85 tff(c_4196, plain, (icext(uri_rdf_Property, uri_rdf_subject)=true)). % 37.69/25.85 tff(c_4153, plain, (icext(uri_rdfs_Datatype, uri_rdf_XMLLiteral)=true)). % 37.69/25.85 tff(c_4083, plain, (icext(uri_rdfs_ContainerMembershipProperty, uri_rdf__3)=true)). % 37.69/25.85 tff(c_4073, plain, (icext(uri_ex_PersonAttribute, uri_ex_name)=true)). % 37.69/25.85 tff(c_4034, plain, (icext(uri_rdf_Property, uri_rdf_value)=true)). % 37.69/25.85 tff(c_3991, plain, (icext(uri_rdf_Property, uri_rdf__2)=true)). % 37.69/25.85 tff(c_3946, plain, (icext(uri_rdfs_Class, uri_rdf_Property)=true)). % 37.69/25.85 tff(c_3906, plain, (icext(uri_rdfs_ContainerMembershipProperty, uri_rdf__1)=true)). % 37.69/25.85 tff(c_3867, plain, (icext(uri_rdf_Property, uri_rdf__1)=true)). % 37.69/25.85 tff(c_3826, plain, (icext(uri_owl_Class, uri_foaf_Person)=true)). % 37.69/25.85 tff(c_3760, plain, (icext(uri_rdf_Property, uri_rdf_first)=true)). % 37.69/25.85 tff(c_3750, plain, (icext(uri_rdf_Property, uri_rdf_rest)=true)). % 37.69/25.85 tff(c_3709, plain, (icext(uri_rdf_Property, uri_rdf_type)=true)). % 37.69/25.85 tff(c_3668, plain, (icext(uri_rdf_List, uri_rdf_nil)=true)). % 37.69/25.85 tff(c_3612, plain, (ip(uri_rdf__3)=true)). % 37.69/25.85 tff(c_3568, plain, (ic(uri_rdf_Alt)=true)). % 37.69/25.85 tff(c_3526, plain, (ip(uri_rdf_subject)=true)). % 37.69/25.85 tff(c_3485, plain, (ip(uri_owl_intersectionOf)=true)). % 37.69/25.85 tff(c_3449, plain, (ip(uri_owl_hasValue)=true)). % 37.69/25.85 tff(c_3408, plain, (ip(uri_rdf__1)=true)). % 37.69/25.85 tff(c_3368, plain, (ip(uri_rdfs_seeAlso)=true)). % 37.69/25.85 tff(c_3333, plain, (ic(uri_rdfs_ContainerMembershipProperty)=true)). % 37.69/25.85 tff(c_3293, plain, (ip(uri_rdf_object)=true)). % 37.69/25.85 tff(c_3257, plain, (ic(uri_rdfs_Seq)=true)). % 37.69/25.85 tff(c_3217, plain, (ic(uri_rdf_Bag)=true)). % 37.69/25.85 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))). % 37.69/25.85 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))). % 37.69/25.85 tff(c_2628, plain, (ip(uri_rdf_first)=true)). % 37.69/25.85 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))). % 37.69/25.85 tff(c_2524, plain, (ip(uri_rdfs_subPropertyOf)=true)). % 37.69/25.85 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))). % 37.69/25.85 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))). % 37.69/25.85 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))). % 37.69/25.85 tff(c_1707, plain, (ip(uri_rdfs_isDefinedBy)=true)). % 37.69/25.85 tff(c_208, plain, (tuple(iext(uri_rdf_type, uri_ex_alice, uri_foaf_Person), iext(uri_rdf_type, uri_ex_name, uri_owl_FunctionalProperty))!=tuple(true, true))). % 37.69/25.85 tff(c_1670, plain, (ip(uri_rdfs_subClassOf)=true)). % 37.69/25.85 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))). % 37.69/25.85 tff(c_1615, plain, (ic(uri_rdfs_Datatype)=true)). % 37.69/25.85 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))). % 37.69/25.85 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))). % 37.69/25.85 tff(c_1514, plain, (ip(uri_ex_name)=true)). % 37.69/25.85 tff(c_1419, plain, (ip(uri_owl_onProperty)=true)). % 37.69/25.85 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))). % 37.69/25.85 tff(c_1337, plain, (ip(uri_rdf__2)=true)). % 37.69/25.85 tff(c_162, plain, (![P_43, Q_44]: (ifeq(iext(uri_rdfs_subPropertyOf, P_43, Q_44), true, ip(Q_44), true)=true))). % 37.69/25.85 tff(c_1305, plain, (ip(uri_rdfs_range)=true)). % 37.69/25.85 tff(c_58, plain, (![C_15]: (ifeq(ic(C_15), true, iext(uri_rdfs_subClassOf, C_15, uri_rdfs_Resource), true)=true))). % 37.69/25.85 tff(c_1241, plain, (ip(uri_rdf_value)=true)). % 37.69/25.85 tff(c_30, plain, (![P_10]: (ifeq(iext(uri_rdf_type, P_10, uri_rdf_Property), true, ip(P_10), true)=true))). % 37.69/25.85 tff(c_1156, plain, (ip(uri_rdf_rest)=true)). % 37.69/25.85 tff(c_1127, plain, (ip(uri_rdfs_domain)=true)). % 37.69/25.85 tff(c_156, plain, (![C_39]: (ifeq(ic(C_39), true, iext(uri_rdfs_subClassOf, C_39, C_39), true)=true))). % 37.69/25.85 tff(c_1073, plain, (ip(uri_rdf_type)=true)). % 37.69/25.85 tff(c_164, plain, (![P_45, Q_46]: (ifeq(iext(uri_rdfs_subPropertyOf, P_45, Q_46), true, ip(P_45), true)=true))). % 37.69/25.85 tff(c_1018, plain, (ic(uri_rdf_XMLLiteral)=true)). % 37.69/25.85 tff(c_4, plain, (![P_4, S_5, O_6]: (ifeq(iext(P_4, S_5, O_6), true, ip(P_4), true)=true))). % 37.69/25.85 tff(c_766, plain, (ic(uri_rdfs_Container)=true)). % 37.69/25.85 tff(c_152, plain, (![C_37, D_38]: (ifeq(iext(uri_rdfs_subClassOf, C_37, D_38), true, ic(C_37), true)=true))). % 37.69/25.85 tff(c_698, plain, (ic(uri_rdfs_Class)=true)). % 37.69/25.85 tff(c_638, plain, (ic(uri_rdfs_Literal)=true)). % 37.69/25.85 tff(c_28, plain, (![P_9]: (ifeq(ip(P_9), true, iext(uri_rdf_type, P_9, uri_rdf_Property), true)=true))). % 37.69/25.85 tff(c_605, plain, (ic(uri_rdf_Property)=true)). % 37.69/25.85 tff(c_170, plain, (![P_51]: (ifeq(ip(P_51), true, iext(uri_rdfs_subPropertyOf, P_51, P_51), true)=true))). % 37.69/25.85 tff(c_150, plain, (![C_35, D_36]: (ifeq(iext(uri_rdfs_subClassOf, C_35, D_36), true, ic(D_36), true)=true))). % 37.69/25.85 tff(c_122, plain, (![X_26]: (ifeq(icext(uri_rdfs_Literal, X_26), true, lv(X_26), true)=true))). % 37.69/25.85 tff(c_114, plain, (![X_22]: (ifeq(ic(X_22), true, icext(uri_rdfs_Class, X_22), true)=true))). % 37.69/25.85 tff(c_116, plain, (![X_23]: (ifeq(icext(uri_rdfs_Class, X_23), true, ic(X_23), true)=true))). % 37.69/25.85 tff(c_124, plain, (![X_27]: (ifeq(lv(X_27), true, icext(uri_rdfs_Literal, X_27), true)=true))). % 37.69/25.85 tff(c_530, plain, (![X_60]: (icext(uri_rdfs_Resource, X_60)=true))). % 37.69/25.85 tff(c_213, plain, (![X_8]: (ifeq(lv(X_8), true, true, true)=true))). % 37.69/25.85 tff(c_200, plain, (iext(uri_ex_name, uri_ex_alice, literal_plain(dat_str_alice))=true)). % 37.69/25.85 tff(c_2, plain, (![A_1, B_2, C_3]: (ifeq(A_1, A_1, B_2, C_3)=B_2))). % 37.69/25.85 tff(c_84, plain, (iext(uri_rdfs_domain, uri_rdf__3, uri_rdfs_Resource)=true)). % 37.69/25.85 tff(c_34, plain, (iext(uri_rdf_type, uri_rdf_type, uri_rdf_Property)=true)). % 37.69/25.85 tff(c_142, plain, (iext(uri_rdfs_domain, uri_rdf_subject, uri_rdfs_Statement)=true)). % 37.69/25.85 tff(c_16, plain, (iext(uri_rdf_type, uri_rdf__1, uri_rdf_Property)=true)). % 37.69/25.85 tff(c_66, plain, (iext(uri_rdfs_range, uri_rdf_rest, uri_rdf_List)=true)). % 37.69/25.85 tff(c_18, plain, (iext(uri_rdf_type, uri_rdf__2, uri_rdf_Property)=true)). % 37.69/25.85 tff(c_176, plain, (iext(uri_rdfs_range, uri_rdf_type, uri_rdfs_Class)=true)). % 37.69/25.85 tff(c_206, plain, (iext(uri_rdf_type, uri_ex_name, uri_ex_PersonAttribute)=true)). % 37.69/25.85 tff(c_144, plain, (iext(uri_rdfs_range, uri_rdf_subject, uri_rdfs_Resource)=true)). % 37.69/25.85 tff(c_74, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, uri_rdf_Property)=true)). % 37.69/25.85 tff(c_180, plain, (iext(uri_rdfs_range, uri_rdf_value, uri_rdfs_Resource)=true)). % 37.69/25.85 tff(c_20, plain, (iext(uri_rdf_type, uri_rdf__3, uri_rdf_Property)=true)). % 37.69/25.85 tff(c_168, plain, (iext(uri_rdfs_range, uri_rdfs_subPropertyOf, uri_rdf_Property)=true)). % 37.69/25.85 tff(c_204, plain, (iext(uri_rdf_type, uri_foaf_Person, uri_owl_Class)=true)). % 37.69/25.85 tff(c_108, plain, (iext(uri_rdfs_domain, uri_rdfs_domain, uri_rdf_Property)=true)). % 37.69/25.85 tff(c_60, plain, (iext(uri_rdfs_domain, uri_rdf_first, uri_rdf_List)=true)). % 37.69/25.85 tff(c_112, plain, (iext(uri_rdfs_range, uri_rdfs_domain, uri_rdfs_Class)=true)). % 37.69/25.85 tff(c_128, plain, (iext(uri_rdfs_domain, uri_rdfs_range, uri_rdf_Property)=true)). % 37.69/25.85 tff(c_98, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Seq, uri_rdfs_Container)=true)). % 37.69/25.85 tff(c_10, plain, (iext(uri_rdf_type, uri_rdf_first, uri_rdf_Property)=true)). % 37.69/25.85 tff(c_140, plain, (iext(uri_rdfs_range, uri_rdf_predicate, uri_rdfs_Resource)=true)). % 37.69/25.85 tff(c_94, plain, (iext(uri_rdf_type, uri_rdf__2, uri_rdfs_ContainerMembershipProperty)=true)). % 37.69/25.85 tff(c_14, plain, (iext(uri_rdf_type, uri_rdf_rest, uri_rdf_Property)=true)). % 37.69/25.85 tff(c_134, plain, (iext(uri_rdfs_domain, uri_rdf_object, uri_rdfs_Statement)=true)). % 37.69/25.85 tff(c_190, plain, (iext(uri_rdf_rest, sK3_testcase_premise_fullish_012_Template_Class_BNODE_l1, sK4_testcase_premise_fullish_012_Template_Class_BNODE_l2)=true)). % 37.69/25.85 tff(c_50, plain, (iext(uri_rdfs_domain, uri_rdfs_seeAlso, uri_rdfs_Resource)=true)). % 37.69/25.85 tff(c_192, plain, (iext(uri_rdf_rest, sK4_testcase_premise_fullish_012_Template_Class_BNODE_l2, sK1_testcase_premise_fullish_012_Template_Class_BNODE_l3)=true)). % 37.69/25.85 tff(c_186, plain, (iext(uri_owl_intersectionOf, uri_ex_PersonAttribute, sK3_testcase_premise_fullish_012_Template_Class_BNODE_l1)=true)). % 37.69/25.85 tff(c_26, plain, (iext(uri_rdf_type, uri_rdf_subject, uri_rdf_Property)=true)). % 37.69/25.85 tff(c_92, plain, (iext(uri_rdf_type, uri_rdf__1, uri_rdfs_ContainerMembershipProperty)=true)). % 37.69/25.85 tff(c_68, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Alt, uri_rdfs_Container)=true)). % 37.69/25.85 tff(c_154, plain, (iext(uri_rdfs_range, uri_rdfs_subClassOf, uri_rdfs_Class)=true)). % 37.69/25.85 tff(c_198, plain, (iext(uri_rdf_first, sK4_testcase_premise_fullish_012_Template_Class_BNODE_l2, uri_owl_FunctionalProperty)=true)). % 37.69/25.85 tff(c_106, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, uri_rdfs_Class)=true)). % 37.69/25.85 tff(c_52, plain, (iext(uri_rdfs_range, uri_rdfs_seeAlso, uri_rdfs_Resource)=true)). % 37.69/25.85 tff(c_64, plain, (iext(uri_rdfs_domain, uri_rdf_rest, uri_rdf_List)=true)). % 37.69/25.85 tff(c_44, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_isDefinedBy, uri_rdfs_seeAlso)=true)). % 37.69/25.85 tff(c_188, plain, (iext(uri_rdf_rest, sK1_testcase_premise_fullish_012_Template_Class_BNODE_l3, uri_rdf_nil)=true)). % 37.69/25.85 tff(c_132, plain, (iext(uri_rdfs_range, uri_rdfs_range, uri_rdfs_Class)=true)). % 37.69/25.85 tff(c_96, plain, (iext(uri_rdf_type, uri_rdf__3, uri_rdfs_ContainerMembershipProperty)=true)). % 37.69/25.85 tff(c_46, plain, (iext(uri_rdfs_domain, uri_rdfs_label, uri_rdfs_Resource)=true)). % 37.69/25.85 tff(c_174, plain, (iext(uri_rdfs_domain, uri_rdf_type, uri_rdfs_Resource)=true)). % 37.69/25.85 tff(c_62, plain, (iext(uri_rdfs_range, uri_rdf_first, uri_rdfs_Resource)=true)). % 37.69/25.85 tff(c_22, plain, (iext(uri_rdf_type, uri_rdf_object, uri_rdf_Property)=true)). % 37.69/25.85 tff(c_42, plain, (iext(uri_rdfs_range, uri_rdfs_isDefinedBy, uri_rdfs_Resource)=true)). % 37.69/25.85 tff(c_102, plain, (iext(uri_rdf_type, uri_rdf_XMLLiteral, uri_rdfs_Datatype)=true)). % 37.69/25.85 tff(c_90, plain, (iext(uri_rdfs_range, uri_rdf__3, uri_rdfs_Resource)=true)). % 37.69/25.85 tff(c_184, plain, (iext(uri_owl_onProperty, sK2_testcase_premise_fullish_012_Template_Class_BNODE_r, uri_rdfs_domain)=true)). % 37.69/25.85 tff(c_160, plain, (iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, uri_rdf_Property)=true)). % 37.69/25.85 tff(c_182, plain, (iext(uri_owl_hasValue, sK2_testcase_premise_fullish_012_Template_Class_BNODE_r, uri_foaf_Person)=true)). % 37.69/25.85 tff(c_196, plain, (iext(uri_rdf_first, sK3_testcase_premise_fullish_012_Template_Class_BNODE_l1, uri_owl_DatatypeProperty)=true)). % 37.69/25.85 tff(c_38, plain, (iext(uri_rdfs_range, uri_rdfs_comment, uri_rdfs_Literal)=true)). % 37.69/25.85 tff(c_24, plain, (iext(uri_rdf_type, uri_rdf_value, uri_rdf_Property)=true)). % 37.69/25.85 tff(c_70, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Bag, uri_rdfs_Container)=true)). % 37.69/25.85 tff(c_48, plain, (iext(uri_rdfs_range, uri_rdfs_label, uri_rdfs_Literal)=true)). % 37.69/25.85 tff(c_82, plain, (iext(uri_rdfs_domain, uri_rdf__2, uri_rdfs_Resource)=true)). % 37.69/25.85 tff(c_86, plain, (iext(uri_rdfs_range, uri_rdf__1, uri_rdfs_Resource)=true)). % 37.69/25.85 tff(c_100, plain, (iext(uri_rdfs_subClassOf, uri_rdf_XMLLiteral, uri_rdfs_Literal)=true)). % 37.69/25.85 tff(c_76, plain, (iext(uri_rdfs_domain, uri_rdfs_member, uri_rdfs_Resource)=true)). % 37.69/25.85 tff(c_126, plain, (iext(uri_rdf_type, uri_rdf_Property, uri_rdfs_Class)=true)). % 37.69/25.85 tff(c_138, plain, (iext(uri_rdfs_domain, uri_rdf_predicate, uri_rdfs_Statement)=true)). % 37.69/25.85 tff(c_36, plain, (iext(uri_rdfs_domain, uri_rdfs_comment, uri_rdfs_Resource)=true)). % 37.69/25.85 tff(c_12, plain, (iext(uri_rdf_type, uri_rdf_nil, uri_rdf_List)=true)). % 37.69/25.85 tff(c_78, plain, (iext(uri_rdfs_range, uri_rdfs_member, uri_rdfs_Resource)=true)). % 37.69/25.85 tff(c_40, plain, (iext(uri_rdfs_domain, uri_rdfs_isDefinedBy, uri_rdfs_Resource)=true)). % 37.69/25.85 tff(c_88, plain, (iext(uri_rdfs_range, uri_rdf__2, uri_rdfs_Resource)=true)). % 37.69/25.85 tff(c_80, plain, (iext(uri_rdfs_domain, uri_rdf__1, uri_rdfs_Resource)=true)). % 37.69/25.85 tff(c_146, plain, (iext(uri_rdfs_domain, uri_rdfs_subClassOf, uri_rdfs_Class)=true)). % 37.69/25.85 tff(c_178, plain, (iext(uri_rdfs_domain, uri_rdf_value, uri_rdfs_Resource)=true)). % 37.69/25.85 tff(c_194, plain, (iext(uri_rdf_first, sK1_testcase_premise_fullish_012_Template_Class_BNODE_l3, sK2_testcase_premise_fullish_012_Template_Class_BNODE_r)=true)). % 37.69/25.85 tff(c_202, plain, (iext(uri_rdf_type, sK2_testcase_premise_fullish_012_Template_Class_BNODE_r, uri_owl_Restriction)=true)). % 37.69/25.85 tff(c_6, plain, (![X_7]: (ir(X_7)=true))). % 37.69/25.85 % SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 37.69/25.85 %------------------------------------------------------------------------------