%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : SWB030+4 : TPTP v9.0.0. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% Computer : n023.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:58 PM UTC 2025
% Result : Satisfiable 12.16s 4.02s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.07/0.12 % Problem : SWB030+4 : TPTP v9.0.0. Released v5.2.0.
% 0.07/0.13 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox2/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox2/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% 0.12/0.34 % Computer : n023.cluster.edu
% 0.12/0.34 % Model : x86_64 x86_64
% 0.12/0.34 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.12/0.34 % Memory : 8042.1875MB
% 0.12/0.34 % OS : Linux 3.10.0-693.el7.x86_64
% 0.12/0.34 % CPULimit : 300
% 0.12/0.34 % WCLimit : 300
% 0.12/0.34 % DateTime : Wed Apr 9 01:04:24 EDT 2025
% 0.12/0.34 % CPUTime :
% 12.16/4.02
% 12.16/4.02 % SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 12.16/4.02
% 12.16/4.02 % SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 12.16/4.03 %$ iext > icext > lv > ir > ip > ic > literal_typed > #nlpp > uri_xsd_boolean > uri_rdfs_subPropertyOf > uri_rdfs_subClassOf > uri_rdfs_seeAlso > uri_rdfs_range > uri_rdfs_member > uri_rdfs_label > uri_rdfs_isDefinedBy > uri_rdfs_domain > uri_rdfs_comment > uri_rdfs_Statement > uri_rdfs_Seq > uri_rdfs_Resource > uri_rdfs_Literal > uri_rdfs_Datatype > uri_rdfs_ContainerMembershipProperty > uri_rdfs_Container > uri_rdfs_Class > uri_rdf_value > uri_rdf_type > uri_rdf_subject > uri_rdf_rest > uri_rdf_predicate > uri_rdf_object > uri_rdf_nil > uri_rdf_first > uri_rdf__3 > uri_rdf__2 > uri_rdf__1 > uri_rdf_XMLLiteral > uri_rdf_Property > uri_rdf_List > uri_rdf_Bag > uri_rdf_Alt > uri_owl_onProperty > uri_owl_hasSelf > uri_owl_complementOf > uri_owl_Restriction > uri_owl_Class > uri_ex_c > dat_str_true > #skF_1
% 12.16/4.03
% 12.16/4.03 %Foreground sorts:
% 12.16/4.03
% 12.16/4.03
% 12.16/4.03 %Background operators:
% 12.16/4.03
% 12.16/4.03
% 12.16/4.03 %Foreground operators:
% 12.16/4.03 tff(uri_rdfs_Datatype, type, uri_rdfs_Datatype: $i).
% 12.16/4.03 tff(uri_owl_complementOf, type, uri_owl_complementOf: $i).
% 12.16/4.03 tff(uri_rdfs_ContainerMembershipProperty, type, uri_rdfs_ContainerMembershipProperty: $i).
% 12.16/4.03 tff(uri_rdfs_Resource, type, uri_rdfs_Resource: $i).
% 12.16/4.03 tff(uri_rdf_Property, type, uri_rdf_Property: $i).
% 12.16/4.03 tff(uri_rdf_subject, type, uri_rdf_subject: $i).
% 12.16/4.03 tff(uri_rdf_type, type, uri_rdf_type: $i).
% 12.16/4.03 tff(uri_owl_onProperty, type, uri_owl_onProperty: $i).
% 12.16/4.03 tff(uri_rdfs_subPropertyOf, type, uri_rdfs_subPropertyOf: $i).
% 12.16/4.03 tff(literal_typed, type, literal_typed: ($i * $i) > $i).
% 12.16/4.03 tff(uri_rdfs_seeAlso, type, uri_rdfs_seeAlso: $i).
% 12.16/4.03 tff(uri_rdfs_range, type, uri_rdfs_range: $i).
% 12.16/4.03 tff(uri_rdf_XMLLiteral, type, uri_rdf_XMLLiteral: $i).
% 12.16/4.03 tff(uri_rdf_List, type, uri_rdf_List: $i).
% 12.16/4.03 tff(uri_rdf_first, type, uri_rdf_first: $i).
% 12.16/4.03 tff(uri_rdf_predicate, type, uri_rdf_predicate: $i).
% 12.16/4.03 tff(uri_ex_c, type, uri_ex_c: $i).
% 12.16/4.03 tff(uri_rdf__3, type, uri_rdf__3: $i).
% 12.16/4.03 tff(icext, type, icext: ($i * $i) > $o).
% 12.16/4.03 tff(uri_rdf_value, type, uri_rdf_value: $i).
% 12.16/4.03 tff(ip, type, ip: $i > $o).
% 12.16/4.03 tff(uri_rdfs_Statement, type, uri_rdfs_Statement: $i).
% 12.16/4.03 tff(uri_rdf__1, type, uri_rdf__1: $i).
% 12.16/4.03 tff(lv, type, lv: $i > $o).
% 12.16/4.03 tff(ir, type, ir: $i > $o).
% 12.16/4.03 tff(uri_xsd_boolean, type, uri_xsd_boolean: $i).
% 12.16/4.03 tff(uri_owl_Restriction, type, uri_owl_Restriction: $i).
% 12.16/4.03 tff(uri_rdf_rest, type, uri_rdf_rest: $i).
% 12.16/4.03 tff(uri_rdfs_label, type, uri_rdfs_label: $i).
% 12.16/4.03 tff(uri_rdfs_Container, type, uri_rdfs_Container: $i).
% 12.16/4.03 tff(ic, type, ic: $i > $o).
% 12.16/4.03 tff('#skF_1', type, '#skF_1': $i).
% 12.16/4.03 tff(uri_rdfs_subClassOf, type, uri_rdfs_subClassOf: $i).
% 12.16/4.03 tff(uri_rdf_object, type, uri_rdf_object: $i).
% 12.16/4.03 tff(uri_rdfs_Class, type, uri_rdfs_Class: $i).
% 12.16/4.03 tff(uri_rdfs_Seq, type, uri_rdfs_Seq: $i).
% 12.16/4.03 tff(uri_owl_Class, type, uri_owl_Class: $i).
% 12.16/4.03 tff(iext, type, iext: ($i * $i * $i) > $o).
% 12.16/4.03 tff(uri_rdfs_member, type, uri_rdfs_member: $i).
% 12.16/4.03 tff(uri_rdf_Bag, type, uri_rdf_Bag: $i).
% 12.16/4.03 tff(uri_rdf__2, type, uri_rdf__2: $i).
% 12.16/4.03 tff(uri_owl_hasSelf, type, uri_owl_hasSelf: $i).
% 12.16/4.03 tff(uri_rdfs_comment, type, uri_rdfs_comment: $i).
% 12.16/4.03 tff(uri_rdfs_Literal, type, uri_rdfs_Literal: $i).
% 12.16/4.03 tff(dat_str_true, type, dat_str_true: $i).
% 12.16/4.03 tff(uri_rdf_Alt, type, uri_rdf_Alt: $i).
% 12.16/4.03 tff(uri_rdf_nil, type, uri_rdf_nil: $i).
% 12.16/4.03 tff(uri_rdfs_isDefinedBy, type, uri_rdfs_isDefinedBy: $i).
% 12.16/4.03 tff(uri_rdfs_domain, type, uri_rdfs_domain: $i).
% 12.16/4.03
% 12.16/4.03 %Saturated clause set:
% 12.16/4.03 tff(c_8979, plain, (![P_87]: (~iext(uri_rdfs_subPropertyOf, uri_owl_hasSelf, P_87) | ~iext(uri_rdfs_subPropertyOf, P_87, uri_rdfs_isDefinedBy)))).
% 12.16/4.04 tff(c_8978, plain, (~icext(uri_rdfs_ContainerMembershipProperty, uri_owl_hasSelf))).
% 12.16/4.04 tff(c_8960, plain, (![P_10]: (~iext(uri_rdfs_subPropertyOf, uri_owl_hasSelf, P_10) | ~icext(uri_rdfs_ContainerMembershipProperty, P_10)))).
% 12.16/4.04 tff(c_8959, plain, (~iext(uri_rdfs_subPropertyOf, uri_owl_hasSelf, uri_rdfs_isDefinedBy))).
% 12.16/4.04 tff(c_5523, plain, (![Q_32, Q_318]: (iext(Q_32, '#skF_1', literal_typed(dat_str_true, uri_xsd_boolean)) | ~iext(uri_rdfs_subPropertyOf, Q_318, Q_32) | ~iext(uri_rdfs_subPropertyOf, uri_owl_hasSelf, Q_318)))).
% 12.16/4.04 tff(c_8933, plain, (![C_80]: (~iext(uri_rdfs_range, uri_owl_hasSelf, C_80) | ~iext(uri_rdfs_subClassOf, C_80, uri_rdf_Bag)))).
% 12.16/4.04 tff(c_8924, plain, (![C_80]: (~iext(uri_rdfs_range, uri_owl_hasSelf, C_80) | ~iext(uri_rdfs_subClassOf, C_80, uri_rdf_Alt)))).
% 12.16/4.04 tff(c_8915, plain, (![C_80]: (~iext(uri_rdfs_range, uri_owl_hasSelf, C_80) | ~iext(uri_rdfs_subClassOf, C_80, uri_rdf_XMLLiteral)))).
% 12.16/4.04 tff(c_7383, plain, (![Q_32, C_331]: (iext(Q_32, C_331, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_32) | ~iext(uri_rdfs_subClassOf, C_331, uri_rdfs_ContainerMembershipProperty)))).
% 12.16/4.04 tff(c_6484, plain, (![Q_32, C_325]: (iext(Q_32, C_325, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_32) | ~iext(uri_rdfs_subClassOf, C_325, uri_rdfs_Datatype)))).
% 12.16/4.04 tff(c_6485, plain, (![C_28, C_325]: (iext(uri_rdfs_subClassOf, C_28, uri_rdfs_Resource) | ~iext(uri_rdfs_subClassOf, C_28, C_325) | ~iext(uri_rdfs_subClassOf, C_325, uri_rdfs_Datatype)))).
% 12.16/4.04 tff(c_8794, plain, (![D_11]: (~iext(uri_rdfs_range, uri_owl_hasSelf, D_11) | ~icext(uri_rdfs_Datatype, D_11)))).
% 12.16/4.04 tff(c_8793, plain, (~iext(uri_rdfs_range, uri_owl_hasSelf, uri_rdf_Bag))).
% 12.16/4.04 tff(c_8792, plain, (~iext(uri_rdfs_range, uri_owl_hasSelf, uri_rdf_XMLLiteral))).
% 12.16/4.04 tff(c_8791, plain, (~iext(uri_rdfs_range, uri_owl_hasSelf, uri_rdf_Alt))).
% 12.16/4.04 tff(c_8790, plain, (~iext(uri_rdfs_range, uri_owl_hasSelf, uri_rdfs_Seq))).
% 12.16/4.04 tff(c_4910, plain, (![D_24, C_292]: (icext(D_24, literal_typed(dat_str_true, uri_xsd_boolean)) | ~iext(uri_rdfs_subClassOf, C_292, D_24) | ~iext(uri_rdfs_range, uri_owl_hasSelf, C_292)))).
% 12.16/4.04 tff(c_7384, plain, (![C_28, C_331]: (iext(uri_rdfs_subClassOf, C_28, uri_rdfs_Resource) | ~iext(uri_rdfs_subClassOf, C_28, C_331) | ~iext(uri_rdfs_subClassOf, C_331, uri_rdfs_ContainerMembershipProperty)))).
% 12.16/4.04 tff(c_6782, plain, (![Q_32, C_326]: (iext(Q_32, C_326, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_32) | ~iext(uri_rdfs_subClassOf, C_326, uri_rdf_Bag)))).
% 12.16/4.04 tff(c_7086, plain, (![C_28, C_330]: (iext(uri_rdfs_subClassOf, C_28, uri_rdfs_Resource) | ~iext(uri_rdfs_subClassOf, C_28, C_330) | ~iext(uri_rdfs_subClassOf, C_330, uri_rdf_XMLLiteral)))).
% 12.16/4.04 tff(c_6783, plain, (![C_28, C_326]: (iext(uri_rdfs_subClassOf, C_28, uri_rdfs_Resource) | ~iext(uri_rdfs_subClassOf, C_28, C_326) | ~iext(uri_rdfs_subClassOf, C_326, uri_rdf_Bag)))).
% 12.16/4.04 tff(c_8402, plain, (~iext(uri_rdfs_subPropertyOf, uri_owl_hasSelf, uri_rdfs_comment))).
% 12.16/4.04 tff(c_6170, plain, (![Q_32, C_322]: (iext(Q_32, C_322, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_32) | ~iext(uri_rdfs_subClassOf, C_322, uri_rdf_Alt)))).
% 12.16/4.04 tff(c_8401, plain, (~iext(uri_rdfs_subPropertyOf, uri_owl_hasSelf, uri_rdfs_label))).
% 12.16/4.04 tff(c_5525, plain, (![C_20, Q_318]: (icext(C_20, literal_typed(dat_str_true, uri_xsd_boolean)) | ~iext(uri_rdfs_range, Q_318, C_20) | ~iext(uri_rdfs_subPropertyOf, uri_owl_hasSelf, Q_318)))).
% 12.16/4.04 tff(c_7085, plain, (![Q_32, C_330]: (iext(Q_32, C_330, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_32) | ~iext(uri_rdfs_subClassOf, C_330, uri_rdf_XMLLiteral)))).
% 12.16/4.04 tff(c_6171, plain, (![C_28, C_322]: (iext(uri_rdfs_subClassOf, C_28, uri_rdfs_Resource) | ~iext(uri_rdfs_subClassOf, C_28, C_322) | ~iext(uri_rdfs_subClassOf, C_322, uri_rdf_Alt)))).
% 12.16/4.04 tff(c_3530, plain, (![Q_32, C_236]: (iext(Q_32, C_236, uri_rdfs_Container) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_32) | ~iext(uri_rdfs_subClassOf, C_236, uri_rdf_Alt)))).
% 12.16/4.04 tff(c_4154, plain, (![Q_32, P_258]: (iext(Q_32, P_258, uri_rdfs_seeAlso) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_32) | ~iext(uri_rdfs_subPropertyOf, P_258, uri_rdfs_isDefinedBy)))).
% 12.16/4.04 tff(c_3881, plain, (![Q_32, C_247]: (iext(Q_32, C_247, uri_rdfs_Literal) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_32) | ~iext(uri_rdfs_subClassOf, C_247, uri_rdf_XMLLiteral)))).
% 12.16/4.04 tff(c_4511, plain, (![C_28, C_267]: (iext(uri_rdfs_subClassOf, C_28, uri_rdfs_Container) | ~iext(uri_rdfs_subClassOf, C_28, C_267) | ~iext(uri_rdfs_subClassOf, C_267, uri_rdf_Bag)))).
% 12.16/4.04 tff(c_8099, plain, (~iext(uri_rdfs_subPropertyOf, uri_rdfs_member, uri_rdfs_isDefinedBy))).
% 12.16/4.04 tff(c_4153, plain, (![P_38, P_258]: (iext(uri_rdfs_subPropertyOf, P_38, uri_rdfs_seeAlso) | ~iext(uri_rdfs_subPropertyOf, P_38, P_258) | ~iext(uri_rdfs_subPropertyOf, P_258, uri_rdfs_isDefinedBy)))).
% 12.16/4.04 tff(c_8080, plain, (~iext(uri_rdfs_subClassOf, uri_rdfs_Container, uri_rdf_XMLLiteral))).
% 12.16/4.04 tff(c_3882, plain, (![C_28, C_247]: (iext(uri_rdfs_subClassOf, C_28, uri_rdfs_Literal) | ~iext(uri_rdfs_subClassOf, C_28, C_247) | ~iext(uri_rdfs_subClassOf, C_247, uri_rdf_XMLLiteral)))).
% 12.16/4.04 tff(c_3531, plain, (![C_28, C_236]: (iext(uri_rdfs_subClassOf, C_28, uri_rdfs_Container) | ~iext(uri_rdfs_subClassOf, C_28, C_236) | ~iext(uri_rdfs_subClassOf, C_236, uri_rdf_Alt)))).
% 12.16/4.04 tff(c_5857, plain, (![C_28, D_319]: (iext(uri_rdfs_subClassOf, C_28, uri_rdfs_Resource) | ~iext(uri_rdfs_subClassOf, C_28, D_319) | ~icext(uri_rdfs_Datatype, D_319)))).
% 12.16/4.04 tff(c_4510, plain, (![Q_32, C_267]: (iext(Q_32, C_267, uri_rdfs_Container) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_32) | ~iext(uri_rdfs_subClassOf, C_267, uri_rdf_Bag)))).
% 12.16/4.04 tff(c_5856, plain, (![Q_32, D_319]: (iext(Q_32, D_319, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_32) | ~icext(uri_rdfs_Datatype, D_319)))).
% 12.16/4.04 tff(c_7798, plain, (~iext(uri_rdfs_subPropertyOf, uri_owl_hasSelf, uri_rdf_rest))).
% 12.16/4.04 tff(c_7797, plain, (~iext(uri_rdfs_subPropertyOf, uri_owl_hasSelf, uri_rdfs_domain))).
% 12.16/4.04 tff(c_7796, plain, (~iext(uri_rdfs_subPropertyOf, uri_owl_hasSelf, uri_rdf_predicate))).
% 12.16/4.04 tff(c_7795, plain, (~iext(uri_rdfs_subPropertyOf, uri_owl_hasSelf, uri_rdf_subject))).
% 12.16/4.04 tff(c_7794, plain, (~iext(uri_rdfs_subPropertyOf, uri_owl_hasSelf, uri_rdf_first))).
% 12.16/4.04 tff(c_7793, plain, (~iext(uri_rdfs_subPropertyOf, uri_owl_hasSelf, uri_rdfs_range))).
% 12.16/4.04 tff(c_7792, plain, (~iext(uri_rdfs_subPropertyOf, uri_owl_hasSelf, uri_rdf_object))).
% 12.16/4.04 tff(c_5526, plain, (![C_13, Q_318]: (icext(C_13, '#skF_1') | ~iext(uri_rdfs_domain, Q_318, C_13) | ~iext(uri_rdfs_subPropertyOf, uri_owl_hasSelf, Q_318)))).
% 12.16/4.04 tff(c_7719, plain, (~icext(uri_rdfs_ContainerMembershipProperty, uri_rdfs_seeAlso))).
% 12.16/4.04 tff(c_1461, plain, (![P_87, P_10]: (iext(uri_rdfs_subPropertyOf, P_87, uri_rdfs_member) | ~iext(uri_rdfs_subPropertyOf, P_87, P_10) | ~icext(uri_rdfs_ContainerMembershipProperty, P_10)))).
% 12.16/4.04 tff(c_1380, plain, (![Q_83, D_11]: (iext(Q_83, D_11, uri_rdfs_Literal) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_83) | ~icext(uri_rdfs_Datatype, D_11)))).
% 12.16/4.04 tff(c_1381, plain, (![Q_83, X_7, C_8]: (iext(Q_83, X_7, C_8) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_83) | ~icext(C_8, X_7)))).
% 12.16/4.04 tff(c_1382, plain, (![Q_83, P_10]: (iext(Q_83, P_10, uri_rdfs_member) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_83) | ~icext(uri_rdfs_ContainerMembershipProperty, P_10)))).
% 12.16/4.04 tff(c_7656, plain, (~icext(uri_rdfs_Datatype, uri_rdfs_Container))).
% 12.16/4.05 tff(c_1224, plain, (![C_80, D_11]: (iext(uri_rdfs_subClassOf, C_80, uri_rdfs_Literal) | ~iext(uri_rdfs_subClassOf, C_80, D_11) | ~icext(uri_rdfs_Datatype, D_11)))).
% 12.16/4.05 tff(c_1386, plain, (![Q_83, P_6]: (iext(Q_83, P_6, uri_rdf_Property) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_83) | ~ip(P_6)))).
% 12.16/4.05 tff(c_7555, plain, (![C_76]: (icext(C_76, uri_rdfs_member) | ~iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_76)))).
% 12.16/4.05 tff(c_7538, plain, (![D_345]: (icext(uri_rdfs_Class, D_345) | ~icext(uri_rdfs_Datatype, D_345)))).
% 12.16/4.05 tff(c_914, plain, (![C_72, D_11]: (icext(C_72, D_11) | ~iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_72) | ~icext(uri_rdfs_Datatype, D_11)))).
% 12.16/4.05 tff(c_7513, plain, (![P_342]: (icext(uri_rdf_Property, P_342) | ~icext(uri_rdfs_ContainerMembershipProperty, P_342)))).
% 12.16/4.05 tff(c_7509, plain, (~iext(uri_rdfs_subClassOf, uri_rdfs_Literal, uri_rdf_Bag))).
% 12.16/4.05 tff(c_916, plain, (![C_72, P_10]: (icext(C_72, P_10) | ~iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_72) | ~icext(uri_rdfs_ContainerMembershipProperty, P_10)))).
% 12.16/4.05 tff(c_7508, plain, (~iext(uri_rdfs_subPropertyOf, uri_owl_hasSelf, uri_rdf_type))).
% 12.16/4.05 tff(c_7507, plain, (~iext(uri_rdfs_subClassOf, uri_rdfs_Literal, uri_rdf_Alt))).
% 12.16/4.05 tff(c_5472, plain, (![Q_32]: (iext(Q_32, uri_rdfs_Datatype, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_32)))).
% 12.16/4.05 tff(c_5324, plain, (![Q_32]: (iext(Q_32, uri_rdfs_Seq, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_32)))).
% 12.16/4.05 tff(c_1384, plain, (![Q_83, P_37]: (iext(Q_83, P_37, P_37) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_83) | ~ip(P_37)))).
% 12.16/4.05 tff(c_5435, plain, (![Q_32]: (iext(Q_32, uri_rdf_Alt, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_32)))).
% 12.16/4.05 tff(c_5371, plain, (![Q_32]: (iext(Q_32, uri_rdfs_ContainerMembershipProperty, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_32)))).
% 12.16/4.05 tff(c_5555, plain, (![Q_32]: (iext(Q_32, uri_rdf_XMLLiteral, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_32)))).
% 12.16/4.05 tff(c_5325, plain, (![C_28]: (iext(uri_rdfs_subClassOf, C_28, uri_rdfs_Resource) | ~iext(uri_rdfs_subClassOf, C_28, uri_rdfs_Seq)))).
% 12.16/4.05 tff(c_5403, plain, (![Q_32]: (iext(Q_32, uri_rdf_Bag, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_32)))).
% 12.16/4.05 tff(c_7393, plain, (~iext(uri_rdfs_range, uri_owl_hasSelf, uri_rdf_Property))).
% 12.16/4.05 tff(c_7392, plain, (~iext(uri_rdfs_range, uri_owl_hasSelf, uri_rdfs_Datatype))).
% 12.16/4.05 tff(c_5372, plain, (![C_28]: (iext(uri_rdfs_subClassOf, C_28, uri_rdfs_Resource) | ~iext(uri_rdfs_subClassOf, C_28, uri_rdfs_ContainerMembershipProperty)))).
% 12.16/4.05 tff(c_5273, plain, (![C_80]: (iext(uri_rdfs_subClassOf, C_80, uri_rdfs_Resource) | ~iext(uri_rdfs_subClassOf, C_80, uri_rdf_XMLLiteral)))).
% 12.16/4.05 tff(c_915, plain, (![C_72, X_7, C_8]: (icext(C_72, X_7) | ~iext(uri_rdfs_domain, uri_rdf_type, C_72) | ~icext(C_8, X_7)))).
% 12.16/4.05 tff(c_5270, plain, (![C_80]: (iext(uri_rdfs_subClassOf, C_80, uri_rdfs_Resource) | ~iext(uri_rdfs_subClassOf, C_80, uri_rdf_Bag)))).
% 12.16/4.05 tff(c_5473, plain, (![C_28]: (iext(uri_rdfs_subClassOf, C_28, uri_rdfs_Resource) | ~iext(uri_rdfs_subClassOf, C_28, uri_rdfs_Datatype)))).
% 12.16/4.05 tff(c_6194, plain, (~iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, uri_rdfs_isDefinedBy))).
% 12.16/4.05 tff(c_1387, plain, (![Q_83, C_27]: (iext(Q_83, C_27, C_27) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_83) | ~ic(C_27)))).
% 12.16/4.05 tff(c_5276, plain, (![C_80]: (iext(uri_rdfs_subClassOf, C_80, uri_rdfs_Resource) | ~iext(uri_rdfs_subClassOf, C_80, uri_rdf_Alt)))).
% 12.16/4.05 tff(c_5880, plain, (~iext(uri_rdfs_range, uri_owl_hasSelf, uri_rdfs_ContainerMembershipProperty))).
% 12.16/4.05 tff(c_1383, plain, (![Q_83, C_9]: (iext(Q_83, C_9, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_83) | ~ic(C_9)))).
% 12.16/4.05 tff(c_5279, plain, (![D_11]: (iext(uri_rdfs_subClassOf, D_11, uri_rdfs_Resource) | ~icext(uri_rdfs_Datatype, D_11)))).
% 12.16/4.05 tff(c_5566, plain, (~iext(uri_rdfs_subPropertyOf, uri_owl_hasSelf, uri_rdfs_subClassOf))).
% 12.16/4.05 tff(c_5565, plain, (~iext(uri_rdfs_subPropertyOf, uri_owl_hasSelf, uri_rdfs_subPropertyOf))).
% 12.16/4.05 tff(c_5301, plain, (iext(uri_rdfs_subClassOf, uri_rdf_XMLLiteral, uri_rdfs_Resource))).
% 12.16/4.05 tff(c_1385, plain, (![Q_83]: (iext(Q_83, '#skF_1', literal_typed(dat_str_true, uri_xsd_boolean)) | ~iext(uri_rdfs_subPropertyOf, uri_owl_hasSelf, Q_83)))).
% 12.16/4.05 tff(c_5298, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, uri_rdfs_Resource))).
% 12.16/4.05 tff(c_5295, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Alt, uri_rdfs_Resource))).
% 12.16/4.05 tff(c_5292, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Bag, uri_rdfs_Resource))).
% 12.16/4.05 tff(c_5289, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, uri_rdfs_Resource))).
% 12.16/4.05 tff(c_5286, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Seq, uri_rdfs_Resource))).
% 12.16/4.05 tff(c_1225, plain, (![C_80, C_9]: (iext(uri_rdfs_subClassOf, C_80, uri_rdfs_Resource) | ~iext(uri_rdfs_subClassOf, C_80, C_9) | ~ic(C_9)))).
% 12.16/4.05 tff(c_5151, plain, (![C_76]: (icext(uri_rdfs_Class, C_76) | ~iext(uri_rdfs_range, uri_owl_hasSelf, C_76)))).
% 12.16/4.05 tff(c_5057, plain, (![C_311, X_312]: (icext(uri_rdfs_Class, C_311) | ~icext(C_311, X_312)))).
% 12.16/4.05 tff(c_1133, plain, (![C_76, C_8, X_7]: (icext(C_76, C_8) | ~iext(uri_rdfs_range, uri_rdf_type, C_76) | ~icext(C_8, X_7)))).
% 12.16/4.05 tff(c_1555, plain, (![D_24, P_90]: (icext(D_24, P_90) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24) | ~ip(P_90)))).
% 12.16/4.05 tff(c_918, plain, (![C_72, P_37]: (icext(C_72, P_37) | ~iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_72) | ~ip(P_37)))).
% 12.16/4.05 tff(c_765, plain, (![D_69, X_16]: (icext(D_69, X_16) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_69) | ~ic(X_16)))).
% 12.16/4.05 tff(c_4991, plain, (~iext(uri_rdfs_subPropertyOf, uri_owl_complementOf, uri_rdfs_isDefinedBy))).
% 12.16/4.05 tff(c_766, plain, (![D_69, X_18]: (icext(D_69, X_18) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Literal, D_69) | ~lv(X_18)))).
% 12.16/4.05 tff(c_1139, plain, (![C_76, C_27]: (icext(C_76, C_27) | ~iext(uri_rdfs_range, uri_rdfs_subClassOf, C_76) | ~ic(C_27)))).
% 12.16/4.05 tff(c_920, plain, (![C_72, P_6]: (icext(C_72, P_6) | ~iext(uri_rdfs_domain, uri_rdf_type, C_72) | ~ip(P_6)))).
% 12.16/4.05 tff(c_4946, plain, (![C_76]: (icext(C_76, uri_rdfs_Resource) | ~iext(uri_rdfs_range, uri_rdfs_subClassOf, C_76)))).
% 12.16/4.05 tff(c_4924, plain, (~iext(uri_rdfs_subPropertyOf, uri_owl_onProperty, uri_rdfs_isDefinedBy))).
% 12.16/4.05 tff(c_921, plain, (![C_72, C_27]: (icext(C_72, C_27) | ~iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_72) | ~ic(C_27)))).
% 12.16/4.05 tff(c_1136, plain, (![C_76, P_37]: (icext(C_76, P_37) | ~iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_76) | ~ip(P_37)))).
% 12.16/4.05 tff(c_4915, plain, (~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, uri_rdfs_isDefinedBy))).
% 12.16/4.05 tff(c_4914, plain, (~iext(uri_rdfs_range, uri_owl_hasSelf, uri_rdfs_Class))).
% 12.16/4.05 tff(c_4913, plain, (~iext(uri_rdfs_range, uri_owl_hasSelf, uri_rdfs_Literal))).
% 12.16/4.05 tff(c_4883, plain, (~iext(uri_rdfs_subPropertyOf, uri_rdf_type, uri_rdfs_isDefinedBy))).
% 12.16/4.05 tff(c_1137, plain, (![C_76]: (icext(C_76, literal_typed(dat_str_true, uri_xsd_boolean)) | ~iext(uri_rdfs_range, uri_owl_hasSelf, C_76)))).
% 12.16/4.05 tff(c_4882, plain, (~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, uri_rdfs_isDefinedBy))).
% 12.16/4.05 tff(c_4881, plain, (~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, uri_rdfs_isDefinedBy))).
% 12.16/4.05 tff(c_1408, plain, (![Q_83]: (iext(Q_83, '#skF_1', uri_owl_Restriction) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_83)))).
% 12.16/4.05 tff(c_1393, plain, (![Q_83]: (iext(Q_83, uri_rdfs_subClassOf, uri_rdfs_Class) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_83)))).
% 12.16/4.06 tff(c_1423, plain, (![Q_83]: (iext(Q_83, uri_rdfs_isDefinedBy, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_83)))).
% 12.16/4.06 tff(c_1405, plain, (![Q_83]: (iext(Q_83, uri_rdf_type, uri_rdf_Property) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_83)))).
% 12.16/4.06 tff(c_1426, plain, (![Q_83]: (iext(Q_83, uri_rdf_Alt, uri_rdfs_Container) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_83)))).
% 12.16/4.06 tff(c_1395, plain, (![Q_83]: (iext(Q_83, uri_rdf__2, uri_rdf_Property) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_83)))).
% 12.16/4.06 tff(c_1417, plain, (![Q_83]: (iext(Q_83, uri_rdfs_subPropertyOf, uri_rdf_Property) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_83)))).
% 12.16/4.06 tff(c_1409, plain, (![Q_83]: (iext(Q_83, uri_rdf__3, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_83)))).
% 12.16/4.06 tff(c_1411, plain, (![Q_83]: (iext(Q_83, uri_rdf__2, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_83)))).
% 12.16/4.06 tff(c_1415, plain, (![Q_83]: (iext(Q_83, uri_rdfs_ContainerMembershipProperty, uri_rdf_Property) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_83)))).
% 12.16/4.06 tff(c_1424, plain, (![Q_83]: (iext(Q_83, uri_rdf_Bag, uri_rdfs_Container) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_83)))).
% 12.16/4.06 tff(c_1407, plain, (![Q_83]: (iext(Q_83, uri_rdf__2, uri_rdfs_ContainerMembershipProperty) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_83)))).
% 12.16/4.06 tff(c_1396, plain, (![Q_83]: (iext(Q_83, uri_rdf__1, uri_rdfs_ContainerMembershipProperty) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_83)))).
% 12.16/4.06 tff(c_1436, plain, (![Q_83]: (iext(Q_83, uri_rdfs_Datatype, uri_rdfs_Class) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_83)))).
% 12.16/4.06 tff(c_1401, plain, (![Q_83]: (iext(Q_83, uri_rdfs_Seq, uri_rdfs_Container) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_83)))).
% 12.16/4.06 tff(c_1228, plain, (![C_80]: (iext(uri_rdfs_subClassOf, C_80, uri_rdf_Property) | ~iext(uri_rdfs_subClassOf, C_80, uri_rdfs_ContainerMembershipProperty)))).
% 12.16/4.06 tff(c_1425, plain, (![Q_83]: (iext(Q_83, uri_rdf_predicate, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_83)))).
% 12.16/4.06 tff(c_4617, plain, (~iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, uri_rdf_Bag))).
% 12.16/4.06 tff(c_1439, plain, (![Q_83]: (iext(Q_83, uri_rdf_first, uri_rdf_List) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_83)))).
% 12.16/4.06 tff(c_4616, plain, (~iext(uri_rdfs_subClassOf, uri_rdf_List, uri_rdf_Bag))).
% 12.16/4.06 tff(c_1447, plain, (![Q_83]: (iext(Q_83, uri_rdf_first, uri_rdf_Property) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_83)))).
% 12.16/4.06 tff(c_4585, plain, (~iext(uri_rdfs_subClassOf, uri_rdfs_Class, uri_rdf_Bag))).
% 12.16/4.06 tff(c_1390, plain, (![Q_83]: (iext(Q_83, uri_rdf_rest, uri_rdf_List) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_83)))).
% 12.16/4.06 tff(c_1444, plain, (![Q_83]: (iext(Q_83, uri_rdf_rest, uri_rdf_Property) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_83)))).
% 12.16/4.06 tff(c_4569, plain, (~iext(uri_rdfs_subClassOf, uri_owl_Class, uri_rdf_Bag))).
% 12.16/4.06 tff(c_4553, plain, (~iext(uri_rdfs_subClassOf, uri_owl_Restriction, uri_rdf_Bag))).
% 12.16/4.06 tff(c_1428, plain, (![Q_83]: (iext(Q_83, uri_rdf__2, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_83)))).
% 12.16/4.06 tff(c_4552, plain, (~icext(uri_rdfs_ContainerMembershipProperty, uri_owl_onProperty))).
% 12.16/4.06 tff(c_1448, plain, (![Q_83]: (iext(Q_83, '#skF_1', uri_rdf_type) | ~iext(uri_rdfs_subPropertyOf, uri_owl_onProperty, Q_83)))).
% 12.16/4.06 tff(c_4536, plain, (~iext(uri_rdfs_subClassOf, uri_rdf_Property, uri_rdf_Bag))).
% 12.16/4.06 tff(c_4520, plain, (~iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, uri_rdf_Bag))).
% 12.16/4.06 tff(c_1446, plain, (![Q_83]: (iext(Q_83, uri_rdf_value, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_83)))).
% 12.16/4.06 tff(c_4519, plain, (~iext(uri_rdfs_subClassOf, uri_rdfs_Resource, uri_rdf_Bag))).
% 12.16/4.06 tff(c_1229, plain, (![C_80]: (iext(uri_rdfs_subClassOf, C_80, uri_rdfs_Container) | ~iext(uri_rdfs_subClassOf, C_80, uri_rdf_Bag)))).
% 12.16/4.06 tff(c_1400, plain, (![Q_83]: (iext(Q_83, uri_rdf_Property, uri_rdfs_Class) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_83)))).
% 12.16/4.06 tff(c_1403, plain, (![Q_83]: (iext(Q_83, uri_rdf_type, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_83)))).
% 12.16/4.06 tff(c_1394, plain, (![Q_83]: (iext(Q_83, uri_rdf_XMLLiteral, uri_rdfs_Datatype) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_83)))).
% 12.16/4.06 tff(c_1434, plain, (![Q_83]: (iext(Q_83, uri_rdfs_range, uri_rdf_Property) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_83)))).
% 12.16/4.06 tff(c_1449, plain, (![Q_83]: (iext(Q_83, uri_rdf_nil, uri_rdf_List) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_83)))).
% 12.16/4.06 tff(c_1440, plain, (![Q_83]: (iext(Q_83, uri_rdf_predicate, uri_rdfs_Statement) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_83)))).
% 12.16/4.06 tff(c_4192, plain, (~icext(uri_rdfs_ContainerMembershipProperty, uri_owl_complementOf))).
% 12.16/4.06 tff(c_1399, plain, (![Q_83]: (iext(Q_83, uri_ex_c, '#skF_1') | ~iext(uri_rdfs_subPropertyOf, uri_owl_complementOf, Q_83)))).
% 12.16/4.06 tff(c_1410, plain, (![Q_83]: (iext(Q_83, uri_rdfs_label, uri_rdfs_Literal) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_83)))).
% 12.16/4.06 tff(c_1463, plain, (![P_87]: (iext(uri_rdfs_subPropertyOf, P_87, uri_rdfs_seeAlso) | ~iext(uri_rdfs_subPropertyOf, P_87, uri_rdfs_isDefinedBy)))).
% 12.16/4.06 tff(c_1435, plain, (![Q_83]: (iext(Q_83, uri_rdfs_domain, uri_rdfs_Class) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_83)))).
% 12.16/4.06 tff(c_1429, plain, (![Q_83]: (iext(Q_83, uri_rdf__1, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_83)))).
% 12.16/4.06 tff(c_1414, plain, (![Q_83]: (iext(Q_83, uri_rdf_object, uri_rdfs_Statement) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_83)))).
% 12.16/4.06 tff(c_3973, plain, (~iext(uri_rdfs_subClassOf, uri_rdfs_Class, uri_rdf_XMLLiteral))).
% 12.16/4.06 tff(c_1445, plain, (![Q_83]: (iext(Q_83, uri_rdfs_domain, uri_rdf_Property) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_83)))).
% 12.16/4.06 tff(c_3961, plain, (~icext(uri_rdfs_ContainerMembershipProperty, uri_rdfs_subClassOf))).
% 12.16/4.06 tff(c_1450, plain, (![Q_83]: (iext(Q_83, uri_rdf_XMLLiteral, uri_rdfs_Literal) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_83)))).
% 12.16/4.06 tff(c_3949, plain, (~iext(uri_rdfs_subClassOf, uri_rdf_List, uri_rdf_XMLLiteral))).
% 12.16/4.06 tff(c_3948, plain, (~iext(uri_rdfs_subClassOf, uri_owl_Restriction, uri_rdf_XMLLiteral))).
% 12.16/4.06 tff(c_1427, plain, (![Q_83]: (iext(Q_83, uri_rdf_object, uri_rdf_Property) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_83)))).
% 12.16/4.06 tff(c_3936, plain, (~icext(uri_rdfs_ContainerMembershipProperty, uri_rdfs_subPropertyOf))).
% 12.16/4.06 tff(c_1441, plain, (![Q_83]: (iext(Q_83, uri_rdfs_isDefinedBy, uri_rdfs_seeAlso) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_83)))).
% 12.16/4.06 tff(c_3924, plain, (~iext(uri_rdfs_subClassOf, uri_owl_Class, uri_rdf_XMLLiteral))).
% 12.16/4.06 tff(c_3912, plain, (~iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, uri_rdf_XMLLiteral))).
% 12.16/4.06 tff(c_1438, plain, (![Q_83]: (iext(Q_83, uri_rdfs_seeAlso, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_83)))).
% 12.16/4.06 tff(c_1231, plain, (![C_80]: (iext(uri_rdfs_subClassOf, C_80, uri_rdfs_Class) | ~iext(uri_rdfs_subClassOf, C_80, uri_rdfs_Datatype)))).
% 12.16/4.06 tff(c_3903, plain, (~iext(uri_rdfs_subClassOf, uri_rdf_Property, uri_rdf_XMLLiteral))).
% 12.16/4.06 tff(c_3891, plain, (~iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, uri_rdf_XMLLiteral))).
% 12.16/4.06 tff(c_1412, plain, (![Q_83]: (iext(Q_83, uri_rdf_value, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_83)))).
% 12.16/4.06 tff(c_3890, plain, (~iext(uri_rdfs_subClassOf, uri_rdfs_Resource, uri_rdf_XMLLiteral))).
% 12.16/4.06 tff(c_1232, plain, (![C_80]: (iext(uri_rdfs_subClassOf, C_80, uri_rdfs_Literal) | ~iext(uri_rdfs_subClassOf, C_80, uri_rdf_XMLLiteral)))).
% 12.16/4.06 tff(c_1437, plain, (![Q_83]: (iext(Q_83, uri_rdf_subject, uri_rdfs_Statement) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_83)))).
% 12.16/4.06 tff(c_1397, plain, (![Q_83]: (iext(Q_83, uri_rdf_type, uri_rdfs_Class) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_83)))).
% 12.16/4.06 tff(c_1442, plain, (![Q_83]: (iext(Q_83, uri_rdfs_member, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_83)))).
% 12.16/4.06 tff(c_3620, plain, (~iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, uri_rdf_Alt))).
% 12.16/4.06 tff(c_1419, plain, (![Q_83]: (iext(Q_83, uri_rdf__3, uri_rdf_Property) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_83)))).
% 12.16/4.06 tff(c_1416, plain, (![Q_83]: (iext(Q_83, uri_rdfs_comment, uri_rdfs_Literal) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_83)))).
% 12.16/4.06 tff(c_3597, plain, (~iext(uri_rdfs_subClassOf, uri_owl_Restriction, uri_rdf_Alt))).
% 12.16/4.06 tff(c_3585, plain, (~iext(uri_rdfs_subClassOf, uri_owl_Class, uri_rdf_Alt))).
% 12.16/4.06 tff(c_1389, plain, (![Q_83]: (iext(Q_83, uri_rdfs_label, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_83)))).
% 12.16/4.06 tff(c_3584, plain, (~iext(uri_rdfs_subClassOf, uri_rdfs_Class, uri_rdf_Alt))).
% 12.16/4.06 tff(c_1388, plain, (![Q_83]: (iext(Q_83, uri_rdfs_range, uri_rdfs_Class) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_83)))).
% 12.16/4.06 tff(c_3572, plain, (~iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, uri_rdf_Alt))).
% 12.16/4.06 tff(c_1431, plain, (![Q_83]: (iext(Q_83, uri_rdfs_isDefinedBy, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_83)))).
% 12.16/4.06 tff(c_3560, plain, (~iext(uri_rdfs_subClassOf, uri_rdf_Property, uri_rdf_Alt))).
% 12.16/4.06 tff(c_3548, plain, (~iext(uri_rdfs_subClassOf, uri_rdf_List, uri_rdf_Alt))).
% 12.16/4.07 tff(c_1402, plain, (![Q_83]: (iext(Q_83, uri_ex_c, uri_owl_Class) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_83)))).
% 12.16/4.07 tff(c_3547, plain, (~iext(uri_rdfs_subClassOf, uri_rdfs_Resource, uri_rdf_Alt))).
% 12.16/4.07 tff(c_1227, plain, (![C_80]: (iext(uri_rdfs_subClassOf, C_80, uri_rdfs_Container) | ~iext(uri_rdfs_subClassOf, C_80, uri_rdfs_Seq)))).
% 12.16/4.07 tff(c_1230, plain, (![C_80]: (iext(uri_rdfs_subClassOf, C_80, uri_rdfs_Container) | ~iext(uri_rdfs_subClassOf, C_80, uri_rdf_Alt)))).
% 12.16/4.07 tff(c_1422, plain, (![Q_83]: (iext(Q_83, uri_rdf_subject, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_83)))).
% 12.16/4.07 tff(c_1418, plain, (![Q_83]: (iext(Q_83, uri_rdfs_seeAlso, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_83)))).
% 12.16/4.07 tff(c_1421, plain, (![Q_83]: (iext(Q_83, uri_rdf_first, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_83)))).
% 12.16/4.07 tff(c_3258, plain, (~icext(uri_rdfs_ContainerMembershipProperty, uri_rdfs_range))).
% 12.16/4.07 tff(c_1404, plain, (![Q_83]: (iext(Q_83, uri_rdf__3, uri_rdfs_ContainerMembershipProperty) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_83)))).
% 12.16/4.07 tff(c_1430, plain, (![Q_83]: (iext(Q_83, uri_rdf__1, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_83)))).
% 12.16/4.07 tff(c_1406, plain, (![Q_83]: (iext(Q_83, uri_rdf__1, uri_rdf_Property) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_83)))).
% 12.16/4.07 tff(c_1420, plain, (![Q_83]: (iext(Q_83, uri_rdf_rest, uri_rdf_List) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_83)))).
% 12.16/4.07 tff(c_1443, plain, (![Q_83]: (iext(Q_83, uri_rdfs_subPropertyOf, uri_rdf_Property) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_83)))).
% 12.16/4.07 tff(c_1796, plain, (![D_24]: (icext(D_24, uri_rdf_predicate) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))).
% 12.16/4.07 tff(c_1766, plain, (![D_24]: (icext(D_24, uri_rdfs_domain) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))).
% 12.16/4.07 tff(c_1819, plain, (![D_24]: (icext(D_24, uri_rdf_Alt) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_24)))).
% 12.16/4.07 tff(c_1739, plain, (![D_24]: (icext(D_24, uri_rdfs_Statement) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_24)))).
% 12.16/4.07 tff(c_1751, plain, (![D_24]: (icext(D_24, uri_rdfs_Resource) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_24)))).
% 12.16/4.07 tff(c_1728, plain, (![D_24]: (icext(D_24, uri_rdfs_isDefinedBy) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))).
% 12.16/4.07 tff(c_1707, plain, (![D_24]: (icext(D_24, uri_rdfs_ContainerMembershipProperty) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_24)))).
% 12.16/4.07 tff(c_1862, plain, (![D_24]: (icext(D_24, uri_rdfs_Class) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_24)))).
% 12.16/4.07 tff(c_1433, plain, (![Q_83]: (iext(Q_83, uri_rdfs_comment, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_83)))).
% 12.16/4.07 tff(c_1909, plain, (![D_24]: (icext(D_24, uri_rdfs_comment) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))).
% 12.16/4.07 tff(c_1891, plain, (![D_24]: (icext(D_24, uri_rdfs_seeAlso) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))).
% 12.16/4.07 tff(c_1645, plain, (![D_24]: (icext(D_24, uri_rdf_Bag) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_24)))).
% 12.16/4.07 tff(c_2089, plain, (![D_24]: (icext(D_24, uri_rdfs_Container) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_24)))).
% 12.16/4.07 tff(c_1783, plain, (![D_24]: (icext(D_24, uri_rdf_List) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_24)))).
% 12.16/4.07 tff(c_2026, plain, (![D_24]: (icext(D_24, uri_rdfs_Literal) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_24)))).
% 12.16/4.07 tff(c_1690, plain, (![D_24]: (icext(D_24, uri_rdfs_subClassOf) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))).
% 12.16/4.07 tff(c_1938, plain, (![D_24]: (icext(D_24, uri_rdfs_Seq) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_24)))).
% 12.16/4.07 tff(c_1971, plain, (![D_24]: (icext(D_24, uri_rdfs_member) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))).
% 12.16/4.07 tff(c_1398, plain, (![Q_83]: (iext(Q_83, uri_rdfs_subClassOf, uri_rdfs_Class) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_83)))).
% 12.16/4.07 tff(c_1982, plain, (![D_24]: (icext(D_24, uri_owl_Restriction) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_24)))).
% 12.16/4.07 tff(c_2046, plain, (![D_24]: (icext(D_24, uri_rdfs_Datatype) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_24)))).
% 12.16/4.07 tff(c_2159, plain, (![D_24]: (icext(D_24, uri_rdfs_label) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))).
% 12.16/4.07 tff(c_2280, plain, (![D_24]: (icext(D_24, uri_rdfs_range) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))).
% 12.16/4.07 tff(c_2152, plain, (![D_24]: (icext(D_24, uri_rdfs_subPropertyOf) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))).
% 12.16/4.07 tff(c_2102, plain, (![D_24]: (icext(D_24, uri_rdf_XMLLiteral) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_24)))).
% 12.16/4.07 tff(c_2236, plain, (![D_24]: (icext(D_24, uri_owl_Class) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_24)))).
% 12.16/4.07 tff(c_1495, plain, (![D_24]: (icext(D_24, uri_rdf__1) | ~iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, D_24)))).
% 12.16/4.07 tff(c_1504, plain, (![D_24]: (icext(D_24, uri_rdf_subject) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))).
% 12.16/4.07 tff(c_1413, plain, (![Q_83]: (iext(Q_83, uri_rdf_subject, uri_rdf_Property) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_83)))).
% 12.16/4.07 tff(c_2655, plain, (~icext(uri_rdfs_ContainerMembershipProperty, uri_rdf_type))).
% 12.16/4.07 tff(c_2654, plain, (~icext(uri_rdfs_Datatype, uri_rdf_List))).
% 12.16/4.07 tff(c_2633, plain, (~icext(uri_rdfs_Datatype, uri_rdfs_Datatype))).
% 12.16/4.07 tff(c_1519, plain, (![D_24]: (icext(D_24, uri_rdf_nil) | ~iext(uri_rdfs_subClassOf, uri_rdf_List, D_24)))).
% 12.16/4.07 tff(c_1478, plain, (![D_24]: (icext(D_24, uri_rdf_XMLLiteral) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, D_24)))).
% 12.16/4.07 tff(c_1528, plain, (![D_24]: (icext(D_24, uri_rdf_first) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))).
% 12.16/4.07 tff(c_1432, plain, (![Q_83]: (iext(Q_83, uri_rdf_value, uri_rdf_Property) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_83)))).
% 12.16/4.07 tff(c_1507, plain, (![D_24]: (icext(D_24, uri_rdf_rest) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))).
% 12.16/4.07 tff(c_2556, plain, (~icext(uri_rdfs_Datatype, uri_owl_Restriction))).
% 12.16/4.07 tff(c_1525, plain, (![D_24]: (icext(D_24, '#skF_1') | ~iext(uri_rdfs_subClassOf, uri_owl_Restriction, D_24)))).
% 12.16/4.07 tff(c_1513, plain, (![D_24]: (icext(D_24, uri_rdf_type) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))).
% 12.16/4.07 tff(c_1510, plain, (![D_24]: (icext(D_24, uri_rdf__1) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))).
% 12.16/4.07 tff(c_2495, plain, (~icext(uri_rdfs_Datatype, uri_rdfs_Class))).
% 12.16/4.07 tff(c_1487, plain, (![D_24]: (icext(D_24, uri_rdf_Property) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_24)))).
% 12.49/4.07 tff(c_1391, plain, (![Q_83]: (iext(Q_83, uri_rdf__3, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_83)))).
% 12.49/4.07 tff(c_1531, plain, (![D_24]: (icext(D_24, uri_rdf_value) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))).
% 12.49/4.07 tff(c_1498, plain, (![D_24]: (icext(D_24, uri_rdf_object) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))).
% 12.49/4.07 tff(c_2423, plain, (~icext(uri_rdfs_ContainerMembershipProperty, uri_rdfs_domain))).
% 12.49/4.07 tff(c_2422, plain, (~icext(uri_rdfs_Datatype, uri_owl_Class))).
% 12.49/4.07 tff(c_1516, plain, (![D_24]: (icext(D_24, uri_ex_c) | ~iext(uri_rdfs_subClassOf, uri_owl_Class, D_24)))).
% 12.49/4.07 tff(c_1492, plain, (![D_24]: (icext(D_24, uri_rdf__2) | ~iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, D_24)))).
% 12.49/4.07 tff(c_1481, plain, (![D_24]: (icext(D_24, uri_rdf__2) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))).
% 12.49/4.07 tff(c_1392, plain, (![Q_83]: (iext(Q_83, uri_rdfs_member, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_83)))).
% 12.49/4.07 tff(c_2345, plain, (~icext(uri_rdfs_Datatype, uri_rdf_Property))).
% 12.49/4.07 tff(c_1501, plain, (![D_24]: (icext(D_24, uri_rdf__3) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))).
% 12.49/4.07 tff(c_2324, plain, (~icext(uri_rdfs_Datatype, uri_rdfs_ContainerMembershipProperty))).
% 12.49/4.07 tff(c_1522, plain, (![D_24]: (icext(D_24, uri_rdf__3) | ~iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, D_24)))).
% 12.49/4.07 tff(c_924, plain, (![C_72]: (icext(C_72, uri_rdf_rest) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_72)))).
% 12.49/4.07 tff(c_968, plain, (![C_72]: (icext(C_72, uri_rdfs_range) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_72)))).
% 12.49/4.07 tff(c_977, plain, (![C_72]: (icext(C_72, uri_rdfs_subPropertyOf) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_72)))).
% 12.49/4.07 tff(c_2272, plain, (icext(uri_rdf_Property, uri_rdfs_range))).
% 12.49/4.07 tff(c_922, plain, (![C_72]: (icext(C_72, uri_rdfs_range) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_72)))).
% 12.49/4.07 tff(c_972, plain, (![C_72]: (icext(C_72, uri_rdfs_seeAlso) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_72)))).
% 12.49/4.07 tff(c_945, plain, (![C_72]: (icext(C_72, uri_rdf__2) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_72)))).
% 12.49/4.07 tff(c_1167, plain, (![C_76]: (icext(C_76, uri_rdf_Property) | ~iext(uri_rdfs_range, uri_rdfs_subClassOf, C_76)))).
% 12.49/4.08 tff(c_931, plain, (![C_72]: (icext(C_72, uri_rdf_type) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_72)))).
% 12.49/4.08 tff(c_952, plain, (![C_72]: (icext(C_72, uri_rdfs_seeAlso) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_72)))).
% 12.49/4.08 tff(c_2237, plain, (ic(uri_owl_Class))).
% 12.49/4.08 tff(c_2230, plain, (icext(uri_rdfs_Class, uri_owl_Class))).
% 12.49/4.08 tff(c_1154, plain, (![C_76]: (icext(C_76, uri_owl_Class) | ~iext(uri_rdfs_range, uri_rdf_type, C_76)))).
% 12.49/4.08 tff(c_970, plain, (![C_72]: (icext(C_72, uri_rdfs_Datatype) | ~iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_72)))).
% 12.49/4.08 tff(c_947, plain, (![C_72]: (icext(C_72, uri_rdf_subject) | ~iext(uri_rdfs_domain, uri_rdf_type, C_72)))).
% 12.49/4.08 tff(c_1169, plain, (![C_76]: (icext(C_76, uri_rdf_Property) | ~iext(uri_rdfs_range, uri_rdfs_range, C_76)))).
% 12.49/4.08 tff(c_1172, plain, (![C_76]: (icext(C_76, uri_rdf_List) | ~iext(uri_rdfs_range, uri_rdfs_domain, C_76)))).
% 12.49/4.08 tff(c_948, plain, (![C_72]: (icext(C_72, uri_rdf_object) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_72)))).
% 12.49/4.08 tff(c_975, plain, (![C_72]: (icext(C_72, uri_rdfs_isDefinedBy) | ~iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_72)))).
% 12.49/4.08 tff(c_1152, plain, (![C_76]: (icext(C_76, uri_rdfs_Class) | ~iext(uri_rdfs_range, uri_rdf_type, C_76)))).
% 12.49/4.08 tff(c_963, plain, (![C_72]: (icext(C_72, uri_rdf__1) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_72)))).
% 12.49/4.08 tff(c_950, plain, (![C_72]: (icext(C_72, uri_rdfs_comment) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_72)))).
% 12.49/4.08 tff(c_1202, plain, (![C_76]: (icext(C_76, uri_rdfs_Literal) | ~iext(uri_rdfs_range, uri_rdfs_subClassOf, C_76)))).
% 12.49/4.08 tff(c_944, plain, (![C_72]: (icext(C_72, uri_rdfs_label) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_72)))).
% 12.49/4.08 tff(c_2158, plain, (ip(uri_rdfs_label))).
% 12.49/4.08 tff(c_2144, plain, (icext(uri_rdf_Property, uri_rdfs_label))).
% 12.49/4.08 tff(c_2139, plain, (icext(uri_rdf_Property, uri_rdfs_subPropertyOf))).
% 12.49/4.08 tff(c_923, plain, (![C_72]: (icext(C_72, uri_rdfs_label) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_72)))).
% 12.49/4.08 tff(c_951, plain, (![C_72]: (icext(C_72, uri_rdfs_subPropertyOf) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_72)))).
% 12.49/4.08 tff(c_934, plain, (![C_72]: (icext(C_72, uri_rdf_Property) | ~iext(uri_rdfs_domain, uri_rdf_type, C_72)))).
% 12.49/4.08 tff(c_928, plain, (![C_72]: (icext(C_72, uri_rdf_XMLLiteral) | ~iext(uri_rdfs_domain, uri_rdf_type, C_72)))).
% 12.49/4.08 tff(c_959, plain, (![C_72]: (icext(C_72, uri_rdf_predicate) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_72)))).
% 12.49/4.08 tff(c_954, plain, (![C_72]: (icext(C_72, uri_rdf_rest) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_72)))).
% 12.49/4.08 tff(c_973, plain, (![C_72]: (icext(C_72, uri_rdf_first) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_72)))).
% 12.49/4.08 tff(c_2096, plain, (icext(uri_rdfs_Class, uri_rdf_XMLLiteral))).
% 12.49/4.08 tff(c_984, plain, (![C_72]: (icext(C_72, uri_rdf_XMLLiteral) | ~iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_72)))).
% 12.49/4.08 tff(c_2083, plain, (icext(uri_rdfs_Class, uri_rdfs_Container))).
% 12.49/4.08 tff(c_1176, plain, (![C_76]: (icext(C_76, uri_rdfs_Container) | ~iext(uri_rdfs_range, uri_rdfs_subClassOf, C_76)))).
% 12.49/4.08 tff(c_2078, plain, (~icext(uri_rdfs_Datatype, uri_rdfs_Resource))).
% 12.49/4.08 tff(c_767, plain, (![D_69, X_17]: (icext(D_69, X_17) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Resource, D_69)))).
% 12.49/4.08 tff(c_978, plain, (![C_72]: (icext(C_72, uri_rdf_rest) | ~iext(uri_rdfs_domain, uri_rdf_type, C_72)))).
% 12.49/4.08 tff(c_966, plain, (![C_72]: (icext(C_72, uri_rdf_value) | ~iext(uri_rdfs_domain, uri_rdf_type, C_72)))).
% 12.49/4.08 tff(c_2040, plain, (icext(uri_rdfs_Class, uri_rdfs_Datatype))).
% 12.49/4.08 tff(c_1146, plain, (![C_76]: (icext(C_76, uri_rdfs_Datatype) | ~iext(uri_rdfs_range, uri_rdf_type, C_76)))).
% 12.49/4.08 tff(c_1151, plain, (![C_76]: (icext(C_76, '#skF_1') | ~iext(uri_rdfs_range, uri_owl_complementOf, C_76)))).
% 12.49/4.08 tff(c_1188, plain, (![C_76]: (icext(C_76, uri_rdfs_Class) | ~iext(uri_rdfs_range, uri_rdfs_subClassOf, C_76)))).
% 12.49/4.08 tff(c_2020, plain, (icext(uri_rdfs_Class, uri_rdfs_Literal))).
% 12.49/4.08 tff(c_1168, plain, (![C_76]: (icext(C_76, uri_rdfs_Literal) | ~iext(uri_rdfs_range, uri_rdfs_range, C_76)))).
% 12.49/4.08 tff(c_946, plain, (![C_72]: (icext(C_72, uri_rdf_value) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_72)))).
% 12.49/4.08 tff(c_919, plain, (![C_72]: (icext(C_72, '#skF_1') | ~iext(uri_rdfs_domain, uri_owl_hasSelf, C_72)))).
% 12.49/4.08 tff(c_933, plain, (![C_72]: (icext(C_72, uri_ex_c) | ~iext(uri_rdfs_domain, uri_owl_complementOf, C_72)))).
% 12.49/4.08 tff(c_956, plain, (![C_72]: (icext(C_72, uri_rdf_subject) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_72)))).
% 12.49/4.08 tff(c_926, plain, (![C_72]: (icext(C_72, uri_rdfs_member) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_72)))).
% 12.49/4.08 tff(c_964, plain, (![C_72]: (icext(C_72, uri_rdf__1) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_72)))).
% 12.49/4.08 tff(c_925, plain, (![C_72]: (icext(C_72, uri_rdf__3) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_72)))).
% 12.49/4.08 tff(c_1983, plain, (ic(uri_owl_Restriction))).
% 12.49/4.08 tff(c_1976, plain, (icext(uri_rdfs_Class, uri_owl_Restriction))).
% 12.49/4.08 tff(c_1160, plain, (![C_76]: (icext(C_76, uri_owl_Restriction) | ~iext(uri_rdfs_range, uri_rdf_type, C_76)))).
% 12.49/4.08 tff(c_1963, plain, (icext(uri_rdf_Property, uri_rdfs_member))).
% 12.49/4.08 tff(c_976, plain, (![C_72]: (icext(C_72, uri_rdfs_member) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_72)))).
% 12.49/4.08 tff(c_937, plain, (![C_72]: (icext(C_72, uri_rdf_type) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_72)))).
% 12.49/4.08 tff(c_1150, plain, (![C_76]: (icext(C_76, uri_rdfs_Class) | ~iext(uri_rdfs_range, uri_rdfs_domain, C_76)))).
% 12.49/4.08 tff(c_936, plain, (![C_72]: (icext(C_72, uri_ex_c) | ~iext(uri_rdfs_domain, uri_rdf_type, C_72)))).
% 12.49/4.08 tff(c_1932, plain, (icext(uri_rdfs_Class, uri_rdfs_Seq))).
% 12.49/4.08 tff(c_935, plain, (![C_72]: (icext(C_72, uri_rdfs_Seq) | ~iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_72)))).
% 12.49/4.08 tff(c_943, plain, (![C_72]: (icext(C_72, uri_rdf__3) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_72)))).
% 12.49/4.08 tff(c_942, plain, (![C_72]: (icext(C_72, '#skF_1') | ~iext(uri_rdfs_domain, uri_rdf_type, C_72)))).
% 12.49/4.08 tff(c_1142, plain, (![C_76]: (icext(C_76, uri_rdf_List) | ~iext(uri_rdfs_range, uri_rdfs_range, C_76)))).
% 12.49/4.08 tff(c_1908, plain, (ip(uri_rdfs_comment))).
% 12.49/4.08 tff(c_1902, plain, (icext(uri_rdf_Property, uri_rdfs_comment))).
% 12.49/4.08 tff(c_967, plain, (![C_72]: (icext(C_72, uri_rdfs_comment) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_72)))).
% 12.49/4.08 tff(c_965, plain, (![C_72]: (icext(C_72, uri_rdfs_isDefinedBy) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_72)))).
% 12.49/4.08 tff(c_1883, plain, (icext(uri_rdf_Property, uri_rdfs_seeAlso))).
% 12.49/4.08 tff(c_1193, plain, (![C_76]: (icext(C_76, uri_rdfs_seeAlso) | ~iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_76)))).
% 12.49/4.08 tff(c_982, plain, (![C_72]: (icext(C_72, '#skF_1') | ~iext(uri_rdfs_domain, uri_owl_onProperty, C_72)))).
% 12.49/4.08 tff(c_939, plain, (![C_72]: (icext(C_72, uri_rdf_type) | ~iext(uri_rdfs_domain, uri_rdf_type, C_72)))).
% 12.49/4.08 tff(c_971, plain, (![C_72]: (icext(C_72, uri_rdf_subject) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_72)))).
% 12.49/4.08 tff(c_1200, plain, (![C_76]: (icext(C_76, uri_rdf_type) | ~iext(uri_rdfs_range, uri_owl_onProperty, C_76)))).
% 12.49/4.08 tff(c_1856, plain, (icext(uri_rdfs_Class, uri_rdfs_Class))).
% 12.49/4.08 tff(c_1149, plain, (![C_76]: (icext(C_76, uri_rdfs_Class) | ~iext(uri_rdfs_range, uri_rdfs_range, C_76)))).
% 12.49/4.08 tff(c_1197, plain, (![C_76]: (icext(C_76, uri_rdf_Property) | ~iext(uri_rdfs_range, uri_rdfs_domain, C_76)))).
% 12.49/4.08 tff(c_941, plain, (![C_72]: (icext(C_72, uri_rdf__2) | ~iext(uri_rdfs_domain, uri_rdf_type, C_72)))).
% 12.49/4.08 tff(c_953, plain, (![C_72]: (icext(C_72, uri_rdf__3) | ~iext(uri_rdfs_domain, uri_rdf_type, C_72)))).
% 12.49/4.08 tff(c_940, plain, (![C_72]: (icext(C_72, uri_rdf__1) | ~iext(uri_rdfs_domain, uri_rdf_type, C_72)))).
% 12.49/4.08 tff(c_980, plain, (![C_72]: (icext(C_72, uri_rdf_value) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_72)))).
% 12.49/4.08 tff(c_1813, plain, (icext(uri_rdfs_Class, uri_rdf_Alt))).
% 12.49/4.08 tff(c_960, plain, (![C_72]: (icext(C_72, uri_rdf_Alt) | ~iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_72)))).
% 12.49/4.08 tff(c_969, plain, (![C_72]: (icext(C_72, uri_rdfs_domain) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_72)))).
% 12.49/4.08 tff(c_1180, plain, (![C_76]: (icext(C_76, uri_rdfs_Resource) | ~iext(uri_rdfs_range, uri_rdfs_domain, C_76)))).
% 12.49/4.08 tff(c_1795, plain, (ip(uri_rdf_predicate))).
% 12.49/4.08 tff(c_1789, plain, (icext(uri_rdf_Property, uri_rdf_predicate))).
% 12.49/4.08 tff(c_1784, plain, (ic(uri_rdf_List))).
% 12.49/4.08 tff(c_974, plain, (![C_72]: (icext(C_72, uri_rdf_predicate) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_72)))).
% 12.49/4.08 tff(c_1777, plain, (icext(uri_rdfs_Class, uri_rdf_List))).
% 12.49/4.08 tff(c_1201, plain, (![C_76]: (icext(C_76, uri_rdf_List) | ~iext(uri_rdfs_range, uri_rdf_type, C_76)))).
% 12.49/4.08 tff(c_1156, plain, (![C_76]: (icext(C_76, uri_rdfs_ContainerMembershipProperty) | ~iext(uri_rdfs_range, uri_rdf_type, C_76)))).
% 12.49/4.08 tff(c_1758, plain, (icext(uri_rdf_Property, uri_rdfs_domain))).
% 12.49/4.08 tff(c_979, plain, (![C_72]: (icext(C_72, uri_rdfs_domain) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_72)))).
% 12.49/4.08 tff(c_1745, plain, (icext(uri_rdfs_Class, uri_rdfs_Resource))).
% 12.49/4.08 tff(c_1740, plain, (ic(uri_rdfs_Statement))).
% 12.49/4.08 tff(c_1161, plain, (![C_76]: (icext(C_76, uri_rdfs_Resource) | ~iext(uri_rdfs_range, uri_rdfs_range, C_76)))).
% 12.49/4.08 tff(c_1733, plain, (icext(uri_rdfs_Class, uri_rdfs_Statement))).
% 12.49/4.08 tff(c_1192, plain, (![C_76]: (icext(C_76, uri_rdfs_Statement) | ~iext(uri_rdfs_range, uri_rdfs_domain, C_76)))).
% 12.49/4.08 tff(c_1720, plain, (icext(uri_rdf_Property, uri_rdfs_isDefinedBy))).
% 12.49/4.08 tff(c_957, plain, (![C_72]: (icext(C_72, uri_rdfs_isDefinedBy) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_72)))).
% 12.49/4.08 tff(c_927, plain, (![C_72]: (icext(C_72, uri_rdfs_subClassOf) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_72)))).
% 12.49/4.08 tff(c_1701, plain, (icext(uri_rdfs_Class, uri_rdfs_ContainerMembershipProperty))).
% 12.49/4.08 tff(c_949, plain, (![C_72]: (icext(C_72, uri_rdfs_ContainerMembershipProperty) | ~iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_72)))).
% 12.49/4.08 tff(c_1171, plain, (![C_76]: (icext(C_76, uri_rdf_Property) | ~iext(uri_rdfs_range, uri_rdf_type, C_76)))).
% 12.49/4.08 tff(c_1676, plain, (icext(uri_rdf_Property, uri_rdfs_subClassOf))).
% 12.49/4.09 tff(c_981, plain, (![C_72]: (icext(C_72, uri_rdf_first) | ~iext(uri_rdfs_domain, uri_rdf_type, C_72)))).
% 12.49/4.09 tff(c_932, plain, (![C_72]: (icext(C_72, uri_rdfs_subClassOf) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_72)))).
% 12.49/4.09 tff(c_962, plain, (![C_72]: (icext(C_72, uri_rdf__2) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_72)))).
% 12.49/4.09 tff(c_955, plain, (![C_72]: (icext(C_72, uri_rdf_first) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_72)))).
% 12.49/4.09 tff(c_961, plain, (![C_72]: (icext(C_72, uri_rdf_object) | ~iext(uri_rdfs_domain, uri_rdf_type, C_72)))).
% 12.49/4.09 tff(c_983, plain, (![C_72]: (icext(C_72, uri_rdf_nil) | ~iext(uri_rdfs_domain, uri_rdf_type, C_72)))).
% 12.49/4.09 tff(c_1639, plain, (icext(uri_rdfs_Class, uri_rdf_Bag))).
% 12.49/4.09 tff(c_958, plain, (![C_72]: (icext(C_72, uri_rdf_Bag) | ~iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_72)))).
% 12.56/4.09 tff(c_652, plain, (![X_64]: (ip(X_64) | ~icext(uri_rdf_Property, X_64)))).
% 12.56/4.09 tff(c_639, plain, (![P_63]: (ip(P_63) | ~icext(uri_rdfs_ContainerMembershipProperty, P_63)))).
% 12.56/4.09 tff(c_669, plain, (![D_66]: (ic(D_66) | ~icext(uri_rdfs_Datatype, D_66)))).
% 12.56/4.09 tff(c_1561, plain, (ip(uri_rdfs_member))).
% 12.56/4.09 tff(c_1551, plain, (ic(uri_rdfs_Resource))).
% 12.56/4.09 tff(c_736, plain, (![P_6]: (icext(uri_rdf_Property, P_6) | ~ip(P_6)))).
% 12.56/4.09 tff(c_750, plain, (icext(uri_rdf_Property, uri_rdf_value))).
% 12.56/4.09 tff(c_752, plain, (icext(uri_rdf_Property, uri_rdf_first))).
% 12.56/4.09 tff(c_746, plain, (icext(uri_owl_Restriction, '#skF_1'))).
% 12.56/4.09 tff(c_742, plain, (icext(uri_rdfs_ContainerMembershipProperty, uri_rdf__3))).
% 12.56/4.09 tff(c_753, plain, (icext(uri_rdf_List, uri_rdf_nil))).
% 12.56/4.09 tff(c_741, plain, (icext(uri_owl_Class, uri_ex_c))).
% 12.56/4.09 tff(c_743, plain, (icext(uri_rdf_Property, uri_rdf_type))).
% 12.56/4.09 tff(c_744, plain, (icext(uri_rdf_Property, uri_rdf__1))).
% 12.56/4.09 tff(c_751, plain, (icext(uri_rdf_Property, uri_rdf_rest))).
% 12.56/4.09 tff(c_747, plain, (icext(uri_rdf_Property, uri_rdf_subject))).
% 12.56/4.09 tff(c_748, plain, (icext(uri_rdf_Property, uri_rdf__3))).
% 12.56/4.09 tff(c_749, plain, (icext(uri_rdf_Property, uri_rdf_object))).
% 12.56/4.09 tff(c_739, plain, (icext(uri_rdfs_ContainerMembershipProperty, uri_rdf__1))).
% 12.56/4.09 tff(c_745, plain, (icext(uri_rdfs_ContainerMembershipProperty, uri_rdf__2))).
% 12.56/4.09 tff(c_740, plain, (icext(uri_rdfs_Class, uri_rdf_Property))).
% 12.56/4.09 tff(c_738, plain, (icext(uri_rdf_Property, uri_rdf__2))).
% 12.56/4.09 tff(c_737, plain, (icext(uri_rdfs_Datatype, uri_rdf_XMLLiteral))).
% 12.56/4.09 tff(c_585, plain, (ip(uri_rdf_value))).
% 12.56/4.09 tff(c_540, plain, (ic(uri_rdfs_ContainerMembershipProperty))).
% 12.56/4.09 tff(c_539, plain, (ic(uri_rdfs_Seq))).
% 12.56/4.09 tff(c_578, plain, (ip(uri_rdf__2))).
% 12.56/4.09 tff(c_170, plain, (![P_38, R_40, Q_39]: (iext(uri_rdfs_subPropertyOf, P_38, R_40) | ~iext(uri_rdfs_subPropertyOf, Q_39, R_40) | ~iext(uri_rdfs_subPropertyOf, P_38, Q_39)))).
% 12.56/4.09 tff(c_160, plain, (![Q_32, X_35, Y_36, P_31]: (iext(Q_32, X_35, Y_36) | ~iext(P_31, X_35, Y_36) | ~iext(uri_rdfs_subPropertyOf, P_31, Q_32)))).
% 12.56/4.09 tff(c_582, plain, (ip(uri_rdf_subject))).
% 12.56/4.09 tff(c_156, plain, (![C_28, E_30, D_29]: (iext(uri_rdfs_subClassOf, C_28, E_30) | ~iext(uri_rdfs_subClassOf, D_29, E_30) | ~iext(uri_rdfs_subClassOf, C_28, D_29)))).
% 12.56/4.09 tff(c_455, plain, (ip(uri_owl_complementOf))).
% 12.56/4.09 tff(c_128, plain, (![C_20, Y_22, P_19, X_21]: (icext(C_20, Y_22) | ~iext(P_19, X_21, Y_22) | ~iext(uri_rdfs_range, P_19, C_20)))).
% 12.56/4.09 tff(c_586, plain, (ip(uri_rdf_rest))).
% 12.56/4.09 tff(c_108, plain, (![C_13, X_14, P_12, Y_15]: (icext(C_13, X_14) | ~iext(P_12, X_14, Y_15) | ~iext(uri_rdfs_domain, P_12, C_13)))).
% 12.56/4.09 tff(c_146, plain, (![D_24, X_26, C_23]: (icext(D_24, X_26) | ~icext(C_23, X_26) | ~iext(uri_rdfs_subClassOf, C_23, D_24)))).
% 12.56/4.09 tff(c_497, plain, (ip(uri_rdfs_subPropertyOf))).
% 12.56/4.09 tff(c_52, plain, (![C_8, X_7]: (icext(C_8, X_7) | ~iext(uri_rdf_type, X_7, C_8)))).
% 12.56/4.09 tff(c_102, plain, (![D_11]: (iext(uri_rdfs_subClassOf, D_11, uri_rdfs_Literal) | ~icext(uri_rdfs_Datatype, D_11)))).
% 12.56/4.09 tff(c_504, plain, (ip(uri_owl_onProperty))).
% 12.56/4.09 tff(c_54, plain, (![X_7, C_8]: (iext(uri_rdf_type, X_7, C_8) | ~icext(C_8, X_7)))).
% 12.56/4.09 tff(c_70, plain, (![P_10]: (iext(uri_rdfs_subPropertyOf, P_10, uri_rdfs_member) | ~icext(uri_rdfs_ContainerMembershipProperty, P_10)))).
% 12.56/4.09 tff(c_623, plain, (ip(uri_rdfs_seeAlso))).
% 12.56/4.09 tff(c_162, plain, (![Q_32, P_31]: (ip(Q_32) | ~iext(uri_rdfs_subPropertyOf, P_31, Q_32)))).
% 12.56/4.09 tff(c_581, plain, (ip(uri_rdf__1))).
% 12.56/4.09 tff(c_613, plain, (ip(uri_rdfs_isDefinedBy))).
% 12.56/4.09 tff(c_164, plain, (![P_31, Q_32]: (ip(P_31) | ~iext(uri_rdfs_subPropertyOf, P_31, Q_32)))).
% 12.56/4.09 tff(c_583, plain, (ip(uri_rdf__3))).
% 12.56/4.09 tff(c_584, plain, (ip(uri_rdf_object))).
% 12.56/4.09 tff(c_471, plain, (ip(uri_rdfs_subClassOf))).
% 12.56/4.09 tff(c_56, plain, (![C_9]: (iext(uri_rdfs_subClassOf, C_9, uri_rdfs_Resource) | ~ic(C_9)))).
% 12.56/4.09 tff(c_587, plain, (ip(uri_rdf_first))).
% 12.56/4.09 tff(c_26, plain, (![P_6]: (ip(P_6) | ~iext(uri_rdf_type, P_6, uri_rdf_Property)))).
% 12.56/4.09 tff(c_541, plain, (ic(uri_rdf_Bag))).
% 12.56/4.09 tff(c_542, plain, (ic(uri_rdf_Alt))).
% 12.56/4.09 tff(c_543, plain, (ic(uri_rdfs_Datatype))).
% 12.56/4.09 tff(c_544, plain, (ic(uri_rdf_XMLLiteral))).
% 12.56/4.09 tff(c_150, plain, (![C_23, D_24]: (ic(C_23) | ~iext(uri_rdfs_subClassOf, C_23, D_24)))).
% 12.56/4.09 tff(c_502, plain, (ip(uri_rdfs_domain))).
% 12.56/4.09 tff(c_168, plain, (![P_37]: (iext(uri_rdfs_subPropertyOf, P_37, P_37) | ~ip(P_37)))).
% 12.56/4.09 tff(c_505, plain, (ip(uri_rdf_type))).
% 12.56/4.09 tff(c_444, plain, (ip(uri_rdfs_range))).
% 12.56/4.09 tff(c_441, plain, (ip(uri_owl_hasSelf))).
% 12.56/4.09 tff(c_2, plain, (![P_2, S_1, O_3]: (ip(P_2) | ~iext(P_2, S_1, O_3)))).
% 12.56/4.09 tff(c_180, plain, (iext(uri_owl_hasSelf, '#skF_1', literal_typed(dat_str_true, uri_xsd_boolean)))).
% 12.56/4.09 tff(c_28, plain, (![P_6]: (iext(uri_rdf_type, P_6, uri_rdf_Property) | ~ip(P_6)))).
% 12.56/4.09 tff(c_233, plain, (ic(uri_rdfs_Literal))).
% 12.56/4.09 tff(c_154, plain, (![C_27]: (iext(uri_rdfs_subClassOf, C_27, C_27) | ~ic(C_27)))).
% 12.56/4.09 tff(c_232, plain, (ic(uri_rdfs_Class))).
% 12.56/4.09 tff(c_229, plain, (ic(uri_rdf_Property))).
% 12.56/4.09 tff(c_228, plain, (ic(uri_rdfs_Container))).
% 12.56/4.09 tff(c_148, plain, (![D_24, C_23]: (ic(D_24) | ~iext(uri_rdfs_subClassOf, C_23, D_24)))).
% 12.56/4.09 tff(c_114, plain, (![X_16]: (ic(X_16) | ~icext(uri_rdfs_Class, X_16)))).
% 12.56/4.09 tff(c_112, plain, (![X_16]: (icext(uri_rdfs_Class, X_16) | ~ic(X_16)))).
% 12.56/4.09 tff(c_122, plain, (![X_18]: (lv(X_18) | ~icext(uri_rdfs_Literal, X_18)))).
% 12.56/4.09 tff(c_120, plain, (![X_18]: (icext(uri_rdfs_Literal, X_18) | ~lv(X_18)))).
% 12.56/4.09 tff(c_130, plain, (iext(uri_rdfs_range, uri_rdfs_range, uri_rdfs_Class))).
% 12.56/4.09 tff(c_44, plain, (iext(uri_rdfs_domain, uri_rdfs_label, uri_rdfs_Resource))).
% 12.56/4.09 tff(c_64, plain, (iext(uri_rdfs_range, uri_rdf_rest, uri_rdf_List))).
% 12.56/4.09 tff(c_82, plain, (iext(uri_rdfs_domain, uri_rdf__3, uri_rdfs_Resource))).
% 12.56/4.09 tff(c_74, plain, (iext(uri_rdfs_domain, uri_rdfs_member, uri_rdfs_Resource))).
% 12.56/4.09 tff(c_152, plain, (iext(uri_rdfs_range, uri_rdfs_subClassOf, uri_rdfs_Class))).
% 12.56/4.09 tff(c_100, plain, (iext(uri_rdf_type, uri_rdf_XMLLiteral, uri_rdfs_Datatype))).
% 12.56/4.09 tff(c_16, plain, (iext(uri_rdf_type, uri_rdf__2, uri_rdf_Property))).
% 12.56/4.09 tff(c_90, plain, (iext(uri_rdf_type, uri_rdf__1, uri_rdfs_ContainerMembershipProperty))).
% 12.56/4.09 tff(c_174, plain, (iext(uri_rdfs_range, uri_rdf_type, uri_rdfs_Class))).
% 12.56/4.09 tff(c_144, plain, (iext(uri_rdfs_domain, uri_rdfs_subClassOf, uri_rdfs_Class))).
% 12.56/4.09 tff(c_186, plain, (iext(uri_owl_complementOf, uri_ex_c, '#skF_1'))).
% 12.56/4.09 tff(c_124, plain, (iext(uri_rdf_type, uri_rdf_Property, uri_rdfs_Class))).
% 12.56/4.09 tff(c_96, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Seq, uri_rdfs_Container))).
% 12.56/4.09 tff(c_188, plain, (iext(uri_rdf_type, uri_ex_c, uri_owl_Class))).
% 12.56/4.09 tff(c_172, plain, (iext(uri_rdfs_domain, uri_rdf_type, uri_rdfs_Resource))).
% 12.56/4.09 tff(c_94, plain, (iext(uri_rdf_type, uri_rdf__3, uri_rdfs_ContainerMembershipProperty))).
% 12.56/4.09 tff(c_32, plain, (iext(uri_rdf_type, uri_rdf_type, uri_rdf_Property))).
% 12.56/4.09 tff(c_14, plain, (iext(uri_rdf_type, uri_rdf__1, uri_rdf_Property))).
% 12.56/4.09 tff(c_92, plain, (iext(uri_rdf_type, uri_rdf__2, uri_rdfs_ContainerMembershipProperty))).
% 12.56/4.09 tff(c_184, plain, (iext(uri_rdf_type, '#skF_1', uri_owl_Restriction))).
% 12.56/4.09 tff(c_88, plain, (iext(uri_rdfs_range, uri_rdf__3, uri_rdfs_Resource))).
% 12.56/4.09 tff(c_46, plain, (iext(uri_rdfs_range, uri_rdfs_label, uri_rdfs_Literal))).
% 12.56/4.09 tff(c_86, plain, (iext(uri_rdfs_range, uri_rdf__2, uri_rdfs_Resource))).
% 12.56/4.09 tff(c_178, plain, (iext(uri_rdfs_range, uri_rdf_value, uri_rdfs_Resource))).
% 12.56/4.09 tff(c_24, plain, (iext(uri_rdf_type, uri_rdf_subject, uri_rdf_Property))).
% 12.56/4.09 tff(c_132, plain, (iext(uri_rdfs_domain, uri_rdf_object, uri_rdfs_Statement))).
% 12.56/4.09 tff(c_72, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, uri_rdf_Property))).
% 12.56/4.09 tff(c_36, plain, (iext(uri_rdfs_range, uri_rdfs_comment, uri_rdfs_Literal))).
% 12.56/4.09 tff(c_166, plain, (iext(uri_rdfs_range, uri_rdfs_subPropertyOf, uri_rdf_Property))).
% 12.56/4.09 tff(c_48, plain, (iext(uri_rdfs_domain, uri_rdfs_seeAlso, uri_rdfs_Resource))).
% 12.56/4.09 tff(c_18, plain, (iext(uri_rdf_type, uri_rdf__3, uri_rdf_Property))).
% 12.56/4.09 tff(c_62, plain, (iext(uri_rdfs_domain, uri_rdf_rest, uri_rdf_List))).
% 12.56/4.09 tff(c_60, plain, (iext(uri_rdfs_range, uri_rdf_first, uri_rdfs_Resource))).
% 12.56/4.09 tff(c_142, plain, (iext(uri_rdfs_range, uri_rdf_subject, uri_rdfs_Resource))).
% 12.56/4.09 tff(c_40, plain, (iext(uri_rdfs_range, uri_rdfs_isDefinedBy, uri_rdfs_Resource))).
% 12.56/4.09 tff(c_68, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Bag, uri_rdfs_Container))).
% 12.56/4.09 tff(c_138, plain, (iext(uri_rdfs_range, uri_rdf_predicate, uri_rdfs_Resource))).
% 12.56/4.09 tff(c_66, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Alt, uri_rdfs_Container))).
% 12.56/4.10 tff(c_20, plain, (iext(uri_rdf_type, uri_rdf_object, uri_rdf_Property))).
% 12.56/4.10 tff(c_80, plain, (iext(uri_rdfs_domain, uri_rdf__2, uri_rdfs_Resource))).
% 12.56/4.10 tff(c_78, plain, (iext(uri_rdfs_domain, uri_rdf__1, uri_rdfs_Resource))).
% 12.56/4.10 tff(c_84, plain, (iext(uri_rdfs_range, uri_rdf__1, uri_rdfs_Resource))).
% 12.56/4.10 tff(c_38, plain, (iext(uri_rdfs_domain, uri_rdfs_isDefinedBy, uri_rdfs_Resource))).
% 12.56/4.10 tff(c_22, plain, (iext(uri_rdf_type, uri_rdf_value, uri_rdf_Property))).
% 12.56/4.10 tff(c_34, plain, (iext(uri_rdfs_domain, uri_rdfs_comment, uri_rdfs_Resource))).
% 12.56/4.10 tff(c_126, plain, (iext(uri_rdfs_domain, uri_rdfs_range, uri_rdf_Property))).
% 12.56/4.10 tff(c_110, plain, (iext(uri_rdfs_range, uri_rdfs_domain, uri_rdfs_Class))).
% 12.56/4.10 tff(c_104, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, uri_rdfs_Class))).
% 12.56/4.10 tff(c_140, plain, (iext(uri_rdfs_domain, uri_rdf_subject, uri_rdfs_Statement))).
% 12.56/4.10 tff(c_50, plain, (iext(uri_rdfs_range, uri_rdfs_seeAlso, uri_rdfs_Resource))).
% 12.56/4.10 tff(c_58, plain, (iext(uri_rdfs_domain, uri_rdf_first, uri_rdf_List))).
% 12.56/4.10 tff(c_136, plain, (iext(uri_rdfs_domain, uri_rdf_predicate, uri_rdfs_Statement))).
% 12.56/4.10 tff(c_42, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_isDefinedBy, uri_rdfs_seeAlso))).
% 12.56/4.10 tff(c_76, plain, (iext(uri_rdfs_range, uri_rdfs_member, uri_rdfs_Resource))).
% 12.56/4.10 tff(c_158, plain, (iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, uri_rdf_Property))).
% 12.56/4.10 tff(c_12, plain, (iext(uri_rdf_type, uri_rdf_rest, uri_rdf_Property))).
% 12.56/4.10 tff(c_106, plain, (iext(uri_rdfs_domain, uri_rdfs_domain, uri_rdf_Property))).
% 12.56/4.10 tff(c_176, plain, (iext(uri_rdfs_domain, uri_rdf_value, uri_rdfs_Resource))).
% 12.56/4.10 tff(c_8, plain, (iext(uri_rdf_type, uri_rdf_first, uri_rdf_Property))).
% 12.56/4.10 tff(c_182, plain, (iext(uri_owl_onProperty, '#skF_1', uri_rdf_type))).
% 12.56/4.10 tff(c_10, plain, (iext(uri_rdf_type, uri_rdf_nil, uri_rdf_List))).
% 12.56/4.10 tff(c_98, plain, (iext(uri_rdfs_subClassOf, uri_rdf_XMLLiteral, uri_rdfs_Literal))).
% 12.56/4.10 tff(c_194, plain, (![X_17]: (icext(uri_rdfs_Resource, X_17)))).
% 12.56/4.10 tff(c_4, plain, (![X_4]: (ir(X_4)))).
% 12.56/4.10 % SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p
% 12.56/4.10
%------------------------------------------------------------------------------