%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : SWB029-10 : TPTP v9.0.0. Released v7.5.0. % Transfm : none % Format : tptp:raw % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % Computer : n005.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:57 PM UTC 2025 % Result : Satisfiable 34.91s 24.25s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.12/0.12 % Problem : SWB029-10 : TPTP v9.0.0. Released v7.5.0. % 0.12/0.13 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s % 0.12/0.34 % Computer : n005.cluster.edu % 0.12/0.34 % Model : x86_64 x86_64 % 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.34 % Memory : 8042.1875MB % 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.34 % CPULimit : 300 % 0.12/0.34 % WCLimit : 300 % 0.12/0.34 % DateTime : Wed Apr 9 01:03:42 EDT 2025 % 0.12/0.35 % CPUTime : % 34.91/24.25 % 34.91/24.25 % SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 34.91/24.25 % 34.91/24.25 % SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 35.00/24.27 %$ ifeq > iext > icext > #nlpp > lv > ir > ip > ic > uri_rdfs_subPropertyOf > uri_rdfs_subClassOf > uri_rdfs_seeAlso > uri_rdfs_range > uri_rdfs_member > uri_rdfs_label > uri_rdfs_isDefinedBy > uri_rdfs_domain > uri_rdfs_comment > uri_rdfs_Statement > uri_rdfs_Seq > uri_rdfs_Resource > uri_rdfs_Literal > uri_rdfs_Datatype > uri_rdfs_ContainerMembershipProperty > uri_rdfs_Container > uri_rdfs_Class > uri_rdf_value > uri_rdf_type > uri_rdf_subject > uri_rdf_rest > uri_rdf_predicate > uri_rdf_object > uri_rdf_nil > uri_rdf_first > uri_rdf__3 > uri_rdf__2 > uri_rdf__1 > uri_rdf_XMLLiteral > uri_rdf_Property > uri_rdf_List > uri_rdf_Bag > uri_rdf_Alt > uri_owl_intersectionOf > uri_owl_complementOf > uri_owl_Class > uri_ex_w > uri_ex_B > uri_ex_A > true > sK4_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l1 > sK3_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_x > sK2_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l2 > sK1_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_y % 35.00/24.27 % 35.00/24.27 %Foreground sorts: % 35.00/24.27 % 35.00/24.27 % 35.00/24.27 %Background operators: % 35.00/24.27 % 35.00/24.27 % 35.00/24.27 %Foreground operators: % 35.00/24.27 tff(uri_rdfs_Datatype, type, uri_rdfs_Datatype: $i). % 35.00/24.27 tff(uri_owl_complementOf, type, uri_owl_complementOf: $i). % 35.00/24.27 tff(uri_rdfs_ContainerMembershipProperty, type, uri_rdfs_ContainerMembershipProperty: $i). % 35.00/24.27 tff(uri_rdfs_Resource, type, uri_rdfs_Resource: $i). % 35.00/24.27 tff(uri_rdf_Property, type, uri_rdf_Property: $i). % 35.00/24.27 tff(uri_rdf_subject, type, uri_rdf_subject: $i). % 35.00/24.27 tff(uri_ex_A, type, uri_ex_A: $i). % 35.00/24.27 tff(sK2_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l2, type, sK2_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l2: $i). % 35.00/24.27 tff(uri_rdf_type, type, uri_rdf_type: $i). % 35.00/24.27 tff(uri_rdfs_subPropertyOf, type, uri_rdfs_subPropertyOf: $i). % 35.00/24.27 tff(sK4_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l1, type, sK4_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l1: $i). % 35.00/24.27 tff(uri_rdfs_seeAlso, type, uri_rdfs_seeAlso: $i). % 35.00/24.27 tff(icext, type, icext: ($i * $i) > $i). % 35.00/24.27 tff(uri_rdfs_range, type, uri_rdfs_range: $i). % 35.00/24.27 tff(uri_rdf_XMLLiteral, type, uri_rdf_XMLLiteral: $i). % 35.00/24.27 tff(uri_rdf_List, type, uri_rdf_List: $i). % 35.00/24.27 tff(uri_rdf_first, type, uri_rdf_first: $i). % 35.00/24.27 tff(uri_rdf_predicate, type, uri_rdf_predicate: $i). % 35.00/24.27 tff(uri_owl_intersectionOf, type, uri_owl_intersectionOf: $i). % 35.00/24.27 tff(ir, type, ir: $i > $i). % 35.00/24.27 tff(lv, type, lv: $i > $i). % 35.00/24.27 tff(sK1_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_y, type, sK1_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_y: $i). % 35.00/24.27 tff(uri_rdf__3, type, uri_rdf__3: $i). % 35.00/24.27 tff(uri_rdf_value, type, uri_rdf_value: $i). % 35.00/24.27 tff(ic, type, ic: $i > $i). % 35.00/24.27 tff(uri_rdfs_Statement, type, uri_rdfs_Statement: $i). % 35.00/24.27 tff(uri_rdf__1, type, uri_rdf__1: $i). % 35.00/24.27 tff(iext, type, iext: ($i * $i * $i) > $i). % 35.00/24.27 tff(uri_ex_w, type, uri_ex_w: $i). % 35.00/24.27 tff(uri_rdf_rest, type, uri_rdf_rest: $i). % 35.00/24.27 tff(uri_rdfs_label, type, uri_rdfs_label: $i). % 35.00/24.27 tff(sK3_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_x, type, sK3_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_x: $i). % 35.00/24.27 tff(uri_rdfs_Container, type, uri_rdfs_Container: $i). % 35.00/24.27 tff(uri_rdfs_subClassOf, type, uri_rdfs_subClassOf: $i). % 35.00/24.27 tff(uri_rdf_object, type, uri_rdf_object: $i). % 35.00/24.27 tff(ip, type, ip: $i > $i). % 35.00/24.27 tff(uri_rdfs_Class, type, uri_rdfs_Class: $i). % 35.00/24.27 tff(uri_rdfs_Seq, type, uri_rdfs_Seq: $i). % 35.00/24.27 tff(uri_owl_Class, type, uri_owl_Class: $i). % 35.00/24.27 tff(uri_rdfs_member, type, uri_rdfs_member: $i). % 35.00/24.27 tff(uri_rdf_Bag, type, uri_rdf_Bag: $i). % 35.00/24.27 tff(uri_rdf__2, type, uri_rdf__2: $i). % 35.00/24.27 tff(uri_rdfs_comment, type, uri_rdfs_comment: $i). % 35.00/24.27 tff(uri_rdfs_Literal, type, uri_rdfs_Literal: $i). % 35.00/24.27 tff(true, type, true: $i). % 35.00/24.27 tff(uri_rdf_Alt, type, uri_rdf_Alt: $i). % 35.00/24.27 tff(uri_rdf_nil, type, uri_rdf_nil: $i). % 35.00/24.27 tff(uri_ex_B, type, uri_ex_B: $i). % 35.00/24.27 tff(uri_rdfs_isDefinedBy, type, uri_rdfs_isDefinedBy: $i). % 35.00/24.27 tff(uri_rdfs_domain, type, uri_rdfs_domain: $i). % 35.00/24.27 tff(ifeq, type, ifeq: ($i * $i * $i * $i) > $i). % 35.00/24.27 % 35.00/24.27 %Saturated clause set: % 35.00/24.27 tff(c_16018, 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))). % 35.00/24.27 tff(c_16404, 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))). % 35.00/24.27 tff(c_16021, 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))). % 35.00/24.27 tff(c_78326, plain, (![X_1313, Y_1314]: (ifeq(iext(uri_rdfs_comment, X_1313, Y_1314), true, iext(uri_rdfs_comment, X_1313, Y_1314), true)=true))). % 35.00/24.27 tff(c_16342, 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))). % 35.00/24.27 tff(c_16277, 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))). % 35.00/24.28 tff(c_78058, plain, (![X_1307, Y_1308]: (ifeq(iext(uri_rdf_predicate, X_1307, Y_1308), true, iext(uri_rdf_predicate, X_1307, Y_1308), true)=true))). % 35.00/24.28 tff(c_19448, 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))). % 35.00/24.28 tff(c_77911, plain, (![X_1302, Y_1303]: (ifeq(iext(uri_rdfs_label, X_1302, Y_1303), true, iext(uri_rdfs_label, X_1302, Y_1303), true)=true))). % 35.00/24.28 tff(c_5361, 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))). % 35.00/24.28 tff(c_15898, 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))). % 35.00/24.28 tff(c_16199, 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))). % 35.00/24.28 tff(c_5364, 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))). % 35.00/24.28 tff(c_15964, 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))). % 35.00/24.28 tff(c_77115, plain, (![X_1291, Y_1292]: (ifeq(iext(uri_rdfs_member, X_1291, Y_1292), true, iext(uri_rdfs_member, X_1291, Y_1292), true)=true))). % 35.00/24.28 tff(c_17335, 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))). % 35.00/24.28 tff(c_17941, 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))). % 35.00/24.28 tff(c_15741, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subClassOf), true, ifeq(iext(P_47, sK3_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_x, sK3_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_x), true, true, true), true)=true))). % 35.00/24.28 tff(c_15618, 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))). % 35.00/24.28 tff(c_15808, 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))). % 35.00/24.28 tff(c_76270, plain, (![C_1283]: (ifeq(iext(uri_rdfs_subClassOf, C_1283, uri_rdfs_Statement), true, iext(uri_rdfs_subClassOf, C_1283, uri_rdfs_Resource), true)=true))). % 35.00/24.28 tff(c_76193, plain, (![C_1282]: (ifeq(iext(uri_rdfs_subClassOf, C_1282, sK3_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_x), true, iext(uri_rdfs_subClassOf, C_1282, uri_rdfs_Resource), true)=true))). % 35.00/24.28 tff(c_76038, plain, (![C_1280]: (ifeq(iext(uri_rdfs_subClassOf, C_1280, uri_rdf_List), true, iext(uri_rdfs_subClassOf, C_1280, uri_rdfs_Resource), true)=true))). % 35.00/24.28 tff(c_75882, plain, (![C_1278]: (ifeq(iext(uri_rdfs_subClassOf, C_1278, uri_owl_Class), true, iext(uri_rdfs_subClassOf, C_1278, uri_rdfs_Resource), true)=true))). % 35.00/24.28 tff(c_17426, 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))). % 35.00/24.28 tff(c_15493, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subClassOf), true, ifeq(iext(P_47, sK3_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_x, uri_rdfs_Resource), true, true, true), true)=true))). % 35.00/24.28 tff(c_18095, 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))). % 35.00/24.28 tff(c_6922, 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))). % 35.00/24.28 tff(c_12996, 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))). % 35.00/24.28 tff(c_15045, 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))). % 35.00/24.28 tff(c_13896, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdf_Property), true, ifeq(iext(P_18, uri_owl_complementOf, Y_21), true, true, true), true)=true))). % 35.00/24.28 tff(c_14923, 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))). % 35.00/24.28 tff(c_14970, 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))). % 35.00/24.28 tff(c_12993, 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))). % 35.00/24.28 tff(c_13893, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdf_Property), true, ifeq(iext(P_28, X_30, uri_owl_complementOf), true, true, true), true)=true))). % 35.00/24.28 tff(c_15093, 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))). % 35.00/24.28 tff(c_9593, 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))). % 35.00/24.28 tff(c_10932, 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))). % 35.00/24.28 tff(c_9590, 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))). % 35.00/24.28 tff(c_15293, 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))). % 35.00/24.28 tff(c_6460, 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))). % 35.00/24.28 tff(c_10929, 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))). % 35.00/24.28 tff(c_8312, 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))). % 35.00/24.28 tff(c_15340, 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))). % 35.00/24.28 tff(c_6919, 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))). % 35.00/24.28 tff(c_6463, 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))). % 35.00/24.28 tff(c_15220, 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))). % 35.00/24.28 tff(c_8309, 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))). % 35.00/24.28 tff(c_15418, 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))). % 35.00/24.28 tff(c_15171, 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))). % 35.00/24.28 tff(c_19218, 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))). % 35.00/24.28 tff(c_14876, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, sK3_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_x, uri_rdfs_Class), true, true, true), true)=true))). % 35.00/24.28 tff(c_14610, 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))). % 35.00/24.28 tff(c_14657, 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))). % 35.00/24.28 tff(c_14828, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, sK2_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l2, uri_rdf_List), true, true, true), true)=true))). % 35.00/24.28 tff(c_14781, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, sK4_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l1, uri_rdf_List), true, true, true), true)=true))). % 35.00/24.28 tff(c_17893, 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))). % 35.00/24.28 tff(c_17288, 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))). % 35.00/24.28 tff(c_14482, 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))). % 35.00/24.28 tff(c_4418, 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))). % 35.00/24.28 tff(c_4460, 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))). % 35.00/24.28 tff(c_8421, 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))). % 35.00/24.29 tff(c_9536, 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))). % 35.00/24.29 tff(c_70910, plain, (![P_1221]: (ifeq(iext(uri_rdfs_subPropertyOf, P_1221, uri_rdf__1), true, iext(uri_rdfs_subPropertyOf, P_1221, uri_rdfs_member), true)=true))). % 35.00/24.29 tff(c_4601, 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))). % 35.00/24.29 tff(c_6837, 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))). % 35.00/24.29 tff(c_70465, plain, (![C_1214]: (ifeq(iext(uri_rdfs_subClassOf, C_1214, uri_rdfs_Container), true, iext(uri_rdfs_subClassOf, C_1214, uri_rdfs_Resource), true)=true))). % 35.00/24.29 tff(c_70452, plain, (![X_1212, Y_1213]: (ifeq(iext(uri_rdf__2, X_1212, Y_1213), true, iext(uri_rdf__2, X_1212, Y_1213), true)=true))). % 35.00/24.29 tff(c_7861, 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))). % 35.00/24.29 tff(c_70265, plain, (![P_1209]: (ifeq(iext(uri_rdfs_subPropertyOf, P_1209, uri_rdf__2), true, iext(uri_rdfs_subPropertyOf, P_1209, uri_rdfs_member), true)=true))). % 35.00/24.29 tff(c_4654, 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))). % 35.00/24.29 tff(c_69853, plain, (![C_1204]: (ifeq(iext(uri_rdfs_subClassOf, C_1204, uri_rdf_XMLLiteral), true, iext(uri_rdfs_subClassOf, C_1204, uri_rdfs_Resource), true)=true))). % 35.00/24.29 tff(c_11471, 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))). % 35.00/24.29 tff(c_69826, plain, (![X_1200, Y_1201]: (ifeq(iext(uri_rdf__2, X_1200, Y_1201), true, iext(uri_rdfs_member, X_1200, Y_1201), true)=true))). % 35.00/24.29 tff(c_4553, 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))). % 35.00/24.29 tff(c_4556, 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))). % 35.00/24.29 tff(c_69516, plain, (![X_1192, Y_1193]: (ifeq(iext(uri_rdf_value, X_1192, Y_1193), true, iext(uri_rdf_value, X_1192, Y_1193), true)=true))). % 35.00/24.29 tff(c_5977, 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))). % 35.00/24.29 tff(c_69240, plain, (![C_1189]: (ifeq(iext(uri_rdfs_subClassOf, C_1189, uri_rdfs_ContainerMembershipProperty), true, iext(uri_rdfs_subClassOf, C_1189, uri_rdfs_Resource), true)=true))). % 35.00/24.29 tff(c_13814, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, uri_owl_complementOf, uri_rdf_Property), true, true, true), true)=true))). % 35.00/24.29 tff(c_10875, 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))). % 35.00/24.29 tff(c_5413, 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))). % 35.00/24.29 tff(c_4503, 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))). % 35.00/24.29 tff(c_68073, plain, (![X_1180, Y_1181]: (ifeq(iext(uri_rdfs_subPropertyOf, X_1180, Y_1181), true, iext(uri_rdfs_subPropertyOf, X_1180, Y_1181), true)=true))). % 35.00/24.29 tff(c_12939, 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))). % 35.00/24.29 tff(c_5629, 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))). % 35.00/24.29 tff(c_4657, 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))). % 35.00/24.29 tff(c_4322, 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))). % 35.00/24.29 tff(c_67109, plain, (![C_1170]: (ifeq(iext(uri_rdfs_subClassOf, C_1170, uri_rdf_Alt), true, iext(uri_rdfs_subClassOf, C_1170, uri_rdfs_Resource), true)=true))). % 35.00/24.29 tff(c_66426, plain, (![X_1166, Y_1167]: (ifeq(iext(uri_rdfs_subClassOf, X_1166, Y_1167), true, iext(uri_rdfs_subClassOf, X_1166, Y_1167), true)=true))). % 35.00/24.29 tff(c_5918, 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))). % 35.00/24.29 tff(c_66143, plain, (![C_1163]: (ifeq(iext(uri_rdfs_subClassOf, C_1163, uri_rdfs_Literal), true, iext(uri_rdfs_subClassOf, C_1163, uri_rdfs_Resource), true)=true))). % 35.00/24.29 tff(c_11335, 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))). % 35.00/24.29 tff(c_9818, 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))). % 35.00/24.29 tff(c_65876, plain, (![X_1157, Y_1158]: (ifeq(iext(uri_rdf_object, X_1157, Y_1158), true, iext(uri_rdf_object, X_1157, Y_1158), true)=true))). % 35.00/24.29 tff(c_11406, 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))). % 35.00/24.29 tff(c_4371, 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))). % 35.00/24.29 tff(c_7972, 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))). % 35.00/24.29 tff(c_10414, 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))). % 35.00/24.29 tff(c_64915, plain, (![C_1148]: (ifeq(iext(uri_rdfs_subClassOf, C_1148, uri_rdf_Property), true, iext(uri_rdfs_subClassOf, C_1148, uri_rdfs_Resource), true)=true))). % 35.00/24.29 tff(c_64752, plain, (![C_1146]: (ifeq(iext(uri_rdfs_subClassOf, C_1146, uri_rdfs_Class), true, iext(uri_rdfs_subClassOf, C_1146, uri_rdfs_Resource), true)=true))). % 35.00/24.29 tff(c_64597, plain, (![C_1144]: (ifeq(iext(uri_rdfs_subClassOf, C_1144, uri_rdfs_Datatype), true, iext(uri_rdfs_subClassOf, C_1144, uri_rdfs_Resource), true)=true))). % 35.00/24.29 tff(c_13518, 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))). % 35.00/24.29 tff(c_11888, 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))). % 35.00/24.29 tff(c_5140, 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))). % 35.00/24.29 tff(c_4264, 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))). % 35.00/24.29 tff(c_63768, plain, (![X_1135, Y_1136]: (ifeq(iext(uri_rdfs_range, X_1135, Y_1136), true, iext(uri_rdfs_range, X_1135, Y_1136), true)=true))). % 35.00/24.29 tff(c_63741, plain, (![X_1131, Y_1132]: (ifeq(iext(uri_rdf__1, X_1131, Y_1132), true, iext(uri_rdfs_member, X_1131, Y_1132), true)=true))). % 35.00/24.29 tff(c_6644, 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))). % 35.00/24.29 tff(c_8255, 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))). % 35.00/24.29 tff(c_4506, 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))). % 35.00/24.29 tff(c_63033, plain, (![X_1121, Y_1122]: (ifeq(iext(uri_rdf__3, X_1121, Y_1122), true, iext(uri_rdf__3, X_1121, Y_1122), true)=true))). % 35.00/24.29 tff(c_11778, 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))). % 35.00/24.29 tff(c_62250, plain, (![X_1112, Y_1113]: (ifeq(iext(uri_owl_complementOf, X_1112, Y_1113), true, iext(uri_owl_complementOf, X_1112, Y_1113), true)=true))). % 35.00/24.29 tff(c_62223, plain, (![X_1108, Y_1109]: (ifeq(iext(uri_rdf__1, X_1108, Y_1109), true, iext(uri_rdf__1, X_1108, Y_1109), true)=true))). % 35.00/24.29 tff(c_4415, 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))). % 35.00/24.29 tff(c_5532, 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))). % 35.00/24.29 tff(c_12851, 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))). % 35.00/24.29 tff(c_60870, plain, (![X_1093, Y_1094]: (ifeq(iext(uri_rdf_first, X_1093, Y_1094), true, iext(uri_rdf_first, X_1093, Y_1094), true)=true))). % 35.00/24.29 tff(c_60793, plain, (![C_1092]: (ifeq(iext(uri_rdfs_subClassOf, C_1092, uri_rdfs_Seq), true, iext(uri_rdfs_subClassOf, C_1092, uri_rdfs_Resource), true)=true))). % 35.00/24.29 tff(c_5694, 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))). % 35.00/24.29 tff(c_7731, 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))). % 35.00/24.29 tff(c_60526, plain, (![X_1086, Y_1087]: (ifeq(iext(uri_rdf_subject, X_1086, Y_1087), true, iext(uri_rdf_subject, X_1086, Y_1087), true)=true))). % 35.00/24.29 tff(c_6214, 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))). % 35.00/24.29 tff(c_59764, plain, (![X_1079, Y_1080]: (ifeq(iext(uri_rdfs_domain, X_1079, Y_1080), true, iext(uri_rdfs_domain, X_1079, Y_1080), true)=true))). % 35.00/24.29 tff(c_4463, 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))). % 35.00/24.29 tff(c_4267, 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))). % 35.00/24.29 tff(c_10326, 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))). % 35.00/24.29 tff(c_4368, 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))). % 35.00/24.30 tff(c_10113, 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))). % 35.00/24.30 tff(c_7208, 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))). % 35.00/24.30 tff(c_58418, plain, (![X_1062, Y_1063]: (ifeq(iext(uri_owl_intersectionOf, X_1062, Y_1063), true, iext(uri_owl_intersectionOf, X_1062, Y_1063), true)=true))). % 35.00/24.30 tff(c_57565, plain, (![C_1054]: (ifeq(iext(uri_rdfs_subClassOf, C_1054, uri_rdf_Bag), true, iext(uri_rdfs_subClassOf, C_1054, uri_rdfs_Resource), true)=true))). % 35.00/24.30 tff(c_57498, plain, (![P_1052]: (ifeq(iext(uri_rdfs_subPropertyOf, P_1052, uri_rdf__3), true, iext(uri_rdfs_subPropertyOf, P_1052, uri_rdfs_member), true)=true))). % 35.00/24.30 tff(c_6278, 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))). % 35.00/24.30 tff(c_57318, plain, (![X_1047, Y_1048]: (ifeq(iext(uri_rdf_rest, X_1047, Y_1048), true, iext(uri_rdf_rest, X_1047, Y_1048), true)=true))). % 35.00/24.30 tff(c_8121, 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))). % 35.00/24.30 tff(c_4915, 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))). % 35.00/24.30 tff(c_12741, 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))). % 35.00/24.30 tff(c_8061, 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))). % 35.00/24.30 tff(c_5049, 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))). % 35.00/24.30 tff(c_54488, plain, (![X_1028, Y_1029]: (ifeq(iext(uri_rdf_type, X_1028, Y_1029), true, iext(uri_rdf_type, X_1028, Y_1029), true)=true))). % 35.00/24.30 tff(c_54461, plain, (![X_1024, Y_1025]: (ifeq(iext(uri_rdfs_seeAlso, X_1024, Y_1025), true, iext(uri_rdfs_seeAlso, X_1024, Y_1025), true)=true))). % 35.00/24.30 tff(c_9349, 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))). % 35.00/24.30 tff(c_4604, 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))). % 35.00/24.30 tff(c_8883, 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))). % 35.00/24.30 tff(c_54047, plain, (![X_1016, Y_1017]: (ifeq(iext(uri_rdf__3, X_1016, Y_1017), true, iext(uri_rdfs_member, X_1016, Y_1017), true)=true))). % 35.00/24.30 tff(c_4990, 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))). % 35.00/24.30 tff(c_53898, plain, (![X_1011, Y_1012]: (ifeq(iext(uri_rdfs_isDefinedBy, X_1011, Y_1012), true, iext(uri_rdfs_isDefinedBy, X_1011, Y_1012), true)=true))). % 35.00/24.30 tff(c_8945, 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))). % 35.00/24.30 tff(c_4325, 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))). % 35.00/24.30 tff(c_7626, 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))). % 35.00/24.30 tff(c_6558, 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))). % 35.00/24.30 tff(c_5828, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subPropertyOf), true, ifeq(iext(P_47, uri_owl_complementOf, uri_owl_complementOf), true, true, true), true)=true))). % 35.00/24.30 tff(c_6403, 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))). % 35.00/24.30 tff(c_14034, 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))). % 35.00/24.30 tff(c_6968, 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))). % 35.00/24.30 tff(c_7289, 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))). % 35.00/24.30 tff(c_5773, 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))). % 35.00/24.30 tff(c_17055, 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))). % 35.00/24.30 tff(c_17677, 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))). % 35.00/24.30 tff(c_4864, plain, (![P_47, X_139]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, X_139, uri_rdfs_Resource), true, true, true), true)=true))). % 35.00/24.30 tff(c_8373, 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_029_Ex_Falso_Quodlibet_BNODE_l1), true, true, true), true)=true))). % 35.00/24.30 tff(c_9650, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdf_List), true, ifeq(iext(P_28, X_30, sK2_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l2), true, true, true), true)=true))). % 35.00/24.30 tff(c_12335, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdfs_Class), true, ifeq(iext(P_28, X_30, sK3_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_x), true, true, true), true)=true))). % 35.00/24.30 tff(c_11077, 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))). % 35.00/24.30 tff(c_6060, 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))). % 35.00/24.30 tff(c_11074, 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))). % 35.00/24.30 tff(c_5776, 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))). % 35.00/24.30 tff(c_19171, 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))). % 35.00/24.30 tff(c_19168, 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))). % 35.00/24.30 tff(c_8376, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdf_List), true, ifeq(iext(P_18, sK4_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l1, Y_21), true, true, true), true)=true))). % 35.00/24.30 tff(c_12338, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdfs_Class), true, ifeq(iext(P_18, sK3_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_x, Y_21), true, true, true), true)=true))). % 35.00/24.30 tff(c_17680, 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))). % 35.00/24.30 tff(c_10205, 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))). % 35.00/24.30 tff(c_10202, 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))). % 35.00/24.30 tff(c_9653, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdf_List), true, ifeq(iext(P_18, sK2_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l2, Y_21), true, true, true), true)=true))). % 35.00/24.30 tff(c_17058, 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))). % 35.00/24.30 tff(c_6063, 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))). % 35.00/24.30 tff(c_3979, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_owl_Class), true, ifeq(iext(P_28, X_30, uri_ex_B), true, true, true), true)=true))). % 35.00/24.30 tff(c_3739, 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))). % 35.00/24.30 tff(c_3779, 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))). % 35.00/24.30 tff(c_3936, 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))). % 35.00/24.30 tff(c_4105, 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))). % 35.00/24.30 tff(c_3939, 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))). % 35.00/24.30 tff(c_3641, 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))). % 35.00/24.30 tff(c_3895, 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))). % 35.00/24.30 tff(c_3690, 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))). % 35.00/24.30 tff(c_4018, 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))). % 35.00/24.30 tff(c_3819, 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))). % 35.00/24.30 tff(c_4021, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdf_Property), true, ifeq(iext(P_18, uri_rdf_first, Y_21), true, true, true), true)=true))). % 35.00/24.30 tff(c_4145, 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))). % 35.00/24.30 tff(c_4069, 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))). % 35.00/24.30 tff(c_4190, 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))). % 35.00/24.30 tff(c_3856, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_owl_Class), true, ifeq(iext(P_28, X_30, uri_ex_A), true, true, true), true)=true))). % 35.00/24.30 tff(c_4226, 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))). % 35.00/24.30 tff(c_3512, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, sK3_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_x), true, ifeq(iext(P_28, X_30, uri_ex_w), true, true, true), true)=true))). % 35.00/24.30 tff(c_3982, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_owl_Class), true, ifeq(iext(P_18, uri_ex_B, Y_21), true, true, true), true)=true))). % 35.00/24.30 tff(c_3564, 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))). % 35.00/24.30 tff(c_4066, 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))). % 35.00/24.30 tff(c_3561, 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))). % 35.00/24.30 tff(c_3859, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_owl_Class), true, ifeq(iext(P_18, uri_ex_A, Y_21), true, true, true), true)=true))). % 35.00/24.30 tff(c_3687, 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))). % 35.00/24.30 tff(c_4108, 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))). % 35.00/24.30 tff(c_3782, 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))). % 35.00/24.30 tff(c_3515, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, sK3_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_x), true, ifeq(iext(P_18, uri_ex_w, Y_21), true, true, true), true)=true))). % 35.00/24.31 tff(c_3816, 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))). % 35.00/24.31 tff(c_4229, 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))). % 35.00/24.31 tff(c_4148, 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))). % 35.00/24.31 tff(c_4187, 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))). % 35.00/24.31 tff(c_3601, 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))). % 35.00/24.31 tff(c_3638, 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))). % 35.00/24.31 tff(c_3598, 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))). % 35.00/24.31 tff(c_3898, 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))). % 35.00/24.31 tff(c_3736, 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))). % 35.00/24.31 tff(c_1869, plain, (![P_92, X_61, Y_95]: (ifeq(iext(uri_rdfs_domain, P_92, uri_rdfs_Resource), true, ifeq(iext(P_92, X_61, Y_95), true, true, true), true)=true))). % 35.00/24.31 tff(c_2248, plain, (![P_96, X_98, X_61]: (ifeq(iext(uri_rdfs_range, P_96, uri_rdfs_Resource), true, ifeq(iext(P_96, X_98, X_61), true, true, true), true)=true))). % 35.00/24.31 tff(c_3113, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_range), true, ifeq(iext(P_106, uri_rdf_subject, uri_rdfs_Resource), true, true, true), true)=true))). % 35.00/24.31 tff(c_2756, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_domain), true, ifeq(iext(P_106, uri_rdf_object, uri_rdfs_Statement), true, true, true), true)=true))). % 35.00/24.31 tff(c_2768, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_domain), true, ifeq(iext(P_106, uri_rdfs_domain, uri_rdf_Property), true, true, true), true)=true))). % 35.00/24.31 tff(c_42425, plain, (![X_868, Y_869]: (ifeq(iext(uri_rdfs_isDefinedBy, X_868, Y_869), true, iext(uri_rdfs_seeAlso, X_868, Y_869), true)=true))). % 35.00/24.31 tff(c_3101, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdf_type), true, ifeq(iext(P_106, uri_rdf_first, uri_rdf_Property), true, true, true), true)=true))). % 35.00/24.31 tff(c_42237, plain, (![C_865]: (ifeq(iext(uri_rdfs_subClassOf, C_865, uri_rdf_Bag), true, iext(uri_rdfs_subClassOf, C_865, uri_rdfs_Container), true)=true))). % 35.00/24.31 tff(c_42186, plain, (![C_863]: (ifeq(iext(uri_rdfs_subClassOf, C_863, uri_rdfs_Datatype), true, iext(uri_rdfs_subClassOf, C_863, uri_rdfs_Class), true)=true))). % 35.00/24.31 tff(c_3071, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_subClassOf), true, ifeq(iext(P_106, uri_rdf_Alt, uri_rdfs_Container), true, true, true), true)=true))). % 35.00/24.31 tff(c_2999, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_range), true, ifeq(iext(P_106, uri_rdfs_label, uri_rdfs_Literal), true, true, true), true)=true))). % 35.00/24.31 tff(c_3017, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_domain), true, ifeq(iext(P_106, uri_rdf_type, uri_rdfs_Resource), true, true, true), true)=true))). % 35.00/24.31 tff(c_3005, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_domain), true, ifeq(iext(P_106, uri_rdf__2, uri_rdfs_Resource), true, true, true), true)=true))). % 35.00/24.31 tff(c_2951, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_range), true, ifeq(iext(P_106, uri_rdfs_domain, uri_rdfs_Class), true, true, true), true)=true))). % 35.00/24.31 tff(c_3065, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdf_type), true, ifeq(iext(P_106, uri_rdf__3, uri_rdf_Property), true, true, true), true)=true))). % 35.00/24.31 tff(c_2762, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_domain), true, ifeq(iext(P_106, uri_rdfs_comment, uri_rdfs_Resource), true, true, true), true)=true))). % 35.00/24.31 tff(c_2774, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_range), true, ifeq(iext(P_106, uri_rdf_value, uri_rdfs_Resource), true, true, true), true)=true))). % 35.00/24.31 tff(c_3119, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_subClassOf), true, ifeq(iext(P_106, uri_rdf_Bag, uri_rdfs_Container), true, true, true), true)=true))). % 35.00/24.31 tff(c_3083, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_range), true, ifeq(iext(P_106, uri_rdf_type, uri_rdfs_Class), true, true, true), true)=true))). % 35.00/24.31 tff(c_3041, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_range), true, ifeq(iext(P_106, uri_rdfs_seeAlso, uri_rdfs_Resource), true, true, true), true)=true))). % 35.00/24.31 tff(c_3077, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_domain), true, ifeq(iext(P_106, uri_rdfs_subClassOf, uri_rdfs_Class), true, true, true), true)=true))). % 35.00/24.31 tff(c_2924, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_domain), true, ifeq(iext(P_106, uri_rdf_value, uri_rdfs_Resource), true, true, true), true)=true))). % 35.00/24.31 tff(c_3053, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_domain), true, ifeq(iext(P_106, uri_rdf_subject, uri_rdfs_Statement), true, true, true), true)=true))). % 35.00/24.31 tff(c_2804, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_range), true, ifeq(iext(P_106, uri_rdf_rest, uri_rdf_List), true, true, true), true)=true))). % 35.00/24.31 tff(c_2957, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_owl_intersectionOf), true, ifeq(iext(P_106, sK3_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_x, sK4_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l1), true, true, true), true)=true))). % 35.00/24.31 tff(c_40159, plain, (![P_845]: (ifeq(iext(uri_rdfs_subPropertyOf, P_845, uri_rdfs_isDefinedBy), true, iext(uri_rdfs_subPropertyOf, P_845, uri_rdfs_seeAlso), true)=true))). % 35.00/24.31 tff(c_2840, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_domain), true, ifeq(iext(P_106, uri_rdf_rest, uri_rdf_List), true, true, true), true)=true))). % 35.00/24.31 tff(c_3107, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_domain), true, ifeq(iext(P_106, uri_rdfs_subPropertyOf, uri_rdf_Property), true, true, true), true)=true))). % 35.00/24.31 tff(c_2858, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdf_first), true, ifeq(iext(P_106, sK2_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l2, sK1_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_y), true, true, true), true)=true))). % 35.00/24.31 tff(c_39734, plain, (![C_840]: (ifeq(iext(uri_rdfs_subClassOf, C_840, uri_rdf_XMLLiteral), true, iext(uri_rdfs_subClassOf, C_840, uri_rdfs_Literal), true)=true))). % 35.00/24.31 tff(c_2750, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdf_type), true, ifeq(iext(P_106, uri_rdf__2, uri_rdf_Property), true, true, true), true)=true))). % 35.00/24.31 tff(c_2975, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdf_rest), true, ifeq(iext(P_106, sK4_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l1, sK2_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l2), true, true, true), true)=true))). % 35.00/24.31 tff(c_2870, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_range), true, ifeq(iext(P_106, uri_rdf__2, uri_rdfs_Resource), true, true, true), true)=true))). % 35.00/24.31 tff(c_2780, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdf_type), true, ifeq(iext(P_106, uri_rdf__1, uri_rdf_Property), true, true, true), true)=true))). % 35.00/24.31 tff(c_2939, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_subPropertyOf), true, ifeq(iext(P_106, uri_rdfs_isDefinedBy, uri_rdfs_seeAlso), true, true, true), true)=true))). % 35.00/24.31 tff(c_39058, plain, (![C_833]: (ifeq(iext(uri_rdfs_subClassOf, C_833, uri_rdfs_Seq), true, iext(uri_rdfs_subClassOf, C_833, uri_rdfs_Container), true)=true))). % 35.00/24.31 tff(c_2906, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdf_type), true, ifeq(iext(P_106, uri_rdf_value, uri_rdf_Property), true, true, true), true)=true))). % 35.00/24.31 tff(c_2882, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_owl_complementOf), true, ifeq(iext(P_106, sK1_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_y, uri_ex_A), true, true, true), true)=true))). % 35.00/24.31 tff(c_3095, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdf_type), true, ifeq(iext(P_106, uri_rdf_nil, uri_rdf_List), true, true, true), true)=true))). % 35.00/24.31 tff(c_2981, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdf_type), true, ifeq(iext(P_106, uri_rdf_subject, uri_rdf_Property), true, true, true), true)=true))). % 35.00/24.31 tff(c_3029, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_domain), true, ifeq(iext(P_106, uri_rdf__1, uri_rdfs_Resource), true, true, true), true)=true))). % 35.00/24.31 tff(c_2918, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdf_type), true, ifeq(iext(P_106, uri_rdf_type, uri_rdf_Property), true, true, true), true)=true))). % 35.00/24.31 tff(c_2912, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdf_type), true, ifeq(iext(P_106, uri_rdf_Property, uri_rdfs_Class), true, true, true), true)=true))). % 35.00/24.31 tff(c_2876, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_range), true, ifeq(iext(P_106, uri_rdfs_isDefinedBy, uri_rdfs_Resource), true, true, true), true)=true))). % 35.00/24.31 tff(c_3059, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdf_type), true, ifeq(iext(P_106, uri_rdf__3, uri_rdfs_ContainerMembershipProperty), true, true, true), true)=true))). % 35.00/24.31 tff(c_2894, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdf_type), true, ifeq(iext(P_106, uri_rdf_object, uri_rdf_Property), true, true, true), true)=true))). % 35.00/24.31 tff(c_2900, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdf_first), true, ifeq(iext(P_106, sK4_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l1, uri_ex_A), true, true, true), true)=true))). % 35.00/24.31 tff(c_2738, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_range), true, ifeq(iext(P_106, uri_rdf__1, uri_rdfs_Resource), true, true, true), true)=true))). % 35.00/24.31 tff(c_3035, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdf_type), true, ifeq(iext(P_106, uri_ex_w, sK3_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_x), true, true, true), true)=true))). % 35.00/24.31 tff(c_37276, plain, (![D_817]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_817), true, icext(D_817, uri_rdfs_member), true)=true))). % 35.00/24.31 tff(c_2963, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_range), true, ifeq(iext(P_106, uri_rdf__3, uri_rdfs_Resource), true, true, true), true)=true))). % 35.00/24.31 tff(c_37210, plain, (![D_815]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_815), true, icext(D_815, uri_rdfs_Resource), true)=true))). % 35.00/24.31 tff(c_37106, plain, (![C_812]: (ifeq(iext(uri_rdfs_subClassOf, C_812, uri_rdf_Alt), true, iext(uri_rdfs_subClassOf, C_812, uri_rdfs_Container), true)=true))). % 35.00/24.31 tff(c_37076, plain, (![D_811]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_811), true, icext(D_811, uri_rdfs_range), true)=true))). % 35.00/24.31 tff(c_37010, plain, (![D_809]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_809), true, icext(D_809, uri_rdfs_isDefinedBy), true)=true))). % 35.00/24.31 tff(c_36943, plain, (![D_807]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_807), true, icext(D_807, uri_rdfs_subPropertyOf), true)=true))). % 35.00/24.31 tff(c_2930, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_subClassOf), true, ifeq(iext(P_106, uri_rdfs_ContainerMembershipProperty, uri_rdf_Property), true, true, true), true)=true))). % 35.00/24.31 tff(c_36757, plain, (![D_804]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_804), true, icext(D_804, uri_owl_complementOf), true)=true))). % 35.00/24.31 tff(c_36691, plain, (![D_802]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_802), true, icext(D_802, uri_rdfs_domain), true)=true))). % 35.00/24.31 tff(c_36624, plain, (![D_800]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_800), true, icext(D_800, uri_rdfs_seeAlso), true)=true))). % 35.00/24.31 tff(c_2810, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_range), true, ifeq(iext(P_106, uri_rdfs_subPropertyOf, uri_rdf_Property), true, true, true), true)=true))). % 35.00/24.31 tff(c_36429, plain, (![D_797]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_797), true, icext(D_797, uri_owl_intersectionOf), true)=true))). % 35.00/24.31 tff(c_36231, plain, (![D_794]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_794), true, icext(D_794, uri_rdfs_Container), true)=true))). % 35.00/24.31 tff(c_2798, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_domain), true, ifeq(iext(P_106, uri_rdf__3, uri_rdfs_Resource), true, true, true), true)=true))). % 35.00/24.31 tff(c_36137, plain, (![D_792]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_792), true, icext(D_792, uri_rdfs_Class), true)=true))). % 35.00/24.31 tff(c_36071, plain, (![D_790]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_790), true, icext(D_790, uri_rdfs_ContainerMembershipProperty), true)=true))). % 35.00/24.31 tff(c_3089, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_range), true, ifeq(iext(P_106, uri_rdf_predicate, uri_rdfs_Resource), true, true, true), true)=true))). % 35.00/24.31 tff(c_35871, plain, (![D_787]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_787), true, icext(D_787, uri_rdf_XMLLiteral), true)=true))). % 35.00/24.31 tff(c_35804, plain, (![D_785]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_785), true, icext(D_785, uri_rdfs_Seq), true)=true))). % 35.00/24.31 tff(c_35738, plain, (![D_783]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_783), true, icext(D_783, uri_rdf_Alt), true)=true))). % 35.00/24.31 tff(c_2852, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_domain), true, ifeq(iext(P_106, uri_rdfs_label, uri_rdfs_Resource), true, true, true), true)=true))). % 35.00/24.31 tff(c_35547, plain, (![D_780]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_780), true, icext(D_780, uri_rdf_Bag), true)=true))). % 35.00/24.31 tff(c_35478, plain, (![D_778]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_778), true, icext(D_778, uri_rdfs_Literal), true)=true))). % 35.00/24.31 tff(c_3125, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_domain), true, ifeq(iext(P_106, uri_rdf_predicate, uri_rdfs_Statement), true, true, true), true)=true))). % 35.00/24.31 tff(c_35290, plain, (![D_775]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_775), true, icext(D_775, uri_rdfs_Datatype), true)=true))). % 35.00/24.31 tff(c_35224, plain, (![D_773]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_773), true, icext(D_773, uri_rdfs_subClassOf), true)=true))). % 35.00/24.31 tff(c_2987, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_range), true, ifeq(iext(P_106, uri_rdfs_subClassOf, uri_rdfs_Class), true, true, true), true)=true))). % 35.00/24.31 tff(c_35034, plain, (![D_770]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_770), true, icext(D_770, sK3_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_x), true)=true))). % 35.00/24.31 tff(c_34968, plain, (![D_768]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_768), true, icext(D_768, uri_rdfs_Statement), true)=true))). % 35.00/24.31 tff(c_34901, plain, (![D_766]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_766), true, icext(D_766, uri_owl_Class), true)=true))). % 35.00/24.31 tff(c_2888, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdf_type), true, ifeq(iext(P_106, uri_rdf__1, uri_rdfs_ContainerMembershipProperty), true, true, true), true)=true))). % 35.00/24.31 tff(c_34715, plain, (![D_763]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_List, D_763), true, icext(D_763, sK2_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l2), true)=true))). % 35.00/24.31 tff(c_34648, plain, (![D_761]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_761), true, icext(D_761, uri_rdf_predicate), true)=true))). % 35.00/24.31 tff(c_34453, plain, (![D_758]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_758), true, icext(D_758, uri_rdfs_label), true)=true))). % 35.00/24.31 tff(c_3023, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_domain), true, ifeq(iext(P_106, uri_rdfs_seeAlso, uri_rdfs_Resource), true, true, true), true)=true))). % 35.00/24.31 tff(c_34386, plain, (![D_756]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_List, D_756), true, icext(D_756, sK4_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l1), true)=true))). % 35.00/24.31 tff(c_34319, plain, (![D_754]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_754), true, icext(D_754, uri_rdfs_comment), true)=true))). % 35.00/24.31 tff(c_34252, plain, (![D_752]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_752), true, icext(D_752, uri_rdf_List), true)=true))). % 35.00/24.31 tff(c_34178, plain, (![D_750]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_750), true, icext(D_750, uri_rdf__2), true)=true))). % 35.00/24.31 tff(c_16423, 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))). % 35.00/24.31 tff(c_16373, 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))). % 35.00/24.32 tff(c_2786, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_subClassOf), true, ifeq(iext(P_106, uri_rdfs_Datatype, uri_rdfs_Class), true, true, true), true)=true))). % 35.00/24.32 tff(c_19479, 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))). % 35.00/24.32 tff(c_33896, plain, (![D_742]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_742), true, icext(D_742, uri_rdf_type), true)=true))). % 35.00/24.32 tff(c_16308, 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))). % 35.00/24.32 tff(c_16236, 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))). % 35.00/24.32 tff(c_2864, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_subClassOf), true, ifeq(iext(P_106, uri_rdfs_Seq, uri_rdfs_Container), true, true, true), true)=true))). % 35.00/24.32 tff(c_15932, 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))). % 35.00/24.32 tff(c_15989, 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))). % 35.00/24.32 tff(c_15652, 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))). % 35.00/24.32 tff(c_15653, 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))). % 35.00/24.32 tff(c_15528, plain, (![E_41]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Resource, E_41), true, iext(uri_rdfs_subClassOf, sK3_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_x, E_41), true)=true))). % 35.00/24.32 tff(c_2828, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_domain), true, ifeq(iext(P_106, uri_rdf_first, uri_rdf_List), true, true, true), true)=true))). % 35.00/24.32 tff(c_15775, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_48), true, iext(Q_48, sK3_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_x, sK3_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_x), true)=true))). % 35.00/24.32 tff(c_17369, 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))). % 35.00/24.32 tff(c_15527, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_48), true, iext(Q_48, sK3_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_x, uri_rdfs_Resource), true)=true))). % 35.00/24.32 tff(c_33300, plain, (![D_724]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, D_724), true, icext(D_724, uri_rdf__2), true)=true))). % 35.00/24.32 tff(c_15842, 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))). % 35.00/24.32 tff(c_17976, 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))). % 35.00/24.32 tff(c_2792, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_range), true, ifeq(iext(P_106, uri_rdfs_range, uri_rdfs_Class), true, true, true), true)=true))). % 35.00/24.32 tff(c_17461, 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))). % 35.00/24.32 tff(c_17975, 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))). % 35.00/24.32 tff(c_17460, 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))). % 35.00/24.32 tff(c_18129, 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))). % 35.00/24.32 tff(c_15112, 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))). % 35.00/24.32 tff(c_14942, 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))). % 35.00/24.32 tff(c_15064, 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))). % 35.00/24.32 tff(c_14989, 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))). % 35.00/24.32 tff(c_15359, 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))). % 35.00/24.32 tff(c_15239, 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))). % 35.00/24.32 tff(c_15190, 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))). % 35.00/24.32 tff(c_15312, 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))). % 35.00/24.32 tff(c_15437, 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))). % 35.00/24.32 tff(c_17307, 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))). % 35.00/24.32 tff(c_2969, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_domain), true, ifeq(iext(P_106, uri_rdfs_member, uri_rdfs_Resource), true, true, true), true)=true))). % 35.00/24.32 tff(c_14847, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, sK2_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l2, uri_rdf_List), true)=true))). % 35.00/24.32 tff(c_17912, 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))). % 35.00/24.32 tff(c_19244, 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))). % 35.00/24.32 tff(c_14629, 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))). % 35.00/24.32 tff(c_14895, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, sK3_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_x, uri_rdfs_Class), true)=true))). % 35.00/24.32 tff(c_14800, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, sK4_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l1, uri_rdf_List), true)=true))). % 35.00/24.32 tff(c_14507, 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))). % 35.00/24.32 tff(c_14682, 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))). % 35.00/24.32 tff(c_3137, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdf_type), true, ifeq(iext(P_106, uri_ex_A, uri_owl_Class), true, true, true), true)=true))). % 35.00/24.32 tff(c_5858, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_48), true, iext(Q_48, uri_owl_complementOf, uri_owl_complementOf), true)=true))). % 35.00/24.32 tff(c_8456, 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))). % 35.00/24.32 tff(c_32329, plain, (![D_689]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_689), true, icext(D_689, uri_rdf_object), true)=true))). % 35.00/24.32 tff(c_7762, 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))). % 35.00/24.32 tff(c_32263, plain, (![C_686]: (ifeq(iext(uri_rdfs_subClassOf, C_686, uri_rdfs_ContainerMembershipProperty), true, iext(uri_rdfs_subClassOf, C_686, uri_rdf_Property), true)=true))). % 35.00/24.32 tff(c_7238, 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))). % 35.00/24.32 tff(c_11369, 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))). % 35.00/24.32 tff(c_10148, 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))). % 35.00/24.32 tff(c_5948, 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))). % 35.00/24.32 tff(c_7322, 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))). % 35.00/24.32 tff(c_8280, 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))). % 35.00/24.32 tff(c_2945, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_subClassOf), true, ifeq(iext(P_106, uri_rdf_XMLLiteral, uri_rdfs_Literal), true, true, true), true)=true))). % 35.00/24.32 tff(c_5568, 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))). % 35.00/24.32 tff(c_11913, 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))). % 35.00/24.32 tff(c_31822, plain, (![D_672]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, D_672), true, icext(D_672, uri_rdf__1), true)=true))). % 35.00/24.32 tff(c_9561, 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))). % 35.00/24.32 tff(c_3047, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_range), true, ifeq(iext(P_106, uri_rdfs_comment, uri_rdfs_Literal), true, true, true), true)=true))). % 35.00/24.32 tff(c_10449, 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))). % 35.00/24.32 tff(c_5447, 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))). % 35.00/24.32 tff(c_8155, 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))). % 35.00/24.32 tff(c_9383, 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))). % 35.00/24.32 tff(c_7001, 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))). % 35.00/24.32 tff(c_6010, 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))). % 35.00/24.32 tff(c_7323, 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))). % 35.00/24.32 tff(c_3011, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_range), true, ifeq(iext(P_106, uri_rdf_first, uri_rdfs_Resource), true, true, true), true)=true))). % 35.00/24.32 tff(c_7002, 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))). % 35.00/24.32 tff(c_10448, 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))). % 35.00/24.32 tff(c_31180, plain, (![D_654]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_654), true, icext(D_654, uri_rdf_value), true)=true))). % 35.00/24.32 tff(c_12883, 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))). % 35.00/24.32 tff(c_5020, 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))). % 35.00/24.32 tff(c_2732, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_domain), true, ifeq(iext(P_106, uri_rdfs_range, uri_rdf_Property), true, true, true), true)=true))). % 35.00/24.32 tff(c_8976, 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))). % 35.00/24.32 tff(c_12964, 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))). % 35.00/24.32 tff(c_11812, 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))). % 35.00/24.32 tff(c_10900, 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))). % 35.00/24.32 tff(c_2822, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdf_type), true, ifeq(iext(P_106, uri_rdf_XMLLiteral, uri_rdfs_Datatype), true, true, true), true)=true))). % 35.00/24.32 tff(c_8002, 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))). % 35.00/24.32 tff(c_5662, 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))). % 35.00/24.32 tff(c_4945, 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))). % 35.00/24.32 tff(c_6590, 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))). % 35.00/24.32 tff(c_2993, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_range), true, ifeq(iext(P_106, uri_rdfs_member, uri_rdfs_Resource), true, true, true), true)=true))). % 35.00/24.32 tff(c_10356, 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))). % 35.00/24.32 tff(c_30230, plain, (![D_627]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, D_627), true, icext(D_627, uri_rdf__3), true)=true))). % 35.00/24.32 tff(c_6245, 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))). % 35.00/24.32 tff(c_6862, 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))). % 35.00/24.32 tff(c_6428, 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))). % 35.00/24.32 tff(c_2816, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdf_type), true, ifeq(iext(P_106, uri_rdf_rest, uri_rdf_Property), true, true, true), true)=true))). % 35.00/24.32 tff(c_13553, 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))). % 35.00/24.32 tff(c_14069, 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))). % 35.00/24.32 tff(c_13839, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, uri_owl_complementOf, uri_rdf_Property), true)=true))). % 35.00/24.32 tff(c_8914, 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))). % 35.00/24.32 tff(c_8156, 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))). % 35.00/24.32 tff(c_5174, 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))). % 35.00/24.32 tff(c_8091, 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))). % 35.00/24.32 tff(c_3131, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdf_rest), true, ifeq(iext(P_106, sK2_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l2, uri_rdf_nil), true, true, true), true)=true))). % 35.00/24.32 tff(c_6309, 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))). % 35.00/24.32 tff(c_9850, 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))). % 35.00/24.32 tff(c_7656, 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))). % 35.00/24.32 tff(c_5173, 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))). % 35.00/24.32 tff(c_7894, 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))). % 35.00/24.32 tff(c_6310, 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))). % 35.00/24.32 tff(c_8975, 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))). % 35.00/24.32 tff(c_11438, 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))). % 35.00/24.32 tff(c_2744, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdf_type), true, ifeq(iext(P_106, uri_rdf__2, uri_rdfs_ContainerMembershipProperty), true, true, true), true)=true))). % 35.00/24.32 tff(c_11502, 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))). % 35.00/24.32 tff(c_9384, 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))). % 35.00/24.32 tff(c_29407, plain, (![D_600]: (ifeq(iext(uri_rdfs_subClassOf, sK3_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_x, D_600), true, icext(D_600, uri_ex_w), true)=true))). % 35.00/24.32 tff(c_5082, 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))). % 35.00/24.32 tff(c_11813, 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))). % 35.00/24.33 tff(c_2834, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdf_type), true, ifeq(iext(P_106, uri_ex_B, uri_owl_Class), true, true, true), true)=true))). % 35.00/24.33 tff(c_12776, 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))). % 35.00/24.33 tff(c_5446, 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))). % 35.00/24.33 tff(c_12775, 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))). % 35.00/24.33 tff(c_5724, 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))). % 35.00/24.33 tff(c_6677, 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))). % 35.00/24.33 tff(c_11501, 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))). % 35.00/24.33 tff(c_2846, plain, (![P_106]: (ifeq(iext(uri_rdfs_subPropertyOf, P_106, uri_rdfs_domain), true, ifeq(iext(P_106, uri_rdfs_isDefinedBy, uri_rdfs_Resource), true, true, true), true)=true))). % 35.00/24.33 tff(c_6678, 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))). % 35.00/24.33 tff(c_28778, plain, (![D_582]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_582), true, icext(D_582, uri_rdf_first), true)=true))). % 35.00/24.33 tff(c_4884, plain, (![Q_48, X_139]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, X_139, uri_rdfs_Resource), true)=true))). % 35.00/24.33 tff(c_3146, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_107), true, iext(Q_107, uri_rdf_object, uri_rdfs_Statement), true)=true))). % 35.00/24.33 tff(c_2705, plain, (![E_104]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, E_104), true, iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, E_104), true)=true))). % 35.00/24.33 tff(c_3206, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_107), true, iext(Q_107, uri_rdf_Bag, uri_rdfs_Container), true)=true))). % 35.00/24.33 tff(c_3170, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_first, Q_107), true, iext(Q_107, sK4_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l1, uri_ex_A), true)=true))). % 35.00/24.33 tff(c_3161, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_107), true, iext(Q_107, uri_rdfs_isDefinedBy, uri_rdfs_Resource), true)=true))). % 35.00/24.33 tff(c_28428, plain, (![D_572]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_List, D_572), true, icext(D_572, uri_rdf_nil), true)=true))). % 35.00/24.33 tff(c_3189, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_107), true, iext(Q_107, uri_rdf_type, uri_rdfs_Resource), true)=true))). % 35.00/24.33 tff(c_3173, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_107), true, iext(Q_107, uri_rdf_type, uri_rdf_Property), true)=true))). % 35.00/24.33 tff(c_3207, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_107), true, iext(Q_107, uri_rdf_predicate, uri_rdfs_Statement), true)=true))). % 35.00/24.33 tff(c_3147, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_107), true, iext(Q_107, uri_rdfs_comment, uri_rdfs_Resource), true)=true))). % 35.00/24.33 tff(c_3178, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_107), true, iext(Q_107, uri_rdfs_domain, uri_rdfs_Class), true)=true))). % 35.00/24.33 tff(c_3167, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_owl_complementOf, Q_107), true, iext(Q_107, sK1_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_y, uri_ex_A), true)=true))). % 35.00/24.33 tff(c_2709, plain, (![E_104]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Container, E_104), true, iext(uri_rdfs_subClassOf, uri_rdf_Alt, E_104), true)=true))). % 35.00/24.33 tff(c_3188, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_107), true, iext(Q_107, uri_rdf_first, uri_rdfs_Resource), true)=true))). % 35.00/24.33 tff(c_3160, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_107), true, iext(Q_107, uri_rdf_rest, uri_rdf_List), true)=true))). % 35.00/24.33 tff(c_3180, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_107), true, iext(Q_107, uri_rdf__3, uri_rdfs_Resource), true)=true))). % 35.00/24.33 tff(c_3157, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_107), true, iext(Q_107, uri_rdf_XMLLiteral, uri_rdfs_Datatype), true)=true))). % 35.00/24.33 tff(c_3165, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_107), true, iext(Q_107, uri_rdf__2, uri_rdfs_Resource), true)=true))). % 35.00/24.33 tff(c_3168, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_107), true, iext(Q_107, uri_rdf__1, uri_rdfs_ContainerMembershipProperty), true)=true))). % 35.00/24.33 tff(c_3195, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_107), true, iext(Q_107, uri_rdf_subject, uri_rdfs_Statement), true)=true))). % 35.00/24.33 tff(c_3179, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_owl_intersectionOf, Q_107), true, iext(Q_107, sK3_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_x, sK4_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l1), true)=true))). % 35.00/24.33 tff(c_3174, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_107), true, iext(Q_107, uri_rdf_value, uri_rdfs_Resource), true)=true))). % 35.00/24.33 tff(c_2708, plain, (![E_104]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Literal, E_104), true, iext(uri_rdfs_subClassOf, uri_rdf_XMLLiteral, E_104), true)=true))). % 35.00/24.33 tff(c_3201, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_107), true, iext(Q_107, uri_rdf_predicate, uri_rdfs_Resource), true)=true))). % 35.00/24.33 tff(c_3159, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_107), true, iext(Q_107, uri_ex_B, uri_owl_Class), true)=true))). % 35.00/24.33 tff(c_3162, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_107), true, iext(Q_107, uri_rdfs_label, uri_rdfs_Resource), true)=true))). % 35.00/24.33 tff(c_2710, plain, (![E_104]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Container, E_104), true, iext(uri_rdfs_subClassOf, uri_rdf_Bag, E_104), true)=true))). % 35.00/24.33 tff(c_3169, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_107), true, iext(Q_107, uri_rdf_object, uri_rdf_Property), true)=true))). % 35.00/24.33 tff(c_3209, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_107), true, iext(Q_107, uri_ex_A, uri_owl_Class), true)=true))). % 35.00/24.33 tff(c_3208, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_rest, Q_107), true, iext(Q_107, sK2_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l2, uri_rdf_nil), true)=true))). % 35.00/24.33 tff(c_3186, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_107), true, iext(Q_107, uri_rdfs_label, uri_rdfs_Literal), true)=true))). % 35.00/24.33 tff(c_27875, plain, (![D_545]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_545), true, icext(D_545, uri_rdf__3), true)=true))). % 35.00/24.33 tff(c_3154, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_107), true, iext(Q_107, uri_rdf_rest, uri_rdf_List), true)=true))). % 35.00/24.33 tff(c_3176, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_107), true, iext(Q_107, uri_rdfs_isDefinedBy, uri_rdfs_seeAlso), true)=true))). % 35.00/24.33 tff(c_3148, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_107), true, iext(Q_107, uri_rdfs_domain, uri_rdf_Property), true)=true))). % 35.00/24.33 tff(c_3185, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_107), true, iext(Q_107, uri_rdfs_member, uri_rdfs_Resource), true)=true))). % 35.00/24.33 tff(c_3171, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_107), true, iext(Q_107, uri_rdf_value, uri_rdf_Property), true)=true))). % 35.00/24.33 tff(c_3192, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_107), true, iext(Q_107, uri_ex_w, sK3_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_x), true)=true))). % 35.00/24.33 tff(c_3183, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_107), true, iext(Q_107, uri_rdf_subject, uri_rdf_Property), true)=true))). % 35.00/24.33 tff(c_27677, plain, (![D_536]: (ifeq(iext(uri_rdfs_subClassOf, uri_owl_Class, D_536), true, icext(D_536, uri_ex_A), true)=true))). % 35.00/24.33 tff(c_3144, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_107), true, iext(Q_107, uri_rdf__2, uri_rdfs_ContainerMembershipProperty), true)=true))). % 35.00/24.33 tff(c_3175, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_107), true, iext(Q_107, uri_rdfs_ContainerMembershipProperty, uri_rdf_Property), true)=true))). % 35.00/24.33 tff(c_3191, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_107), true, iext(Q_107, uri_rdf__1, uri_rdfs_Resource), true)=true))). % 35.00/24.33 tff(c_3202, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_107), true, iext(Q_107, uri_rdf_nil, uri_rdf_List), true)=true))). % 35.00/24.33 tff(c_3145, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_107), true, iext(Q_107, uri_rdf__2, uri_rdf_Property), true)=true))). % 35.00/24.33 tff(c_3184, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_107), true, iext(Q_107, uri_rdfs_subClassOf, uri_rdfs_Class), true)=true))). % 35.00/24.33 tff(c_3198, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_107), true, iext(Q_107, uri_rdf_Alt, uri_rdfs_Container), true)=true))). % 35.00/24.33 tff(c_27493, plain, (![D_527]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_527), true, icext(D_527, uri_rdf_rest), true)=true))). % 35.00/24.33 tff(c_3143, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_107), true, iext(Q_107, uri_rdf__1, uri_rdfs_Resource), true)=true))). % 35.00/24.33 tff(c_3187, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_107), true, iext(Q_107, uri_rdf__2, uri_rdfs_Resource), true)=true))). % 35.00/24.33 tff(c_3182, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_rest, Q_107), true, iext(Q_107, sK4_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l1, sK2_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l2), true)=true))). % 35.00/24.33 tff(c_3156, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_107), true, iext(Q_107, uri_rdf_rest, uri_rdf_Property), true)=true))). % 35.00/24.33 tff(c_3193, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_107), true, iext(Q_107, uri_rdfs_seeAlso, uri_rdfs_Resource), true)=true))). % 35.00/24.33 tff(c_2707, plain, (![E_104]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, E_104), true, iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, E_104), true)=true))). % 35.00/24.33 tff(c_3142, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_107), true, iext(Q_107, uri_rdfs_range, uri_rdf_Property), true)=true))). % 35.00/24.33 tff(c_27271, plain, (![D_518]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_518), true, icext(D_518, uri_rdf__1), true)=true))). % 35.00/24.33 tff(c_16377, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_predicate), true)=true))). % 35.00/24.33 tff(c_3194, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_107), true, iext(Q_107, uri_rdfs_comment, uri_rdfs_Literal), true)=true))). % 35.00/24.33 tff(c_16376, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_predicate), true)=true))). % 35.00/24.33 tff(c_16311, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_label), true)=true))). % 35.00/24.33 tff(c_16312, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_label), true)=true))). % 35.00/24.33 tff(c_27088, plain, (![D_511]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_511), true, icext(D_511, uri_rdf_Property), true)=true))). % 35.00/24.33 tff(c_19482, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_comment), true)=true))). % 35.00/24.33 tff(c_19483, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_comment), true)=true))). % 35.00/24.33 tff(c_16240, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdfs_Resource), true)=true))). % 35.00/24.33 tff(c_3200, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_107), true, iext(Q_107, uri_rdf_type, uri_rdfs_Class), true)=true))). % 35.00/24.33 tff(c_15936, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_member), true)=true))). % 35.00/24.33 tff(c_3172, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_107), true, iext(Q_107, uri_rdf_Property, uri_rdfs_Class), true)=true))). % 35.00/24.33 tff(c_15531, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, sK3_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_x), true)=true))). % 35.00/24.33 tff(c_17372, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_owl_Class), true)=true))). % 35.00/24.33 tff(c_15846, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdfs_Statement), true)=true))). % 35.00/24.33 tff(c_15778, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, sK3_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_x), true)=true))). % 35.00/24.33 tff(c_18132, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdf_List), true)=true))). % 35.00/24.33 tff(c_3163, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_first, Q_107), true, iext(Q_107, sK2_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l2, sK1_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_y), true)=true))). % 35.00/24.33 tff(c_17373, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_owl_Class), true)=true))). % 35.00/24.33 tff(c_17979, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdf_List), true)=true))). % 35.00/24.33 tff(c_26689, plain, (![D_495]: (ifeq(iext(uri_rdfs_subClassOf, uri_owl_Class, D_495), true, icext(D_495, uri_ex_B), true)=true))). % 35.00/24.33 tff(c_15845, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdfs_Statement), true)=true))). % 35.00/24.33 tff(c_3205, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_107), true, iext(Q_107, uri_rdf_subject, uri_rdfs_Resource), true)=true))). % 35.00/24.33 tff(c_3153, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_107), true, iext(Q_107, uri_rdf__3, uri_rdfs_Resource), true)=true))). % 35.00/24.33 tff(c_26540, plain, (![D_490]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_490), true, icext(D_490, uri_rdf_subject), true)=true))). % 35.00/24.33 tff(c_3164, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_107), true, iext(Q_107, uri_rdfs_Seq, uri_rdfs_Container), true)=true))). % 35.00/24.33 tff(c_3197, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_107), true, iext(Q_107, uri_rdf__3, uri_rdf_Property), true)=true))). % 35.00/24.33 tff(c_26413, plain, (![D_486]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, D_486), true, icext(D_486, uri_rdf_XMLLiteral), true)=true))). % 35.00/24.33 tff(c_3152, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_107), true, iext(Q_107, uri_rdfs_range, uri_rdfs_Class), true)=true))). % 35.00/24.33 tff(c_26200, plain, (![C_89, X_61]: (ifeq(icext(C_89, X_61), true, true, true)=true))). % 35.00/24.33 tff(c_7766, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_domain), true)=true))). % 35.00/24.33 tff(c_3166, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_107), true, iext(Q_107, uri_rdfs_isDefinedBy, uri_rdfs_Resource), true)=true))). % 35.00/24.33 tff(c_7658, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_range), true)=true))). % 35.00/24.33 tff(c_12886, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_subPropertyOf), true)=true))). % 35.00/24.33 tff(c_25646, plain, (![D_475, X_476]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Resource, D_475), true, icext(D_475, X_476), true)=true))). % 35.00/24.33 tff(c_2608, plain, (![R_101]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_seeAlso, R_101), true, iext(uri_rdfs_subPropertyOf, uri_rdfs_isDefinedBy, R_101), true)=true))). % 35.00/24.33 tff(c_8459, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdf_Bag), true)=true))). % 35.00/24.33 tff(c_25016, plain, (![X_468, Y_469]: (ifeq(iext(uri_rdfs_subClassOf, X_468, Y_469), true, icext(uri_rdfs_Class, Y_469), true)=true))). % 35.00/24.33 tff(c_7659, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_range), true)=true))). % 35.00/24.33 tff(c_8005, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_owl_intersectionOf), true)=true))). % 35.00/24.33 tff(c_3203, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_107), true, iext(Q_107, uri_rdf_first, uri_rdf_Property), true)=true))). % 35.00/24.33 tff(c_7896, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdfs_Seq), true)=true))). % 35.00/24.33 tff(c_24523, plain, (![X_460, Y_461]: (ifeq(iext(uri_rdfs_domain, X_460, Y_461), true, icext(uri_rdf_Property, X_460), true)=true))). % 35.00/24.33 tff(c_6248, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf__3), true)=true))). % 35.00/24.33 tff(c_3190, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_107), true, iext(Q_107, uri_rdfs_seeAlso, uri_rdfs_Resource), true)=true))). % 35.00/24.33 tff(c_9853, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_first), true)=true))). % 35.00/24.33 tff(c_24357, plain, (![X_453, Y_454]: (ifeq(iext(uri_rdf_rest, X_453, Y_454), true, icext(uri_rdf_List, Y_454), true)=true))). % 35.00/24.33 tff(c_5726, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_isDefinedBy), true)=true))). % 35.00/24.33 tff(c_6593, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf__2), true)=true))). % 35.00/24.33 tff(c_3150, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_107), true, iext(Q_107, uri_rdf__1, uri_rdf_Property), true)=true))). % 35.00/24.33 tff(c_11442, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_seeAlso), true)=true))). % 35.00/24.33 tff(c_7765, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_domain), true)=true))). % 35.00/24.33 tff(c_23908, plain, (![X_444, Y_445]: (ifeq(iext(uri_rdfs_domain, X_444, Y_445), true, icext(uri_rdfs_Class, Y_445), true)=true))). % 35.00/24.33 tff(c_5860, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_owl_complementOf), true)=true))). % 35.00/24.33 tff(c_2706, plain, (![E_104]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Container, E_104), true, iext(uri_rdfs_subClassOf, uri_rdfs_Seq, E_104), true)=true))). % 35.00/24.33 tff(c_6247, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf__3), true)=true))). % 35.00/24.33 tff(c_4947, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_value), true)=true))). % 35.00/24.33 tff(c_23387, plain, (![X_436, Y_437]: (ifeq(iext(uri_rdfs_subPropertyOf, X_436, Y_437), true, icext(uri_rdf_Property, X_436), true)=true))). % 35.00/24.34 tff(c_8004, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_owl_intersectionOf), true)=true))). % 35.00/24.34 tff(c_3151, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_107), true, iext(Q_107, uri_rdfs_Datatype, uri_rdfs_Class), true)=true))). % 35.00/24.34 tff(c_5664, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdf_XMLLiteral), true)=true))). % 35.00/24.34 tff(c_9854, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_first), true)=true))). % 35.00/24.34 tff(c_23254, plain, (![X_428, Y_429]: (ifeq(iext(uri_rdf_object, X_428, Y_429), true, icext(uri_rdfs_Statement, X_428), true)=true))). % 35.00/24.34 tff(c_10359, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf__1), true)=true))). % 35.00/24.34 tff(c_6313, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf__2), true)=true))). % 35.00/24.34 tff(c_3196, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_107), true, iext(Q_107, uri_rdf__3, uri_rdfs_ContainerMembershipProperty), true)=true))). % 35.00/24.34 tff(c_5023, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_subClassOf), true)=true))). % 35.00/24.34 tff(c_6012, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdf_Alt), true)=true))). % 35.00/24.34 tff(c_22729, plain, (![X_419, Y_420]: (ifeq(iext(uri_rdfs_subPropertyOf, X_419, Y_420), true, icext(uri_rdf_Property, Y_420), true)=true))). % 35.00/24.34 tff(c_6312, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_member), true)=true))). % 35.00/24.34 tff(c_8093, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_rest), true)=true))). % 35.00/24.34 tff(c_4948, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_value), true)=true))). % 35.00/24.34 tff(c_3158, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_107), true, iext(Q_107, uri_rdf_first, uri_rdf_List), true)=true))). % 35.00/24.34 tff(c_5022, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_subClassOf), true)=true))). % 35.00/24.34 tff(c_7240, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_type), true)=true))). % 35.00/24.34 tff(c_22244, plain, (![X_409, Y_410]: (ifeq(iext(uri_rdfs_range, X_409, Y_410), true, icext(uri_rdf_Property, X_409), true)=true))). % 35.00/24.34 tff(c_8917, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_subject), true)=true))). % 35.00/24.34 tff(c_3149, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_107), true, iext(Q_107, uri_rdf_value, uri_rdfs_Resource), true)=true))). % 35.00/24.34 tff(c_7324, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdfs_Resource), true)=true))). % 35.00/24.34 tff(c_8916, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_subject), true)=true))). % 35.00/24.34 tff(c_22110, plain, (![X_401, Y_402]: (ifeq(iext(uri_rdf_subject, X_401, Y_402), true, icext(uri_rdfs_Statement, X_401), true)=true))). % 35.00/24.34 tff(c_10151, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdfs_Datatype), true)=true))). % 35.00/24.34 tff(c_3204, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_107), true, iext(Q_107, uri_rdfs_subPropertyOf, uri_rdf_Property), true)=true))). % 35.00/24.34 tff(c_8094, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_rest), true)=true))). % 35.00/24.34 tff(c_5571, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdfs_Literal), true)=true))). % 35.00/24.34 tff(c_21368, plain, (![X_392, Y_393]: (ifeq(iext(uri_rdfs_subClassOf, X_392, Y_393), true, icext(uri_rdfs_Class, X_392), true)=true))). % 35.00/24.34 tff(c_11372, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdfs_ContainerMembershipProperty), true)=true))). % 35.00/24.34 tff(c_7241, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_type), true)=true))). % 35.00/24.34 tff(c_3181, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_107), true, iext(Q_107, uri_rdfs_member, uri_rdfs_Resource), true)=true))). % 35.00/24.34 tff(c_5950, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_object), true)=true))). % 35.00/24.34 tff(c_21194, plain, (![X_384, Y_385]: (ifeq(iext(uri_rdf_rest, X_384, Y_385), true, icext(uri_rdf_List, X_384), true)=true))). % 35.00/24.34 tff(c_5951, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_object), true)=true))). % 35.00/24.34 tff(c_13557, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdfs_Class), true)=true))). % 35.00/24.34 tff(c_3155, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_107), true, iext(Q_107, uri_rdfs_subPropertyOf, uri_rdf_Property), true)=true))). % 35.00/24.34 tff(c_21045, plain, (![X_377, Y_378]: (ifeq(iext(uri_rdf_first, X_377, Y_378), true, icext(uri_rdf_List, X_377), true)=true))). % 35.00/24.34 tff(c_12887, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_subPropertyOf), true)=true))). % 35.00/24.34 tff(c_3199, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_107), true, iext(Q_107, uri_rdfs_subClassOf, uri_rdfs_Class), true)=true))). % 35.00/24.34 tff(c_6680, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdf_Property), true)=true))). % 35.00/24.34 tff(c_5861, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_owl_complementOf), true)=true))). % 35.00/24.34 tff(c_12779, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdfs_Container), true)=true))). % 35.00/24.34 tff(c_20888, plain, (![X_368, Y_369]: (ifeq(iext(uri_rdfs_label, X_368, Y_369), true, icext(uri_rdfs_Literal, Y_369), true)=true))). % 35.00/24.34 tff(c_10358, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf__1), true)=true))). % 35.00/24.34 tff(c_3177, plain, (![Q_107]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_107), true, iext(Q_107, uri_rdf_XMLLiteral, uri_rdfs_Literal), true)=true))). % 35.00/24.34 tff(c_4886, plain, (![C_19, X_139]: (ifeq(iext(uri_rdfs_domain, uri_rdf_type, C_19), true, icext(C_19, X_139), true)=true))). % 35.00/24.34 tff(c_4885, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_29), true, icext(C_29, uri_rdfs_Resource), true)=true))). % 35.00/24.34 tff(c_2199, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_93), true, icext(C_93, uri_rdf_Alt), true)=true))). % 35.00/24.34 tff(c_20066, plain, (![X_352, Y_353]: (ifeq(iext(uri_rdfs_range, X_352, Y_353), true, icext(uri_rdfs_Class, Y_353), true)=true))). % 35.00/24.34 tff(c_2155, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_93), true, icext(C_93, uri_rdfs_isDefinedBy), true)=true))). % 35.00/24.34 tff(c_2172, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_93), true, icext(C_93, uri_rdfs_isDefinedBy), true)=true))). % 35.00/24.34 tff(c_2524, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdfs_range, C_97), true, icext(C_97, uri_rdf_Property), true)=true))). % 35.00/24.34 tff(c_2176, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_93), true, icext(C_93, uri_rdf__3), true)=true))). % 35.00/24.34 tff(c_2161, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_93), true, icext(C_93, uri_rdfs_isDefinedBy), true)=true))). % 35.00/24.34 tff(c_2554, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdf_rest, C_97), true, icext(C_97, sK2_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l2), true)=true))). % 35.00/24.34 tff(c_2148, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_93), true, icext(C_93, uri_rdfs_subPropertyOf), true)=true))). % 35.00/24.34 tff(c_2523, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdfs_range, C_97), true, icext(C_97, uri_rdf_List), true)=true))). % 35.00/24.34 tff(c_2160, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_93), true, icext(C_93, uri_rdf__2), true)=true))). % 35.00/24.34 tff(c_2185, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_93), true, icext(C_93, uri_rdf__2), true)=true))). % 35.00/24.34 tff(c_2175, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_owl_intersectionOf, C_93), true, icext(C_93, sK3_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_x), true)=true))). % 35.00/24.34 tff(c_2139, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_93), true, icext(C_93, uri_rdfs_comment), true)=true))). % 35.00/24.34 tff(c_2205, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_93), true, icext(C_93, uri_rdfs_subPropertyOf), true)=true))). % 35.00/24.34 tff(c_19639, plain, (![X_333, Y_334]: (ifeq(iext(uri_rdf_predicate, X_333, Y_334), true, icext(uri_rdfs_Statement, X_333), true)=true))). % 35.00/24.34 tff(c_2143, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_93), true, icext(C_93, uri_rdfs_Datatype), true)=true))). % 35.00/24.34 tff(c_2158, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdf_first, C_93), true, icext(C_93, sK2_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l2), true)=true))). % 35.00/24.34 tff(c_2147, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_93), true, icext(C_93, uri_rdf_rest), true)=true))). % 35.00/24.34 tff(c_2543, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_97), true, icext(C_97, uri_rdfs_Class), true)=true))). % 35.00/24.34 tff(c_2137, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_93), true, icext(C_93, uri_rdf_object), true)=true))). % 35.00/24.34 tff(c_2162, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_owl_complementOf, C_93), true, icext(C_93, sK1_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_y), true)=true))). % 35.00/24.34 tff(c_2194, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_93), true, icext(C_93, uri_rdfs_seeAlso), true)=true))). % 35.00/24.34 tff(c_2178, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_93), true, icext(C_93, uri_rdfs_member), true)=true))). % 35.00/24.34 tff(c_2181, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_93), true, icext(C_93, uri_rdfs_subClassOf), true)=true))). % 35.00/24.34 tff(c_2547, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_97), true, icext(C_97, uri_rdfs_seeAlso), true)=true))). % 35.00/24.34 tff(c_2201, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_93), true, icext(C_93, uri_rdf_type), true)=true))). % 35.00/24.34 tff(c_19428, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_comment, uri_rdfs_comment)=true)). % 35.00/24.34 tff(c_19259, plain, (ip(uri_rdfs_comment)=true)). % 35.00/24.34 tff(c_19198, plain, (iext(uri_rdf_type, uri_rdfs_comment, uri_rdf_Property)=true)). % 35.00/24.34 tff(c_19142, plain, (icext(uri_rdf_Property, uri_rdfs_comment)=true)). % 35.00/24.34 tff(c_2195, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_93), true, icext(C_93, uri_rdfs_comment), true)=true))). % 35.00/24.34 tff(c_2171, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_93), true, icext(C_93, uri_rdfs_ContainerMembershipProperty), true)=true))). % 35.00/24.34 tff(c_2170, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_93), true, icext(C_93, uri_rdf_value), true)=true))). % 35.00/24.34 tff(c_2196, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_93), true, icext(C_93, uri_rdf_subject), true)=true))). % 35.00/24.34 tff(c_2532, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdf_first, C_97), true, icext(C_97, sK1_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_y), true)=true))). % 35.00/24.34 tff(c_2173, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_93), true, icext(C_93, uri_rdf_XMLLiteral), true)=true))). % 35.00/24.34 tff(c_18390, plain, (![X_308, Y_309]: (ifeq(iext(uri_rdf_type, X_308, Y_309), true, icext(uri_rdfs_Class, Y_309), true)=true))). % 35.00/24.34 tff(c_2574, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdfs_domain, C_97), true, icext(C_97, uri_rdfs_Class), true)=true))). % 35.00/24.34 tff(c_2538, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_owl_complementOf, C_97), true, icext(C_97, uri_ex_A), true)=true))). % 35.00/24.34 tff(c_2134, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_93), true, icext(C_93, uri_rdf__1), true)=true))). % 35.00/24.34 tff(c_2140, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_93), true, icext(C_93, uri_rdfs_domain), true)=true))). % 35.00/24.34 tff(c_2527, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdfs_domain, C_97), true, icext(C_97, uri_rdf_List), true)=true))). % 35.00/24.34 tff(c_2186, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_93), true, icext(C_93, uri_rdf_first), true)=true))). % 35.00/24.34 tff(c_2206, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_93), true, icext(C_93, uri_rdf_subject), true)=true))). % 35.00/24.34 tff(c_2569, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdfs_range, C_97), true, icext(C_97, uri_rdfs_Literal), true)=true))). % 35.00/24.34 tff(c_18134, plain, (![X_33]: (ifeq(icext(uri_rdf_List, X_33), true, icext(uri_rdf_List, X_33), true)=true))). % 35.00/24.34 tff(c_18078, plain, (iext(uri_rdfs_subClassOf, uri_rdf_List, uri_rdf_List)=true)). % 35.00/24.34 tff(c_17924, plain, (iext(uri_rdfs_subClassOf, uri_rdf_List, uri_rdfs_Resource)=true)). % 35.00/24.34 tff(c_17876, plain, (iext(uri_rdf_type, uri_rdf_List, uri_rdfs_Class)=true)). % 35.00/24.34 tff(c_17717, plain, (ic(uri_rdf_List)=true)). % 35.00/24.34 tff(c_17626, plain, (icext(uri_rdfs_Class, uri_rdf_List)=true)). % 35.00/24.34 tff(c_2159, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_93), true, icext(C_93, uri_rdfs_Seq), true)=true))). % 35.00/24.34 tff(c_2578, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_97), true, icext(C_97, uri_rdf_List), true)=true))). % 35.00/24.34 tff(c_2192, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_93), true, icext(C_93, uri_rdf__1), true)=true))). % 35.00/24.34 tff(c_17374, plain, (![X_33]: (ifeq(icext(uri_owl_Class, X_33), true, icext(uri_owl_Class, X_33), true)=true))). % 35.00/24.34 tff(c_17384, plain, (iext(uri_rdfs_subClassOf, uri_owl_Class, uri_rdfs_Resource)=true)). % 35.00/24.34 tff(c_2208, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_93), true, icext(C_93, uri_rdf_predicate), true)=true))). % 35.00/24.34 tff(c_17318, plain, (iext(uri_rdfs_subClassOf, uri_owl_Class, uri_owl_Class)=true)). % 35.00/24.34 tff(c_17271, plain, (iext(uri_rdf_type, uri_owl_Class, uri_rdfs_Class)=true)). % 35.00/24.34 tff(c_2133, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_93), true, icext(C_93, uri_rdfs_range), true)=true))). % 35.00/24.34 tff(c_17095, plain, (ic(uri_owl_Class)=true)). % 35.00/24.34 tff(c_17029, plain, (icext(uri_rdfs_Class, uri_owl_Class)=true)). % 35.00/24.34 tff(c_2586, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_97), true, icext(C_97, uri_owl_Class), true)=true))). % 35.00/24.34 tff(c_2182, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_93), true, icext(C_93, uri_rdfs_member), true)=true))). % 35.00/24.34 tff(c_2174, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_93), true, icext(C_93, uri_rdfs_domain), true)=true))). % 35.00/24.34 tff(c_15780, plain, (![X_33]: (ifeq(icext(sK3_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_x, X_33), true, icext(sK3_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_x, X_33), true)=true))). % 35.00/24.34 tff(c_15847, plain, (![X_33]: (ifeq(icext(uri_rdfs_Statement, X_33), true, icext(uri_rdfs_Statement, X_33), true)=true))). % 35.00/24.34 tff(c_16456, plain, (![X_273, Y_274]: (ifeq(iext(uri_rdfs_comment, X_273, Y_274), true, icext(uri_rdfs_Literal, Y_274), true)=true))). % 35.00/24.34 tff(c_11374, plain, (![X_33]: (ifeq(icext(uri_rdfs_ContainerMembershipProperty, X_33), true, icext(uri_rdfs_ContainerMembershipProperty, X_33), true)=true))). % 35.00/24.34 tff(c_5666, plain, (![X_33]: (ifeq(icext(uri_rdf_XMLLiteral, X_33), true, icext(uri_rdf_XMLLiteral, X_33), true)=true))). % 35.00/24.34 tff(c_10153, plain, (![X_33]: (ifeq(icext(uri_rdfs_Datatype, X_33), true, icext(uri_rdfs_Datatype, X_33), true)=true))). % 35.00/24.34 tff(c_2526, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_97), true, icext(C_97, uri_rdfs_Datatype), true)=true))). % 35.00/24.34 tff(c_5086, plain, (![X_33]: (ifeq(icext(uri_rdf_Property, X_33), true, icext(uri_rdf_Property, X_33), true)=true))). % 35.00/24.34 tff(c_5572, plain, (![X_33]: (ifeq(icext(uri_rdfs_Literal, X_33), true, icext(uri_rdfs_Literal, X_33), true)=true))). % 35.00/24.34 tff(c_13558, plain, (![X_33]: (ifeq(icext(uri_rdfs_Class, X_33), true, icext(uri_rdfs_Class, X_33), true)=true))). % 35.00/24.34 tff(c_14074, plain, (![X_33]: (ifeq(icext(uri_rdfs_Container, X_33), true, icext(uri_rdfs_Container, X_33), true)=true))). % 35.00/24.34 tff(c_8461, plain, (![X_33]: (ifeq(icext(uri_rdf_Bag, X_33), true, icext(uri_rdf_Bag, X_33), true)=true))). % 35.00/24.34 tff(c_7898, plain, (![X_33]: (ifeq(icext(uri_rdfs_Seq, X_33), true, icext(uri_rdfs_Seq, X_33), true)=true))). % 35.00/24.34 tff(c_6014, plain, (![X_33]: (ifeq(icext(uri_rdf_Alt, X_33), true, icext(uri_rdf_Alt, X_33), true)=true))). % 35.00/24.34 tff(c_16387, plain, (iext(uri_rdf_type, uri_rdfs_Resource, uri_rdfs_Class)=true)). % 35.00/24.34 tff(c_16322, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_predicate, uri_rdf_predicate)=true)). % 35.00/24.34 tff(c_16257, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_label, uri_rdfs_label)=true)). % 35.00/24.34 tff(c_16182, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Resource, uri_rdfs_Resource)=true)). % 35.00/24.34 tff(c_2207, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_93), true, icext(C_93, uri_rdf_Bag), true)=true))). % 35.00/24.34 tff(c_16001, plain, (icext(uri_rdf_Property, uri_rdfs_member)=true)). % 35.00/24.34 tff(c_15947, plain, (iext(uri_rdf_type, uri_rdfs_member, uri_rdf_Property)=true)). % 35.00/24.34 tff(c_15878, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_member, uri_rdfs_member)=true)). % 35.00/24.34 tff(c_2550, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_owl_intersectionOf, C_97), true, icext(C_97, sK4_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l1), true)=true))). % 35.00/24.34 tff(c_15791, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Statement, uri_rdfs_Statement)=true)). % 35.00/24.34 tff(c_15724, plain, (iext(uri_rdfs_subClassOf, sK3_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_x, sK3_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_x)=true)). % 35.00/24.34 tff(c_15601, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Statement, uri_rdfs_Resource)=true)). % 35.00/24.34 tff(c_15476, plain, (iext(uri_rdfs_subClassOf, sK3_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_x, uri_rdfs_Resource)=true)). % 35.00/24.34 tff(c_2190, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_93), true, icext(C_93, uri_rdfs_seeAlso), true)=true))). % 35.00/24.34 tff(c_15401, plain, (iext(uri_rdf_type, uri_rdfs_Class, uri_rdfs_Class)=true)). % 35.00/24.34 tff(c_2141, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_93), true, icext(C_93, uri_rdf_value), true)=true))). % 35.00/24.34 tff(c_15323, plain, (iext(uri_rdf_type, uri_rdf_XMLLiteral, uri_rdfs_Class)=true)). % 35.00/24.34 tff(c_15276, plain, (iext(uri_rdf_type, uri_rdf_Alt, uri_rdfs_Class)=true)). % 35.00/24.34 tff(c_2153, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_93), true, icext(C_93, uri_rdf_rest), true)=true))). % 35.00/24.34 tff(c_15203, plain, (iext(uri_rdf_type, uri_rdfs_Datatype, uri_rdfs_Class)=true)). % 35.00/24.34 tff(c_15154, plain, (iext(uri_rdf_type, uri_rdfs_Container, uri_rdfs_Class)=true)). % 35.00/24.34 tff(c_2146, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_93), true, icext(C_93, uri_rdf__3), true)=true))). % 35.00/24.34 tff(c_15076, plain, (iext(uri_rdf_type, uri_rdfs_Seq, uri_rdfs_Class)=true)). % 35.00/24.34 tff(c_15028, plain, (iext(uri_rdf_type, uri_rdf_Bag, uri_rdfs_Class)=true)). % 35.00/24.34 tff(c_2548, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_97), true, icext(C_97, uri_rdfs_Literal), true)=true))). % 35.00/24.34 tff(c_14953, plain, (iext(uri_rdf_type, uri_rdfs_Literal, uri_rdfs_Class)=true)). % 35.00/24.34 tff(c_14906, plain, (iext(uri_rdf_type, uri_rdfs_ContainerMembershipProperty, uri_rdfs_Class)=true)). % 35.00/24.34 tff(c_14858, plain, (iext(uri_rdf_type, sK3_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_x, uri_rdfs_Class)=true)). % 35.00/24.34 tff(c_14811, plain, (iext(uri_rdf_type, sK2_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l2, uri_rdf_List)=true)). % 35.00/24.35 tff(c_14764, plain, (iext(uri_rdf_type, sK4_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l1, uri_rdf_List)=true)). % 35.00/24.35 tff(c_14697, plain, (ip(uri_rdf_predicate)=true)). % 35.00/24.35 tff(c_2546, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_97), true, icext(C_97, uri_rdf_Property), true)=true))). % 35.00/24.35 tff(c_14640, plain, (iext(uri_rdf_type, uri_rdf_predicate, uri_rdf_Property)=true)). % 35.00/24.35 tff(c_14593, plain, (iext(uri_rdf_type, uri_rdfs_Statement, uri_rdfs_Class)=true)). % 35.00/24.35 tff(c_14522, plain, (ip(uri_rdfs_label)=true)). % 35.00/24.35 tff(c_14465, plain, (iext(uri_rdf_type, uri_rdfs_label, uri_rdf_Property)=true)). % 35.00/24.35 tff(c_3428, plain, (![S_5, O_6]: (ifeq(iext(uri_rdfs_subPropertyOf, S_5, O_6), true, true, true)=true))). % 35.00/24.35 tff(c_2625, plain, (![S_5, O_6]: (ifeq(iext(uri_rdfs_subClassOf, S_5, O_6), true, true, true)=true))). % 35.00/24.35 tff(c_2512, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_97), true, icext(C_97, uri_rdfs_ContainerMembershipProperty), true)=true))). % 35.00/24.35 tff(c_14015, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Container, uri_rdfs_Container)=true)). % 35.00/24.35 tff(c_13876, plain, (icext(uri_rdf_Property, uri_owl_complementOf)=true)). % 35.00/24.35 tff(c_2183, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_93), true, icext(C_93, uri_rdfs_label), true)=true))). % 35.00/24.35 tff(c_13797, plain, (iext(uri_rdf_type, uri_owl_complementOf, uri_rdf_Property)=true)). % 35.00/24.35 tff(c_13499, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Class, uri_rdfs_Class)=true)). % 35.00/24.35 tff(c_2585, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdf_rest, C_97), true, icext(C_97, uri_rdf_nil), true)=true))). % 35.00/24.35 tff(c_12976, plain, (icext(uri_rdf_Property, uri_owl_intersectionOf)=true)). % 35.00/24.35 tff(c_12897, plain, (iext(uri_rdf_type, uri_owl_intersectionOf, uri_rdf_Property)=true)). % 35.00/24.35 tff(c_2151, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_93), true, icext(C_93, uri_rdf_first), true)=true))). % 35.00/24.35 tff(c_12829, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf)=true)). % 35.00/24.35 tff(c_12724, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Container, uri_rdfs_Resource)=true)). % 35.00/24.35 tff(c_2565, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdfs_domain, C_97), true, icext(C_97, uri_rdfs_Resource), true)=true))). % 35.00/24.35 tff(c_12373, plain, (ic(sK3_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_x)=true)). % 35.00/24.35 tff(c_12315, plain, (icext(uri_rdfs_Class, sK3_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_x)=true)). % 35.00/24.35 tff(c_2566, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_97), true, icext(C_97, sK3_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_x), true)=true))). % 35.00/24.35 tff(c_11871, plain, (iext(uri_rdf_type, uri_rdfs_subClassOf, uri_rdf_Property)=true)). % 35.00/24.35 tff(c_11736, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, uri_rdfs_Resource)=true)). % 35.00/24.35 tff(c_2165, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdf_first, C_93), true, icext(C_93, sK4_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l1), true)=true))). % 35.00/24.35 tff(c_11453, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf__1, uri_rdfs_member)=true)). % 35.00/24.35 tff(c_11384, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_seeAlso, uri_rdfs_seeAlso)=true)). % 35.00/24.35 tff(c_11318, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, uri_rdfs_ContainerMembershipProperty)=true)). % 35.00/24.35 tff(c_1755, plain, (![S_5, O_6]: (ifeq(iext(uri_rdfs_range, S_5, O_6), true, true, true)=true))). % 35.00/24.35 tff(c_11111, plain, (ic(uri_rdfs_Statement)=true)). % 35.00/24.35 tff(c_11054, plain, (icext(uri_rdfs_Class, uri_rdfs_Statement)=true)). % 35.00/24.35 tff(c_2584, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdfs_domain, C_97), true, icext(C_97, uri_rdfs_Statement), true)=true))). % 35.00/24.35 tff(c_10912, plain, (icext(uri_rdf_Property, uri_rdfs_isDefinedBy)=true)). % 35.00/24.35 tff(c_10858, plain, (iext(uri_rdf_type, uri_rdfs_isDefinedBy, uri_rdf_Property)=true)). % 35.00/24.35 tff(c_3230, plain, (![S_5, O_6]: (ifeq(iext(uri_rdf_object, S_5, O_6), true, true, true)=true))). % 35.00/24.35 tff(c_10397, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, uri_rdfs_Resource)=true)). % 35.00/24.35 tff(c_10308, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf__1, uri_rdf__1)=true)). % 35.00/24.35 tff(c_10182, plain, (icext(uri_rdf_Property, uri_rdfs_label)=true)). % 35.00/24.35 tff(c_2157, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_93), true, icext(C_93, uri_rdfs_label), true)=true))). % 35.00/24.35 tff(c_10094, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, uri_rdfs_Datatype)=true)). % 35.00/24.35 tff(c_9796, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_first, uri_rdf_first)=true)). % 35.00/24.35 tff(c_1175, plain, (![S_81, O_82]: (ifeq(iext(uri_rdf_rest, S_81, O_82), true, true, true)=true))). % 35.00/24.35 tff(c_9635, plain, (icext(uri_rdf_List, sK2_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l2)=true)). % 35.00/24.35 tff(c_2209, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdf_rest, C_93), true, icext(C_93, sK2_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l2), true)=true))). % 35.00/24.35 tff(c_9573, plain, (icext(uri_rdf_Property, uri_rdfs_subPropertyOf)=true)). % 35.00/24.35 tff(c_9519, plain, (iext(uri_rdf_type, uri_rdfs_subPropertyOf, uri_rdf_Property)=true)). % 35.00/24.35 tff(c_2144, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_93), true, icext(C_93, uri_rdfs_range), true)=true))). % 35.00/24.35 tff(c_9332, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Seq, uri_rdfs_Resource)=true)). % 35.00/24.35 tff(c_2188, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_93), true, icext(C_93, uri_rdf_type), true)=true))). % 35.00/24.35 tff(c_8927, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf__3, uri_rdfs_member)=true)). % 35.00/24.35 tff(c_8863, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_subject, uri_rdf_subject)=true)). % 35.00/24.35 tff(c_8402, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Bag, uri_rdf_Bag)=true)). % 35.00/24.35 tff(c_8358, plain, (icext(uri_rdf_List, sK4_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l1)=true)). % 35.00/24.35 tff(c_2179, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdf_rest, C_93), true, icext(C_93, sK4_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l1), true)=true))). % 35.00/24.35 tff(c_8292, plain, (icext(uri_rdf_Property, uri_rdfs_domain)=true)). % 35.00/24.35 tff(c_8238, plain, (iext(uri_rdf_type, uri_rdfs_domain, uri_rdf_Property)=true)). % 35.00/24.35 tff(c_3305, plain, (![S_5, O_6]: (ifeq(iext(uri_owl_complementOf, S_5, O_6), true, true, true)=true))). % 35.00/24.35 tff(c_8104, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Alt, uri_rdfs_Resource)=true)). % 35.00/24.35 tff(c_8043, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_rest, uri_rdf_rest)=true)). % 35.00/24.35 tff(c_7954, plain, (iext(uri_rdfs_subPropertyOf, uri_owl_intersectionOf, uri_owl_intersectionOf)=true)). % 35.00/24.35 tff(c_7846, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Seq, uri_rdfs_Seq)=true)). % 35.00/24.35 tff(c_7711, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, uri_rdfs_domain)=true)). % 35.00/24.35 tff(c_7608, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_range, uri_rdfs_range)=true)). % 35.00/24.35 tff(c_2509, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdfs_domain, C_97), true, icext(C_97, uri_rdf_Property), true)=true))). % 35.00/24.35 tff(c_1710, plain, (![S_5, O_6]: (ifeq(iext(uri_rdfs_domain, S_5, O_6), true, true, true)=true))). % 35.00/24.35 tff(c_7251, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Bag, uri_rdfs_Resource)=true)). % 35.00/24.35 tff(c_2541, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdf_first, C_97), true, icext(C_97, uri_ex_A), true)=true))). % 35.00/24.35 tff(c_7190, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_type, uri_rdf_type)=true)). % 35.00/24.35 tff(c_6953, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Literal, uri_rdfs_Resource)=true)). % 35.00/24.35 tff(c_6902, plain, (icext(uri_rdf_Property, uri_rdfs_seeAlso)=true)). % 35.00/24.35 tff(c_6820, plain, (iext(uri_rdf_type, uri_rdfs_seeAlso, uri_rdf_Property)=true)). % 35.00/24.35 tff(c_6604, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Property, uri_rdfs_Resource)=true)). % 35.00/24.35 tff(c_2575, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdfs_range, C_97), true, icext(C_97, uri_rdfs_Class), true)=true))). % 35.00/24.35 tff(c_6536, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf__2, uri_rdf__2)=true)). % 35.00/24.35 tff(c_2542, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_97), true, icext(C_97, uri_rdf_Property), true)=true))). % 35.00/24.35 tff(c_6443, plain, (icext(uri_rdf_Property, uri_rdfs_range)=true)). % 35.00/24.35 tff(c_6386, plain, (iext(uri_rdf_type, uri_rdfs_range, uri_rdf_Property)=true)). % 35.00/24.35 tff(c_6322, plain, (ip(uri_rdfs_member)=true)). % 35.00/24.35 tff(c_2577, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdfs_range, C_97), true, icext(C_97, uri_rdfs_Resource), true)=true))). % 35.00/24.35 tff(c_6258, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf__2, uri_rdfs_member)=true)). % 35.00/24.35 tff(c_6194, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf__3, uri_rdf__3)=true)). % 35.00/24.35 tff(c_2573, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_97), true, icext(C_97, uri_rdfs_Container), true)=true))). % 35.00/24.35 tff(c_6042, plain, (icext(uri_rdf_Property, uri_rdf_predicate)=true)). % 35.00/24.35 tff(c_2202, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_93), true, icext(C_93, uri_rdf_predicate), true)=true))). % 35.00/24.35 tff(c_5962, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Alt, uri_rdf_Alt)=true)). % 35.00/24.35 tff(c_5900, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_object, uri_rdf_object)=true)). % 35.00/24.35 tff(c_2520, plain, (![C_97]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_97), true, icext(C_97, uri_rdfs_Class), true)=true))). % 35.00/24.35 tff(c_5810, plain, (iext(uri_rdfs_subPropertyOf, uri_owl_complementOf, uri_owl_complementOf)=true)). % 35.00/24.35 tff(c_5755, plain, (icext(uri_rdf_Property, uri_rdfs_subClassOf)=true)). % 35.00/24.35 tff(c_2200, plain, (![C_93]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_93), true, icext(C_93, uri_rdfs_subClassOf), true)=true))). % 35.00/24.35 tff(c_5676, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_isDefinedBy, uri_rdfs_isDefinedBy)=true)). % 35.00/24.35 tff(c_5614, plain, (iext(uri_rdfs_subClassOf, uri_rdf_XMLLiteral, uri_rdf_XMLLiteral)=true)). % 35.00/24.35 tff(c_1821, plain, (![X_90]: (ifeq(icext(uri_rdf_Bag, X_90), true, icext(uri_rdfs_Container, X_90), true)=true))). % 35.00/24.35 tff(c_5517, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Literal, uri_rdfs_Literal)=true)). % 35.00/24.35 tff(c_1818, plain, (![X_90]: (ifeq(icext(uri_rdfs_ContainerMembershipProperty, X_90), true, icext(uri_rdf_Property, X_90), true)=true))). % 35.00/24.35 tff(c_5398, plain, (iext(uri_rdfs_subClassOf, uri_rdf_XMLLiteral, uri_rdfs_Resource)=true)). % 35.00/24.35 tff(c_5344, plain, (icext(uri_rdfs_Class, uri_rdfs_Resource)=true)). % 35.00/24.35 tff(c_1817, plain, (![X_90]: (ifeq(icext(uri_rdfs_Seq, X_90), true, icext(uri_rdfs_Container, X_90), true)=true))). % 35.00/24.35 tff(c_1816, plain, (![X_90]: (ifeq(icext(uri_rdfs_Datatype, X_90), true, icext(uri_rdfs_Class, X_90), true)=true))). % 35.00/24.35 tff(c_5186, plain, (ic(uri_rdfs_Resource)=true)). % 35.00/24.35 tff(c_5125, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Class, uri_rdfs_Resource)=true)). % 35.00/24.35 tff(c_1611, plain, (![S_5, O_6]: (ifeq(iext(uri_owl_intersectionOf, S_5, O_6), true, true, true)=true))). % 35.00/24.35 tff(c_1820, plain, (![X_90]: (ifeq(icext(uri_rdf_Alt, X_90), true, icext(uri_rdfs_Container, X_90), true)=true))). % 35.00/24.35 tff(c_5034, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Property, uri_rdf_Property)=true)). % 35.00/24.35 tff(c_4972, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, uri_rdfs_subClassOf)=true)). % 35.00/24.35 tff(c_1819, plain, (![X_90]: (ifeq(icext(uri_rdf_XMLLiteral, X_90), true, icext(uri_rdfs_Literal, X_90), true)=true))). % 35.00/24.35 tff(c_4897, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_value, uri_rdf_value)=true)). % 35.00/24.35 tff(c_4844, plain, (![X_138]: (iext(uri_rdf_type, X_138, uri_rdfs_Resource)=true))). % 35.00/24.35 tff(c_2576, plain, (![X_98, Y_99]: (ifeq(iext(uri_rdf_predicate, X_98, Y_99), true, true, true)=true))). % 35.00/24.35 tff(c_2138, plain, (![X_94, Y_95]: (ifeq(iext(uri_rdfs_comment, X_94, Y_95), true, true, true)=true))). % 35.00/24.35 tff(c_2187, plain, (![X_94, Y_95]: (ifeq(iext(uri_rdf_type, X_94, Y_95), true, true, true)=true))). % 35.00/24.35 tff(c_2561, plain, (![X_98, Y_99]: (ifeq(iext(uri_rdf_first, X_98, Y_99), true, true, true)=true))). % 35.00/24.35 tff(c_2534, plain, (![X_98, Y_99]: (ifeq(iext(uri_rdf__2, X_98, Y_99), true, true, true)=true))). % 35.00/24.35 tff(c_2536, plain, (![X_98, Y_99]: (ifeq(iext(uri_rdfs_isDefinedBy, X_98, Y_99), true, true, true)=true))). % 35.00/24.35 tff(c_2169, plain, (![X_94, Y_95]: (ifeq(iext(uri_rdf_value, X_94, Y_95), true, true, true)=true))). % 35.00/24.35 tff(c_2156, plain, (![X_94, Y_95]: (ifeq(iext(uri_rdfs_label, X_94, Y_95), true, true, true)=true))). % 35.00/24.35 tff(c_2567, plain, (![X_98, Y_99]: (ifeq(iext(uri_rdfs_seeAlso, X_98, Y_99), true, true, true)=true))). % 35.00/24.35 tff(c_2581, plain, (![X_98, Y_99]: (ifeq(iext(uri_rdf_subject, X_98, Y_99), true, true, true)=true))). % 35.00/24.35 tff(c_4640, plain, (icext(uri_rdfs_Class, uri_rdfs_Datatype)=true)). % 35.00/24.35 tff(c_2191, plain, (![X_94, Y_95]: (ifeq(iext(uri_rdf__1, X_94, Y_95), true, true, true)=true))). % 35.00/24.35 tff(c_4587, plain, (icext(uri_rdfs_Class, uri_rdf_XMLLiteral)=true)). % 35.00/24.35 tff(c_4534, plain, (icext(uri_rdfs_Class, uri_rdfs_ContainerMembershipProperty)=true)). % 35.00/24.35 tff(c_2145, plain, (![X_94, Y_95]: (ifeq(iext(uri_rdf__3, X_94, Y_95), true, true, true)=true))). % 35.00/24.35 tff(c_4491, plain, (icext(uri_rdfs_Class, uri_rdfs_Class)=true)). % 35.00/24.35 tff(c_4448, plain, (icext(uri_rdfs_Class, uri_rdfs_Seq)=true)). % 35.00/24.35 tff(c_4403, plain, (icext(uri_rdfs_Class, uri_rdf_Bag)=true)). % 35.00/24.35 tff(c_4354, plain, (icext(uri_rdfs_Class, uri_rdfs_Container)=true)). % 35.00/24.35 tff(c_4303, plain, (icext(uri_rdfs_Class, uri_rdf_Alt)=true)). % 35.00/24.35 tff(c_2177, plain, (![X_94, Y_95]: (ifeq(iext(uri_rdfs_member, X_94, Y_95), true, true, true)=true))). % 35.00/24.35 tff(c_4252, plain, (icext(uri_rdfs_Class, uri_rdfs_Literal)=true)). % 35.00/24.35 tff(c_4212, plain, (icext(uri_rdf_Property, uri_rdf_object)=true)). % 35.00/24.35 tff(c_4173, plain, (icext(uri_rdf_Property, uri_rdf_rest)=true)). % 35.00/24.35 tff(c_4131, plain, (icext(uri_rdf_Property, uri_rdf_subject)=true)). % 35.00/24.35 tff(c_4091, plain, (icext(uri_rdf_Property, uri_rdf_type)=true)). % 35.00/24.35 tff(c_4052, plain, (icext(uri_rdf_Property, uri_rdf_value)=true)). % 35.00/24.35 tff(c_4004, plain, (icext(uri_rdf_Property, uri_rdf_first)=true)). % 35.00/24.35 tff(c_3965, plain, (icext(uri_owl_Class, uri_ex_B)=true)). % 35.00/24.35 tff(c_3922, plain, (icext(uri_rdfs_Datatype, uri_rdf_XMLLiteral)=true)). % 35.00/24.35 tff(c_3881, plain, (icext(uri_rdf_Property, uri_rdf__3)=true)). % 35.00/24.35 tff(c_3844, plain, (icext(uri_owl_Class, uri_ex_A)=true)). % 35.00/24.35 tff(c_3803, plain, (icext(uri_rdfs_ContainerMembershipProperty, uri_rdf__3)=true)). % 35.00/24.35 tff(c_3765, plain, (icext(uri_rdf_List, uri_rdf_nil)=true)). % 35.00/24.35 tff(c_3724, plain, (icext(uri_rdf_Property, uri_rdf__1)=true)). % 35.00/24.35 tff(c_3674, plain, (icext(uri_rdfs_Class, uri_rdf_Property)=true)). % 35.00/24.35 tff(c_3626, plain, (icext(uri_rdfs_ContainerMembershipProperty, uri_rdf__2)=true)). % 35.00/24.35 tff(c_3585, plain, (icext(uri_rdfs_ContainerMembershipProperty, uri_rdf__1)=true)). % 35.00/24.35 tff(c_3549, plain, (icext(uri_rdf_Property, uri_rdf__2)=true)). % 35.00/24.35 tff(c_3498, plain, (icext(sK3_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_x, uri_ex_w)=true)). % 35.00/24.35 tff(c_3455, plain, (ic(uri_rdfs_ContainerMembershipProperty)=true)). % 35.00/24.35 tff(c_3416, plain, (ip(uri_rdfs_subPropertyOf)=true)). % 35.00/24.35 tff(c_3368, plain, (ip(uri_rdfs_seeAlso)=true)). % 35.00/24.35 tff(c_3332, plain, (ip(uri_rdfs_isDefinedBy)=true)). % 35.00/24.35 tff(c_3293, plain, (ip(uri_owl_complementOf)=true)). % 35.00/24.35 tff(c_3257, plain, (ic(uri_rdfs_Seq)=true)). % 35.00/24.35 tff(c_3216, plain, (ip(uri_rdf_object)=true)). % 35.00/24.35 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))). % 35.00/24.35 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))). % 35.00/24.35 tff(c_2613, plain, (ip(uri_rdfs_subClassOf)=true)). % 35.00/24.35 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))). % 35.00/24.35 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))). % 35.00/24.35 tff(c_1852, plain, (ic(uri_rdf_Property)=true)). % 35.00/24.35 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))). % 35.00/24.35 tff(c_1782, plain, (ic(uri_rdf_XMLLiteral)=true)). % 35.00/24.35 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))). % 35.00/24.35 tff(c_1733, plain, (ip(uri_rdfs_range)=true)). % 35.00/24.35 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))). % 35.00/24.35 tff(c_1698, plain, (ip(uri_rdfs_domain)=true)). % 35.00/24.35 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))). % 35.00/24.35 tff(c_1599, plain, (ip(uri_owl_intersectionOf)=true)). % 35.00/24.35 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))). % 35.00/24.35 tff(c_1553, plain, (ip(uri_rdf__1)=true)). % 35.00/24.35 tff(c_1518, plain, (ic(uri_rdfs_Datatype)=true)). % 35.00/24.35 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))). % 35.00/24.35 tff(c_1419, plain, (ic(uri_rdf_Alt)=true)). % 35.00/24.35 tff(c_4, plain, (![P_4, S_5, O_6]: (ifeq(iext(P_4, S_5, O_6), true, ip(P_4), true)=true))). % 35.00/24.35 tff(c_1102, plain, (ic(uri_rdf_Bag)=true)). % 35.00/24.35 tff(c_162, plain, (![P_43, Q_44]: (ifeq(iext(uri_rdfs_subPropertyOf, P_43, Q_44), true, ip(Q_44), true)=true))). % 35.00/24.35 tff(c_1028, plain, (ic(uri_rdfs_Class)=true)). % 35.00/24.35 tff(c_152, plain, (![C_37, D_38]: (ifeq(iext(uri_rdfs_subClassOf, C_37, D_38), true, ic(C_37), true)=true))). % 35.00/24.35 tff(c_956, plain, (ic(uri_rdfs_Literal)=true)). % 35.00/24.35 tff(c_28, plain, (![P_9]: (ifeq(ip(P_9), true, iext(uri_rdf_type, P_9, uri_rdf_Property), true)=true))). % 35.00/24.35 tff(c_856, plain, (ip(uri_rdf_type)=true)). % 35.00/24.35 tff(c_170, plain, (![P_51]: (ifeq(ip(P_51), true, iext(uri_rdfs_subPropertyOf, P_51, P_51), true)=true))). % 35.00/24.35 tff(c_799, plain, (ic(uri_rdfs_Container)=true)). % 35.00/24.35 tff(c_775, plain, (ip(uri_rdf__3)=true)). % 35.00/24.35 tff(c_164, plain, (![P_45, Q_46]: (ifeq(iext(uri_rdfs_subPropertyOf, P_45, Q_46), true, ip(P_45), true)=true))). % 35.00/24.35 tff(c_729, plain, (ip(uri_rdf_first)=true)). % 35.00/24.35 tff(c_150, plain, (![C_35, D_36]: (ifeq(iext(uri_rdfs_subClassOf, C_35, D_36), true, ic(D_36), true)=true))). % 35.00/24.35 tff(c_683, plain, (ip(uri_rdf_value)=true)). % 35.00/24.35 tff(c_647, plain, (ip(uri_rdf_subject)=true)). % 35.00/24.35 tff(c_156, plain, (![C_39]: (ifeq(ic(C_39), true, iext(uri_rdfs_subClassOf, C_39, C_39), true)=true))). % 35.00/24.35 tff(c_619, plain, (ip(uri_rdf_rest)=true)). % 35.00/24.35 tff(c_58, plain, (![C_15]: (ifeq(ic(C_15), true, iext(uri_rdfs_subClassOf, C_15, uri_rdfs_Resource), true)=true))). % 35.00/24.35 tff(c_598, plain, (ip(uri_rdf__2)=true)). % 35.00/24.35 tff(c_30, plain, (![P_10]: (ifeq(iext(uri_rdf_type, P_10, uri_rdf_Property), true, ip(P_10), true)=true))). % 35.00/24.35 tff(c_124, plain, (![X_27]: (ifeq(lv(X_27), true, icext(uri_rdfs_Literal, X_27), true)=true))). % 35.00/24.35 tff(c_114, plain, (![X_22]: (ifeq(ic(X_22), true, icext(uri_rdfs_Class, X_22), true)=true))). % 35.00/24.35 tff(c_122, plain, (![X_26]: (ifeq(icext(uri_rdfs_Literal, X_26), true, lv(X_26), true)=true))). % 35.00/24.35 tff(c_116, plain, (![X_23]: (ifeq(icext(uri_rdfs_Class, X_23), true, ic(X_23), true)=true))). % 35.00/24.35 tff(c_513, plain, (![X_61]: (icext(uri_rdfs_Resource, X_61)=true))). % 35.00/24.35 tff(c_205, plain, (![X_8]: (ifeq(lv(X_8), true, true, true)=true))). % 35.00/24.35 tff(c_2, plain, (![A_1, B_2, C_3]: (ifeq(A_1, A_1, B_2, C_3)=B_2))). % 35.00/24.35 tff(c_128, plain, (iext(uri_rdfs_domain, uri_rdfs_range, uri_rdf_Property)=true)). % 35.00/24.35 tff(c_86, plain, (iext(uri_rdfs_range, uri_rdf__1, uri_rdfs_Resource)=true)). % 35.00/24.35 tff(c_94, plain, (iext(uri_rdf_type, uri_rdf__2, uri_rdfs_ContainerMembershipProperty)=true)). % 35.00/24.35 tff(c_18, plain, (iext(uri_rdf_type, uri_rdf__2, uri_rdf_Property)=true)). % 35.00/24.35 tff(c_134, plain, (iext(uri_rdfs_domain, uri_rdf_object, uri_rdfs_Statement)=true)). % 35.00/24.35 tff(c_36, plain, (iext(uri_rdfs_domain, uri_rdfs_comment, uri_rdfs_Resource)=true)). % 35.00/24.35 tff(c_108, plain, (iext(uri_rdfs_domain, uri_rdfs_domain, uri_rdf_Property)=true)). % 35.00/24.35 tff(c_180, plain, (iext(uri_rdfs_range, uri_rdf_value, uri_rdfs_Resource)=true)). % 35.00/24.35 tff(c_16, plain, (iext(uri_rdf_type, uri_rdf__1, uri_rdf_Property)=true)). % 35.00/24.35 tff(c_106, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, uri_rdfs_Class)=true)). % 35.00/24.35 tff(c_132, plain, (iext(uri_rdfs_range, uri_rdfs_range, uri_rdfs_Class)=true)). % 35.00/24.36 tff(c_84, plain, (iext(uri_rdfs_domain, uri_rdf__3, uri_rdfs_Resource)=true)). % 35.00/24.36 tff(c_66, plain, (iext(uri_rdfs_range, uri_rdf_rest, uri_rdf_List)=true)). % 35.00/24.36 tff(c_168, plain, (iext(uri_rdfs_range, uri_rdfs_subPropertyOf, uri_rdf_Property)=true)). % 35.00/24.36 tff(c_14, plain, (iext(uri_rdf_type, uri_rdf_rest, uri_rdf_Property)=true)). % 35.00/24.36 tff(c_102, plain, (iext(uri_rdf_type, uri_rdf_XMLLiteral, uri_rdfs_Datatype)=true)). % 35.00/24.36 tff(c_60, plain, (iext(uri_rdfs_domain, uri_rdf_first, uri_rdf_List)=true)). % 35.00/24.36 tff(c_196, plain, (iext(uri_rdf_type, uri_ex_B, uri_owl_Class)=true)). % 35.00/24.36 tff(c_64, plain, (iext(uri_rdfs_domain, uri_rdf_rest, uri_rdf_List)=true)). % 35.00/24.36 tff(c_40, plain, (iext(uri_rdfs_domain, uri_rdfs_isDefinedBy, uri_rdfs_Resource)=true)). % 35.00/24.36 tff(c_46, plain, (iext(uri_rdfs_domain, uri_rdfs_label, uri_rdfs_Resource)=true)). % 35.00/24.36 tff(c_190, plain, (iext(uri_rdf_first, sK2_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l2, sK1_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_y)=true)). % 35.00/24.36 tff(c_98, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Seq, uri_rdfs_Container)=true)). % 35.00/24.36 tff(c_88, plain, (iext(uri_rdfs_range, uri_rdf__2, uri_rdfs_Resource)=true)). % 35.00/24.36 tff(c_42, plain, (iext(uri_rdfs_range, uri_rdfs_isDefinedBy, uri_rdfs_Resource)=true)). % 35.00/24.36 tff(c_182, plain, (iext(uri_owl_complementOf, sK1_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_y, uri_ex_A)=true)). % 35.00/24.36 tff(c_92, plain, (iext(uri_rdf_type, uri_rdf__1, uri_rdfs_ContainerMembershipProperty)=true)). % 35.00/24.36 tff(c_22, plain, (iext(uri_rdf_type, uri_rdf_object, uri_rdf_Property)=true)). % 35.00/24.36 tff(c_192, plain, (iext(uri_rdf_first, sK4_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l1, uri_ex_A)=true)). % 35.00/24.36 tff(c_24, plain, (iext(uri_rdf_type, uri_rdf_value, uri_rdf_Property)=true)). % 35.00/24.36 tff(c_126, plain, (iext(uri_rdf_type, uri_rdf_Property, uri_rdfs_Class)=true)). % 35.00/24.36 tff(c_34, plain, (iext(uri_rdf_type, uri_rdf_type, uri_rdf_Property)=true)). % 35.00/24.36 tff(c_178, plain, (iext(uri_rdfs_domain, uri_rdf_value, uri_rdfs_Resource)=true)). % 35.00/24.36 tff(c_74, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, uri_rdf_Property)=true)). % 35.00/24.36 tff(c_44, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_isDefinedBy, uri_rdfs_seeAlso)=true)). % 35.00/24.36 tff(c_100, plain, (iext(uri_rdfs_subClassOf, uri_rdf_XMLLiteral, uri_rdfs_Literal)=true)). % 35.00/24.36 tff(c_112, plain, (iext(uri_rdfs_range, uri_rdfs_domain, uri_rdfs_Class)=true)). % 35.00/24.36 tff(c_184, plain, (iext(uri_owl_intersectionOf, sK3_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_x, sK4_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l1)=true)). % 35.00/24.36 tff(c_90, plain, (iext(uri_rdfs_range, uri_rdf__3, uri_rdfs_Resource)=true)). % 35.00/24.36 tff(c_76, plain, (iext(uri_rdfs_domain, uri_rdfs_member, uri_rdfs_Resource)=true)). % 35.00/24.36 tff(c_188, plain, (iext(uri_rdf_rest, sK4_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l1, sK2_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l2)=true)). % 35.00/24.36 tff(c_26, plain, (iext(uri_rdf_type, uri_rdf_subject, uri_rdf_Property)=true)). % 35.00/24.36 tff(c_154, plain, (iext(uri_rdfs_range, uri_rdfs_subClassOf, uri_rdfs_Class)=true)). % 35.00/24.36 tff(c_78, plain, (iext(uri_rdfs_range, uri_rdfs_member, uri_rdfs_Resource)=true)). % 35.00/24.36 tff(c_48, plain, (iext(uri_rdfs_range, uri_rdfs_label, uri_rdfs_Literal)=true)). % 35.00/24.36 tff(c_82, plain, (iext(uri_rdfs_domain, uri_rdf__2, uri_rdfs_Resource)=true)). % 35.00/24.36 tff(c_62, plain, (iext(uri_rdfs_range, uri_rdf_first, uri_rdfs_Resource)=true)). % 35.00/24.36 tff(c_174, plain, (iext(uri_rdfs_domain, uri_rdf_type, uri_rdfs_Resource)=true)). % 35.00/24.36 tff(c_50, plain, (iext(uri_rdfs_domain, uri_rdfs_seeAlso, uri_rdfs_Resource)=true)). % 35.00/24.36 tff(c_80, plain, (iext(uri_rdfs_domain, uri_rdf__1, uri_rdfs_Resource)=true)). % 35.00/24.36 tff(c_198, plain, (iext(uri_rdf_type, uri_ex_w, sK3_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_x)=true)). % 35.00/24.36 tff(c_52, plain, (iext(uri_rdfs_range, uri_rdfs_seeAlso, uri_rdfs_Resource)=true)). % 35.00/24.36 tff(c_38, plain, (iext(uri_rdfs_range, uri_rdfs_comment, uri_rdfs_Literal)=true)). % 35.00/24.36 tff(c_142, plain, (iext(uri_rdfs_domain, uri_rdf_subject, uri_rdfs_Statement)=true)). % 35.00/24.36 tff(c_96, plain, (iext(uri_rdf_type, uri_rdf__3, uri_rdfs_ContainerMembershipProperty)=true)). % 35.00/24.36 tff(c_20, plain, (iext(uri_rdf_type, uri_rdf__3, uri_rdf_Property)=true)). % 35.00/24.36 tff(c_68, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Alt, uri_rdfs_Container)=true)). % 35.00/24.36 tff(c_146, plain, (iext(uri_rdfs_domain, uri_rdfs_subClassOf, uri_rdfs_Class)=true)). % 35.00/24.36 tff(c_176, plain, (iext(uri_rdfs_range, uri_rdf_type, uri_rdfs_Class)=true)). % 35.00/24.36 tff(c_140, plain, (iext(uri_rdfs_range, uri_rdf_predicate, uri_rdfs_Resource)=true)). % 35.00/24.36 tff(c_12, plain, (iext(uri_rdf_type, uri_rdf_nil, uri_rdf_List)=true)). % 35.00/24.36 tff(c_10, plain, (iext(uri_rdf_type, uri_rdf_first, uri_rdf_Property)=true)). % 35.00/24.36 tff(c_160, plain, (iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, uri_rdf_Property)=true)). % 35.00/24.36 tff(c_144, plain, (iext(uri_rdfs_range, uri_rdf_subject, uri_rdfs_Resource)=true)). % 35.00/24.36 tff(c_70, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Bag, uri_rdfs_Container)=true)). % 35.00/24.36 tff(c_138, plain, (iext(uri_rdfs_domain, uri_rdf_predicate, uri_rdfs_Statement)=true)). % 35.00/24.36 tff(c_186, plain, (iext(uri_rdf_rest, sK2_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l2, uri_rdf_nil)=true)). % 35.00/24.36 tff(c_194, plain, (iext(uri_rdf_type, uri_ex_A, uri_owl_Class)=true)). % 35.00/24.36 tff(c_200, plain, (iext(uri_rdf_type, uri_ex_w, uri_ex_B)!=true)). % 35.00/24.36 tff(c_6, plain, (![X_7]: (ir(X_7)=true))). % 35.00/24.36 % SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 35.00/24.36 %------------------------------------------------------------------------------