↑ Up

Beagle---0.9.52.SAT-Ass.s

View TPTP
Problem
Process solution in
SystemOnTSTP
Download .tgz
%------------------------------------------------------------------------------
% File     : Beagle---0.9.52
% Problem  : SWB018-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 : n019.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:52 PM UTC 2025

% Result   : Satisfiable 28.82s 18.15s
% Output   : Assurance 0s
% Verified : 
% SZS Type : -

% Comments : 
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12  % Problem  : SWB018-10 : TPTP v9.0.0. Released v7.5.0.
% 0.07/0.13  % Command  : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% 0.13/0.34  % Computer : n019.cluster.edu
% 0.13/0.34  % Model    : x86_64 x86_64
% 0.13/0.34  % CPU      : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.13/0.34  % Memory   : 8042.1875MB
% 0.13/0.34  % OS       : Linux 3.10.0-693.el7.x86_64
% 0.13/0.34  % CPULimit : 300
% 0.13/0.34  % WCLimit  : 300
% 0.13/0.34  % DateTime : Wed Apr  9 00:58:02 EDT 2025
% 0.13/0.34  % CPUTime  : 
% 28.82/18.15  
% 28.82/18.15  % SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 28.82/18.16  
% 28.82/18.16  % SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 28.82/18.17  %$ ifeq > iext > icext > #nlpp > lv > ir > ip > ic > uri_rdfs_subPropertyOf > uri_rdfs_subClassOf > uri_rdfs_seeAlso > uri_rdfs_range > uri_rdfs_member > uri_rdfs_label > uri_rdfs_isDefinedBy > uri_rdfs_domain > uri_rdfs_comment > uri_rdfs_Statement > uri_rdfs_Seq > uri_rdfs_Resource > uri_rdfs_Literal > uri_rdfs_Datatype > uri_rdfs_ContainerMembershipProperty > uri_rdfs_Container > uri_rdfs_Class > uri_rdf_value > uri_rdf_type > uri_rdf_subject > uri_rdf_rest > uri_rdf_predicate > uri_rdf_object > uri_rdf_nil > uri_rdf_first > uri_rdf__3 > uri_rdf__2 > uri_rdf__1 > uri_rdf_XMLLiteral > uri_rdf_Property > uri_rdf_List > uri_rdf_Bag > uri_rdf_Alt > uri_owl_sameAs > uri_ex_w > uri_ex_u > uri_ex_Person > true
% 28.82/18.17  
% 28.82/18.17  %Foreground sorts:
% 28.82/18.17  
% 28.82/18.17  
% 28.82/18.17  %Background operators:
% 28.82/18.17  
% 28.82/18.17  
% 28.82/18.17  %Foreground operators:
% 28.82/18.17  tff(uri_rdfs_Datatype, type, uri_rdfs_Datatype: $i).
% 28.82/18.17  tff(uri_rdfs_ContainerMembershipProperty, type, uri_rdfs_ContainerMembershipProperty: $i).
% 28.82/18.17  tff(uri_rdfs_Resource, type, uri_rdfs_Resource: $i).
% 28.82/18.17  tff(uri_rdf_Property, type, uri_rdf_Property: $i).
% 28.82/18.17  tff(uri_rdf_subject, type, uri_rdf_subject: $i).
% 28.82/18.17  tff(uri_rdf_type, type, uri_rdf_type: $i).
% 28.82/18.17  tff(uri_rdfs_subPropertyOf, type, uri_rdfs_subPropertyOf: $i).
% 28.82/18.17  tff(uri_ex_u, type, uri_ex_u: $i).
% 28.82/18.17  tff(uri_rdfs_seeAlso, type, uri_rdfs_seeAlso: $i).
% 28.82/18.17  tff(icext, type, icext: ($i * $i) > $i).
% 28.82/18.17  tff(uri_rdfs_range, type, uri_rdfs_range: $i).
% 28.82/18.17  tff(uri_rdf_XMLLiteral, type, uri_rdf_XMLLiteral: $i).
% 28.82/18.17  tff(uri_rdf_List, type, uri_rdf_List: $i).
% 28.82/18.17  tff(uri_rdf_first, type, uri_rdf_first: $i).
% 28.82/18.17  tff(uri_rdf_predicate, type, uri_rdf_predicate: $i).
% 28.82/18.17  tff(ir, type, ir: $i > $i).
% 28.82/18.17  tff(uri_ex_Person, type, uri_ex_Person: $i).
% 28.82/18.17  tff(lv, type, lv: $i > $i).
% 28.82/18.17  tff(uri_rdf__3, type, uri_rdf__3: $i).
% 28.82/18.17  tff(uri_rdf_value, type, uri_rdf_value: $i).
% 28.82/18.17  tff(ic, type, ic: $i > $i).
% 28.82/18.17  tff(uri_rdfs_Statement, type, uri_rdfs_Statement: $i).
% 28.82/18.17  tff(uri_rdf__1, type, uri_rdf__1: $i).
% 28.82/18.17  tff(iext, type, iext: ($i * $i * $i) > $i).
% 28.82/18.17  tff(uri_ex_w, type, uri_ex_w: $i).
% 28.82/18.17  tff(uri_rdf_rest, type, uri_rdf_rest: $i).
% 28.82/18.17  tff(uri_rdfs_label, type, uri_rdfs_label: $i).
% 28.82/18.17  tff(uri_rdfs_Container, type, uri_rdfs_Container: $i).
% 28.82/18.17  tff(uri_rdfs_subClassOf, type, uri_rdfs_subClassOf: $i).
% 28.82/18.17  tff(uri_owl_sameAs, type, uri_owl_sameAs: $i).
% 28.82/18.17  tff(uri_rdf_object, type, uri_rdf_object: $i).
% 28.82/18.17  tff(ip, type, ip: $i > $i).
% 28.82/18.17  tff(uri_rdfs_Class, type, uri_rdfs_Class: $i).
% 28.82/18.17  tff(uri_rdfs_Seq, type, uri_rdfs_Seq: $i).
% 28.82/18.17  tff(uri_rdfs_member, type, uri_rdfs_member: $i).
% 28.82/18.17  tff(uri_rdf_Bag, type, uri_rdf_Bag: $i).
% 28.82/18.17  tff(uri_rdf__2, type, uri_rdf__2: $i).
% 28.82/18.17  tff(uri_rdfs_comment, type, uri_rdfs_comment: $i).
% 28.82/18.17  tff(uri_rdfs_Literal, type, uri_rdfs_Literal: $i).
% 28.82/18.17  tff(true, type, true: $i).
% 28.82/18.17  tff(uri_rdf_Alt, type, uri_rdf_Alt: $i).
% 28.82/18.17  tff(uri_rdf_nil, type, uri_rdf_nil: $i).
% 28.82/18.17  tff(uri_rdfs_isDefinedBy, type, uri_rdfs_isDefinedBy: $i).
% 28.82/18.17  tff(uri_rdfs_domain, type, uri_rdfs_domain: $i).
% 28.82/18.17  tff(ifeq, type, ifeq: ($i * $i * $i * $i) > $i).
% 28.82/18.17  
% 28.82/18.17  %Saturated clause set:
% 28.82/18.18  tff(c_16291, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subClassOf), true, ifeq(iext(P_47, uri_ex_Person, uri_rdfs_Resource), true, true, true), true)=true))).
% 28.82/18.18  tff(c_65558, plain, (![C_1180]: (ifeq(iext(uri_rdfs_subClassOf, C_1180, uri_ex_Person), true, iext(uri_rdfs_subClassOf, C_1180, uri_rdfs_Resource), true)=true))).
% 28.82/18.18  tff(c_12808, 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))).
% 28.82/18.18  tff(c_16500, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subClassOf), true, ifeq(iext(P_47, uri_ex_Person, uri_ex_Person), true, true, true), true)=true))).
% 28.82/18.18  tff(c_12746, 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))).
% 28.92/18.18  tff(c_65184, plain, (![X_1173, Y_1174]: (ifeq(iext(uri_rdf_predicate, X_1173, Y_1174), true, iext(uri_rdf_predicate, X_1173, Y_1174), true)=true))).
% 28.92/18.18  tff(c_65157, plain, (![X_1169, Y_1170]: (ifeq(iext(uri_rdfs_member, X_1169, Y_1170), true, iext(uri_rdfs_member, X_1169, Y_1170), true)=true))).
% 28.92/18.18  tff(c_13750, 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))).
% 28.92/18.18  tff(c_65012, plain, (![X_1164, Y_1165]: (ifeq(iext(uri_rdfs_comment, X_1164, Y_1165), true, iext(uri_rdfs_comment, X_1164, Y_1165), true)=true))).
% 28.92/18.18  tff(c_12086, 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))).
% 28.92/18.18  tff(c_64865, plain, (![X_1159, Y_1160]: (ifeq(iext(uri_rdfs_label, X_1159, Y_1160), true, iext(uri_rdfs_label, X_1159, Y_1160), true)=true))).
% 28.92/18.18  tff(c_5011, 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))).
% 28.92/18.18  tff(c_16231, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, uri_ex_Person, uri_rdfs_Class), true, true, true), true)=true))).
% 28.92/18.18  tff(c_12151, 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))).
% 28.92/18.18  tff(c_5014, 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))).
% 28.92/18.18  tff(c_13685, 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))).
% 28.92/18.18  tff(c_63984, plain, (![C_1150]: (ifeq(iext(uri_rdfs_subClassOf, C_1150, uri_rdfs_Statement), true, iext(uri_rdfs_subClassOf, C_1150, uri_rdfs_Resource), true)=true))).
% 28.92/18.18  tff(c_11863, 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))).
% 28.92/18.18  tff(c_11929, 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))).
% 28.92/18.18  tff(c_12562, 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))).
% 28.92/18.18  tff(c_63482, plain, (![C_1145]: (ifeq(iext(uri_rdfs_subClassOf, C_1145, uri_rdf_List), true, iext(uri_rdfs_subClassOf, C_1145, uri_rdfs_Resource), true)=true))).
% 28.92/18.18  tff(c_12496, 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))).
% 28.92/18.18  tff(c_8127, 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))).
% 28.92/18.18  tff(c_11659, 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))).
% 28.92/18.18  tff(c_8130, 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))).
% 28.92/18.18  tff(c_15987, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdfs_Class), true, ifeq(iext(P_18, uri_ex_Person, Y_21), true, true, true), true)=true))).
% 28.92/18.18  tff(c_6561, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdf_Property), true, ifeq(iext(P_18, uri_rdfs_seeAlso, Y_21), true, true, true), true)=true))).
% 28.92/18.18  tff(c_8652, 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))).
% 28.92/18.18  tff(c_11296, 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))).
% 28.92/18.18  tff(c_11200, 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))).
% 28.92/18.18  tff(c_8655, 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))).
% 28.92/18.18  tff(c_15990, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdfs_Class), true, ifeq(iext(P_28, X_30, uri_ex_Person), true, true, true), true)=true))).
% 28.92/18.18  tff(c_5486, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_rdf_Property), true, ifeq(iext(P_18, uri_owl_sameAs, Y_21), true, true, true), true)=true))).
% 28.92/18.18  tff(c_11780, 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))).
% 28.92/18.18  tff(c_5489, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdf_Property), true, ifeq(iext(P_28, X_30, uri_owl_sameAs), true, true, true), true)=true))).
% 28.92/18.18  tff(c_11563, 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))).
% 28.92/18.18  tff(c_11611, 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))).
% 28.92/18.18  tff(c_6564, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdf_Property), true, ifeq(iext(P_28, X_30, uri_rdfs_seeAlso), true, true, true), true)=true))).
% 28.92/18.18  tff(c_11732, 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))).
% 28.92/18.18  tff(c_11249, 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))).
% 28.92/18.18  tff(c_11151, 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))).
% 28.92/18.18  tff(c_12440, 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))).
% 28.92/18.18  tff(c_11025, 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))).
% 28.92/18.18  tff(c_11414, 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))).
% 28.92/18.18  tff(c_10949, 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))).
% 28.92/18.18  tff(c_14885, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, uri_ex_w, uri_ex_Person), true, true, true), true)=true))).
% 28.92/18.18  tff(c_60294, plain, (![C_1108]: (ifeq(iext(uri_rdfs_subClassOf, C_1108, uri_rdfs_Container), true, iext(uri_rdfs_subClassOf, C_1108, uri_rdfs_Resource), true)=true))).
% 28.92/18.18  tff(c_59609, plain, (![X_1104, Y_1105]: (ifeq(iext(uri_rdf_type, X_1104, Y_1105), true, iext(uri_rdf_type, X_1104, Y_1105), true)=true))).
% 28.92/18.18  tff(c_4309, 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))).
% 28.92/18.18  tff(c_59334, plain, (![C_1100]: (ifeq(iext(uri_rdfs_subClassOf, C_1100, uri_rdf_XMLLiteral), true, iext(uri_rdfs_subClassOf, C_1100, uri_rdfs_Resource), true)=true))).
% 28.92/18.19  tff(c_8458, 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))).
% 28.92/18.19  tff(c_9982, 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))).
% 28.92/18.19  tff(c_4214, 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))).
% 28.92/18.19  tff(c_58939, plain, (![X_1092, Y_1093]: (ifeq(iext(uri_rdf__3, X_1092, Y_1093), true, iext(uri_rdfs_member, X_1092, Y_1093), true)=true))).
% 28.92/18.19  tff(c_58705, plain, (![X_1086, Y_1087]: (ifeq(iext(uri_rdf_rest, X_1086, Y_1087), true, iext(uri_rdf_rest, X_1086, Y_1087), true)=true))).
% 28.92/18.19  tff(c_4312, 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))).
% 28.92/18.19  tff(c_58678, plain, (![X_1082, Y_1083]: (ifeq(iext(uri_rdf_object, X_1082, Y_1083), true, iext(uri_rdf_object, X_1082, Y_1083), true)=true))).
% 28.92/18.19  tff(c_10117, 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))).
% 28.92/18.19  tff(c_6119, 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))).
% 28.92/18.19  tff(c_58299, plain, (![C_1078]: (ifeq(iext(uri_rdfs_subClassOf, C_1078, uri_rdfs_ContainerMembershipProperty), true, iext(uri_rdfs_subClassOf, C_1078, uri_rdfs_Resource), true)=true))).
% 28.92/18.19  tff(c_58144, plain, (![C_1076]: (ifeq(iext(uri_rdfs_subClassOf, C_1076, uri_rdf_Property), true, iext(uri_rdfs_subClassOf, C_1076, uri_rdfs_Resource), true)=true))).
% 28.92/18.19  tff(c_8387, 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))).
% 28.92/18.19  tff(c_10813, 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))).
% 28.92/18.19  tff(c_4267, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_rdfs_Class), true, ifeq(iext(P_28, X_30, uri_rdf_Bag), true, true, true), true)=true))).
% 28.92/18.19  tff(c_10516, 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))).
% 28.92/18.19  tff(c_57628, plain, (![X_1067, Y_1068]: (ifeq(iext(uri_owl_sameAs, X_1067, Y_1068), true, iext(uri_owl_sameAs, X_1067, Y_1068), true)=true))).
% 28.92/18.19  tff(c_3935, 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))).
% 28.92/18.19  tff(c_6483, 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))).
% 28.92/18.19  tff(c_4811, 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))).
% 28.92/18.19  tff(c_57103, plain, (![C_1061]: (ifeq(iext(uri_rdfs_subClassOf, C_1061, uri_rdfs_Class), true, iext(uri_rdfs_subClassOf, C_1061, uri_rdfs_Resource), true)=true))).
% 28.92/18.19  tff(c_13483, 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))).
% 28.92/18.19  tff(c_56841, plain, (![C_1058]: (ifeq(iext(uri_rdfs_subClassOf, C_1058, uri_rdf_Alt), true, iext(uri_rdfs_subClassOf, C_1058, uri_rdfs_Resource), true)=true))).
% 28.92/18.19  tff(c_56814, plain, (![X_1054, Y_1055]: (ifeq(iext(uri_rdf__1, X_1054, Y_1055), true, iext(uri_rdf__1, X_1054, Y_1055), true)=true))).
% 28.92/18.19  tff(c_10183, 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))).
% 28.92/18.19  tff(c_5634, 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))).
% 28.92/18.19  tff(c_56265, plain, (![X_1048, Y_1049]: (ifeq(iext(uri_rdfs_range, X_1048, Y_1049), true, iext(uri_rdfs_range, X_1048, Y_1049), true)=true))).
% 28.92/18.19  tff(c_10883, 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))).
% 28.92/18.19  tff(c_56123, plain, (![X_1043, Y_1044]: (ifeq(iext(uri_rdf__2, X_1043, Y_1044), true, iext(uri_rdf__2, X_1043, Y_1044), true)=true))).
% 28.92/18.19  tff(c_8892, 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))).
% 28.92/18.19  tff(c_4586, 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))).
% 28.92/18.19  tff(c_55731, plain, (![C_1039]: (ifeq(iext(uri_rdfs_subClassOf, C_1039, uri_rdfs_Literal), true, iext(uri_rdfs_subClassOf, C_1039, uri_rdfs_Resource), true)=true))).
% 28.92/18.19  tff(c_8072, 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))).
% 28.92/18.19  tff(c_55463, plain, (![C_1036]: (ifeq(iext(uri_rdfs_subClassOf, C_1036, uri_rdf_Bag), true, iext(uri_rdfs_subClassOf, C_1036, uri_rdfs_Resource), true)=true))).
% 28.92/18.19  tff(c_10583, 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))).
% 28.92/18.19  tff(c_4880, 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))).
% 28.92/18.19  tff(c_55199, plain, (![X_1030, Y_1031]: (ifeq(iext(uri_rdfs_seeAlso, X_1030, Y_1031), true, iext(uri_rdfs_seeAlso, X_1030, Y_1031), true)=true))).
% 28.92/18.19  tff(c_10649, 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))).
% 28.92/18.19  tff(c_8327, 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))).
% 28.92/18.19  tff(c_54326, plain, (![X_1024, Y_1025]: (ifeq(iext(uri_rdfs_subClassOf, X_1024, Y_1025), true, iext(uri_rdfs_subClassOf, X_1024, Y_1025), true)=true))).
% 28.92/18.19  tff(c_54299, plain, (![X_1020, Y_1021]: (ifeq(iext(uri_rdf__3, X_1020, Y_1021), true, iext(uri_rdf__3, X_1020, Y_1021), true)=true))).
% 28.92/18.19  tff(c_13582, 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))).
% 28.92/18.19  tff(c_10273, 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))).
% 28.92/18.19  tff(c_7090, 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))).
% 28.92/18.19  tff(c_9144, 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))).
% 28.92/18.19  tff(c_4167, 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))).
% 28.92/18.19  tff(c_52704, plain, (![X_1006, Y_1007]: (ifeq(iext(uri_rdfs_subPropertyOf, X_1006, Y_1007), true, iext(uri_rdfs_subPropertyOf, X_1006, Y_1007), true)=true))).
% 28.92/18.19  tff(c_52677, plain, (![X_1002, Y_1003]: (ifeq(iext(uri_rdf_value, X_1002, Y_1003), true, iext(uri_rdf_value, X_1002, Y_1003), true)=true))).
% 28.92/18.19  tff(c_6019, 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))).
% 28.92/18.19  tff(c_8229, 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))).
% 28.92/18.19  tff(c_4750, 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))).
% 28.92/18.19  tff(c_9767, 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))).
% 28.92/18.19  tff(c_4029, 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))).
% 28.92/18.19  tff(c_4119, 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))).
% 28.92/18.19  tff(c_5703, 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))).
% 28.92/18.19  tff(c_51242, plain, (![P_987]: (ifeq(iext(uri_rdfs_subPropertyOf, P_987, uri_rdf__2), true, iext(uri_rdfs_subPropertyOf, P_987, uri_rdfs_member), true)=true))).
% 28.92/18.19  tff(c_4264, 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))).
% 28.92/18.19  tff(c_9520, 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))).
% 28.92/18.19  tff(c_4170, 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))).
% 28.92/18.19  tff(c_50554, plain, (![X_976, Y_977]: (ifeq(iext(uri_rdf_first, X_976, Y_977), true, iext(uri_rdf_first, X_976, Y_977), true)=true))).
% 28.92/18.19  tff(c_3932, 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))).
% 28.92/18.19  tff(c_7955, 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))).
% 28.92/18.20  tff(c_9913, 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))).
% 28.92/18.20  tff(c_5397, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, uri_owl_sameAs, uri_rdf_Property), true, true, true), true)=true))).
% 28.92/18.20  tff(c_9304, 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))).
% 28.92/18.20  tff(c_10042, 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))).
% 28.92/18.20  tff(c_3979, 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))).
% 28.92/18.20  tff(c_7810, 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))).
% 28.92/18.20  tff(c_8598, 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))).
% 28.92/18.20  tff(c_10344, 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))).
% 28.92/18.20  tff(c_7285, 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))).
% 28.92/18.20  tff(c_48801, plain, (![C_959]: (ifeq(iext(uri_rdfs_subClassOf, C_959, uri_rdfs_Datatype), true, iext(uri_rdfs_subClassOf, C_959, uri_rdfs_Resource), true)=true))).
% 28.92/18.20  tff(c_4217, 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))).
% 28.92/18.20  tff(c_48523, plain, (![C_955]: (ifeq(iext(uri_rdfs_subClassOf, C_955, uri_rdfs_Seq), true, iext(uri_rdfs_subClassOf, C_955, uri_rdfs_Resource), true)=true))).
% 28.92/18.20  tff(c_48496, plain, (![X_951, Y_952]: (ifeq(iext(uri_rdf__1, X_951, Y_952), true, iext(uri_rdfs_member, X_951, Y_952), true)=true))).
% 28.92/18.20  tff(c_4026, 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))).
% 28.92/18.20  tff(c_6179, 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))).
% 28.92/18.20  tff(c_48182, plain, (![P_946]: (ifeq(iext(uri_rdfs_subPropertyOf, P_946, uri_rdf__1), true, iext(uri_rdfs_subPropertyOf, P_946, uri_rdfs_member), true)=true))).
% 28.92/18.20  tff(c_9665, 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))).
% 28.92/18.20  tff(c_48040, plain, (![X_941, Y_942]: (ifeq(iext(uri_rdf__2, X_941, Y_942), true, iext(uri_rdfs_member, X_941, Y_942), true)=true))).
% 28.92/18.20  tff(c_4682, plain, (![P_47]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdfs_subPropertyOf), true, ifeq(iext(P_47, uri_owl_sameAs, uri_owl_sameAs), true, true, true), true)=true))).
% 28.92/18.20  tff(c_47858, plain, (![P_938]: (ifeq(iext(uri_rdfs_subPropertyOf, P_938, uri_rdf__3), true, iext(uri_rdfs_subPropertyOf, P_938, uri_rdfs_member), true)=true))).
% 28.92/18.20  tff(c_47831, plain, (![X_934, Y_935]: (ifeq(iext(uri_rdf_subject, X_934, Y_935), true, iext(uri_rdf_subject, X_934, Y_935), true)=true))).
% 28.92/18.20  tff(c_3976, 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))).
% 28.92/18.20  tff(c_47356, plain, (![X_928, Y_929]: (ifeq(iext(uri_rdfs_domain, X_928, Y_929), true, iext(uri_rdfs_domain, X_928, Y_929), true)=true))).
% 28.92/18.20  tff(c_6265, 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))).
% 28.92/18.20  tff(c_4072, 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))).
% 28.92/18.20  tff(c_4116, 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))).
% 28.92/18.20  tff(c_8017, 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))).
% 28.92/18.20  tff(c_4069, 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))).
% 28.92/18.20  tff(c_6896, 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))).
% 28.92/18.20  tff(c_9607, 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))).
% 28.92/18.20  tff(c_6645, 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))).
% 28.92/18.20  tff(c_5889, 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))).
% 28.92/18.20  tff(c_44876, plain, (![X_902, Y_903]: (ifeq(iext(uri_rdfs_isDefinedBy, X_902, Y_903), true, iext(uri_rdfs_isDefinedBy, X_902, Y_903), true)=true))).
% 28.92/18.20  tff(c_6329, 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))).
% 28.92/18.20  tff(c_11372, 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))).
% 28.92/18.20  tff(c_12241, 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))).
% 28.92/18.20  tff(c_9393, 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))).
% 28.92/18.20  tff(c_14732, plain, (![P_18, Y_21]: (ifeq(iext(uri_rdfs_domain, P_18, uri_ex_Person), true, ifeq(iext(P_18, uri_ex_w, Y_21), true, true, true), true)=true))).
% 28.92/18.20  tff(c_7367, 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))).
% 28.92/18.20  tff(c_11369, 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))).
% 28.92/18.20  tff(c_7370, 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))).
% 28.92/18.20  tff(c_8955, 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))).
% 28.92/18.20  tff(c_8952, 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))).
% 28.92/18.20  tff(c_6728, 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))).
% 28.92/18.20  tff(c_4508, plain, (![P_47, X_138]: (ifeq(iext(uri_rdfs_subPropertyOf, P_47, uri_rdf_type), true, ifeq(iext(P_47, X_138, uri_rdfs_Resource), true, true, true), true)=true))).
% 28.92/18.20  tff(c_9396, 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))).
% 28.92/18.20  tff(c_14735, plain, (![P_28, X_30]: (ifeq(iext(uri_rdfs_range, P_28, uri_ex_Person), true, ifeq(iext(P_28, X_30, uri_ex_w), true, true, true), true)=true))).
% 28.92/18.20  tff(c_6725, 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))).
% 28.92/18.20  tff(c_6332, 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))).
% 28.92/18.20  tff(c_12244, 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))).
% 28.92/18.20  tff(c_3353, 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))).
% 28.92/18.20  tff(c_3394, 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))).
% 28.92/18.20  tff(c_3428, 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))).
% 28.92/18.20  tff(c_3609, 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))).
% 28.92/18.20  tff(c_3520, 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))).
% 28.92/18.20  tff(c_3310, 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))).
% 28.92/18.20  tff(c_3764, 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))).
% 28.92/18.20  tff(c_3847, 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))).
% 28.92/18.20  tff(c_13221, 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))).
% 28.92/18.20  tff(c_3850, 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))).
% 28.92/18.20  tff(c_3767, 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))).
% 28.92/18.20  tff(c_3803, 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))).
% 28.92/18.20  tff(c_13186, 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))).
% 28.92/18.20  tff(c_3566, 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))).
% 28.92/18.20  tff(c_3350, 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))).
% 28.92/18.20  tff(c_3890, 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))).
% 28.92/18.20  tff(c_3391, 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))).
% 28.92/18.20  tff(c_3725, 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))).
% 28.92/18.20  tff(c_3686, 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))).
% 28.92/18.20  tff(c_13218, 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))).
% 28.92/18.20  tff(c_3806, 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))).
% 28.92/18.20  tff(c_3653, 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))).
% 28.92/18.20  tff(c_13183, 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))).
% 28.92/18.20  tff(c_3683, 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))).
% 28.92/18.20  tff(c_3887, 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))).
% 28.92/18.20  tff(c_3483, 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))).
% 28.92/18.20  tff(c_3563, 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))).
% 28.92/18.21  tff(c_3480, 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))).
% 28.92/18.21  tff(c_3606, 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))).
% 28.92/18.21  tff(c_3656, 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))).
% 28.92/18.21  tff(c_3523, 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))).
% 28.92/18.21  tff(c_3431, 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))).
% 28.92/18.21  tff(c_3722, 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))).
% 28.92/18.21  tff(c_3307, 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))).
% 28.92/18.21  tff(c_1581, plain, (![P_91, X_93, X_60]: (ifeq(iext(uri_rdfs_range, P_91, uri_rdfs_Resource), true, ifeq(iext(P_91, X_93, X_60), true, true, true), true)=true))).
% 28.92/18.21  tff(c_1905, plain, (![P_95, X_60, Y_98]: (ifeq(iext(uri_rdfs_domain, P_95, uri_rdfs_Resource), true, ifeq(iext(P_95, X_60, Y_98), true, true, true), true)=true))).
% 28.92/18.21  tff(c_2614, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_range), true, ifeq(iext(P_102, uri_rdf_first, uri_rdfs_Resource), true, true, true), true)=true))).
% 28.92/18.21  tff(c_2569, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_subClassOf), true, ifeq(iext(P_102, uri_rdf_Alt, uri_rdfs_Container), true, true, true), true)=true))).
% 28.92/18.21  tff(c_36530, plain, (![C_790]: (ifeq(iext(uri_rdfs_subClassOf, C_790, uri_rdfs_Datatype), true, iext(uri_rdfs_subClassOf, C_790, uri_rdfs_Class), true)=true))).
% 28.92/18.21  tff(c_2443, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_range), true, ifeq(iext(P_102, uri_rdf_subject, uri_rdfs_Resource), true, true, true), true)=true))).
% 28.92/18.21  tff(c_2503, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_domain), true, ifeq(iext(P_102, uri_rdf_rest, uri_rdf_List), true, true, true), true)=true))).
% 28.92/18.21  tff(c_2323, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_range), true, ifeq(iext(P_102, uri_rdf_type, uri_rdfs_Class), true, true, true), true)=true))).
% 28.92/18.21  tff(c_2359, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_domain), true, ifeq(iext(P_102, uri_rdf_subject, uri_rdfs_Statement), true, true, true), true)=true))).
% 28.92/18.21  tff(c_2539, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_domain), true, ifeq(iext(P_102, uri_rdfs_domain, uri_rdf_Property), true, true, true), true)=true))).
% 28.92/18.21  tff(c_2509, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_subClassOf), true, ifeq(iext(P_102, uri_rdfs_Seq, uri_rdfs_Container), true, true, true), true)=true))).
% 28.92/18.21  tff(c_2341, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_domain), true, ifeq(iext(P_102, uri_owl_sameAs, uri_ex_Person), true, true, true), true)=true))).
% 28.92/18.21  tff(c_2608, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_domain), true, ifeq(iext(P_102, uri_rdfs_comment, uri_rdfs_Resource), true, true, true), true)=true))).
% 28.92/18.21  tff(c_2311, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_domain), true, ifeq(iext(P_102, uri_rdfs_isDefinedBy, uri_rdfs_Resource), true, true, true), true)=true))).
% 28.92/18.21  tff(c_2365, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_range), true, ifeq(iext(P_102, uri_rdf__1, uri_rdfs_Resource), true, true, true), true)=true))).
% 28.92/18.21  tff(c_2557, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_domain), true, ifeq(iext(P_102, uri_rdfs_member, uri_rdfs_Resource), true, true, true), true)=true))).
% 28.92/18.21  tff(c_2620, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdf_type), true, ifeq(iext(P_102, uri_rdf_first, uri_rdf_Property), true, true, true), true)=true))).
% 28.92/18.21  tff(c_34938, plain, (![C_775]: (ifeq(iext(uri_rdfs_subClassOf, C_775, uri_rdf_XMLLiteral), true, iext(uri_rdfs_subClassOf, C_775, uri_rdfs_Literal), true)=true))).
% 28.92/18.21  tff(c_2401, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdf_type), true, ifeq(iext(P_102, uri_rdf_rest, uri_rdf_Property), true, true, true), true)=true))).
% 28.92/18.21  tff(c_2335, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdf_type), true, ifeq(iext(P_102, uri_rdf__1, uri_rdf_Property), true, true, true), true)=true))).
% 28.92/18.21  tff(c_2461, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_subClassOf), true, ifeq(iext(P_102, uri_rdf_Bag, uri_rdfs_Container), true, true, true), true)=true))).
% 28.92/18.21  tff(c_2650, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_range), true, ifeq(iext(P_102, uri_rdfs_seeAlso, uri_rdfs_Resource), true, true, true), true)=true))).
% 28.92/18.21  tff(c_2632, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_subClassOf), true, ifeq(iext(P_102, uri_rdf_XMLLiteral, uri_rdfs_Literal), true, true, true), true)=true))).
% 28.92/18.21  tff(c_2473, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_domain), true, ifeq(iext(P_102, uri_rdf__2, uri_rdfs_Resource), true, true, true), true)=true))).
% 28.92/18.21  tff(c_2449, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_range), true, ifeq(iext(P_102, uri_rdfs_comment, uri_rdfs_Literal), true, true, true), true)=true))).
% 28.92/18.21  tff(c_2644, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_domain), true, ifeq(iext(P_102, uri_rdfs_seeAlso, uri_rdfs_Resource), true, true, true), true)=true))).
% 28.92/18.21  tff(c_2563, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_domain), true, ifeq(iext(P_102, uri_rdf_value, uri_rdfs_Resource), true, true, true), true)=true))).
% 28.92/18.21  tff(c_33930, plain, (![C_765]: (ifeq(iext(uri_rdfs_subClassOf, C_765, uri_rdfs_ContainerMembershipProperty), true, iext(uri_rdfs_subClassOf, C_765, uri_rdf_Property), true)=true))).
% 28.92/18.21  tff(c_2455, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_range), true, ifeq(iext(P_102, uri_rdfs_subPropertyOf, uri_rdf_Property), true, true, true), true)=true))).
% 28.92/18.21  tff(c_2299, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdf_type), true, ifeq(iext(P_102, uri_rdf__3, uri_rdf_Property), true, true, true), true)=true))).
% 28.92/18.21  tff(c_2533, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_domain), true, ifeq(iext(P_102, uri_rdfs_subPropertyOf, uri_rdf_Property), true, true, true), true)=true))).
% 28.92/18.21  tff(c_2515, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdf_type), true, ifeq(iext(P_102, uri_rdf_XMLLiteral, uri_rdfs_Datatype), true, true, true), true)=true))).
% 28.92/18.21  tff(c_2491, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_domain), true, ifeq(iext(P_102, uri_rdf_first, uri_rdf_List), true, true, true), true)=true))).
% 28.92/18.21  tff(c_2431, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_domain), true, ifeq(iext(P_102, uri_rdf__1, uri_rdfs_Resource), true, true, true), true)=true))).
% 28.92/18.21  tff(c_2479, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_range), true, ifeq(iext(P_102, uri_rdfs_isDefinedBy, uri_rdfs_Resource), true, true, true), true)=true))).
% 28.92/18.21  tff(c_2305, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_owl_sameAs), true, ifeq(iext(P_102, uri_ex_w, uri_ex_u), true, true, true), true)=true))).
% 28.92/18.21  tff(c_2383, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_range), true, ifeq(iext(P_102, uri_rdf__3, uri_rdfs_Resource), true, true, true), true)=true))).
% 28.92/18.21  tff(c_2590, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdf_type), true, ifeq(iext(P_102, uri_rdf__2, uri_rdf_Property), true, true, true), true)=true))).
% 28.92/18.21  tff(c_2662, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_range), true, ifeq(iext(P_102, uri_rdf_value, uri_rdfs_Resource), true, true, true), true)=true))).
% 28.92/18.21  tff(c_2602, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_range), true, ifeq(iext(P_102, uri_rdfs_range, uri_rdfs_Class), true, true, true), true)=true))).
% 28.92/18.21  tff(c_2467, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_range), true, ifeq(iext(P_102, uri_rdfs_member, uri_rdfs_Resource), true, true, true), true)=true))).
% 28.92/18.21  tff(c_32226, plain, (![X_747, Y_748]: (ifeq(iext(uri_rdfs_isDefinedBy, X_747, Y_748), true, iext(uri_rdfs_seeAlso, X_747, Y_748), true)=true))).
% 28.92/18.21  tff(c_2485, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_domain), true, ifeq(iext(P_102, uri_rdf_type, uri_rdfs_Resource), true, true, true), true)=true))).
% 28.92/18.21  tff(c_2377, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdf_type), true, ifeq(iext(P_102, uri_rdf__2, uri_rdfs_ContainerMembershipProperty), true, true, true), true)=true))).
% 28.92/18.21  tff(c_2407, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_subClassOf), true, ifeq(iext(P_102, uri_rdfs_Datatype, uri_rdfs_Class), true, true, true), true)=true))).
% 28.92/18.21  tff(c_2389, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_range), true, ifeq(iext(P_102, uri_rdfs_domain, uri_rdfs_Class), true, true, true), true)=true))).
% 28.92/18.21  tff(c_2413, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_domain), true, ifeq(iext(P_102, uri_rdf__3, uri_rdfs_Resource), true, true, true), true)=true))).
% 28.92/18.21  tff(c_31687, plain, (![D_741]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_741), true, icext(D_741, uri_rdfs_Resource), true)=true))).
% 28.92/18.21  tff(c_31619, plain, (![D_739]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_739), true, icext(D_739, uri_rdfs_subClassOf), true)=true))).
% 28.92/18.21  tff(c_31553, plain, (![D_737]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_737), true, icext(D_737, uri_rdfs_seeAlso), true)=true))).
% 28.92/18.21  tff(c_31487, plain, (![D_735]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_735), true, icext(D_735, uri_ex_Person), true)=true))).
% 28.92/18.21  tff(c_2638, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_domain), true, ifeq(iext(P_102, uri_rdfs_range, uri_rdf_Property), true, true, true), true)=true))).
% 28.92/18.21  tff(c_31302, plain, (![D_732]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_732), true, icext(D_732, uri_rdfs_range), true)=true))).
% 28.92/18.21  tff(c_31236, plain, (![D_730]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_730), true, icext(D_730, uri_owl_sameAs), true)=true))).
% 28.92/18.21  tff(c_31142, plain, (![D_728]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_728), true, icext(D_728, uri_rdfs_Class), true)=true))).
% 28.92/18.21  tff(c_2425, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdf_type), true, ifeq(iext(P_102, uri_rdf_object, uri_rdf_Property), true, true, true), true)=true))).
% 28.92/18.21  tff(c_30960, plain, (![D_725]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_725), true, icext(D_725, uri_rdf_Bag), true)=true))).
% 28.92/18.21  tff(c_30892, plain, (![D_723]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_723), true, icext(D_723, uri_rdfs_Seq), true)=true))).
% 28.92/18.21  tff(c_2575, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdf_type), true, ifeq(iext(P_102, uri_rdf_Property, uri_rdfs_Class), true, true, true), true)=true))).
% 28.92/18.21  tff(c_30711, plain, (![D_720]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_720), true, icext(D_720, uri_rdfs_Datatype), true)=true))).
% 28.92/18.21  tff(c_30526, plain, (![D_717]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_717), true, icext(D_717, uri_rdfs_Container), true)=true))).
% 28.92/18.21  tff(c_2371, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdf_type), true, ifeq(iext(P_102, uri_rdf_nil, uri_rdf_List), true, true, true), true)=true))).
% 28.92/18.21  tff(c_30460, plain, (![D_715]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_715), true, icext(D_715, uri_rdfs_ContainerMembershipProperty), true)=true))).
% 28.92/18.21  tff(c_30394, plain, (![D_713]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_713), true, icext(D_713, uri_rdfs_Literal), true)=true))).
% 28.92/18.21  tff(c_2545, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdf_type), true, ifeq(iext(P_102, uri_rdf_subject, uri_rdf_Property), true, true, true), true)=true))).
% 28.92/18.21  tff(c_30203, plain, (![D_710]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_710), true, icext(D_710, uri_rdf_XMLLiteral), true)=true))).
% 28.92/18.21  tff(c_30137, plain, (![D_708]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_708), true, icext(D_708, uri_rdf_Alt), true)=true))).
% 28.92/18.21  tff(c_30069, plain, (![C_706]: (ifeq(iext(uri_rdfs_subClassOf, C_706, uri_rdfs_Seq), true, iext(uri_rdfs_subClassOf, C_706, uri_rdfs_Container), true)=true))).
% 28.92/18.21  tff(c_30004, plain, (![D_704]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_704), true, icext(D_704, uri_rdfs_Statement), true)=true))).
% 28.92/18.21  tff(c_29938, plain, (![D_702]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_702), true, icext(D_702, uri_rdfs_isDefinedBy), true)=true))).
% 28.92/18.21  tff(c_29872, plain, (![D_700]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_700), true, icext(D_700, uri_rdfs_subPropertyOf), true)=true))).
% 28.92/18.21  tff(c_29805, plain, (![D_698]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_698), true, icext(D_698, uri_rdf_List), true)=true))).
% 28.92/18.21  tff(c_29739, plain, (![D_696]: (ifeq(iext(uri_rdfs_subClassOf, uri_ex_Person, D_696), true, icext(D_696, uri_ex_w), true)=true))).
% 28.92/18.21  tff(c_29673, plain, (![D_694]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_694), true, icext(D_694, uri_rdfs_domain), true)=true))).
% 28.92/18.21  tff(c_2353, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_range), true, ifeq(iext(P_102, uri_rdf_predicate, uri_rdfs_Resource), true, true, true), true)=true))).
% 28.92/18.21  tff(c_29487, plain, (![D_691]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_691), true, icext(D_691, uri_rdfs_member), true)=true))).
% 28.92/18.21  tff(c_29421, plain, (![D_689]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_689), true, icext(D_689, uri_rdf_predicate), true)=true))).
% 28.92/18.21  tff(c_29339, plain, (![D_687]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, D_687), true, icext(D_687, uri_rdf__1), true)=true))).
% 28.92/18.21  tff(c_16528, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_48), true, iext(Q_48, uri_ex_Person, uri_ex_Person), true)=true))).
% 28.92/18.21  tff(c_2419, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdf_type), true, ifeq(iext(P_102, uri_rdf__3, uri_rdfs_ContainerMembershipProperty), true, true, true), true)=true))).
% 28.92/18.21  tff(c_12827, 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))).
% 28.92/18.21  tff(c_16317, plain, (![E_41]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Resource, E_41), true, iext(uri_rdfs_subClassOf, uri_ex_Person, E_41), true)=true))).
% 28.92/18.21  tff(c_16319, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_48), true, iext(Q_48, uri_ex_Person, uri_rdfs_Resource), true)=true))).
% 28.92/18.21  tff(c_12777, 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))).
% 28.92/18.21  tff(c_12116, 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))).
% 28.92/18.21  tff(c_2656, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_range), true, ifeq(iext(P_102, uri_rdfs_subClassOf, uri_rdfs_Class), true, true, true), true)=true))).
% 28.92/18.21  tff(c_12185, 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))).
% 28.92/18.22  tff(c_16251, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, uri_ex_Person, uri_rdfs_Class), true)=true))).
% 28.92/18.22  tff(c_13716, 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))).
% 28.92/18.22  tff(c_28796, plain, (![D_671]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, D_671), true, icext(D_671, uri_rdf_XMLLiteral), true)=true))).
% 28.92/18.22  tff(c_13781, 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))).
% 28.92/18.22  tff(c_2584, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_subPropertyOf), true, ifeq(iext(P_102, uri_rdfs_isDefinedBy, uri_rdfs_seeAlso), true, true, true), true)=true))).
% 28.92/18.22  tff(c_11956, 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))).
% 28.92/18.22  tff(c_11890, 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))).
% 28.92/18.22  tff(c_28496, plain, (![D_662]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_662), true, icext(D_662, uri_rdf_rest), true)=true))).
% 28.92/18.22  tff(c_11888, 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))).
% 28.92/18.22  tff(c_12589, 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))).
% 28.92/18.22  tff(c_2596, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_subClassOf), true, ifeq(iext(P_102, uri_rdfs_ContainerMembershipProperty, uri_rdf_Property), true, true, true), true)=true))).
% 28.92/18.22  tff(c_12523, 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))).
% 28.92/18.22  tff(c_12587, 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))).
% 28.92/18.22  tff(c_28180, plain, (![D_653]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_653), true, icext(D_653, uri_rdf_first), true)=true))).
% 28.92/18.22  tff(c_11630, 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))).
% 28.92/18.22  tff(c_11678, 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))).
% 28.92/18.22  tff(c_11315, 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))).
% 28.92/18.22  tff(c_2551, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_range), true, ifeq(iext(P_102, uri_rdf_rest, uri_rdf_List), true, true, true), true)=true))).
% 28.92/18.22  tff(c_11582, 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))).
% 28.92/18.22  tff(c_11219, 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))).
% 28.92/18.22  tff(c_11170, 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))).
% 28.92/18.22  tff(c_11268, 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))).
% 28.92/18.22  tff(c_11751, 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))).
% 28.92/18.22  tff(c_11799, 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))).
% 28.92/18.22  tff(c_12459, 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))).
% 28.92/18.22  tff(c_10968, 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))).
% 28.92/18.22  tff(c_2317, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_range), true, ifeq(iext(P_102, uri_rdfs_label, uri_rdfs_Literal), true, true, true), true)=true))).
% 28.92/18.22  tff(c_11050, 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))).
% 28.92/18.22  tff(c_14904, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, uri_ex_w, uri_ex_Person), true)=true))).
% 28.92/18.22  tff(c_11439, 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))).
% 28.92/18.22  tff(c_10674, 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))).
% 28.92/18.22  tff(c_10304, 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))).
% 28.92/18.22  tff(c_9792, 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))).
% 28.92/18.22  tff(c_8917, 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))).
% 28.92/18.22  tff(c_5664, 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))).
% 28.92/18.22  tff(c_2329, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_range), true, ifeq(iext(P_102, uri_rdf__2, uri_rdfs_Resource), true, true, true), true)=true))).
% 28.92/18.22  tff(c_7115, 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))).
% 28.92/18.22  tff(c_9696, 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))).
% 28.92/18.22  tff(c_5730, 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))).
% 28.92/18.22  tff(c_27297, plain, (![C_623]: (ifeq(iext(uri_rdfs_subClassOf, C_623, uri_rdf_Bag), true, iext(uri_rdfs_subClassOf, C_623, uri_rdfs_Container), true)=true))).
% 28.92/18.22  tff(c_8623, 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))).
% 28.92/18.22  tff(c_27146, plain, (![D_618]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_List, D_618), true, icext(D_618, uri_rdf_nil), true)=true))).
% 28.92/18.22  tff(c_27072, plain, (![P_615]: (ifeq(iext(uri_rdfs_subPropertyOf, P_615, uri_rdfs_isDefinedBy), true, iext(uri_rdfs_subPropertyOf, P_615, uri_rdfs_seeAlso), true)=true))).
% 28.92/18.22  tff(c_4611, 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))).
% 28.92/18.22  tff(c_10676, 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))).
% 28.92/18.22  tff(c_26940, plain, (![D_610]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_610), true, icext(D_610, uri_rdf__3), true)=true))).
% 28.92/18.22  tff(c_4841, 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))).
% 28.92/18.22  tff(c_5422, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, uri_owl_sameAs, uri_rdf_Property), true)=true))).
% 28.92/18.22  tff(c_6672, 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))).
% 28.92/18.22  tff(c_2521, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdf_type), true, ifeq(iext(P_102, uri_rdf_type, uri_rdf_Property), true, true, true), true)=true))).
% 28.92/18.22  tff(c_8259, 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))).
% 28.92/18.22  tff(c_9335, 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))).
% 28.92/18.22  tff(c_9169, 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))).
% 28.92/18.22  tff(c_8919, 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))).
% 28.92/18.22  tff(c_6923, 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))).
% 28.92/18.22  tff(c_7986, 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))).
% 28.92/18.22  tff(c_10914, 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))).
% 28.92/18.22  tff(c_2437, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_domain), true, ifeq(iext(P_102, uri_rdf_predicate, uri_rdfs_Statement), true, true, true), true)=true))).
% 28.92/18.22  tff(c_6508, 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))).
% 28.92/18.22  tff(c_6050, 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))).
% 28.92/18.22  tff(c_6210, 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))).
% 28.92/18.22  tff(c_7835, 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))).
% 28.92/18.22  tff(c_10067, 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))).
% 28.92/18.22  tff(c_2395, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_domain), true, ifeq(iext(P_102, uri_rdfs_label, uri_rdfs_Resource), true, true, true), true)=true))).
% 28.92/18.22  tff(c_5919, 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))).
% 28.92/18.22  tff(c_8485, 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))).
% 28.92/18.22  tff(c_10371, 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))).
% 28.92/18.22  tff(c_26068, plain, (![D_583]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_583), true, icext(D_583, uri_rdfs_label), true)=true))).
% 28.92/18.22  tff(c_9336, 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))).
% 28.92/18.22  tff(c_6146, 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))).
% 28.92/18.22  tff(c_2527, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_domain), true, ifeq(iext(P_102, uri_rdf_object, uri_rdfs_Statement), true, true, true), true)=true))).
% 28.92/18.22  tff(c_25745, plain, (![D_574]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_574), true, icext(D_574, uri_rdf_object), true)=true))).
% 28.92/18.22  tff(c_10214, 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))).
% 28.92/18.22  tff(c_9940, 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))).
% 28.92/18.22  tff(c_2497, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdfs_domain), true, ifeq(iext(P_102, uri_rdfs_subClassOf, uri_rdfs_Class), true, true, true), true)=true))).
% 28.92/18.22  tff(c_10844, 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))).
% 28.92/18.22  tff(c_8418, 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))).
% 28.92/18.22  tff(c_25446, plain, (![D_565]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_565), true, icext(D_565, uri_rdf_Property), true)=true))).
% 28.92/18.22  tff(c_10369, 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))).
% 28.92/18.22  tff(c_9794, 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))).
% 28.92/18.22  tff(c_7837, 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))).
% 28.92/18.22  tff(c_4907, 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))).
% 28.92/18.22  tff(c_10009, 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))).
% 28.92/18.22  tff(c_25254, plain, (![D_557]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_557), true, icext(D_557, uri_rdf_type), true)=true))).
% 28.92/18.22  tff(c_25164, plain, (![C_554]: (ifeq(iext(uri_rdfs_subClassOf, C_554, uri_rdf_Alt), true, iext(uri_rdfs_subClassOf, C_554, uri_rdfs_Container), true)=true))).
% 28.92/18.22  tff(c_7315, 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))).
% 28.92/18.22  tff(c_8097, 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))).
% 28.92/18.22  tff(c_5920, 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))).
% 28.92/18.22  tff(c_10215, 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))).
% 28.92/18.22  tff(c_7117, 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))).
% 28.92/18.22  tff(c_6921, 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))).
% 28.92/18.22  tff(c_10148, 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))).
% 28.92/18.22  tff(c_9551, 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))).
% 28.92/18.22  tff(c_8354, 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))).
% 28.92/18.22  tff(c_4780, 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))).
% 28.92/18.22  tff(c_6297, 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))).
% 28.92/18.22  tff(c_13508, 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))).
% 28.92/18.22  tff(c_4905, 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))).
% 28.92/18.22  tff(c_8042, 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))).
% 28.92/18.22  tff(c_2626, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdf_type), true, ifeq(iext(P_102, uri_rdf_value, uri_rdf_Property), true, true, true), true)=true))).
% 28.92/18.22  tff(c_9171, 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))).
% 28.92/18.22  tff(c_8483, 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))).
% 28.92/18.22  tff(c_9632, 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))).
% 28.92/18.22  tff(c_13607, 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))).
% 28.92/18.22  tff(c_2347, plain, (![P_102]: (ifeq(iext(uri_rdfs_subPropertyOf, P_102, uri_rdf_type), true, ifeq(iext(P_102, uri_rdf__1, uri_rdfs_ContainerMembershipProperty), true, true, true), true)=true))).
% 28.92/18.22  tff(c_10610, 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))).
% 28.92/18.22  tff(c_10543, 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))).
% 28.92/18.22  tff(c_4712, plain, (![Q_48]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_48), true, iext(Q_48, uri_owl_sameAs, uri_owl_sameAs), true)=true))).
% 28.92/18.22  tff(c_4528, plain, (![Q_48, X_138]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_48), true, iext(Q_48, X_138, uri_rdfs_Resource), true)=true))).
% 28.92/18.22  tff(c_2671, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_103), true, iext(Q_103, uri_rdf_type, uri_rdfs_Class), true)=true))).
% 28.92/18.22  tff(c_2707, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_103), true, iext(Q_103, uri_rdfs_domain, uri_rdf_Property), true)=true))).
% 28.92/18.22  tff(c_2722, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_103), true, iext(Q_103, uri_rdf_XMLLiteral, uri_rdfs_Literal), true)=true))).
% 28.92/18.22  tff(c_2725, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_103), true, iext(Q_103, uri_rdfs_seeAlso, uri_rdfs_Resource), true)=true))).
% 28.92/18.22  tff(c_2726, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_103), true, iext(Q_103, uri_rdfs_subClassOf, uri_rdfs_Class), true)=true))).
% 28.92/18.22  tff(c_2675, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_103), true, iext(Q_103, uri_rdf__1, uri_rdfs_ContainerMembershipProperty), true)=true))).
% 28.92/18.23  tff(c_2794, plain, (![E_107]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Class, E_107), true, iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, E_107), true)=true))).
% 28.92/18.23  tff(c_23974, plain, (![D_513]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_513), true, icext(D_513, uri_rdf__2), true)=true))).
% 28.92/18.23  tff(c_2708, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_103), true, iext(Q_103, uri_rdf_subject, uri_rdf_Property), true)=true))).
% 28.92/18.23  tff(c_2694, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_103), true, iext(Q_103, uri_rdf_Bag, uri_rdfs_Container), true)=true))).
% 28.92/18.23  tff(c_2712, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_103), true, iext(Q_103, uri_rdf_Alt, uri_rdfs_Container), true)=true))).
% 28.92/18.23  tff(c_2699, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_103), true, iext(Q_103, uri_rdf_first, uri_rdf_List), true)=true))).
% 28.92/18.23  tff(c_2700, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_103), true, iext(Q_103, uri_rdfs_subClassOf, uri_rdfs_Class), true)=true))).
% 28.92/18.23  tff(c_2711, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_103), true, iext(Q_103, uri_rdf_value, uri_rdfs_Resource), true)=true))).
% 28.92/18.23  tff(c_2672, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_103), true, iext(Q_103, uri_rdf__2, uri_rdfs_Resource), true)=true))).
% 28.92/18.23  tff(c_2716, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_103), true, iext(Q_103, uri_rdfs_ContainerMembershipProperty, uri_rdf_Property), true)=true))).
% 28.92/18.23  tff(c_2717, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_103), true, iext(Q_103, uri_rdfs_range, uri_rdfs_Class), true)=true))).
% 28.92/18.23  tff(c_2697, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_103), true, iext(Q_103, uri_rdfs_isDefinedBy, uri_rdfs_Resource), true)=true))).
% 28.92/18.23  tff(c_2693, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_103), true, iext(Q_103, uri_rdfs_subPropertyOf, uri_rdf_Property), true)=true))).
% 28.92/18.23  tff(c_2685, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_103), true, iext(Q_103, uri_rdfs_Datatype, uri_rdfs_Class), true)=true))).
% 28.92/18.23  tff(c_2705, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_103), true, iext(Q_103, uri_rdf_object, uri_rdfs_Statement), true)=true))).
% 28.92/18.23  tff(c_2670, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_103), true, iext(Q_103, uri_rdfs_label, uri_rdfs_Literal), true)=true))).
% 28.92/18.23  tff(c_2796, plain, (![E_107]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Container, E_107), true, iext(uri_rdfs_subClassOf, uri_rdfs_Seq, E_107), true)=true))).
% 28.92/18.23  tff(c_2679, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_103), true, iext(Q_103, uri_rdf_nil, uri_rdf_List), true)=true))).
% 28.92/18.23  tff(c_23602, plain, (![D_495]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_495), true, icext(D_495, uri_rdf_value), true)=true))).
% 28.92/18.23  tff(c_2684, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_103), true, iext(Q_103, uri_rdf_rest, uri_rdf_Property), true)=true))).
% 28.92/18.23  tff(c_2710, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_103), true, iext(Q_103, uri_rdfs_member, uri_rdfs_Resource), true)=true))).
% 28.92/18.23  tff(c_2798, plain, (![E_107]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, E_107), true, iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, E_107), true)=true))).
% 28.92/18.23  tff(c_2724, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_103), true, iext(Q_103, uri_rdfs_seeAlso, uri_rdfs_Resource), true)=true))).
% 28.92/18.23  tff(c_2718, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_103), true, iext(Q_103, uri_rdfs_comment, uri_rdfs_Resource), true)=true))).
% 28.92/18.23  tff(c_2681, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_103), true, iext(Q_103, uri_rdf__3, uri_rdfs_Resource), true)=true))).
% 28.92/18.23  tff(c_2720, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_103), true, iext(Q_103, uri_rdf_first, uri_rdf_Property), true)=true))).
% 28.92/18.23  tff(c_23371, plain, (![D_486]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, D_486), true, icext(D_486, uri_rdf__2), true)=true))).
% 28.92/18.23  tff(c_2713, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_103), true, iext(Q_103, uri_rdf_Property, uri_rdfs_Class), true)=true))).
% 28.92/18.23  tff(c_2797, plain, (![E_107]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Container, E_107), true, iext(uri_rdfs_subClassOf, uri_rdf_Alt, E_107), true)=true))).
% 28.92/18.23  tff(c_2677, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_103), true, iext(Q_103, uri_rdf_subject, uri_rdfs_Statement), true)=true))).
% 28.92/18.23  tff(c_2719, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_103), true, iext(Q_103, uri_rdf_first, uri_rdfs_Resource), true)=true))).
% 28.92/18.23  tff(c_2704, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_103), true, iext(Q_103, uri_rdf_type, uri_rdf_Property), true)=true))).
% 28.92/18.23  tff(c_2680, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_103), true, iext(Q_103, uri_rdf__2, uri_rdfs_ContainerMembershipProperty), true)=true))).
% 28.92/18.23  tff(c_2695, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_103), true, iext(Q_103, uri_rdfs_member, uri_rdfs_Resource), true)=true))).
% 28.92/18.23  tff(c_23164, plain, (![D_477]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_477), true, icext(D_477, uri_rdfs_comment), true)=true))).
% 28.92/18.23  tff(c_2709, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_103), true, iext(Q_103, uri_rdf_rest, uri_rdf_List), true)=true))).
% 28.92/18.23  tff(c_2667, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_103), true, iext(Q_103, uri_rdf__3, uri_rdf_Property), true)=true))).
% 28.92/18.23  tff(c_2690, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_103), true, iext(Q_103, uri_rdf_predicate, uri_rdfs_Statement), true)=true))).
% 28.92/18.23  tff(c_2723, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_103), true, iext(Q_103, uri_rdfs_range, uri_rdf_Property), true)=true))).
% 28.92/18.23  tff(c_2683, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_103), true, iext(Q_103, uri_rdfs_label, uri_rdfs_Resource), true)=true))).
% 28.92/18.23  tff(c_2727, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_103), true, iext(Q_103, uri_rdf_value, uri_rdfs_Resource), true)=true))).
% 28.92/18.23  tff(c_2688, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_103), true, iext(Q_103, uri_rdf_object, uri_rdf_Property), true)=true))).
% 28.92/18.23  tff(c_22963, plain, (![D_468]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_468), true, icext(D_468, uri_rdf__1), true)=true))).
% 28.92/18.23  tff(c_2676, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_103), true, iext(Q_103, uri_rdf_predicate, uri_rdfs_Resource), true)=true))).
% 28.92/18.23  tff(c_2795, plain, (![E_107]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Container, E_107), true, iext(uri_rdfs_subClassOf, uri_rdf_Bag, E_107), true)=true))).
% 28.92/18.23  tff(c_2686, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_103), true, iext(Q_103, uri_rdf__3, uri_rdfs_Resource), true)=true))).
% 28.92/18.23  tff(c_16529, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_ex_Person), true)=true))).
% 28.92/18.23  tff(c_16530, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_ex_Person), true)=true))).
% 28.92/18.23  tff(c_12781, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_predicate), true)=true))).
% 28.92/18.23  tff(c_12780, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_predicate), true)=true))).
% 28.92/18.23  tff(c_2799, plain, (![E_107]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Literal, E_107), true, iext(uri_rdfs_subClassOf, uri_rdf_XMLLiteral, E_107), true)=true))).
% 28.92/18.23  tff(c_12188, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_member), true)=true))).
% 28.92/18.23  tff(c_13784, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_label), true)=true))).
% 28.92/18.23  tff(c_13720, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_comment), true)=true))).
% 28.92/18.23  tff(c_13719, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_comment), true)=true))).
% 28.92/18.23  tff(c_12117, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdfs_Resource), true)=true))).
% 28.92/18.23  tff(c_13785, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_label), true)=true))).
% 28.92/18.23  tff(c_2706, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_103), true, iext(Q_103, uri_rdfs_subPropertyOf, uri_rdf_Property), true)=true))).
% 28.92/18.23  tff(c_12525, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdf_List), true)=true))).
% 28.92/18.23  tff(c_11958, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdfs_Statement), true)=true))).
% 28.92/18.23  tff(c_22466, plain, (![D_449]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdf_Property, D_449), true, icext(D_449, uri_rdf_subject), true)=true))).
% 28.92/18.23  tff(c_12590, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdf_List), true)=true))).
% 28.92/18.23  tff(c_2678, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_103), true, iext(Q_103, uri_rdf__1, uri_rdfs_Resource), true)=true))).
% 28.92/18.23  tff(c_11891, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdfs_Statement), true)=true))).
% 28.92/18.23  tff(c_2674, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_103), true, iext(Q_103, uri_owl_sameAs, uri_ex_Person), true)=true))).
% 28.92/18.23  tff(c_2698, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_103), true, iext(Q_103, uri_rdf_type, uri_rdfs_Resource), true)=true))).
% 28.92/18.23  tff(c_22253, plain, (![D_442]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, D_442), true, icext(D_442, uri_rdf__3), true)=true))).
% 28.92/18.23  tff(c_14906, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_29), true, icext(C_29, uri_ex_Person), true)=true))).
% 28.92/18.23  tff(c_2682, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_103), true, iext(Q_103, uri_rdfs_domain, uri_rdfs_Class), true)=true))).
% 28.92/18.23  tff(c_22040, plain, (![C_88, X_60]: (ifeq(icext(C_88, X_60), true, true, true)=true))).
% 28.92/18.23  tff(c_10612, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdfs_Seq), true)=true))).
% 28.92/18.23  tff(c_2279, plain, (![R_100]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_seeAlso, R_100), true, iext(uri_rdfs_subPropertyOf, uri_rdfs_isDefinedBy, R_100), true)=true))).
% 28.92/18.23  tff(c_4613, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdfs_Datatype), true)=true))).
% 28.92/18.23  tff(c_21575, plain, (![D_431, X_432]: (ifeq(iext(uri_rdfs_subClassOf, uri_rdfs_Resource, D_431), true, icext(D_431, X_432), true)=true))).
% 28.92/18.23  tff(c_10151, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_subPropertyOf), true)=true))).
% 28.92/18.23  tff(c_2669, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_103), true, iext(Q_103, uri_rdfs_isDefinedBy, uri_rdfs_Resource), true)=true))).
% 28.92/18.23  tff(c_10848, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_domain), true)=true))).
% 28.92/18.23  tff(c_21453, plain, (![X_424, Y_425]: (ifeq(iext(uri_rdf_predicate, X_424, Y_425), true, icext(uri_rdfs_Statement, X_424), true)=true))).
% 28.92/18.23  tff(c_2701, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_103), true, iext(Q_103, uri_rdf_rest, uri_rdf_List), true)=true))).
% 28.92/18.23  tff(c_21080, plain, (![X_419, Y_420]: (ifeq(iext(uri_rdfs_range, X_419, Y_420), true, icext(uri_rdf_Property, X_419), true)=true))).
% 28.92/18.23  tff(c_10011, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdf_XMLLiteral), true)=true))).
% 28.92/18.23  tff(c_5666, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf__3), true)=true))).
% 28.92/18.23  tff(c_2721, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_103), true, iext(Q_103, uri_rdf_value, uri_rdf_Property), true)=true))).
% 28.92/18.23  tff(c_20454, plain, (![X_411, Y_412]: (ifeq(iext(uri_rdfs_subClassOf, X_411, Y_412), true, icext(uri_rdfs_Class, Y_412), true)=true))).
% 28.92/18.23  tff(c_10152, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_subPropertyOf), true)=true))).
% 28.92/18.23  tff(c_7838, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdfs_Class), true)=true))).
% 28.92/18.23  tff(c_2692, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_103), true, iext(Q_103, uri_rdfs_comment, uri_rdfs_Literal), true)=true))).
% 28.92/18.23  tff(c_8356, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdfs_ContainerMembershipProperty), true)=true))).
% 28.92/18.23  tff(c_20317, plain, (![X_403, Y_404]: (ifeq(iext(uri_rdf_object, X_403, Y_404), true, icext(uri_rdfs_Statement, X_403), true)=true))).
% 28.92/18.23  tff(c_2691, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_103), true, iext(Q_103, uri_rdf_subject, uri_rdfs_Resource), true)=true))).
% 28.92/18.23  tff(c_8422, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_subject), true)=true))).
% 28.92/18.23  tff(c_4843, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_type), true)=true))).
% 28.92/18.23  tff(c_20211, plain, (![X_396, Y_397]: (ifeq(iext(uri_rdf_subject, X_396, Y_397), true, icext(uri_rdfs_Statement, X_396), true)=true))).
% 28.92/18.23  tff(c_10307, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_rest), true)=true))).
% 28.92/18.23  tff(c_8421, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_subject), true)=true))).
% 28.92/18.23  tff(c_7989, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_object), true)=true))).
% 28.92/18.23  tff(c_2714, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_103), true, iext(Q_103, uri_rdfs_isDefinedBy, uri_rdfs_seeAlso), true)=true))).
% 28.92/18.23  tff(c_10308, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_rest), true)=true))).
% 28.92/18.23  tff(c_20054, plain, (![X_387, Y_388]: (ifeq(iext(uri_rdf_first, X_387, Y_388), true, icext(uri_rdf_List, X_387), true)=true))).
% 28.92/18.23  tff(c_9554, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_seeAlso), true)=true))).
% 28.92/18.23  tff(c_2703, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_103), true, iext(Q_103, uri_rdf_XMLLiteral, uri_rdfs_Datatype), true)=true))).
% 28.92/18.23  tff(c_7839, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdfs_Resource), true)=true))).
% 28.92/18.23  tff(c_19589, plain, (![X_380, Y_381]: (ifeq(iext(uri_rdfs_subPropertyOf, X_380, Y_381), true, icext(uri_rdf_Property, Y_381), true)=true))).
% 28.92/18.23  tff(c_10918, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf__1), true)=true))).
% 28.92/18.23  tff(c_6213, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_value), true)=true))).
% 28.92/18.23  tff(c_2715, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_103), true, iext(Q_103, uri_rdf__2, uri_rdf_Property), true)=true))).
% 28.92/18.23  tff(c_6674, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdf_Bag), true)=true))).
% 28.92/18.23  tff(c_19444, plain, (![X_372, Y_373]: (ifeq(iext(uri_owl_sameAs, X_372, Y_373), true, icext(uri_ex_Person, X_372), true)=true))).
% 28.92/18.23  tff(c_7317, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_subClassOf), true)=true))).
% 28.92/18.23  tff(c_10847, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_domain), true)=true))).
% 28.92/18.23  tff(c_2668, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_owl_sameAs, Q_103), true, iext(Q_103, uri_ex_w, uri_ex_u), true)=true))).
% 28.92/18.23  tff(c_4714, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_owl_sameAs), true)=true))).
% 28.92/18.23  tff(c_19299, plain, (![X_364, Y_365]: (ifeq(iext(uri_rdf_rest, X_364, Y_365), true, icext(uri_rdf_List, X_364), true)=true))).
% 28.92/18.23  tff(c_9699, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_first), true)=true))).
% 28.92/18.23  tff(c_2696, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_103), true, iext(Q_103, uri_rdf__2, uri_rdfs_Resource), true)=true))).
% 28.92/18.23  tff(c_10545, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_29), true, icext(C_29, uri_rdf_Alt), true)=true))).
% 28.92/18.23  tff(c_19189, plain, (![X_357, Y_358]: (ifeq(iext(uri_rdfs_comment, X_357, Y_358), true, icext(uri_rdfs_Literal, Y_358), true)=true))).
% 28.92/18.23  tff(c_4715, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_owl_sameAs), true)=true))).
% 28.92/18.23  tff(c_6300, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdfs_range), true)=true))).
% 28.92/18.23  tff(c_2687, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_103), true, iext(Q_103, uri_rdf__3, uri_rdfs_ContainerMembershipProperty), true)=true))).
% 28.92/18.23  tff(c_10372, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdfs_Container), true)=true))).
% 28.92/18.23  tff(c_5667, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf__3), true)=true))).
% 28.92/18.23  tff(c_19036, plain, (![X_348, Y_349]: (ifeq(iext(uri_rdfs_label, X_348, Y_349), true, icext(uri_rdfs_Literal, Y_349), true)=true))).
% 28.92/18.23  tff(c_8260, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdfs_Literal), true)=true))).
% 28.92/18.23  tff(c_6054, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_isDefinedBy), true)=true))).
% 28.92/18.23  tff(c_2689, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_103), true, iext(Q_103, uri_rdf__1, uri_rdfs_Resource), true)=true))).
% 28.92/18.23  tff(c_5922, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_member), true)=true))).
% 28.92/18.23  tff(c_7990, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_object), true)=true))).
% 28.92/18.23  tff(c_9700, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_first), true)=true))).
% 28.92/18.23  tff(c_18570, plain, (![X_338, Y_339]: (ifeq(iext(uri_rdfs_domain, X_338, Y_339), true, icext(uri_rdfs_Class, Y_339), true)=true))).
% 28.92/18.23  tff(c_4844, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf_type), true)=true))).
% 28.92/18.24  tff(c_6212, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf_value), true)=true))).
% 28.92/18.24  tff(c_2702, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_103), true, iext(Q_103, uri_rdfs_Seq, uri_rdfs_Container), true)=true))).
% 28.92/18.24  tff(c_4782, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf__2), true)=true))).
% 28.92/18.24  tff(c_4783, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdf__2), true)=true))).
% 28.92/18.24  tff(c_18061, plain, (![X_329, Y_330]: (ifeq(iext(uri_rdfs_subPropertyOf, X_329, Y_330), true, icext(uri_rdf_Property, X_329), true)=true))).
% 28.92/18.24  tff(c_6301, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_range), true)=true))).
% 28.92/18.24  tff(c_5921, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_19), true, icext(C_19, uri_rdf__1), true)=true))).
% 28.92/18.24  tff(c_2673, plain, (![Q_103]: (ifeq(iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_103), true, iext(Q_103, uri_rdf__1, uri_rdf_Property), true)=true))).
% 28.92/18.24  tff(c_7318, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_29), true, icext(C_29, uri_rdfs_subClassOf), true)=true))).
% 28.92/18.24  tff(c_4908, plain, (![C_19]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_19), true, icext(C_19, uri_rdf_Property), true)=true))).
% 28.92/18.24  tff(c_4530, plain, (![C_29]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_29), true, icext(C_29, uri_rdfs_Resource), true)=true))).
% 28.92/18.24  tff(c_17580, plain, (![X_319, Y_320]: (ifeq(iext(uri_rdfs_range, X_319, Y_320), true, icext(uri_rdfs_Class, Y_320), true)=true))).
% 28.92/18.24  tff(c_4529, plain, (![C_19, X_138]: (ifeq(iext(uri_rdfs_domain, uri_rdf_type, C_19), true, icext(C_19, X_138), true)=true))).
% 28.92/18.24  tff(c_2177, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_96), true, icext(C_96, uri_rdf__1), true)=true))).
% 28.92/18.24  tff(c_2201, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_96), true, icext(C_96, uri_rdfs_member), true)=true))).
% 28.92/18.24  tff(c_1864, plain, (![C_92]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_92), true, icext(C_92, uri_rdfs_Datatype), true)=true))).
% 28.92/18.24  tff(c_2179, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_96), true, icext(C_96, uri_rdf_subject), true)=true))).
% 28.92/18.24  tff(c_2221, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_96), true, icext(C_96, uri_rdf_value), true)=true))).
% 29.19/18.24  tff(c_17103, plain, (![X_304, Y_305]: (ifeq(iext(uri_rdf_rest, X_304, Y_305), true, icext(uri_rdf_List, Y_305), true)=true))).
% 29.19/18.24  tff(c_2167, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_96), true, icext(C_96, uri_rdfs_domain), true)=true))).
% 29.19/18.24  tff(c_2199, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_96), true, icext(C_96, uri_rdf_rest), true)=true))).
% 29.19/18.24  tff(c_2155, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_96), true, icext(C_96, uri_rdfs_label), true)=true))).
% 29.19/18.24  tff(c_2189, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_96), true, icext(C_96, uri_rdf_first), true)=true))).
% 29.19/18.24  tff(c_2166, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_96), true, icext(C_96, uri_rdf__3), true)=true))).
% 29.19/18.24  tff(c_2156, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_96), true, icext(C_96, uri_rdf_type), true)=true))).
% 29.19/18.24  tff(c_2218, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_96), true, icext(C_96, uri_rdfs_seeAlso), true)=true))).
% 29.19/18.24  tff(c_2169, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_96), true, icext(C_96, uri_rdfs_label), true)=true))).
% 29.19/18.24  tff(c_2154, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_96), true, icext(C_96, uri_rdfs_isDefinedBy), true)=true))).
% 29.19/18.24  tff(c_2206, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_96), true, icext(C_96, uri_rdfs_isDefinedBy), true)=true))).
% 29.19/18.24  tff(c_2173, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_96), true, icext(C_96, uri_rdf__3), true)=true))).
% 29.19/18.24  tff(c_1884, plain, (![C_92]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_92), true, icext(C_92, uri_rdfs_Literal), true)=true))).
% 29.19/18.24  tff(c_2182, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_96), true, icext(C_96, uri_rdf_Bag), true)=true))).
% 29.19/18.24  tff(c_15743, plain, (![X_285, Y_286]: (ifeq(iext(uri_rdf_type, X_285, Y_286), true, icext(uri_rdfs_Class, Y_286), true)=true))).
% 29.19/18.24  tff(c_16531, plain, (![X_33]: (ifeq(icext(uri_ex_Person, X_33), true, icext(uri_ex_Person, X_33), true)=true))).
% 29.19/18.24  tff(c_16470, plain, (iext(uri_rdfs_subClassOf, uri_ex_Person, uri_ex_Person)=true)).
% 29.19/18.24  tff(c_16262, plain, (iext(uri_rdfs_subClassOf, uri_ex_Person, uri_rdfs_Resource)=true)).
% 29.19/18.24  tff(c_16211, plain, (iext(uri_rdf_type, uri_ex_Person, uri_rdfs_Class)=true)).
% 29.19/18.24  tff(c_1829, plain, (![C_92]: (ifeq(iext(uri_rdfs_range, uri_rdfs_domain, C_92), true, icext(C_92, uri_ex_Person), true)=true))).
% 29.19/18.24  tff(c_16027, plain, (ic(uri_ex_Person)=true)).
% 29.19/18.24  tff(c_15913, plain, (icext(uri_rdfs_Class, uri_ex_Person)=true)).
% 29.19/18.24  tff(c_1875, plain, (![C_92]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_92), true, icext(C_92, uri_rdfs_seeAlso), true)=true))).
% 29.19/18.24  tff(c_2209, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_96), true, icext(C_96, uri_rdfs_range), true)=true))).
% 29.19/18.24  tff(c_2157, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_96), true, icext(C_96, uri_rdf__2), true)=true))).
% 29.19/18.24  tff(c_2180, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_96), true, icext(C_96, uri_rdfs_comment), true)=true))).
% 29.19/18.24  tff(c_2191, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_96), true, icext(C_96, uri_rdf_rest), true)=true))).
% 29.19/18.24  tff(c_2215, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_96), true, icext(C_96, uri_rdf_XMLLiteral), true)=true))).
% 29.19/18.24  tff(c_2212, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_96), true, icext(C_96, uri_rdf_first), true)=true))).
% 29.19/18.24  tff(c_2192, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_96), true, icext(C_96, uri_rdfs_Seq), true)=true))).
% 29.19/18.24  tff(c_14494, plain, (![X_258, Y_259]: (ifeq(iext(uri_rdfs_subClassOf, X_258, Y_259), true, icext(uri_rdfs_Class, X_258), true)=true))).
% 29.19/18.24  tff(c_2220, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_96), true, icext(C_96, uri_rdfs_subClassOf), true)=true))).
% 29.19/18.24  tff(c_2190, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_96), true, icext(C_96, uri_rdfs_subClassOf), true)=true))).
% 29.19/18.24  tff(c_14868, plain, (iext(uri_rdf_type, uri_ex_w, uri_ex_Person)=true)).
% 29.19/18.24  tff(c_14717, plain, (icext(uri_ex_Person, uri_ex_w)=true)).
% 29.19/18.24  tff(c_2152, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_owl_sameAs, C_96), true, icext(C_96, uri_ex_w), true)=true))).
% 29.19/18.24  tff(c_2196, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_96), true, icext(C_96, uri_rdfs_subPropertyOf), true)=true))).
% 29.19/18.24  tff(c_2185, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_96), true, icext(C_96, uri_rdf__2), true)=true))).
% 29.19/18.24  tff(c_1870, plain, (![C_92]: (ifeq(iext(uri_rdfs_range, uri_rdfs_range, C_92), true, icext(C_92, uri_rdf_List), true)=true))).
% 29.19/18.24  tff(c_1874, plain, (![C_92]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_92), true, icext(C_92, uri_rdfs_Class), true)=true))).
% 29.19/18.24  tff(c_1877, plain, (![C_92]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_92), true, icext(C_92, uri_rdf_Property), true)=true))).
% 29.19/18.24  tff(c_2211, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_96), true, icext(C_96, uri_rdfs_comment), true)=true))).
% 29.19/18.24  tff(c_1836, plain, (![C_92]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_92), true, icext(C_92, uri_rdf_List), true)=true))).
% 29.19/18.24  tff(c_1843, plain, (![C_92]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_92), true, icext(C_92, uri_rdfs_Class), true)=true))).
% 29.19/18.24  tff(c_12526, plain, (![X_33]: (ifeq(icext(uri_rdf_List, X_33), true, icext(uri_rdf_List, X_33), true)=true))).
% 29.19/18.24  tff(c_11959, plain, (![X_33]: (ifeq(icext(uri_rdfs_Statement, X_33), true, icext(uri_rdfs_Statement, X_33), true)=true))).
% 29.19/18.24  tff(c_10012, plain, (![X_33]: (ifeq(icext(uri_rdf_XMLLiteral, X_33), true, icext(uri_rdf_XMLLiteral, X_33), true)=true))).
% 29.19/18.24  tff(c_9943, plain, (![X_33]: (ifeq(icext(uri_rdf_Property, X_33), true, icext(uri_rdf_Property, X_33), true)=true))).
% 29.19/18.24  tff(c_8262, plain, (![X_33]: (ifeq(icext(uri_rdfs_Literal, X_33), true, icext(uri_rdfs_Literal, X_33), true)=true))).
% 29.19/18.24  tff(c_13004, plain, (![X_239, Y_240]: (ifeq(iext(uri_rdfs_domain, X_239, Y_240), true, icext(uri_rdf_Property, X_239), true)=true))).
% 29.19/18.24  tff(c_4614, plain, (![X_33]: (ifeq(icext(uri_rdfs_Datatype, X_33), true, icext(uri_rdfs_Datatype, X_33), true)=true))).
% 29.19/18.24  tff(c_10613, plain, (![X_33]: (ifeq(icext(uri_rdfs_Seq, X_33), true, icext(uri_rdfs_Seq, X_33), true)=true))).
% 29.19/18.24  tff(c_2219, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_96), true, icext(C_96, uri_rdfs_seeAlso), true)=true))).
% 29.19/18.24  tff(c_13730, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_label, uri_rdfs_label)=true)).
% 29.19/18.24  tff(c_13665, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_comment, uri_rdfs_comment)=true)).
% 29.19/18.24  tff(c_13623, plain, (ip(uri_rdfs_comment)=true)).
% 29.19/18.24  tff(c_13565, plain, (iext(uri_rdf_type, uri_rdfs_comment, uri_rdf_Property)=true)).
% 29.19/18.24  tff(c_13523, plain, (ip(uri_rdfs_label)=true)).
% 29.19/18.24  tff(c_13465, plain, (iext(uri_rdf_type, uri_rdfs_label, uri_rdf_Property)=true)).
% 29.19/18.24  tff(c_13169, plain, (icext(uri_rdf_Property, uri_rdfs_comment)=true)).
% 29.19/18.24  tff(c_13155, plain, (icext(uri_rdf_Property, uri_rdfs_label)=true)).
% 29.19/18.24  tff(c_5733, plain, (![X_33]: (ifeq(icext(uri_rdfs_Class, X_33), true, icext(uri_rdfs_Class, X_33), true)=true))).
% 29.19/18.24  tff(c_10546, plain, (![X_33]: (ifeq(icext(uri_rdf_Alt, X_33), true, icext(uri_rdf_Alt, X_33), true)=true))).
% 29.19/18.24  tff(c_6675, plain, (![X_33]: (ifeq(icext(uri_rdf_Bag, X_33), true, icext(uri_rdf_Bag, X_33), true)=true))).
% 29.19/18.24  tff(c_6149, plain, (![X_33]: (ifeq(icext(uri_rdfs_Container, X_33), true, icext(uri_rdfs_Container, X_33), true)=true))).
% 29.19/18.24  tff(c_8357, plain, (![X_33]: (ifeq(icext(uri_rdfs_ContainerMembershipProperty, X_33), true, icext(uri_rdfs_ContainerMembershipProperty, X_33), true)=true))).
% 29.19/18.24  tff(c_12791, plain, (iext(uri_rdf_type, uri_rdfs_Resource, uri_rdfs_Class)=true)).
% 29.19/18.24  tff(c_12726, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_predicate, uri_rdf_predicate)=true)).
% 29.19/18.24  tff(c_1861, plain, (![C_92]: (ifeq(iext(uri_rdfs_range, uri_rdfs_domain, C_92), true, icext(C_92, uri_rdfs_Class), true)=true))).
% 29.19/18.24  tff(c_12536, plain, (iext(uri_rdfs_subClassOf, uri_rdf_List, uri_rdfs_Resource)=true)).
% 29.19/18.24  tff(c_12470, plain, (iext(uri_rdfs_subClassOf, uri_rdf_List, uri_rdf_List)=true)).
% 29.19/18.24  tff(c_12422, plain, (iext(uri_rdf_type, uri_rdf_List, uri_rdfs_Class)=true)).
% 29.19/18.24  tff(c_12279, plain, (ic(uri_rdf_List)=true)).
% 29.19/18.24  tff(c_12221, plain, (icext(uri_rdfs_Class, uri_rdf_List)=true)).
% 29.19/18.24  tff(c_1862, plain, (![C_92]: (ifeq(iext(uri_rdfs_range, uri_rdfs_domain, C_92), true, icext(C_92, uri_rdf_List), true)=true))).
% 29.19/18.24  tff(c_12131, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_member, uri_rdfs_member)=true)).
% 29.19/18.24  tff(c_12060, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Resource, uri_rdfs_Resource)=true)).
% 29.19/18.24  tff(c_11903, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Statement, uri_rdfs_Statement)=true)).
% 29.19/18.24  tff(c_11837, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Statement, uri_rdfs_Resource)=true)).
% 29.19/18.24  tff(c_1888, plain, (![C_92]: (ifeq(iext(uri_rdfs_range, uri_rdfs_range, C_92), true, icext(C_92, uri_rdfs_Resource), true)=true))).
% 29.19/18.24  tff(c_11763, plain, (iext(uri_rdf_type, uri_rdf_XMLLiteral, uri_rdfs_Class)=true)).
% 29.19/18.24  tff(c_11715, plain, (iext(uri_rdf_type, uri_rdf_Alt, uri_rdfs_Class)=true)).
% 29.19/18.24  tff(c_2161, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_96), true, icext(C_96, uri_rdf_predicate), true)=true))).
% 29.19/18.24  tff(c_11642, plain, (iext(uri_rdf_type, uri_rdfs_ContainerMembershipProperty, uri_rdfs_Class)=true)).
% 29.19/18.24  tff(c_11594, plain, (iext(uri_rdf_type, uri_rdfs_Datatype, uri_rdfs_Class)=true)).
% 29.19/18.24  tff(c_11546, plain, (iext(uri_rdf_type, uri_rdf_Bag, uri_rdfs_Class)=true)).
% 29.19/18.24  tff(c_11397, plain, (iext(uri_rdf_type, uri_rdfs_member, uri_rdf_Property)=true)).
% 29.19/18.24  tff(c_11349, plain, (icext(uri_rdf_Property, uri_rdfs_member)=true)).
% 29.19/18.24  tff(c_2183, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_96), true, icext(C_96, uri_rdfs_member), true)=true))).
% 29.19/18.24  tff(c_11279, plain, (iext(uri_rdf_type, uri_rdfs_Container, uri_rdfs_Class)=true)).
% 29.19/18.24  tff(c_11232, plain, (iext(uri_rdf_type, uri_rdfs_Literal, uri_rdfs_Class)=true)).
% 29.19/18.24  tff(c_11183, plain, (iext(uri_rdf_type, uri_rdfs_Seq, uri_rdfs_Class)=true)).
% 29.19/18.24  tff(c_11134, plain, (iext(uri_rdf_type, uri_rdfs_Class, uri_rdfs_Class)=true)).
% 29.19/18.24  tff(c_2162, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_96), true, icext(C_96, uri_rdf_subject), true)=true))).
% 29.19/18.24  tff(c_11065, plain, (ip(uri_rdf_predicate)=true)).
% 29.19/18.24  tff(c_11008, plain, (iext(uri_rdf_type, uri_rdf_predicate, uri_rdf_Property)=true)).
% 29.19/18.24  tff(c_10932, plain, (iext(uri_rdf_type, uri_rdfs_Statement, uri_rdfs_Class)=true)).
% 29.19/18.24  tff(c_10862, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf__1, uri_rdf__1)=true)).
% 29.19/18.24  tff(c_10793, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, uri_rdfs_domain)=true)).
% 29.19/18.24  tff(c_2208, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_96), true, icext(C_96, uri_rdfs_ContainerMembershipProperty), true)=true))).
% 29.19/18.24  tff(c_10623, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Seq, uri_rdfs_Resource)=true)).
% 29.19/18.24  tff(c_10557, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Seq, uri_rdfs_Seq)=true)).
% 29.19/18.24  tff(c_10465, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Alt, uri_rdf_Alt)=true)).
% 29.19/18.24  tff(c_1825, plain, (![C_92]: (ifeq(iext(uri_rdfs_range, uri_rdfs_range, C_92), true, icext(C_92, uri_rdfs_Class), true)=true))).
% 29.19/18.24  tff(c_10318, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Container, uri_rdfs_Resource)=true)).
% 29.19/18.24  tff(c_10228, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_rest, uri_rdf_rest)=true)).
% 29.19/18.24  tff(c_1852, plain, (![C_92]: (ifeq(iext(uri_rdfs_range, uri_rdfs_range, C_92), true, icext(C_92, uri_rdf_Property), true)=true))).
% 29.19/18.24  tff(c_10163, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf__3, uri_rdfs_member)=true)).
% 29.19/18.24  tff(c_10097, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf)=true)).
% 29.19/18.24  tff(c_1822, plain, (![C_92]: (ifeq(iext(uri_rdfs_range, uri_owl_sameAs, C_92), true, icext(C_92, uri_ex_u), true)=true))).
% 29.19/18.24  tff(c_10025, plain, (iext(uri_rdf_type, uri_rdfs_domain, uri_rdf_Property)=true)).
% 29.19/18.24  tff(c_9956, plain, (iext(uri_rdfs_subClassOf, uri_rdf_XMLLiteral, uri_rdf_XMLLiteral)=true)).
% 29.19/18.24  tff(c_9887, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Property, uri_rdf_Property)=true)).
% 29.19/18.24  tff(c_9741, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Literal, uri_rdfs_Resource)=true)).
% 29.19/18.24  tff(c_9645, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_first, uri_rdf_first)=true)).
% 29.19/18.24  tff(c_9590, plain, (iext(uri_rdf_type, uri_rdfs_isDefinedBy, uri_rdf_Property)=true)).
% 29.19/18.24  tff(c_2159, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_96), true, icext(C_96, uri_owl_sameAs), true)=true))).
% 29.19/18.24  tff(c_9500, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_seeAlso, uri_rdfs_seeAlso)=true)).
% 29.19/18.24  tff(c_847, plain, (![S_75, O_76]: (ifeq(iext(uri_rdf_rest, S_75, O_76), true, true, true)=true))).
% 29.19/18.24  tff(c_9373, plain, (icext(uri_rdf_Property, uri_rdfs_domain)=true)).
% 29.19/18.24  tff(c_2197, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_96), true, icext(C_96, uri_rdfs_domain), true)=true))).
% 29.19/18.24  tff(c_9284, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf__2, uri_rdfs_member)=true)).
% 29.19/18.24  tff(c_2204, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_96), true, icext(C_96, uri_rdf_Alt), true)=true))).
% 29.19/18.24  tff(c_9118, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Alt, uri_rdfs_Resource)=true)).
% 29.19/18.24  tff(c_8932, plain, (icext(uri_rdf_Property, uri_rdfs_isDefinedBy)=true)).
% 29.19/18.24  tff(c_8846, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, uri_rdfs_Resource)=true)).
% 29.19/18.24  tff(c_2186, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_96), true, icext(C_96, uri_rdfs_isDefinedBy), true)=true))).
% 29.19/18.24  tff(c_1059, plain, (![S_5, O_6]: (ifeq(iext(uri_rdfs_range, S_5, O_6), true, true, true)=true))).
% 29.19/18.24  tff(c_8635, plain, (icext(uri_rdf_Property, uri_rdfs_subClassOf)=true)).
% 29.19/18.24  tff(c_8581, plain, (iext(uri_rdf_type, uri_rdfs_subClassOf, uri_rdf_Property)=true)).
% 29.19/18.24  tff(c_2203, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_96), true, icext(C_96, uri_rdf_value), true)=true))).
% 29.19/18.24  tff(c_8432, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Bag, uri_rdfs_Resource)=true)).
% 29.19/18.24  tff(c_8367, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_subject, uri_rdf_subject)=true)).
% 29.19/18.24  tff(c_8301, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, uri_rdfs_ContainerMembershipProperty)=true)).
% 29.19/18.24  tff(c_2216, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_96), true, icext(C_96, uri_rdfs_range), true)=true))).
% 29.19/18.24  tff(c_8203, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Literal, uri_rdfs_Literal)=true)).
% 29.19/18.24  tff(c_8110, plain, (icext(uri_rdf_Property, uri_rdfs_range)=true)).
% 29.19/18.24  tff(c_8055, plain, (iext(uri_rdf_type, uri_rdfs_range, uri_rdf_Property)=true)).
% 29.19/18.25  tff(c_8000, plain, (iext(uri_rdf_type, uri_rdfs_subPropertyOf, uri_rdf_Property)=true)).
% 29.19/18.25  tff(c_7935, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_object, uri_rdf_object)=true)).
% 29.19/18.25  tff(c_7784, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Class, uri_rdfs_Resource)=true)).
% 29.19/18.25  tff(c_2862, plain, (![S_5, O_6]: (ifeq(iext(uri_rdfs_subPropertyOf, S_5, O_6), true, true, true)=true))).
% 29.19/18.25  tff(c_1224, plain, (![S_5, O_6]: (ifeq(iext(uri_rdfs_domain, S_5, O_6), true, true, true)=true))).
% 29.19/18.25  tff(c_1869, plain, (![C_92]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_92), true, icext(C_92, uri_rdf_Property), true)=true))).
% 29.19/18.25  tff(c_7347, plain, (icext(uri_rdf_Property, uri_rdf_predicate)=true)).
% 29.19/18.25  tff(c_2178, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_96), true, icext(C_96, uri_rdf_predicate), true)=true))).
% 29.19/18.25  tff(c_7267, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, uri_rdfs_subClassOf)=true)).
% 29.19/18.25  tff(c_1845, plain, (![C_92]: (ifeq(iext(uri_rdfs_range, uri_rdf_type, C_92), true, icext(C_92, uri_rdfs_ContainerMembershipProperty), true)=true))).
% 29.19/18.25  tff(c_7064, plain, (iext(uri_rdfs_subClassOf, uri_rdf_XMLLiteral, uri_rdfs_Resource)=true)).
% 29.19/18.25  tff(c_6847, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, uri_rdfs_Resource)=true)).
% 29.19/18.25  tff(c_1873, plain, (![C_92]: (ifeq(iext(uri_rdfs_range, uri_rdfs_subClassOf, C_92), true, icext(C_92, uri_rdfs_Container), true)=true))).
% 29.19/18.25  tff(c_6705, plain, (icext(uri_rdf_Property, uri_rdfs_subPropertyOf)=true)).
% 29.19/18.25  tff(c_2181, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_96), true, icext(C_96, uri_rdfs_subPropertyOf), true)=true))).
% 29.19/18.25  tff(c_6619, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Bag, uri_rdf_Bag)=true)).
% 29.19/18.25  tff(c_6520, plain, (icext(uri_rdf_Property, uri_rdfs_seeAlso)=true)).
% 29.19/18.25  tff(c_2195, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_96), true, icext(C_96, uri_rdf_object), true)=true))).
% 29.19/18.25  tff(c_6466, plain, (iext(uri_rdf_type, uri_rdfs_seeAlso, uri_rdf_Property)=true)).
% 29.19/18.25  tff(c_1851, plain, (![C_92]: (ifeq(iext(uri_rdfs_range, uri_rdfs_range, C_92), true, icext(C_92, uri_rdfs_Literal), true)=true))).
% 29.19/18.25  tff(c_6365, plain, (ic(uri_rdfs_Statement)=true)).
% 29.19/18.25  tff(c_6311, plain, (icext(uri_rdfs_Class, uri_rdfs_Statement)=true)).
% 29.19/18.25  tff(c_6224, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_range, uri_rdfs_range)=true)).
% 29.19/18.25  tff(c_1848, plain, (![C_92]: (ifeq(iext(uri_rdfs_range, uri_rdfs_domain, C_92), true, icext(C_92, uri_rdfs_Statement), true)=true))).
% 29.19/18.25  tff(c_6159, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_value, uri_rdf_value)=true)).
% 29.19/18.25  tff(c_6093, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Container, uri_rdfs_Container)=true)).
% 29.19/18.25  tff(c_1867, plain, (![C_92]: (ifeq(iext(uri_rdfs_range, uri_rdfs_domain, C_92), true, icext(C_92, uri_rdf_Property), true)=true))).
% 29.19/18.25  tff(c_5999, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_isDefinedBy, uri_rdfs_isDefinedBy)=true)).
% 29.19/18.25  tff(c_5954, plain, (ip(uri_rdfs_member)=true)).
% 29.19/18.25  tff(c_2188, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_domain, C_96), true, icext(C_96, uri_rdf_type), true)=true))).
% 29.19/18.25  tff(c_5871, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf__1, uri_rdfs_member)=true)).
% 29.19/18.25  tff(c_2163, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_range, C_96), true, icext(C_96, uri_rdf__1), true)=true))).
% 29.19/18.25  tff(c_5677, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Class, uri_rdfs_Class)=true)).
% 29.19/18.25  tff(c_5616, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf__3, uri_rdf__3)=true)).
% 29.19/18.25  tff(c_1847, plain, (![C_92]: (ifeq(iext(uri_rdfs_range, uri_rdfs_domain, C_92), true, icext(C_92, uri_rdfs_Resource), true)=true))).
% 29.19/18.25  tff(c_3019, plain, (![S_5, O_6]: (ifeq(iext(uri_owl_sameAs, S_5, O_6), true, true, true)=true))).
% 29.19/18.25  tff(c_5469, plain, (icext(uri_rdf_Property, uri_owl_sameAs)=true)).
% 29.19/18.25  tff(c_2171, plain, (![C_96]: (ifeq(iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_96), true, icext(C_96, uri_rdfs_Datatype), true)=true))).
% 29.19/18.25  tff(c_5380, plain, (iext(uri_rdf_type, uri_owl_sameAs, uri_rdf_Property)=true)).
% 29.19/18.25  tff(c_1560, plain, (![X_89]: (ifeq(icext(uri_rdfs_ContainerMembershipProperty, X_89), true, icext(uri_rdf_Property, X_89), true)=true))).
% 29.19/18.25  tff(c_1189, plain, (![S_5, O_6]: (ifeq(iext(uri_rdfs_subClassOf, S_5, O_6), true, true, true)=true))).
% 29.19/18.25  tff(c_1558, plain, (![X_89]: (ifeq(icext(uri_rdfs_Seq, X_89), true, icext(uri_rdfs_Container, X_89), true)=true))).
% 29.19/18.25  tff(c_1561, plain, (![X_89]: (ifeq(icext(uri_rdf_XMLLiteral, X_89), true, icext(uri_rdfs_Literal, X_89), true)=true))).
% 29.19/18.25  tff(c_4996, plain, (icext(uri_rdfs_Class, uri_rdfs_Resource)=true)).
% 29.19/18.25  tff(c_4961, plain, (ic(uri_rdfs_Resource)=true)).
% 29.19/18.25  tff(c_1556, plain, (![X_89]: (ifeq(icext(uri_rdfs_Datatype, X_89), true, icext(uri_rdfs_Class, X_89), true)=true))).
% 29.19/18.25  tff(c_4854, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Property, uri_rdfs_Resource)=true)).
% 29.19/18.25  tff(c_4793, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf_type, uri_rdf_type)=true)).
% 29.19/18.25  tff(c_4732, plain, (iext(uri_rdfs_subPropertyOf, uri_rdf__2, uri_rdf__2)=true)).
% 29.19/18.25  tff(c_1557, plain, (![X_89]: (ifeq(icext(uri_rdf_Bag, X_89), true, icext(uri_rdfs_Container, X_89), true)=true))).
% 29.19/18.25  tff(c_4664, plain, (iext(uri_rdfs_subPropertyOf, uri_owl_sameAs, uri_owl_sameAs)=true)).
% 29.19/18.25  tff(c_4562, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, uri_rdfs_Datatype)=true)).
% 29.19/18.25  tff(c_1559, plain, (![X_89]: (ifeq(icext(uri_rdf_Alt, X_89), true, icext(uri_rdfs_Container, X_89), true)=true))).
% 29.19/18.25  tff(c_3172, plain, (![S_5, O_6]: (ifeq(iext(uri_rdf_object, S_5, O_6), true, true, true)=true))).
% 29.19/18.25  tff(c_4488, plain, (![X_137]: (iext(uri_rdf_type, X_137, uri_rdfs_Resource)=true))).
% 29.19/18.25  tff(c_1834, plain, (![X_93, Y_94]: (ifeq(iext(uri_rdf__1, X_93, Y_94), true, true, true)=true))).
% 29.19/18.25  tff(c_2168, plain, (![X_97, Y_98]: (ifeq(iext(uri_rdfs_label, X_97, Y_98), true, true, true)=true))).
% 29.19/18.25  tff(c_1831, plain, (![X_93, Y_94]: (ifeq(iext(uri_rdf_predicate, X_93, Y_94), true, true, true)=true))).
% 29.19/18.25  tff(c_2187, plain, (![X_97, Y_98]: (ifeq(iext(uri_rdf_type, X_97, Y_98), true, true, true)=true))).
% 29.19/18.25  tff(c_1849, plain, (![X_93, Y_94]: (ifeq(iext(uri_rdf_subject, X_93, Y_94), true, true, true)=true))).
% 29.19/18.25  tff(c_2172, plain, (![X_97, Y_98]: (ifeq(iext(uri_rdf__3, X_97, Y_98), true, true, true)=true))).
% 29.19/18.25  tff(c_2217, plain, (![X_97, Y_98]: (ifeq(iext(uri_rdfs_seeAlso, X_97, Y_98), true, true, true)=true))).
% 29.19/18.25  tff(c_1826, plain, (![X_93, Y_94]: (ifeq(iext(uri_rdf__2, X_93, Y_94), true, true, true)=true))).
% 29.19/18.25  tff(c_1880, plain, (![X_93, Y_94]: (ifeq(iext(uri_rdf_first, X_93, Y_94), true, true, true)=true))).
% 29.19/18.25  tff(c_2202, plain, (![X_97, Y_98]: (ifeq(iext(uri_rdf_value, X_97, Y_98), true, true, true)=true))).
% 29.19/18.25  tff(c_4297, plain, (icext(uri_rdfs_Class, uri_rdfs_Class)=true)).
% 29.19/18.25  tff(c_4252, plain, (icext(uri_rdfs_Class, uri_rdf_Bag)=true)).
% 29.19/18.25  tff(c_1854, plain, (![X_93, Y_94]: (ifeq(iext(uri_rdfs_member, X_93, Y_94), true, true, true)=true))).
% 29.19/18.25  tff(c_4200, plain, (icext(uri_rdfs_Class, uri_rdfs_Datatype)=true)).
% 29.19/18.25  tff(c_4155, plain, (icext(uri_rdfs_Class, uri_rdf_Alt)=true)).
% 29.19/18.25  tff(c_1857, plain, (![X_93, Y_94]: (ifeq(iext(uri_rdfs_isDefinedBy, X_93, Y_94), true, true, true)=true))).
% 29.19/18.25  tff(c_4104, plain, (icext(uri_rdfs_Class, uri_rdfs_ContainerMembershipProperty)=true)).
% 29.19/18.25  tff(c_4057, plain, (icext(uri_rdfs_Class, uri_rdf_XMLLiteral)=true)).
% 29.19/18.25  tff(c_4014, plain, (icext(uri_rdfs_Class, uri_rdfs_Seq)=true)).
% 29.19/18.25  tff(c_2210, plain, (![X_97, Y_98]: (ifeq(iext(uri_rdfs_comment, X_97, Y_98), true, true, true)=true))).
% 29.19/18.25  tff(c_3964, plain, (icext(uri_rdfs_Class, uri_rdfs_Container)=true)).
% 29.19/18.25  tff(c_3920, plain, (icext(uri_rdfs_Class, uri_rdfs_Literal)=true)).
% 29.19/18.25  tff(c_3873, plain, (icext(uri_rdfs_Class, uri_rdf_Property)=true)).
% 29.19/18.25  tff(c_3833, plain, (icext(uri_rdf_Property, uri_rdf_first)=true)).
% 29.19/18.25  tff(c_3788, plain, (icext(uri_rdf_Property, uri_rdf__3)=true)).
% 29.19/18.25  tff(c_3750, plain, (icext(uri_rdf_Property, uri_rdf__1)=true)).
% 29.19/18.25  tff(c_3708, plain, (icext(uri_rdfs_ContainerMembershipProperty, uri_rdf__2)=true)).
% 29.19/18.25  tff(c_3641, plain, (icext(uri_rdf_Property, uri_rdf_type)=true)).
% 29.19/18.25  tff(c_3631, plain, (icext(uri_rdfs_ContainerMembershipProperty, uri_rdf__1)=true)).
% 29.19/18.25  tff(c_3592, plain, (icext(uri_rdf_Property, uri_rdf_subject)=true)).
% 29.19/18.25  tff(c_3549, plain, (icext(uri_rdf_Property, uri_rdf_object)=true)).
% 29.19/18.25  tff(c_3506, plain, (icext(uri_rdf_Property, uri_rdf_value)=true)).
% 29.19/18.25  tff(c_3466, plain, (icext(uri_rdf_Property, uri_rdf__2)=true)).
% 29.19/18.25  tff(c_3416, plain, (icext(uri_rdfs_ContainerMembershipProperty, uri_rdf__3)=true)).
% 29.19/18.25  tff(c_3379, plain, (icext(uri_rdf_Property, uri_rdf_rest)=true)).
% 29.19/18.25  tff(c_3336, plain, (icext(uri_rdf_List, uri_rdf_nil)=true)).
% 29.19/18.25  tff(c_3293, plain, (icext(uri_rdfs_Datatype, uri_rdf_XMLLiteral)=true)).
% 29.19/18.25  tff(c_3234, plain, (ip(uri_rdf_subject)=true)).
% 29.19/18.25  tff(c_3197, plain, (ic(uri_rdf_Alt)=true)).
% 29.19/18.25  tff(c_3155, plain, (ip(uri_rdf_object)=true)).
% 29.19/18.25  tff(c_3119, plain, (ic(uri_rdf_XMLLiteral)=true)).
% 29.19/18.25  tff(c_3083, plain, (ic(uri_rdf_Property)=true)).
% 29.19/18.25  tff(c_3042, plain, (ic(uri_rdfs_Seq)=true)).
% 29.19/18.25  tff(c_3004, plain, (ip(uri_owl_sameAs)=true)).
% 29.19/18.25  tff(c_2965, plain, (ic(uri_rdfs_Datatype)=true)).
% 29.19/18.25  tff(c_2922, plain, (ic(uri_rdfs_Class)=true)).
% 29.19/18.25  tff(c_2886, plain, (ip(uri_rdfs_seeAlso)=true)).
% 29.19/18.25  tff(c_2847, plain, (ip(uri_rdfs_subPropertyOf)=true)).
% 29.19/18.25  tff(c_2803, plain, (ip(uri_rdf__2)=true)).
% 29.19/18.25  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))).
% 29.19/18.25  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))).
% 29.19/18.25  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))).
% 29.19/18.25  tff(c_2227, plain, (ip(uri_rdf__1)=true)).
% 29.19/18.25  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))).
% 29.19/18.25  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))).
% 29.19/18.25  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))).
% 29.19/18.25  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))).
% 29.19/18.25  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))).
% 29.19/18.25  tff(c_1412, plain, (ic(uri_rdfs_Container)=true)).
% 29.19/18.25  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))).
% 29.19/18.25  tff(c_1373, plain, (ip(uri_rdf_type)=true)).
% 29.19/18.25  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))).
% 29.19/18.25  tff(c_1283, plain, (ic(uri_rdfs_Literal)=true)).
% 29.19/18.25  tff(c_150, plain, (![C_35, D_36]: (ifeq(iext(uri_rdfs_subClassOf, C_35, D_36), true, ic(D_36), true)=true))).
% 29.19/18.25  tff(c_1209, plain, (ip(uri_rdfs_domain)=true)).
% 29.19/18.25  tff(c_1174, plain, (ip(uri_rdfs_subClassOf)=true)).
% 29.19/18.25  tff(c_58, plain, (![C_15]: (ifeq(ic(C_15), true, iext(uri_rdfs_subClassOf, C_15, uri_rdfs_Resource), true)=true))).
% 29.19/18.25  tff(c_1079, plain, (ic(uri_rdf_Bag)=true)).
% 29.19/18.25  tff(c_162, plain, (![P_43, Q_44]: (ifeq(iext(uri_rdfs_subPropertyOf, P_43, Q_44), true, ip(Q_44), true)=true))).
% 29.19/18.25  tff(c_1047, plain, (ip(uri_rdfs_range)=true)).
% 29.19/18.25  tff(c_4, plain, (![P_4, S_5, O_6]: (ifeq(iext(P_4, S_5, O_6), true, ip(P_4), true)=true))).
% 29.19/18.25  tff(c_795, plain, (ip(uri_rdf_first)=true)).
% 29.19/18.25  tff(c_170, plain, (![P_51]: (ifeq(ip(P_51), true, iext(uri_rdfs_subPropertyOf, P_51, P_51), true)=true))).
% 29.19/18.25  tff(c_746, plain, (ip(uri_rdfs_isDefinedBy)=true)).
% 29.19/18.25  tff(c_698, plain, (ic(uri_rdfs_ContainerMembershipProperty)=true)).
% 29.19/18.25  tff(c_164, plain, (![P_45, Q_46]: (ifeq(iext(uri_rdfs_subPropertyOf, P_45, Q_46), true, ip(P_45), true)=true))).
% 29.19/18.25  tff(c_152, plain, (![C_37, D_38]: (ifeq(iext(uri_rdfs_subClassOf, C_37, D_38), true, ic(C_37), true)=true))).
% 29.19/18.25  tff(c_640, plain, (ip(uri_rdf_value)=true)).
% 29.19/18.25  tff(c_576, plain, (ip(uri_rdf_rest)=true)).
% 29.19/18.25  tff(c_28, plain, (![P_9]: (ifeq(ip(P_9), true, iext(uri_rdf_type, P_9, uri_rdf_Property), true)=true))).
% 29.19/18.25  tff(c_548, plain, (ip(uri_rdf__3)=true)).
% 29.19/18.25  tff(c_156, plain, (![C_39]: (ifeq(ic(C_39), true, iext(uri_rdfs_subClassOf, C_39, C_39), true)=true))).
% 29.19/18.25  tff(c_30, plain, (![P_10]: (ifeq(iext(uri_rdf_type, P_10, uri_rdf_Property), true, ip(P_10), true)=true))).
% 29.19/18.25  tff(c_124, plain, (![X_27]: (ifeq(lv(X_27), true, icext(uri_rdfs_Literal, X_27), true)=true))).
% 29.19/18.25  tff(c_122, plain, (![X_26]: (ifeq(icext(uri_rdfs_Literal, X_26), true, lv(X_26), true)=true))).
% 29.19/18.25  tff(c_114, plain, (![X_22]: (ifeq(ic(X_22), true, icext(uri_rdfs_Class, X_22), true)=true))).
% 29.19/18.25  tff(c_116, plain, (![X_23]: (ifeq(icext(uri_rdfs_Class, X_23), true, ic(X_23), true)=true))).
% 29.19/18.25  tff(c_464, plain, (![X_60]: (icext(uri_rdfs_Resource, X_60)=true))).
% 29.19/18.25  tff(c_189, plain, (![X_8]: (ifeq(lv(X_8), true, true, true)=true))).
% 29.19/18.25  tff(c_2, plain, (![A_1, B_2, C_3]: (ifeq(A_1, A_1, B_2, C_3)=B_2))).
% 29.19/18.25  tff(c_20, plain, (iext(uri_rdf_type, uri_rdf__3, uri_rdf_Property)=true)).
% 29.19/18.25  tff(c_184, plain, (iext(uri_owl_sameAs, uri_ex_w, uri_ex_u)=true)).
% 29.19/18.25  tff(c_40, plain, (iext(uri_rdfs_domain, uri_rdfs_isDefinedBy, uri_rdfs_Resource)=true)).
% 29.19/18.25  tff(c_48, plain, (iext(uri_rdfs_range, uri_rdfs_label, uri_rdfs_Literal)=true)).
% 29.19/18.25  tff(c_176, plain, (iext(uri_rdfs_range, uri_rdf_type, uri_rdfs_Class)=true)).
% 29.19/18.25  tff(c_88, plain, (iext(uri_rdfs_range, uri_rdf__2, uri_rdfs_Resource)=true)).
% 29.19/18.25  tff(c_16, plain, (iext(uri_rdf_type, uri_rdf__1, uri_rdf_Property)=true)).
% 29.19/18.25  tff(c_182, plain, (iext(uri_rdfs_domain, uri_owl_sameAs, uri_ex_Person)=true)).
% 29.19/18.25  tff(c_92, plain, (iext(uri_rdf_type, uri_rdf__1, uri_rdfs_ContainerMembershipProperty)=true)).
% 29.19/18.25  tff(c_140, plain, (iext(uri_rdfs_range, uri_rdf_predicate, uri_rdfs_Resource)=true)).
% 29.19/18.25  tff(c_142, plain, (iext(uri_rdfs_domain, uri_rdf_subject, uri_rdfs_Statement)=true)).
% 29.19/18.25  tff(c_86, plain, (iext(uri_rdfs_range, uri_rdf__1, uri_rdfs_Resource)=true)).
% 29.19/18.25  tff(c_12, plain, (iext(uri_rdf_type, uri_rdf_nil, uri_rdf_List)=true)).
% 29.19/18.25  tff(c_94, plain, (iext(uri_rdf_type, uri_rdf__2, uri_rdfs_ContainerMembershipProperty)=true)).
% 29.19/18.25  tff(c_90, plain, (iext(uri_rdfs_range, uri_rdf__3, uri_rdfs_Resource)=true)).
% 29.19/18.25  tff(c_112, plain, (iext(uri_rdfs_range, uri_rdfs_domain, uri_rdfs_Class)=true)).
% 29.19/18.25  tff(c_46, plain, (iext(uri_rdfs_domain, uri_rdfs_label, uri_rdfs_Resource)=true)).
% 29.19/18.25  tff(c_14, plain, (iext(uri_rdf_type, uri_rdf_rest, uri_rdf_Property)=true)).
% 29.19/18.25  tff(c_106, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, uri_rdfs_Class)=true)).
% 29.19/18.25  tff(c_84, plain, (iext(uri_rdfs_domain, uri_rdf__3, uri_rdfs_Resource)=true)).
% 29.19/18.25  tff(c_96, plain, (iext(uri_rdf_type, uri_rdf__3, uri_rdfs_ContainerMembershipProperty)=true)).
% 29.19/18.25  tff(c_22, plain, (iext(uri_rdf_type, uri_rdf_object, uri_rdf_Property)=true)).
% 29.19/18.25  tff(c_80, plain, (iext(uri_rdfs_domain, uri_rdf__1, uri_rdfs_Resource)=true)).
% 29.19/18.25  tff(c_138, plain, (iext(uri_rdfs_domain, uri_rdf_predicate, uri_rdfs_Statement)=true)).
% 29.19/18.25  tff(c_144, plain, (iext(uri_rdfs_range, uri_rdf_subject, uri_rdfs_Resource)=true)).
% 29.19/18.25  tff(c_38, plain, (iext(uri_rdfs_range, uri_rdfs_comment, uri_rdfs_Literal)=true)).
% 29.19/18.25  tff(c_168, plain, (iext(uri_rdfs_range, uri_rdfs_subPropertyOf, uri_rdf_Property)=true)).
% 29.19/18.25  tff(c_70, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Bag, uri_rdfs_Container)=true)).
% 29.19/18.25  tff(c_78, plain, (iext(uri_rdfs_range, uri_rdfs_member, uri_rdfs_Resource)=true)).
% 29.19/18.25  tff(c_82, plain, (iext(uri_rdfs_domain, uri_rdf__2, uri_rdfs_Resource)=true)).
% 29.19/18.25  tff(c_42, plain, (iext(uri_rdfs_range, uri_rdfs_isDefinedBy, uri_rdfs_Resource)=true)).
% 29.19/18.25  tff(c_174, plain, (iext(uri_rdfs_domain, uri_rdf_type, uri_rdfs_Resource)=true)).
% 29.19/18.25  tff(c_60, plain, (iext(uri_rdfs_domain, uri_rdf_first, uri_rdf_List)=true)).
% 29.19/18.25  tff(c_146, plain, (iext(uri_rdfs_domain, uri_rdfs_subClassOf, uri_rdfs_Class)=true)).
% 29.19/18.25  tff(c_64, plain, (iext(uri_rdfs_domain, uri_rdf_rest, uri_rdf_List)=true)).
% 29.19/18.25  tff(c_98, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Seq, uri_rdfs_Container)=true)).
% 29.19/18.25  tff(c_102, plain, (iext(uri_rdf_type, uri_rdf_XMLLiteral, uri_rdfs_Datatype)=true)).
% 29.19/18.25  tff(c_34, plain, (iext(uri_rdf_type, uri_rdf_type, uri_rdf_Property)=true)).
% 29.19/18.25  tff(c_134, plain, (iext(uri_rdfs_domain, uri_rdf_object, uri_rdfs_Statement)=true)).
% 29.19/18.25  tff(c_160, plain, (iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, uri_rdf_Property)=true)).
% 29.19/18.25  tff(c_108, plain, (iext(uri_rdfs_domain, uri_rdfs_domain, uri_rdf_Property)=true)).
% 29.19/18.25  tff(c_26, plain, (iext(uri_rdf_type, uri_rdf_subject, uri_rdf_Property)=true)).
% 29.19/18.25  tff(c_66, plain, (iext(uri_rdfs_range, uri_rdf_rest, uri_rdf_List)=true)).
% 29.19/18.25  tff(c_76, plain, (iext(uri_rdfs_domain, uri_rdfs_member, uri_rdfs_Resource)=true)).
% 29.19/18.25  tff(c_178, plain, (iext(uri_rdfs_domain, uri_rdf_value, uri_rdfs_Resource)=true)).
% 29.19/18.25  tff(c_68, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Alt, uri_rdfs_Container)=true)).
% 29.19/18.25  tff(c_126, plain, (iext(uri_rdf_type, uri_rdf_Property, uri_rdfs_Class)=true)).
% 29.19/18.25  tff(c_44, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_isDefinedBy, uri_rdfs_seeAlso)=true)).
% 29.19/18.25  tff(c_18, plain, (iext(uri_rdf_type, uri_rdf__2, uri_rdf_Property)=true)).
% 29.19/18.25  tff(c_74, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, uri_rdf_Property)=true)).
% 29.19/18.25  tff(c_132, plain, (iext(uri_rdfs_range, uri_rdfs_range, uri_rdfs_Class)=true)).
% 29.19/18.25  tff(c_36, plain, (iext(uri_rdfs_domain, uri_rdfs_comment, uri_rdfs_Resource)=true)).
% 29.19/18.25  tff(c_62, plain, (iext(uri_rdfs_range, uri_rdf_first, uri_rdfs_Resource)=true)).
% 29.19/18.25  tff(c_10, plain, (iext(uri_rdf_type, uri_rdf_first, uri_rdf_Property)=true)).
% 29.19/18.25  tff(c_24, plain, (iext(uri_rdf_type, uri_rdf_value, uri_rdf_Property)=true)).
% 29.19/18.25  tff(c_100, plain, (iext(uri_rdfs_subClassOf, uri_rdf_XMLLiteral, uri_rdfs_Literal)=true)).
% 29.19/18.25  tff(c_128, plain, (iext(uri_rdfs_domain, uri_rdfs_range, uri_rdf_Property)=true)).
% 29.19/18.25  tff(c_50, plain, (iext(uri_rdfs_domain, uri_rdfs_seeAlso, uri_rdfs_Resource)=true)).
% 29.19/18.25  tff(c_52, plain, (iext(uri_rdfs_range, uri_rdfs_seeAlso, uri_rdfs_Resource)=true)).
% 29.19/18.25  tff(c_154, plain, (iext(uri_rdfs_range, uri_rdfs_subClassOf, uri_rdfs_Class)=true)).
% 29.19/18.25  tff(c_180, plain, (iext(uri_rdfs_range, uri_rdf_value, uri_rdfs_Resource)=true)).
% 29.19/18.25  tff(c_186, plain, (iext(uri_rdf_type, uri_ex_u, uri_ex_Person)!=true)).
% 29.19/18.25  tff(c_6, plain, (![X_7]: (ir(X_7)=true))).
% 29.19/18.25  % SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 29.19/18.25  
%------------------------------------------------------------------------------