%------------------------------------------------------------------------------
% File : Beagle---0.9.52
% Problem : SWB014+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/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 : n012.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:50 PM UTC 2025
% Result : CounterSatisfiable 10.66s 3.78s
% Output : Assurance 0s
% Verified :
% SZS Type : -
% Comments :
%------------------------------------------------------------------------------
%----No solution output by system
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SWB014+4 : TPTP v9.0.0. Released v5.2.0.
% 0.12/0.13 % Command : java -Dfile.encoding=UTF-8 -Xms512M -Xmx4G -Xss10M -jar /export/starexec/sandbox/solver/bin/beagle.jar -auto -q -proof -print tff -smtsolver /export/starexec/sandbox/solver/bin/cvc4-1.4-x86_64-linux-opt -liasolver cooper -t %d %s
% 0.12/0.34 % Computer : n012.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 00:56:29 EDT 2025
% 0.18/0.34 % CPUTime :
% 10.66/3.77
% 10.66/3.78 % SZS status CounterSatisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p
% 10.66/3.78
% 10.66/3.78 % SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 10.66/3.78 %$ iext > icext > lv > ir > ip > ic > #nlpp > 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_unionOf > uri_ex_harry > uri_ex_Species > uri_ex_Falcon > uri_ex_Eagle > #skF_2 > #skF_3 > #skF_1
% 10.66/3.78
% 10.66/3.78 %Foreground sorts:
% 10.66/3.78
% 10.66/3.78
% 10.66/3.78 %Background operators:
% 10.66/3.78
% 10.66/3.78
% 10.66/3.78 %Foreground operators:
% 10.66/3.78 tff(uri_rdfs_Datatype, type, uri_rdfs_Datatype: $i).
% 10.66/3.78 tff(uri_ex_harry, type, uri_ex_harry: $i).
% 10.66/3.78 tff(uri_rdfs_ContainerMembershipProperty, type, uri_rdfs_ContainerMembershipProperty: $i).
% 10.66/3.78 tff(uri_rdfs_Resource, type, uri_rdfs_Resource: $i).
% 10.66/3.78 tff(uri_rdf_Property, type, uri_rdf_Property: $i).
% 10.66/3.78 tff(uri_rdf_subject, type, uri_rdf_subject: $i).
% 10.66/3.78 tff(uri_ex_Falcon, type, uri_ex_Falcon: $i).
% 10.66/3.78 tff(uri_rdf_type, type, uri_rdf_type: $i).
% 10.66/3.78 tff(uri_rdfs_subPropertyOf, type, uri_rdfs_subPropertyOf: $i).
% 10.66/3.78 tff(uri_rdfs_seeAlso, type, uri_rdfs_seeAlso: $i).
% 10.66/3.78 tff(uri_rdfs_range, type, uri_rdfs_range: $i).
% 10.66/3.78 tff(uri_rdf_XMLLiteral, type, uri_rdf_XMLLiteral: $i).
% 10.66/3.78 tff(uri_rdf_List, type, uri_rdf_List: $i).
% 10.66/3.78 tff(uri_rdf_first, type, uri_rdf_first: $i).
% 10.66/3.78 tff(uri_rdf_predicate, type, uri_rdf_predicate: $i).
% 10.66/3.78 tff(uri_rdf__3, type, uri_rdf__3: $i).
% 10.66/3.78 tff(icext, type, icext: ($i * $i) > $o).
% 10.66/3.78 tff(uri_ex_Eagle, type, uri_ex_Eagle: $i).
% 10.66/3.78 tff(uri_rdf_value, type, uri_rdf_value: $i).
% 10.66/3.78 tff(ip, type, ip: $i > $o).
% 10.66/3.78 tff(uri_rdfs_Statement, type, uri_rdfs_Statement: $i).
% 10.66/3.78 tff(uri_rdf__1, type, uri_rdf__1: $i).
% 10.66/3.78 tff(lv, type, lv: $i > $o).
% 10.66/3.78 tff(ir, type, ir: $i > $o).
% 10.66/3.78 tff(uri_owl_unionOf, type, uri_owl_unionOf: $i).
% 10.66/3.78 tff(uri_rdf_rest, type, uri_rdf_rest: $i).
% 10.66/3.78 tff(uri_rdfs_label, type, uri_rdfs_label: $i).
% 10.66/3.78 tff(uri_ex_Species, type, uri_ex_Species: $i).
% 10.66/3.78 tff(uri_rdfs_Container, type, uri_rdfs_Container: $i).
% 10.66/3.78 tff(ic, type, ic: $i > $o).
% 10.66/3.78 tff('#skF_2', type, '#skF_2': $i).
% 10.66/3.78 tff('#skF_3', type, '#skF_3': $i).
% 10.66/3.78 tff('#skF_1', type, '#skF_1': $i).
% 10.66/3.78 tff(uri_rdfs_subClassOf, type, uri_rdfs_subClassOf: $i).
% 10.66/3.78 tff(uri_rdf_object, type, uri_rdf_object: $i).
% 10.66/3.78 tff(uri_rdfs_Class, type, uri_rdfs_Class: $i).
% 10.66/3.78 tff(uri_rdfs_Seq, type, uri_rdfs_Seq: $i).
% 10.66/3.78 tff(iext, type, iext: ($i * $i * $i) > $o).
% 10.66/3.78 tff(uri_rdfs_member, type, uri_rdfs_member: $i).
% 10.66/3.78 tff(uri_rdf_Bag, type, uri_rdf_Bag: $i).
% 10.66/3.78 tff(uri_rdf__2, type, uri_rdf__2: $i).
% 10.66/3.78 tff(uri_rdfs_comment, type, uri_rdfs_comment: $i).
% 10.66/3.78 tff(uri_rdfs_Literal, type, uri_rdfs_Literal: $i).
% 10.66/3.78 tff(uri_rdf_Alt, type, uri_rdf_Alt: $i).
% 10.66/3.78 tff(uri_rdf_nil, type, uri_rdf_nil: $i).
% 10.66/3.78 tff(uri_rdfs_isDefinedBy, type, uri_rdfs_isDefinedBy: $i).
% 10.66/3.78 tff(uri_rdfs_domain, type, uri_rdfs_domain: $i).
% 10.66/3.78
% 10.66/3.78 %Saturated clause set:
% 10.66/3.79 tff(c_7547, plain, (![C_28, C_359]: (iext(uri_rdfs_subClassOf, C_28, uri_rdfs_Resource) | ~iext(uri_rdfs_subClassOf, C_28, C_359) | ~iext(uri_rdfs_subClassOf, C_359, uri_rdfs_Datatype)))).
% 10.66/3.79 tff(c_7906, plain, (![Q_32, C_364]: (iext(Q_32, C_364, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_32) | ~iext(uri_rdfs_subClassOf, C_364, uri_rdfs_ContainerMembershipProperty)))).
% 10.66/3.79 tff(c_7907, plain, (![C_28, C_364]: (iext(uri_rdfs_subClassOf, C_28, uri_rdfs_Resource) | ~iext(uri_rdfs_subClassOf, C_28, C_364) | ~iext(uri_rdfs_subClassOf, C_364, uri_rdfs_ContainerMembershipProperty)))).
% 10.66/3.79 tff(c_7546, plain, (![Q_32, C_359]: (iext(Q_32, C_359, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_32) | ~iext(uri_rdfs_subClassOf, C_359, uri_rdfs_Datatype)))).
% 10.66/3.79 tff(c_6877, plain, (![C_28, C_354]: (iext(uri_rdfs_subClassOf, C_28, uri_rdfs_Resource) | ~iext(uri_rdfs_subClassOf, C_28, C_354) | ~iext(uri_rdfs_subClassOf, C_354, uri_rdf_Bag)))).
% 10.66/3.79 tff(c_7193, plain, (![C_28, C_355]: (iext(uri_rdfs_subClassOf, C_28, uri_rdfs_Resource) | ~iext(uri_rdfs_subClassOf, C_28, C_355) | ~iext(uri_rdfs_subClassOf, C_355, uri_rdf_XMLLiteral)))).
% 10.66/3.79 tff(c_7192, plain, (![Q_32, C_355]: (iext(Q_32, C_355, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_32) | ~iext(uri_rdfs_subClassOf, C_355, uri_rdf_XMLLiteral)))).
% 10.66/3.79 tff(c_6546, plain, (![C_28, C_351]: (iext(uri_rdfs_subClassOf, C_28, uri_rdfs_Resource) | ~iext(uri_rdfs_subClassOf, C_28, C_351) | ~iext(uri_rdfs_subClassOf, C_351, uri_rdf_Alt)))).
% 10.66/3.79 tff(c_6876, plain, (![Q_32, C_354]: (iext(Q_32, C_354, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_32) | ~iext(uri_rdfs_subClassOf, C_354, uri_rdf_Bag)))).
% 10.66/3.79 tff(c_6545, plain, (![Q_32, C_351]: (iext(Q_32, C_351, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_32) | ~iext(uri_rdfs_subClassOf, C_351, uri_rdf_Alt)))).
% 10.66/3.79 tff(c_2846, plain, (![Q_32, C_206]: (iext(Q_32, C_206, uri_rdfs_Container) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_32) | ~iext(uri_rdfs_subClassOf, C_206, uri_rdf_Bag)))).
% 10.66/3.79 tff(c_2847, plain, (![C_28, C_206]: (iext(uri_rdfs_subClassOf, C_28, uri_rdfs_Container) | ~iext(uri_rdfs_subClassOf, C_28, C_206) | ~iext(uri_rdfs_subClassOf, C_206, uri_rdf_Bag)))).
% 10.66/3.79 tff(c_3217, plain, (![C_28, C_217]: (iext(uri_rdfs_subClassOf, C_28, uri_rdfs_Container) | ~iext(uri_rdfs_subClassOf, C_28, C_217) | ~iext(uri_rdfs_subClassOf, C_217, uri_rdf_Alt)))).
% 10.66/3.79 tff(c_3216, plain, (![Q_32, C_217]: (iext(Q_32, C_217, uri_rdfs_Container) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_32) | ~iext(uri_rdfs_subClassOf, C_217, uri_rdf_Alt)))).
% 10.66/3.79 tff(c_8273, plain, (~iext(uri_rdfs_subClassOf, uri_rdfs_Container, uri_rdf_XMLLiteral))).
% 10.66/3.79 tff(c_4021, plain, (![Q_32, P_246]: (iext(Q_32, P_246, uri_rdfs_seeAlso) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_32) | ~iext(uri_rdfs_subPropertyOf, P_246, uri_rdfs_isDefinedBy)))).
% 10.66/3.79 tff(c_4606, plain, (![C_28, C_268]: (iext(uri_rdfs_subClassOf, C_28, uri_rdfs_Literal) | ~iext(uri_rdfs_subClassOf, C_28, C_268) | ~iext(uri_rdfs_subClassOf, C_268, uri_rdf_XMLLiteral)))).
% 10.66/3.79 tff(c_8182, plain, (~iext(uri_rdfs_subPropertyOf, uri_rdfs_member, uri_rdfs_isDefinedBy))).
% 10.66/3.79 tff(c_4022, plain, (![P_38, P_246]: (iext(uri_rdfs_subPropertyOf, P_38, uri_rdfs_seeAlso) | ~iext(uri_rdfs_subPropertyOf, P_38, P_246) | ~iext(uri_rdfs_subPropertyOf, P_246, uri_rdfs_isDefinedBy)))).
% 10.66/3.79 tff(c_4605, plain, (![Q_32, C_268]: (iext(Q_32, C_268, uri_rdfs_Literal) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_32) | ~iext(uri_rdfs_subClassOf, C_268, uri_rdf_XMLLiteral)))).
% 10.66/3.79 tff(c_6230, plain, (![C_28, D_350]: (iext(uri_rdfs_subClassOf, C_28, uri_rdfs_Resource) | ~iext(uri_rdfs_subClassOf, C_28, D_350) | ~icext(uri_rdfs_Datatype, D_350)))).
% 10.66/3.79 tff(c_6229, plain, (![Q_32, D_350]: (iext(Q_32, D_350, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_32) | ~icext(uri_rdfs_Datatype, D_350)))).
% 10.66/3.79 tff(c_1541, plain, (![Q_90, X_7, C_8]: (iext(Q_90, X_7, C_8) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_90) | ~icext(C_8, X_7)))).
% 10.66/3.79 tff(c_1540, plain, (![Q_90, D_11]: (iext(Q_90, D_11, uri_rdfs_Literal) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_90) | ~icext(uri_rdfs_Datatype, D_11)))).
% 10.66/3.79 tff(c_8022, plain, (~icext(uri_rdfs_Datatype, uri_rdfs_Container))).
% 10.66/3.79 tff(c_1344, plain, (![C_84, D_11]: (iext(uri_rdfs_subClassOf, C_84, uri_rdfs_Literal) | ~iext(uri_rdfs_subClassOf, C_84, D_11) | ~icext(uri_rdfs_Datatype, D_11)))).
% 10.66/3.79 tff(c_7931, plain, (~iext(uri_rdfs_subClassOf, uri_rdfs_Literal, uri_rdf_Alt))).
% 10.66/3.79 tff(c_1539, plain, (![Q_90, P_10]: (iext(Q_90, P_10, uri_rdfs_member) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_90) | ~icext(uri_rdfs_ContainerMembershipProperty, P_10)))).
% 10.66/3.79 tff(c_7930, plain, (~iext(uri_rdfs_subClassOf, uri_rdfs_Literal, uri_rdf_Bag))).
% 10.66/3.79 tff(c_5754, plain, (![Q_32]: (iext(Q_32, uri_rdfs_Datatype, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_32)))).
% 10.66/3.79 tff(c_5913, plain, (![C_28]: (iext(uri_rdfs_subClassOf, C_28, uri_rdfs_Resource) | ~iext(uri_rdfs_subClassOf, C_28, uri_rdfs_ContainerMembershipProperty)))).
% 10.66/3.79 tff(c_5717, plain, (![Q_32]: (iext(Q_32, uri_rdf_Bag, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_32)))).
% 10.66/3.79 tff(c_7583, plain, (~icext(uri_rdfs_ContainerMembershipProperty, uri_rdfs_seeAlso))).
% 10.66/3.79 tff(c_1369, 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)))).
% 10.66/3.79 tff(c_5865, plain, (![Q_32]: (iext(Q_32, uri_rdfs_Seq, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_32)))).
% 10.66/3.79 tff(c_5755, plain, (![C_28]: (iext(uri_rdfs_subClassOf, C_28, uri_rdfs_Resource) | ~iext(uri_rdfs_subClassOf, C_28, uri_rdfs_Datatype)))).
% 10.66/3.79 tff(c_5912, plain, (![Q_32]: (iext(Q_32, uri_rdfs_ContainerMembershipProperty, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_32)))).
% 10.66/3.79 tff(c_5833, plain, (![Q_32]: (iext(Q_32, uri_rdf_Alt, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_32)))).
% 10.66/3.79 tff(c_5866, plain, (![C_28]: (iext(uri_rdfs_subClassOf, C_28, uri_rdfs_Resource) | ~iext(uri_rdfs_subClassOf, C_28, uri_rdfs_Seq)))).
% 10.66/3.80 tff(c_5663, plain, (![C_84]: (iext(uri_rdfs_subClassOf, C_84, uri_rdfs_Resource) | ~iext(uri_rdfs_subClassOf, C_84, uri_rdf_XMLLiteral)))).
% 10.66/3.80 tff(c_5669, plain, (![C_84]: (iext(uri_rdfs_subClassOf, C_84, uri_rdfs_Resource) | ~iext(uri_rdfs_subClassOf, C_84, uri_rdf_Bag)))).
% 10.66/3.80 tff(c_1543, plain, (![Q_90, C_9]: (iext(Q_90, C_9, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_90) | ~ic(C_9)))).
% 10.66/3.80 tff(c_5666, plain, (![C_84]: (iext(uri_rdfs_subClassOf, C_84, uri_rdfs_Resource) | ~iext(uri_rdfs_subClassOf, C_84, uri_rdf_Alt)))).
% 10.66/3.80 tff(c_5672, plain, (![D_11]: (iext(uri_rdfs_subClassOf, D_11, uri_rdfs_Resource) | ~icext(uri_rdfs_Datatype, D_11)))).
% 10.66/3.80 tff(c_5688, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, uri_rdfs_Resource))).
% 10.66/3.80 tff(c_5691, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Seq, uri_rdfs_Resource))).
% 10.66/3.80 tff(c_5685, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Alt, uri_rdfs_Resource))).
% 10.66/3.80 tff(c_5786, plain, (![Q_32]: (iext(Q_32, uri_rdf_XMLLiteral, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_32)))).
% 10.66/3.80 tff(c_5682, plain, (iext(uri_rdfs_subClassOf, uri_rdf_XMLLiteral, uri_rdfs_Resource))).
% 10.66/3.80 tff(c_5694, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, uri_rdfs_Resource))).
% 10.66/3.80 tff(c_5679, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Bag, uri_rdfs_Resource))).
% 10.66/3.80 tff(c_1346, plain, (![C_84, C_9]: (iext(uri_rdfs_subClassOf, C_84, uri_rdfs_Resource) | ~iext(uri_rdfs_subClassOf, C_84, C_9) | ~ic(C_9)))).
% 10.66/3.80 tff(c_5620, plain, (~iext(uri_rdfs_subPropertyOf, uri_owl_unionOf, uri_rdfs_isDefinedBy))).
% 10.66/3.80 tff(c_1544, plain, (![Q_90, P_6]: (iext(Q_90, P_6, uri_rdf_Property) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_90) | ~ip(P_6)))).
% 10.66/3.80 tff(c_5613, plain, (![C_75]: (icext(C_75, uri_rdfs_member) | ~iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_75)))).
% 10.66/3.80 tff(c_1245, plain, (![C_79, X_7, C_8]: (icext(C_79, X_7) | ~iext(uri_rdfs_domain, uri_rdf_type, C_79) | ~icext(C_8, X_7)))).
% 10.66/3.80 tff(c_5586, plain, (![P_339]: (icext(uri_rdf_Property, P_339) | ~icext(uri_rdfs_ContainerMembershipProperty, P_339)))).
% 10.66/3.80 tff(c_5582, plain, (~iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, uri_rdfs_isDefinedBy))).
% 10.66/3.80 tff(c_1243, plain, (![C_79, P_10]: (icext(C_79, P_10) | ~iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_79) | ~icext(uri_rdfs_ContainerMembershipProperty, P_10)))).
% 10.66/3.80 tff(c_5575, plain, (![D_336]: (icext(uri_rdfs_Class, D_336) | ~icext(uri_rdfs_Datatype, D_336)))).
% 10.66/3.80 tff(c_1244, plain, (![C_79, D_11]: (icext(C_79, D_11) | ~iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_79) | ~icext(uri_rdfs_Datatype, D_11)))).
% 10.66/3.80 tff(c_5378, plain, (![C_331, X_332]: (icext(uri_rdfs_Class, C_331) | ~icext(C_331, X_332)))).
% 10.66/3.80 tff(c_1014, plain, (![C_75, C_8, X_7]: (icext(C_75, C_8) | ~iext(uri_rdfs_range, uri_rdf_type, C_75) | ~icext(C_8, X_7)))).
% 10.66/3.80 tff(c_1545, plain, (![Q_90, P_37]: (iext(Q_90, P_37, P_37) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_90) | ~ip(P_37)))).
% 10.66/3.80 tff(c_1663, plain, (![D_24, P_95]: (icext(D_24, P_95) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24) | ~ip(P_95)))).
% 10.66/3.80 tff(c_1542, plain, (![Q_90, C_27]: (iext(Q_90, C_27, C_27) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_90) | ~ic(C_27)))).
% 10.66/3.80 tff(c_1015, plain, (![C_75, C_27]: (icext(C_75, C_27) | ~iext(uri_rdfs_range, uri_rdfs_subClassOf, C_75) | ~ic(C_27)))).
% 10.66/3.80 tff(c_1248, plain, (![C_79, P_6]: (icext(C_79, P_6) | ~iext(uri_rdfs_domain, uri_rdf_type, C_79) | ~ip(P_6)))).
% 10.66/3.80 tff(c_5306, plain, (~iext(uri_rdfs_subPropertyOf, uri_rdf_rest, uri_rdfs_isDefinedBy))).
% 10.66/3.80 tff(c_853, plain, (![D_72, X_18]: (icext(D_72, X_18) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Literal, D_72) | ~lv(X_18)))).
% 10.66/3.80 tff(c_5270, plain, (![C_75]: (icext(C_75, uri_rdfs_Resource) | ~iext(uri_rdfs_range, uri_rdfs_subClassOf, C_75)))).
% 10.66/3.80 tff(c_5219, plain, (~iext(uri_rdfs_subPropertyOf, uri_rdf_type, uri_rdfs_isDefinedBy))).
% 10.66/3.80 tff(c_852, plain, (![D_72, X_16]: (icext(D_72, X_16) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_72) | ~ic(X_16)))).
% 10.66/3.80 tff(c_1246, plain, (![C_79, C_27]: (icext(C_79, C_27) | ~iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_79) | ~ic(C_27)))).
% 10.66/3.80 tff(c_5214, plain, (~iext(uri_rdfs_subPropertyOf, uri_rdf_first, uri_rdfs_isDefinedBy))).
% 10.66/3.80 tff(c_5209, plain, (~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, uri_rdfs_isDefinedBy))).
% 10.66/3.80 tff(c_1249, plain, (![C_79, P_37]: (icext(C_79, P_37) | ~iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_79) | ~ip(P_37)))).
% 10.66/3.80 tff(c_5208, plain, (~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, uri_rdfs_isDefinedBy))).
% 10.66/3.80 tff(c_1018, plain, (![C_75, P_37]: (icext(C_75, P_37) | ~iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_75) | ~ip(P_37)))).
% 10.66/3.80 tff(c_5203, plain, (~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, uri_rdfs_isDefinedBy))).
% 10.66/3.80 tff(c_1588, plain, (![Q_90]: (iext(Q_90, uri_rdfs_domain, uri_rdfs_Class) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_90)))).
% 10.66/3.80 tff(c_1566, plain, (![Q_90]: (iext(Q_90, uri_rdfs_range, uri_rdfs_Class) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_90)))).
% 10.66/3.80 tff(c_1608, plain, (![Q_90]: (iext(Q_90, '#skF_3', uri_ex_Falcon) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_first, Q_90)))).
% 10.66/3.80 tff(c_1599, plain, (![Q_90]: (iext(Q_90, '#skF_3', uri_rdf_nil) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_rest, Q_90)))).
% 10.66/3.80 tff(c_1598, plain, (![Q_90]: (iext(Q_90, uri_rdfs_Seq, uri_rdfs_Container) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_90)))).
% 10.66/3.80 tff(c_1587, plain, (![Q_90]: (iext(Q_90, uri_rdfs_label, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_90)))).
% 10.66/3.80 tff(c_1556, plain, (![Q_90]: (iext(Q_90, uri_rdfs_domain, uri_rdf_Property) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_90)))).
% 10.66/3.80 tff(c_1597, plain, (![Q_90]: (iext(Q_90, uri_rdfs_isDefinedBy, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_90)))).
% 10.66/3.80 tff(c_1558, plain, (![Q_90]: (iext(Q_90, uri_rdf__2, uri_rdf_Property) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_90)))).
% 10.66/3.80 tff(c_1549, plain, (![Q_90]: (iext(Q_90, uri_rdf_Bag, uri_rdfs_Container) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_90)))).
% 10.66/3.80 tff(c_1563, plain, (![Q_90]: (iext(Q_90, uri_rdfs_subClassOf, uri_rdfs_Class) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_90)))).
% 10.66/3.80 tff(c_1581, plain, (![Q_90]: (iext(Q_90, uri_rdf_predicate, uri_rdfs_Statement) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_90)))).
% 10.66/3.80 tff(c_1557, plain, (![Q_90]: (iext(Q_90, uri_rdf_nil, uri_rdf_List) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_90)))).
% 10.66/3.80 tff(c_1550, plain, (![Q_90]: (iext(Q_90, uri_rdf_type, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_90)))).
% 10.66/3.80 tff(c_1605, plain, (![Q_90]: (iext(Q_90, uri_rdf__1, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_90)))).
% 10.66/3.80 tff(c_1589, plain, (![Q_90]: (iext(Q_90, uri_rdfs_seeAlso, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_90)))).
% 10.66/3.80 tff(c_4954, plain, (~icext(uri_rdfs_ContainerMembershipProperty, uri_rdf_rest))).
% 10.66/3.80 tff(c_1352, plain, (![C_84]: (iext(uri_rdfs_subClassOf, C_84, uri_rdfs_Class) | ~iext(uri_rdfs_subClassOf, C_84, uri_rdfs_Datatype)))).
% 10.66/3.80 tff(c_1579, plain, (![Q_90]: (iext(Q_90, '#skF_2', '#skF_3') | ~iext(uri_rdfs_subPropertyOf, uri_rdf_rest, Q_90)))).
% 10.66/3.80 tff(c_1603, plain, (![Q_90]: (iext(Q_90, uri_ex_Eagle, uri_ex_Species) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_90)))).
% 10.66/3.80 tff(c_1591, plain, (![Q_90]: (iext(Q_90, uri_rdfs_member, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_90)))).
% 10.66/3.80 tff(c_1568, plain, (![Q_90]: (iext(Q_90, uri_rdf_type, uri_rdf_Property) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_90)))).
% 10.66/3.80 tff(c_1600, plain, (![Q_90]: (iext(Q_90, uri_rdf_subject, uri_rdfs_Statement) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_90)))).
% 10.66/3.80 tff(c_1555, plain, (![Q_90]: (iext(Q_90, uri_rdf__3, uri_rdf_Property) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_90)))).
% 10.66/3.81 tff(c_1560, plain, (![Q_90]: (iext(Q_90, uri_ex_harry, '#skF_1') | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_90)))).
% 10.66/3.81 tff(c_1583, plain, (![Q_90]: (iext(Q_90, uri_rdfs_ContainerMembershipProperty, uri_rdf_Property) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_90)))).
% 10.66/3.81 tff(c_1570, plain, (![Q_90]: (iext(Q_90, uri_rdf__1, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_90)))).
% 10.66/3.81 tff(c_1580, plain, (![Q_90]: (iext(Q_90, uri_rdf__3, uri_rdfs_ContainerMembershipProperty) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_90)))).
% 10.66/3.81 tff(c_1611, plain, (![Q_90]: (iext(Q_90, uri_rdfs_Datatype, uri_rdfs_Class) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_90)))).
% 10.66/3.81 tff(c_1574, plain, (![Q_90]: (iext(Q_90, uri_rdf_rest, uri_rdf_List) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_90)))).
% 10.66/3.81 tff(c_1552, plain, (![Q_90]: (iext(Q_90, uri_rdf_XMLLiteral, uri_rdfs_Literal) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_90)))).
% 10.66/3.81 tff(c_4758, plain, (~icext(uri_rdfs_ContainerMembershipProperty, uri_rdfs_subClassOf))).
% 10.66/3.81 tff(c_1573, plain, (![Q_90]: (iext(Q_90, uri_rdf_Alt, uri_rdfs_Container) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_90)))).
% 10.66/3.81 tff(c_1590, plain, (![Q_90]: (iext(Q_90, uri_rdfs_comment, uri_rdfs_Literal) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_90)))).
% 10.66/3.81 tff(c_1586, plain, (![Q_90]: (iext(Q_90, uri_rdf_type, uri_rdfs_Class) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_90)))).
% 10.66/3.81 tff(c_1612, plain, (![Q_90]: (iext(Q_90, uri_rdfs_subClassOf, uri_rdfs_Class) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_90)))).
% 10.66/3.81 tff(c_4697, plain, (~iext(uri_rdfs_subClassOf, '#skF_1', uri_rdf_XMLLiteral))).
% 10.66/3.81 tff(c_1595, plain, (![Q_90]: (iext(Q_90, uri_rdf_first, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_90)))).
% 10.66/3.81 tff(c_4681, plain, (~iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, uri_rdf_XMLLiteral))).
% 10.66/3.81 tff(c_1351, plain, (![C_84]: (iext(uri_rdfs_subClassOf, C_84, uri_rdfs_Container) | ~iext(uri_rdfs_subClassOf, C_84, uri_rdfs_Seq)))).
% 10.66/3.81 tff(c_4672, plain, (~iext(uri_rdfs_subClassOf, uri_rdfs_Class, uri_rdf_XMLLiteral))).
% 10.66/3.81 tff(c_1559, plain, (![Q_90]: (iext(Q_90, uri_rdf_rest, uri_rdf_List) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_90)))).
% 10.66/3.81 tff(c_4656, plain, (~iext(uri_rdfs_subClassOf, uri_rdf_List, uri_rdf_XMLLiteral))).
% 10.66/3.81 tff(c_1548, plain, (![Q_90]: (iext(Q_90, uri_rdf_subject, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_90)))).
% 10.66/3.81 tff(c_4632, plain, (~iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, uri_rdf_XMLLiteral))).
% 10.66/3.81 tff(c_1350, plain, (![C_84]: (iext(uri_rdfs_subClassOf, C_84, uri_rdf_Property) | ~iext(uri_rdfs_subClassOf, C_84, uri_rdfs_ContainerMembershipProperty)))).
% 10.66/3.81 tff(c_4631, plain, (~iext(uri_rdfs_subClassOf, uri_rdf_Property, uri_rdf_XMLLiteral))).
% 10.66/3.81 tff(c_4615, plain, (~iext(uri_rdfs_subClassOf, uri_ex_Species, uri_rdf_XMLLiteral))).
% 10.66/3.81 tff(c_1594, plain, (![Q_90]: (iext(Q_90, uri_rdfs_seeAlso, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_90)))).
% 10.66/3.81 tff(c_4614, plain, (~iext(uri_rdfs_subClassOf, uri_rdfs_Resource, uri_rdf_XMLLiteral))).
% 10.66/3.81 tff(c_1348, plain, (![C_84]: (iext(uri_rdfs_subClassOf, C_84, uri_rdfs_Literal) | ~iext(uri_rdfs_subClassOf, C_84, uri_rdf_XMLLiteral)))).
% 10.66/3.81 tff(c_1567, plain, (![Q_90]: (iext(Q_90, uri_ex_Falcon, uri_ex_Species) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_90)))).
% 10.66/3.81 tff(c_1572, plain, (![Q_90]: (iext(Q_90, uri_rdf_XMLLiteral, uri_rdfs_Datatype) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_90)))).
% 10.66/3.81 tff(c_1562, plain, (![Q_90]: (iext(Q_90, uri_rdf_object, uri_rdfs_Statement) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_90)))).
% 10.66/3.81 tff(c_1561, plain, (![Q_90]: (iext(Q_90, uri_rdf_value, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_90)))).
% 10.66/3.81 tff(c_4302, plain, (~icext(uri_rdfs_ContainerMembershipProperty, uri_owl_unionOf))).
% 10.66/3.81 tff(c_1610, plain, (![Q_90]: (iext(Q_90, '#skF_1', '#skF_2') | ~iext(uri_rdfs_subPropertyOf, uri_owl_unionOf, Q_90)))).
% 10.66/3.81 tff(c_1592, plain, (![Q_90]: (iext(Q_90, uri_rdfs_label, uri_rdfs_Literal) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_90)))).
% 10.66/3.81 tff(c_1593, plain, (![Q_90]: (iext(Q_90, uri_rdf_predicate, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_90)))).
% 10.66/3.81 tff(c_1601, plain, (![Q_90]: (iext(Q_90, uri_rdf_Property, uri_rdfs_Class) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_90)))).
% 10.66/3.81 tff(c_1584, plain, (![Q_90]: (iext(Q_90, uri_rdf__3, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_90)))).
% 10.66/3.81 tff(c_1602, plain, (![Q_90]: (iext(Q_90, uri_rdf_object, uri_rdf_Property) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_90)))).
% 10.66/3.81 tff(c_1546, plain, (![Q_90]: (iext(Q_90, uri_rdf_value, uri_rdf_Property) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_90)))).
% 10.66/3.81 tff(c_4196, plain, (~icext(uri_rdfs_ContainerMembershipProperty, uri_rdf_first))).
% 10.66/3.81 tff(c_1564, plain, (![Q_90]: (iext(Q_90, '#skF_2', uri_ex_Eagle) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_first, Q_90)))).
% 10.66/3.81 tff(c_1604, plain, (![Q_90]: (iext(Q_90, uri_rdf_first, uri_rdf_List) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_90)))).
% 10.66/3.81 tff(c_1553, plain, (![Q_90]: (iext(Q_90, uri_rdf__1, uri_rdf_Property) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_90)))).
% 10.66/3.81 tff(c_1606, plain, (![Q_90]: (iext(Q_90, uri_rdf_rest, uri_rdf_Property) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_90)))).
% 10.66/3.81 tff(c_1576, plain, (![Q_90]: (iext(Q_90, uri_rdfs_range, uri_rdf_Property) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_90)))).
% 10.66/3.81 tff(c_1585, plain, (![Q_90]: (iext(Q_90, uri_rdf__2, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_90)))).
% 10.66/3.81 tff(c_1596, plain, (![Q_90]: (iext(Q_90, uri_rdfs_isDefinedBy, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_90)))).
% 10.66/3.81 tff(c_4090, plain, (~icext(uri_rdfs_ContainerMembershipProperty, uri_rdfs_subPropertyOf))).
% 10.66/3.81 tff(c_1571, plain, (![Q_90]: (iext(Q_90, uri_rdfs_isDefinedBy, uri_rdfs_seeAlso) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_90)))).
% 10.66/3.81 tff(c_1582, plain, (![Q_90]: (iext(Q_90, uri_rdf__1, uri_rdfs_ContainerMembershipProperty) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_90)))).
% 10.66/3.81 tff(c_1989, plain, (![D_24]: (icext(D_24, '#skF_2') | ~iext(uri_rdfs_subClassOf, uri_rdf_List, D_24)))).
% 10.66/3.81 tff(c_1371, plain, (![P_87]: (iext(uri_rdfs_subPropertyOf, P_87, uri_rdfs_seeAlso) | ~iext(uri_rdfs_subPropertyOf, P_87, uri_rdfs_isDefinedBy)))).
% 10.66/3.81 tff(c_1834, plain, (![D_24]: (icext(D_24, uri_rdfs_Container) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_24)))).
% 10.66/3.81 tff(c_2027, plain, (![D_24]: (icext(D_24, uri_rdfs_range) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))).
% 10.66/3.81 tff(c_1975, plain, (![D_24]: (icext(D_24, '#skF_3') | ~iext(uri_rdfs_subClassOf, uri_rdf_List, D_24)))).
% 10.66/3.81 tff(c_1914, plain, (![D_24]: (icext(D_24, '#skF_1') | ~iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_24)))).
% 10.66/3.81 tff(c_2114, plain, (![D_24]: (icext(D_24, uri_rdfs_seeAlso) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))).
% 10.66/3.81 tff(c_1783, plain, (![D_24]: (icext(D_24, uri_rdf_Bag) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_24)))).
% 10.66/3.81 tff(c_1886, plain, (![D_24]: (icext(D_24, uri_rdfs_domain) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))).
% 10.66/3.81 tff(c_1578, plain, (![Q_90]: (iext(Q_90, uri_rdf__2, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_90)))).
% 10.66/3.81 tff(c_1865, plain, (![D_24]: (icext(D_24, uri_rdfs_ContainerMembershipProperty) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_24)))).
% 10.83/3.81 tff(c_2093, plain, (![D_24]: (icext(D_24, uri_rdfs_Seq) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_24)))).
% 10.83/3.81 tff(c_3681, plain, (~iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, uri_rdf_Bag))).
% 10.83/3.81 tff(c_1752, plain, (![D_24]: (icext(D_24, uri_rdfs_Resource) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_24)))).
% 10.83/3.81 tff(c_2044, plain, (![D_24]: (icext(D_24, uri_rdf_XMLLiteral) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_24)))).
% 10.83/3.81 tff(c_2075, plain, (![D_24]: (icext(D_24, uri_ex_Species) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_24)))).
% 10.83/3.81 tff(c_1569, plain, (![Q_90]: (iext(Q_90, uri_rdf__3, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_90)))).
% 10.83/3.81 tff(c_3579, plain, (~iext(uri_rdfs_subClassOf, uri_rdfs_Class, uri_rdf_Alt))).
% 10.83/3.81 tff(c_3548, plain, (~iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, uri_rdf_Alt))).
% 10.83/3.81 tff(c_2008, plain, (![D_24]: (icext(D_24, uri_rdfs_member) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))).
% 10.83/3.81 tff(c_1551, plain, (![Q_90]: (iext(Q_90, uri_rdf__2, uri_rdfs_ContainerMembershipProperty) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_90)))).
% 10.83/3.81 tff(c_3536, plain, (~iext(uri_rdfs_subClassOf, '#skF_1', uri_rdf_Alt))).
% 10.83/3.81 tff(c_3535, plain, (~iext(uri_rdfs_subClassOf, uri_rdf_List, uri_rdf_Alt))).
% 10.83/3.81 tff(c_2137, plain, (![D_24]: (icext(D_24, uri_rdf_Alt) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_24)))).
% 10.83/3.81 tff(c_1554, plain, (![Q_90]: (iext(Q_90, uri_rdfs_subPropertyOf, uri_rdf_Property) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_90)))).
% 10.83/3.81 tff(c_3493, plain, (~iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, uri_rdf_Alt))).
% 10.83/3.81 tff(c_1959, plain, (![D_24]: (icext(D_24, uri_rdfs_Class) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_24)))).
% 10.83/3.81 tff(c_1766, plain, (![D_24]: (icext(D_24, uri_rdf_predicate) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))).
% 10.83/3.81 tff(c_3432, plain, (~icext(uri_rdfs_ContainerMembershipProperty, uri_rdfs_range))).
% 10.83/3.82 tff(c_1607, plain, (![Q_90]: (iext(Q_90, uri_rdf_value, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_90)))).
% 10.83/3.82 tff(c_3420, plain, (~iext(uri_rdfs_subClassOf, '#skF_1', uri_rdf_Bag))).
% 10.83/3.82 tff(c_3419, plain, (~iext(uri_rdfs_subClassOf, uri_ex_Species, uri_rdf_Alt))).
% 10.83/3.82 tff(c_1821, plain, (![D_24]: (icext(D_24, uri_rdfs_Datatype) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_24)))).
% 10.83/3.82 tff(c_1796, plain, (![D_24]: (icext(D_24, uri_rdf_List) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_24)))).
% 10.83/3.82 tff(c_1810, plain, (![D_24]: (icext(D_24, uri_rdfs_isDefinedBy) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))).
% 10.83/3.82 tff(c_1575, plain, (![Q_90]: (iext(Q_90, uri_rdfs_subPropertyOf, uri_rdf_Property) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_90)))).
% 10.83/3.82 tff(c_3317, plain, (~iext(uri_rdfs_subClassOf, uri_rdf_Property, uri_rdf_Alt))).
% 10.83/3.82 tff(c_1927, plain, (![D_24]: (icext(D_24, uri_rdfs_Literal) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_24)))).
% 10.83/3.82 tff(c_2176, plain, (![D_24]: (icext(D_24, uri_rdfs_subPropertyOf) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))).
% 10.83/3.82 tff(c_3226, plain, (~iext(uri_rdfs_subClassOf, uri_ex_Species, uri_rdf_Bag))).
% 10.83/3.82 tff(c_2351, plain, (![D_24]: (icext(D_24, uri_rdfs_comment) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))).
% 10.83/3.82 tff(c_3225, plain, (~iext(uri_rdfs_subClassOf, uri_rdfs_Resource, uri_rdf_Alt))).
% 10.83/3.82 tff(c_1349, plain, (![C_84]: (iext(uri_rdfs_subClassOf, C_84, uri_rdfs_Container) | ~iext(uri_rdfs_subClassOf, C_84, uri_rdf_Alt)))).
% 10.83/3.82 tff(c_3088, plain, (~iext(uri_rdfs_subClassOf, uri_rdfs_Class, uri_rdf_Bag))).
% 10.83/3.82 tff(c_2248, plain, (![D_24]: (icext(D_24, uri_rdfs_label) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))).
% 10.83/3.82 tff(c_2314, plain, (![D_24]: (icext(D_24, uri_rdfs_Statement) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_24)))).
% 10.83/3.82 tff(c_3026, plain, (~iext(uri_rdfs_subClassOf, uri_rdf_List, uri_rdf_Bag))).
% 10.83/3.82 tff(c_1547, plain, (![Q_90]: (iext(Q_90, uri_rdf_subject, uri_rdf_Property) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_90)))).
% 10.83/3.82 tff(c_3025, plain, (~iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, uri_rdf_Bag))).
% 10.83/3.82 tff(c_2999, plain, (~iext(uri_rdfs_subClassOf, uri_rdf_Property, uri_rdf_Bag))).
% 10.83/3.82 tff(c_2303, plain, (![D_24]: (icext(D_24, uri_rdfs_subClassOf) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))).
% 10.83/3.82 tff(c_2998, plain, (~icext(uri_rdfs_ContainerMembershipProperty, uri_rdf_type))).
% 10.83/3.82 tff(c_1609, plain, (![Q_90]: (iext(Q_90, uri_rdf_first, uri_rdf_Property) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_90)))).
% 10.83/3.82 tff(c_2986, plain, (~iext(uri_rdfs_subClassOf, uri_rdfs_Resource, uri_rdf_Bag))).
% 10.83/3.82 tff(c_1383, plain, (![D_24]: (icext(D_24, uri_ex_Falcon) | ~iext(uri_rdfs_subClassOf, uri_ex_Species, D_24)))).
% 10.83/3.82 tff(c_1377, plain, (![D_24]: (icext(D_24, uri_rdf__2) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))).
% 10.83/3.82 tff(c_1386, plain, (![D_24]: (icext(D_24, uri_rdf__1) | ~iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, D_24)))).
% 10.83/3.82 tff(c_1358, plain, (![D_24]: (icext(D_24, uri_rdf_rest) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))).
% 10.83/3.82 tff(c_2880, plain, (~icext(uri_rdfs_Datatype, uri_rdf_List))).
% 10.83/3.82 tff(c_1389, plain, (![D_24]: (icext(D_24, uri_rdf_nil) | ~iext(uri_rdfs_subClassOf, uri_rdf_List, D_24)))).
% 10.83/3.82 tff(c_1347, plain, (![C_84]: (iext(uri_rdfs_subClassOf, C_84, uri_rdfs_Container) | ~iext(uri_rdfs_subClassOf, C_84, uri_rdf_Bag)))).
% 10.83/3.82 tff(c_2758, plain, (~icext(uri_rdfs_Datatype, uri_rdfs_Datatype))).
% 10.83/3.82 tff(c_1618, plain, (![D_24]: (icext(D_24, uri_rdf_XMLLiteral) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, D_24)))).
% 10.83/3.82 tff(c_1615, plain, (![D_24]: (icext(D_24, uri_rdf__2) | ~iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, D_24)))).
% 10.83/3.82 tff(c_2707, plain, (~icext(uri_rdfs_Datatype, uri_rdfs_ContainerMembershipProperty))).
% 10.83/3.82 tff(c_1642, plain, (![D_24]: (icext(D_24, uri_rdf__3) | ~iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, D_24)))).
% 10.83/3.82 tff(c_2681, plain, (~icext(uri_rdfs_Datatype, uri_rdfs_Class))).
% 10.83/3.82 tff(c_1565, plain, (![Q_90]: (iext(Q_90, uri_rdfs_member, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_90)))).
% 10.83/3.82 tff(c_1648, plain, (![D_24]: (icext(D_24, uri_rdf_Property) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_24)))).
% 10.83/3.82 tff(c_1624, plain, (![D_24]: (icext(D_24, uri_rdf__3) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))).
% 10.83/3.82 tff(c_2629, plain, (~icext(uri_rdfs_Datatype, '#skF_1'))).
% 10.83/3.82 tff(c_2608, plain, (~icext(uri_rdfs_ContainerMembershipProperty, uri_rdfs_domain))).
% 10.83/3.82 tff(c_1374, plain, (![D_24]: (icext(D_24, uri_ex_harry) | ~iext(uri_rdfs_subClassOf, '#skF_1', D_24)))).
% 10.83/3.82 tff(c_2607, plain, (~icext(uri_rdfs_Datatype, uri_ex_Species))).
% 10.83/3.82 tff(c_1577, plain, (![Q_90]: (iext(Q_90, uri_rdfs_comment, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_90)))).
% 10.83/3.82 tff(c_1636, plain, (![D_24]: (icext(D_24, uri_ex_Eagle) | ~iext(uri_rdfs_subClassOf, uri_ex_Species, D_24)))).
% 10.83/3.82 tff(c_1355, plain, (![D_24]: (icext(D_24, uri_rdf_first) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))).
% 10.83/3.82 tff(c_1621, plain, (![D_24]: (icext(D_24, uri_rdf_value) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))).
% 10.83/3.82 tff(c_1627, plain, (![D_24]: (icext(D_24, uri_rdf_type) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))).
% 10.83/3.82 tff(c_1630, plain, (![D_24]: (icext(D_24, uri_rdf__1) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))).
% 10.83/3.82 tff(c_1361, plain, (![D_24]: (icext(D_24, uri_rdf_object) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))).
% 10.83/3.82 tff(c_2475, plain, (~icext(uri_rdfs_Datatype, uri_rdf_Property))).
% 10.83/3.82 tff(c_1639, plain, (![D_24]: (icext(D_24, uri_rdf_subject) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))).
% 10.83/3.82 tff(c_1271, plain, (![C_79]: (icext(C_79, uri_ex_Falcon) | ~iext(uri_rdfs_domain, uri_rdf_type, C_79)))).
% 10.83/3.82 tff(c_1313, plain, (![C_79]: (icext(C_79, uri_rdf_first) | ~iext(uri_rdfs_domain, uri_rdf_type, C_79)))).
% 10.83/3.82 tff(c_1314, plain, (![C_79]: (icext(C_79, '#skF_1') | ~iext(uri_rdfs_domain, uri_owl_unionOf, C_79)))).
% 10.83/3.82 tff(c_1254, plain, (![C_79]: (icext(C_79, uri_rdf_type) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_79)))).
% 10.83/3.82 tff(c_1273, plain, (![C_79]: (icext(C_79, uri_rdf__3) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_79)))).
% 10.83/3.82 tff(c_1290, plain, (![C_79]: (icext(C_79, uri_rdf_type) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_79)))).
% 10.83/3.82 tff(c_1274, plain, (![C_79]: (icext(C_79, uri_rdf__1) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_79)))).
% 10.83/3.82 tff(c_1264, plain, (![C_79]: (icext(C_79, uri_ex_harry) | ~iext(uri_rdfs_domain, uri_rdf_type, C_79)))).
% 10.83/3.82 tff(c_1294, plain, (![C_79]: (icext(C_79, uri_rdfs_comment) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_79)))).
% 10.83/3.82 tff(c_1267, plain, (![C_79]: (icext(C_79, uri_rdfs_subClassOf) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_79)))).
% 10.83/3.82 tff(c_1311, plain, (![C_79]: (icext(C_79, uri_rdf_value) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_79)))).
% 10.83/3.82 tff(c_1027, plain, (![C_75]: (icext(C_75, uri_rdf_Property) | ~iext(uri_rdfs_range, uri_rdfs_range, C_75)))).
% 10.83/3.82 tff(c_1283, plain, (![C_79]: (icext(C_79, '#skF_2') | ~iext(uri_rdfs_domain, uri_rdf_rest, C_79)))).
% 10.83/3.82 tff(c_1308, plain, (![C_79]: (icext(C_79, uri_rdf_first) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_79)))).
% 10.83/3.82 tff(c_1044, plain, (![C_75]: (icext(C_75, uri_rdfs_seeAlso) | ~iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_75)))).
% 10.83/3.82 tff(c_1304, plain, (![C_79]: (icext(C_79, uri_rdf_subject) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_79)))).
% 10.83/3.82 tff(c_1296, plain, (![C_79]: (icext(C_79, uri_rdfs_label) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_79)))).
% 10.83/3.82 tff(c_1303, plain, (![C_79]: (icext(C_79, '#skF_3') | ~iext(uri_rdfs_domain, uri_rdf_rest, C_79)))).
% 10.83/3.82 tff(c_2350, plain, (ip(uri_rdfs_comment))).
% 10.83/3.82 tff(c_2344, plain, (icext(uri_rdf_Property, uri_rdfs_comment))).
% 10.83/3.82 tff(c_1281, plain, (![C_79]: (icext(C_79, uri_rdfs_comment) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_79)))).
% 10.83/3.82 tff(c_1292, plain, (![C_79]: (icext(C_79, uri_rdfs_domain) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_79)))).
% 10.83/3.82 tff(c_1282, plain, (![C_79]: (icext(C_79, uri_rdf__2) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_79)))).
% 10.83/3.82 tff(c_1287, plain, (![C_79]: (icext(C_79, uri_rdfs_ContainerMembershipProperty) | ~iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_79)))).
% 10.83/3.82 tff(c_1301, plain, (![C_79]: (icext(C_79, uri_rdfs_isDefinedBy) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_79)))).
% 10.83/3.82 tff(c_2315, plain, (ic(uri_rdfs_Statement))).
% 10.83/3.82 tff(c_2308, plain, (icext(uri_rdfs_Class, uri_rdfs_Statement))).
% 10.83/3.82 tff(c_1054, plain, (![C_75]: (icext(C_75, uri_rdfs_Statement) | ~iext(uri_rdfs_range, uri_rdfs_domain, C_75)))).
% 10.83/3.82 tff(c_2289, plain, (icext(uri_rdf_Property, uri_rdfs_subClassOf))).
% 10.83/3.82 tff(c_1255, plain, (![C_79]: (icext(C_79, uri_rdf__2) | ~iext(uri_rdfs_domain, uri_rdf_type, C_79)))).
% 10.83/3.82 tff(c_1316, plain, (![C_79]: (icext(C_79, uri_rdfs_subClassOf) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_79)))).
% 10.83/3.82 tff(c_1289, plain, (![C_79]: (icext(C_79, uri_rdf__2) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_79)))).
% 10.83/3.82 tff(c_1072, plain, (![C_75]: (icext(C_75, uri_rdf_nil) | ~iext(uri_rdfs_range, uri_rdf_rest, C_75)))).
% 10.83/3.83 tff(c_1065, plain, (![C_75]: (icext(C_75, uri_rdfs_Literal) | ~iext(uri_rdfs_range, uri_rdfs_range, C_75)))).
% 10.83/3.83 tff(c_1074, plain, (![C_75]: (icext(C_75, uri_rdfs_Class) | ~iext(uri_rdfs_range, uri_rdf_type, C_75)))).
% 10.83/3.83 tff(c_1261, plain, (![C_79]: (icext(C_79, uri_rdf_nil) | ~iext(uri_rdfs_domain, uri_rdf_type, C_79)))).
% 10.83/3.83 tff(c_1258, plain, (![C_79]: (icext(C_79, uri_rdfs_subPropertyOf) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_79)))).
% 10.83/3.83 tff(c_2247, plain, (ip(uri_rdfs_label))).
% 10.83/3.83 tff(c_2241, plain, (icext(uri_rdf_Property, uri_rdfs_label))).
% 10.83/3.83 tff(c_1291, plain, (![C_79]: (icext(C_79, uri_rdfs_label) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_79)))).
% 10.83/3.83 tff(c_1049, plain, (![C_75]: (icext(C_75, uri_rdf_Property) | ~iext(uri_rdfs_range, uri_rdfs_domain, C_75)))).
% 10.83/3.83 tff(c_1300, plain, (![C_79]: (icext(C_79, uri_rdfs_isDefinedBy) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_79)))).
% 10.83/3.83 tff(c_1276, plain, (![C_79]: (icext(C_79, uri_rdf_XMLLiteral) | ~iext(uri_rdfs_domain, uri_rdf_type, C_79)))).
% 10.83/3.83 tff(c_1251, plain, (![C_79]: (icext(C_79, uri_rdf_subject) | ~iext(uri_rdfs_domain, uri_rdf_type, C_79)))).
% 10.83/3.83 tff(c_1259, plain, (![C_79]: (icext(C_79, uri_rdf__3) | ~iext(uri_rdfs_domain, uri_rdf_type, C_79)))).
% 10.83/3.83 tff(c_1307, plain, (![C_79]: (icext(C_79, uri_ex_Eagle) | ~iext(uri_rdfs_domain, uri_rdf_type, C_79)))).
% 10.83/3.83 tff(c_1047, plain, (![C_75]: (icext(C_75, uri_rdf_List) | ~iext(uri_rdfs_range, uri_rdfs_range, C_75)))).
% 10.83/3.83 tff(c_1280, plain, (![C_79]: (icext(C_79, uri_rdfs_range) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_79)))).
% 10.83/3.83 tff(c_1305, plain, (![C_79]: (icext(C_79, uri_rdf_Property) | ~iext(uri_rdfs_domain, uri_rdf_type, C_79)))).
% 10.83/3.83 tff(c_1045, plain, (![C_75]: (icext(C_75, uri_rdfs_Datatype) | ~iext(uri_rdfs_range, uri_rdf_type, C_75)))).
% 10.83/3.83 tff(c_2168, plain, (icext(uri_rdf_Property, uri_rdfs_subPropertyOf))).
% 10.83/3.83 tff(c_1279, plain, (![C_79]: (icext(C_79, uri_rdfs_subPropertyOf) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_79)))).
% 10.83/3.83 tff(c_1036, plain, (![C_75]: (icext(C_75, uri_rdfs_Class) | ~iext(uri_rdfs_range, uri_rdfs_domain, C_75)))).
% 10.83/3.83 tff(c_1299, plain, (![C_79]: (icext(C_79, uri_rdf_first) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_79)))).
% 10.83/3.83 tff(c_1272, plain, (![C_79]: (icext(C_79, uri_rdf_type) | ~iext(uri_rdfs_domain, uri_rdf_type, C_79)))).
% 10.83/3.83 tff(c_1310, plain, (![C_79]: (icext(C_79, uri_rdf_rest) | ~iext(uri_rdfs_domain, uri_rdf_type, C_79)))).
% 10.83/3.83 tff(c_2131, plain, (icext(uri_rdfs_Class, uri_rdf_Alt))).
% 10.83/3.83 tff(c_1277, plain, (![C_79]: (icext(C_79, uri_rdf_Alt) | ~iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_79)))).
% 10.83/3.83 tff(c_1293, plain, (![C_79]: (icext(C_79, uri_rdfs_seeAlso) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_79)))).
% 10.83/3.83 tff(c_1309, plain, (![C_79]: (icext(C_79, uri_rdf__1) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_79)))).
% 10.83/3.83 tff(c_2106, plain, (icext(uri_rdf_Property, uri_rdfs_seeAlso))).
% 10.83/3.83 tff(c_1298, plain, (![C_79]: (icext(C_79, uri_rdfs_seeAlso) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_79)))).
% 10.83/3.83 tff(c_1084, plain, (![C_75]: (icext(C_75, uri_rdfs_Class) | ~iext(uri_rdfs_range, uri_rdfs_subClassOf, C_75)))).
% 10.83/3.83 tff(c_2081, plain, (icext(uri_rdfs_Class, uri_rdfs_Seq))).
% 10.83/3.83 tff(c_1295, plain, (![C_79]: (icext(C_79, uri_rdfs_member) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_79)))).
% 10.83/3.83 tff(c_1302, plain, (![C_79]: (icext(C_79, uri_rdfs_Seq) | ~iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_79)))).
% 10.83/3.83 tff(c_2076, plain, (ic(uri_ex_Species))).
% 10.83/3.83 tff(c_2069, plain, (icext(uri_rdfs_Class, uri_ex_Species))).
% 10.83/3.83 tff(c_1076, plain, (![C_75]: (icext(C_75, uri_ex_Species) | ~iext(uri_rdfs_range, uri_rdf_type, C_75)))).
% 10.83/3.83 tff(c_1312, plain, (![C_79]: (icext(C_79, '#skF_3') | ~iext(uri_rdfs_domain, uri_rdf_first, C_79)))).
% 10.83/3.83 tff(c_1288, plain, (![C_79]: (icext(C_79, uri_rdf__3) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_79)))).
% 10.83/3.83 tff(c_1265, plain, (![C_79]: (icext(C_79, uri_rdf_value) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_79)))).
% 10.83/3.83 tff(c_2038, plain, (icext(uri_rdfs_Class, uri_rdf_XMLLiteral))).
% 10.83/3.83 tff(c_1256, plain, (![C_79]: (icext(C_79, uri_rdf_XMLLiteral) | ~iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_79)))).
% 10.83/3.83 tff(c_1286, plain, (![C_79]: (icext(C_79, uri_rdf__1) | ~iext(uri_rdfs_domain, uri_rdf_type, C_79)))).
% 10.83/3.83 tff(c_2019, plain, (icext(uri_rdf_Property, uri_rdfs_range))).
% 10.83/3.83 tff(c_1270, plain, (![C_79]: (icext(C_79, uri_rdfs_range) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_79)))).
% 10.83/3.83 tff(c_1081, plain, (![C_75]: (icext(C_75, uri_ex_Falcon) | ~iext(uri_rdfs_range, uri_rdf_first, C_75)))).
% 10.83/3.83 tff(c_2000, plain, (icext(uri_rdf_Property, uri_rdfs_member))).
% 10.83/3.83 tff(c_1269, plain, (![C_79]: (icext(C_79, uri_rdfs_member) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_79)))).
% 10.83/3.83 tff(c_1266, plain, (![C_79]: (icext(C_79, uri_rdf_object) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_79)))).
% 10.83/3.83 tff(c_1986, plain, (icext(uri_rdf_List, '#skF_2'))).
% 10.83/3.83 tff(c_1268, plain, (![C_79]: (icext(C_79, '#skF_2') | ~iext(uri_rdfs_domain, uri_rdf_first, C_79)))).
% 10.83/3.83 tff(c_1306, plain, (![C_79]: (icext(C_79, uri_rdf_object) | ~iext(uri_rdfs_domain, uri_rdf_type, C_79)))).
% 10.83/3.83 tff(c_1972, plain, (icext(uri_rdf_List, '#skF_3'))).
% 10.83/3.83 tff(c_1052, plain, (![C_75]: (icext(C_75, '#skF_3') | ~iext(uri_rdfs_range, uri_rdf_rest, C_75)))).
% 10.83/3.83 tff(c_1031, plain, (![C_75]: (icext(C_75, uri_rdf_Property) | ~iext(uri_rdfs_range, uri_rdf_type, C_75)))).
% 10.83/3.83 tff(c_1953, plain, (icext(uri_rdfs_Class, uri_rdfs_Class))).
% 10.83/3.83 tff(c_1039, plain, (![C_75]: (icext(C_75, uri_rdfs_Class) | ~iext(uri_rdfs_range, uri_rdfs_range, C_75)))).
% 10.83/3.83 tff(c_1297, plain, (![C_79]: (icext(C_79, uri_rdf_predicate) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_79)))).
% 10.83/3.83 tff(c_1252, plain, (![C_79]: (icext(C_79, uri_rdf_subject) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_79)))).
% 10.83/3.83 tff(c_1278, plain, (![C_79]: (icext(C_79, uri_rdf_rest) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_79)))).
% 10.83/3.83 tff(c_1083, plain, (![C_75]: (icext(C_75, '#skF_2') | ~iext(uri_rdfs_range, uri_owl_unionOf, C_75)))).
% 10.83/3.83 tff(c_1916, plain, (~icext(uri_rdfs_Datatype, uri_rdfs_Resource))).
% 10.83/3.83 tff(c_1921, plain, (icext(uri_rdfs_Class, uri_rdfs_Literal))).
% 10.83/3.83 tff(c_1025, plain, (![C_75]: (icext(C_75, uri_rdfs_Literal) | ~iext(uri_rdfs_range, uri_rdfs_subClassOf, C_75)))).
% 10.83/3.83 tff(c_1915, plain, (ic('#skF_1'))).
% 10.83/3.83 tff(c_1908, plain, (icext(uri_rdfs_Class, '#skF_1'))).
% 10.83/3.83 tff(c_1033, plain, (![C_75]: (icext(C_75, '#skF_1') | ~iext(uri_rdfs_range, uri_rdf_type, C_75)))).
% 10.83/3.83 tff(c_854, plain, (![D_72, X_17]: (icext(D_72, X_17) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Resource, D_72)))).
% 10.83/3.83 tff(c_1878, plain, (icext(uri_rdf_Property, uri_rdfs_domain))).
% 10.83/3.83 tff(c_1260, plain, (![C_79]: (icext(C_79, uri_rdfs_domain) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_79)))).
% 10.83/3.83 tff(c_1037, plain, (![C_75]: (icext(C_75, uri_ex_Eagle) | ~iext(uri_rdfs_range, uri_rdf_first, C_75)))).
% 10.83/3.83 tff(c_1859, plain, (icext(uri_rdfs_Class, uri_rdfs_ContainerMembershipProperty))).
% 10.83/3.83 tff(c_1053, plain, (![C_75]: (icext(C_75, uri_rdfs_ContainerMembershipProperty) | ~iext(uri_rdfs_range, uri_rdf_type, C_75)))).
% 10.83/3.83 tff(c_1077, plain, (![C_75]: (icext(C_75, uri_rdf_List) | ~iext(uri_rdfs_range, uri_rdfs_domain, C_75)))).
% 10.83/3.83 tff(c_1042, plain, (![C_75]: (icext(C_75, uri_rdfs_Resource) | ~iext(uri_rdfs_range, uri_rdfs_range, C_75)))).
% 10.83/3.83 tff(c_1056, plain, (![C_75]: (icext(C_75, uri_rdf_Property) | ~iext(uri_rdfs_range, uri_rdfs_subClassOf, C_75)))).
% 10.83/3.83 tff(c_1828, plain, (icext(uri_rdfs_Class, uri_rdfs_Container))).
% 10.83/3.83 tff(c_1071, plain, (![C_75]: (icext(C_75, uri_rdfs_Container) | ~iext(uri_rdfs_range, uri_rdfs_subClassOf, C_75)))).
% 10.83/3.83 tff(c_1815, plain, (icext(uri_rdfs_Class, uri_rdfs_Datatype))).
% 10.83/3.83 tff(c_1315, plain, (![C_79]: (icext(C_79, uri_rdfs_Datatype) | ~iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_79)))).
% 10.83/3.83 tff(c_1802, plain, (icext(uri_rdf_Property, uri_rdfs_isDefinedBy))).
% 10.83/3.83 tff(c_1275, plain, (![C_79]: (icext(C_79, uri_rdfs_isDefinedBy) | ~iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_79)))).
% 10.83/3.83 tff(c_1797, plain, (ic(uri_rdf_List))).
% 10.83/3.83 tff(c_1790, plain, (icext(uri_rdfs_Class, uri_rdf_List))).
% 10.83/3.83 tff(c_1030, plain, (![C_75]: (icext(C_75, uri_rdf_List) | ~iext(uri_rdfs_range, uri_rdf_type, C_75)))).
% 10.83/3.83 tff(c_1777, plain, (icext(uri_rdfs_Class, uri_rdf_Bag))).
% 10.83/3.83 tff(c_1253, plain, (![C_79]: (icext(C_79, uri_rdf_Bag) | ~iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_79)))).
% 10.83/3.83 tff(c_1250, plain, (![C_79]: (icext(C_79, uri_rdf_value) | ~iext(uri_rdfs_domain, uri_rdf_type, C_79)))).
% 10.83/3.83 tff(c_1765, plain, (ip(uri_rdf_predicate))).
% 10.83/3.83 tff(c_1759, plain, (icext(uri_rdf_Property, uri_rdf_predicate))).
% 10.83/3.83 tff(c_1285, plain, (![C_79]: (icext(C_79, uri_rdf_predicate) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_79)))).
% 10.83/3.83 tff(c_1746, plain, (icext(uri_rdfs_Class, uri_rdfs_Resource))).
% 10.83/3.83 tff(c_1051, plain, (![C_75]: (icext(C_75, uri_rdfs_Resource) | ~iext(uri_rdfs_range, uri_rdfs_domain, C_75)))).
% 10.83/3.83 tff(c_1263, plain, (![C_79]: (icext(C_79, uri_rdf_rest) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_79)))).
% 10.83/3.83 tff(c_1735, plain, (ip(uri_rdfs_member))).
% 10.83/3.83 tff(c_777, plain, (![X_67]: (ip(X_67) | ~icext(uri_rdf_Property, X_67)))).
% 10.83/3.83 tff(c_835, plain, (![P_71]: (ip(P_71) | ~icext(uri_rdfs_ContainerMembershipProperty, P_71)))).
% 10.83/3.83 tff(c_733, plain, (![P_6]: (icext(uri_rdf_Property, P_6) | ~ip(P_6)))).
% 10.83/3.83 tff(c_816, plain, (![D_70]: (ic(D_70) | ~icext(uri_rdfs_Datatype, D_70)))).
% 10.83/3.83 tff(c_747, plain, (icext(uri_rdfs_Class, uri_rdf_Property))).
% 10.83/3.83 tff(c_745, plain, (icext(uri_rdfs_ContainerMembershipProperty, uri_rdf__3))).
% 10.83/3.83 tff(c_735, plain, (icext(uri_rdf_Property, uri_rdf_subject))).
% 10.83/3.83 tff(c_749, plain, (icext(uri_ex_Species, uri_ex_Eagle))).
% 10.83/3.83 tff(c_737, plain, (icext(uri_rdf_Property, uri_rdf__1))).
% 10.83/3.83 tff(c_743, plain, (icext(uri_rdf_Property, uri_rdf_type))).
% 10.83/3.83 tff(c_738, plain, (icext(uri_rdf_Property, uri_rdf__3))).
% 10.83/3.83 tff(c_734, plain, (icext(uri_rdf_Property, uri_rdf_value))).
% 10.83/3.83 tff(c_744, plain, (icext(uri_rdfs_Datatype, uri_rdf_XMLLiteral))).
% 10.83/3.83 tff(c_736, plain, (icext(uri_rdfs_ContainerMembershipProperty, uri_rdf__2))).
% 10.83/3.83 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)))).
% 10.83/3.83 tff(c_739, plain, (icext(uri_rdf_List, uri_rdf_nil))).
% 10.83/3.83 tff(c_746, plain, (icext(uri_rdfs_ContainerMembershipProperty, uri_rdf__1))).
% 10.83/3.83 tff(c_742, plain, (icext(uri_ex_Species, uri_ex_Falcon))).
% 10.83/3.83 tff(c_740, plain, (icext(uri_rdf_Property, uri_rdf__2))).
% 10.83/3.84 tff(c_741, plain, (icext('#skF_1', uri_ex_harry))).
% 10.83/3.84 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)))).
% 10.83/3.84 tff(c_748, plain, (icext(uri_rdf_Property, uri_rdf_object))).
% 10.83/3.84 tff(c_750, plain, (icext(uri_rdf_Property, uri_rdf_rest))).
% 10.83/3.84 tff(c_751, plain, (icext(uri_rdf_Property, uri_rdf_first))).
% 10.83/3.84 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)))).
% 10.83/3.84 tff(c_1089, plain, (~ip(uri_ex_harry))).
% 10.83/3.84 tff(c_796, plain, (![C_8]: (~icext(uri_ex_Species, C_8) | ~icext(C_8, uri_ex_harry)))).
% 10.83/3.84 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)))).
% 10.83/3.84 tff(c_672, plain, (ip(uri_owl_unionOf))).
% 10.83/3.84 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)))).
% 10.83/3.84 tff(c_798, plain, (~icext(uri_ex_Species, '#skF_1'))).
% 10.83/3.84 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)))).
% 10.83/3.84 tff(c_778, plain, (~icext(uri_ex_Falcon, uri_ex_harry))).
% 10.93/3.84 tff(c_70, plain, (![P_10]: (iext(uri_rdfs_subPropertyOf, P_10, uri_rdfs_member) | ~icext(uri_rdfs_ContainerMembershipProperty, P_10)))).
% 10.93/3.84 tff(c_364, plain, (ip(uri_rdf__1))).
% 10.93/3.84 tff(c_616, plain, (ip(uri_rdf_first))).
% 10.93/3.84 tff(c_363, plain, (ip(uri_rdf_subject))).
% 10.93/3.84 tff(c_779, plain, (~icext(uri_ex_Eagle, uri_ex_harry))).
% 10.93/3.84 tff(c_625, plain, (ip(uri_rdfs_subPropertyOf))).
% 10.93/3.84 tff(c_102, plain, (![D_11]: (iext(uri_rdfs_subClassOf, D_11, uri_rdfs_Literal) | ~icext(uri_rdfs_Datatype, D_11)))).
% 10.93/3.84 tff(c_780, plain, (![X_67]: (~iext(uri_rdf_type, uri_ex_harry, X_67) | ~icext(uri_ex_Species, X_67)))).
% 10.93/3.84 tff(c_54, plain, (![X_7, C_8]: (iext(uri_rdf_type, X_7, C_8) | ~icext(C_8, X_7)))).
% 10.93/3.84 tff(c_632, plain, (ip(uri_rdfs_domain))).
% 10.93/3.84 tff(c_623, plain, (ip(uri_rdfs_range))).
% 10.93/3.84 tff(c_365, plain, (ip(uri_rdf__3))).
% 10.93/3.84 tff(c_52, plain, (![C_8, X_7]: (icext(C_8, X_7) | ~iext(uri_rdf_type, X_7, C_8)))).
% 10.93/3.84 tff(c_673, plain, (ip(uri_rdfs_subClassOf))).
% 10.93/3.84 tff(c_368, plain, (ip(uri_rdf_object))).
% 10.93/3.84 tff(c_369, plain, (ip(uri_rdf_rest))).
% 10.93/3.84 tff(c_2, plain, (![P_2, S_1, O_3]: (ip(P_2) | ~iext(P_2, S_1, O_3)))).
% 10.93/3.84 tff(c_367, plain, (ip(uri_rdf_type))).
% 10.93/3.84 tff(c_366, plain, (ip(uri_rdf__2))).
% 10.93/3.84 tff(c_362, plain, (ip(uri_rdf_value))).
% 10.93/3.84 tff(c_26, plain, (![P_6]: (ip(P_6) | ~iext(uri_rdf_type, P_6, uri_rdf_Property)))).
% 10.93/3.84 tff(c_320, plain, (ic(uri_rdfs_Resource))).
% 10.93/3.84 tff(c_154, plain, (![C_27]: (iext(uri_rdfs_subClassOf, C_27, C_27) | ~ic(C_27)))).
% 10.93/3.84 tff(c_282, plain, (ic(uri_rdf_XMLLiteral))).
% 10.93/3.84 tff(c_56, plain, (![C_9]: (iext(uri_rdfs_subClassOf, C_9, uri_rdfs_Resource) | ~ic(C_9)))).
% 10.93/3.84 tff(c_295, plain, (ip(uri_rdfs_isDefinedBy))).
% 10.93/3.84 tff(c_283, plain, (ic(uri_rdf_Alt))).
% 10.93/3.84 tff(c_284, plain, (ic(uri_rdfs_ContainerMembershipProperty))).
% 10.93/3.84 tff(c_285, plain, (ic(uri_rdfs_Seq))).
% 10.93/3.84 tff(c_286, plain, (ic(uri_rdfs_Datatype))).
% 10.93/3.84 tff(c_164, plain, (![P_31, Q_32]: (ip(P_31) | ~iext(uri_rdfs_subPropertyOf, P_31, Q_32)))).
% 10.93/3.84 tff(c_281, plain, (ic(uri_rdf_Bag))).
% 10.93/3.84 tff(c_150, plain, (![C_23, D_24]: (ic(C_23) | ~iext(uri_rdfs_subClassOf, C_23, D_24)))).
% 10.93/3.84 tff(c_28, plain, (![P_6]: (iext(uri_rdf_type, P_6, uri_rdf_Property) | ~ip(P_6)))).
% 10.93/3.84 tff(c_247, plain, (ic(uri_rdf_Property))).
% 10.93/3.84 tff(c_249, plain, (ic(uri_rdfs_Class))).
% 10.93/3.84 tff(c_258, plain, (ip(uri_rdfs_seeAlso))).
% 10.93/3.84 tff(c_245, plain, (ic(uri_rdfs_Literal))).
% 10.93/3.84 tff(c_162, plain, (![Q_32, P_31]: (ip(Q_32) | ~iext(uri_rdfs_subPropertyOf, P_31, Q_32)))).
% 10.93/3.84 tff(c_244, plain, (ic(uri_rdfs_Container))).
% 10.93/3.84 tff(c_148, plain, (![D_24, C_23]: (ic(D_24) | ~iext(uri_rdfs_subClassOf, C_23, D_24)))).
% 10.93/3.84 tff(c_168, plain, (![P_37]: (iext(uri_rdfs_subPropertyOf, P_37, P_37) | ~ip(P_37)))).
% 10.93/3.84 tff(c_112, plain, (![X_16]: (icext(uri_rdfs_Class, X_16) | ~ic(X_16)))).
% 10.93/3.84 tff(c_120, plain, (![X_18]: (icext(uri_rdfs_Literal, X_18) | ~lv(X_18)))).
% 10.93/3.84 tff(c_122, plain, (![X_18]: (lv(X_18) | ~icext(uri_rdfs_Literal, X_18)))).
% 10.93/3.84 tff(c_114, plain, (![X_16]: (ic(X_16) | ~icext(uri_rdfs_Class, X_16)))).
% 10.93/3.84 tff(c_22, plain, (iext(uri_rdf_type, uri_rdf_value, uri_rdf_Property))).
% 10.93/3.84 tff(c_24, plain, (iext(uri_rdf_type, uri_rdf_subject, uri_rdf_Property))).
% 10.93/3.84 tff(c_142, plain, (iext(uri_rdfs_range, uri_rdf_subject, uri_rdfs_Resource))).
% 10.93/3.84 tff(c_68, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Bag, uri_rdfs_Container))).
% 10.93/3.84 tff(c_172, plain, (iext(uri_rdfs_domain, uri_rdf_type, uri_rdfs_Resource))).
% 10.93/3.84 tff(c_92, plain, (iext(uri_rdf_type, uri_rdf__2, uri_rdfs_ContainerMembershipProperty))).
% 10.93/3.84 tff(c_98, plain, (iext(uri_rdfs_subClassOf, uri_rdf_XMLLiteral, uri_rdfs_Literal))).
% 10.93/3.84 tff(c_14, plain, (iext(uri_rdf_type, uri_rdf__1, uri_rdf_Property))).
% 10.93/3.84 tff(c_166, plain, (iext(uri_rdfs_range, uri_rdfs_subPropertyOf, uri_rdf_Property))).
% 10.93/3.84 tff(c_18, plain, (iext(uri_rdf_type, uri_rdf__3, uri_rdf_Property))).
% 10.93/3.84 tff(c_106, plain, (iext(uri_rdfs_domain, uri_rdfs_domain, uri_rdf_Property))).
% 10.93/3.84 tff(c_10, plain, (iext(uri_rdf_type, uri_rdf_nil, uri_rdf_List))).
% 10.93/3.84 tff(c_211, plain, (~iext(uri_rdf_type, uri_ex_harry, uri_ex_Falcon))).
% 10.93/3.84 tff(c_16, plain, (iext(uri_rdf_type, uri_rdf__2, uri_rdf_Property))).
% 10.93/3.84 tff(c_62, plain, (iext(uri_rdfs_domain, uri_rdf_rest, uri_rdf_List))).
% 10.93/3.84 tff(c_192, plain, (iext(uri_rdf_type, uri_ex_harry, '#skF_1'))).
% 10.93/3.84 tff(c_176, plain, (iext(uri_rdfs_domain, uri_rdf_value, uri_rdfs_Resource))).
% 10.93/3.84 tff(c_132, plain, (iext(uri_rdfs_domain, uri_rdf_object, uri_rdfs_Statement))).
% 10.93/3.84 tff(c_144, plain, (iext(uri_rdfs_domain, uri_rdfs_subClassOf, uri_rdfs_Class))).
% 10.93/3.84 tff(c_188, plain, (iext(uri_rdf_first, '#skF_2', uri_ex_Eagle))).
% 10.93/3.84 tff(c_74, plain, (iext(uri_rdfs_domain, uri_rdfs_member, uri_rdfs_Resource))).
% 10.93/3.84 tff(c_130, plain, (iext(uri_rdfs_range, uri_rdfs_range, uri_rdfs_Class))).
% 10.93/3.84 tff(c_194, plain, (iext(uri_rdf_type, uri_ex_Falcon, uri_ex_Species))).
% 10.93/3.84 tff(c_32, plain, (iext(uri_rdf_type, uri_rdf_type, uri_rdf_Property))).
% 10.93/3.84 tff(c_88, plain, (iext(uri_rdfs_range, uri_rdf__3, uri_rdfs_Resource))).
% 10.93/3.84 tff(c_78, plain, (iext(uri_rdfs_domain, uri_rdf__1, uri_rdfs_Resource))).
% 10.93/3.84 tff(c_42, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_isDefinedBy, uri_rdfs_seeAlso))).
% 10.93/3.84 tff(c_100, plain, (iext(uri_rdf_type, uri_rdf_XMLLiteral, uri_rdfs_Datatype))).
% 10.93/3.84 tff(c_66, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Alt, uri_rdfs_Container))).
% 10.93/3.84 tff(c_64, plain, (iext(uri_rdfs_range, uri_rdf_rest, uri_rdf_List))).
% 10.93/3.84 tff(c_158, plain, (iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, uri_rdf_Property))).
% 10.93/3.84 tff(c_126, plain, (iext(uri_rdfs_domain, uri_rdfs_range, uri_rdf_Property))).
% 10.93/3.84 tff(c_34, plain, (iext(uri_rdfs_domain, uri_rdfs_comment, uri_rdfs_Resource))).
% 10.93/3.84 tff(c_80, plain, (iext(uri_rdfs_domain, uri_rdf__2, uri_rdfs_Resource))).
% 10.93/3.84 tff(c_186, plain, (iext(uri_rdf_rest, '#skF_2', '#skF_3'))).
% 10.93/3.84 tff(c_94, plain, (iext(uri_rdf_type, uri_rdf__3, uri_rdfs_ContainerMembershipProperty))).
% 10.93/3.84 tff(c_136, plain, (iext(uri_rdfs_domain, uri_rdf_predicate, uri_rdfs_Statement))).
% 10.93/3.84 tff(c_90, plain, (iext(uri_rdf_type, uri_rdf__1, uri_rdfs_ContainerMembershipProperty))).
% 10.93/3.84 tff(c_72, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, uri_rdf_Property))).
% 10.93/3.84 tff(c_82, plain, (iext(uri_rdfs_domain, uri_rdf__3, uri_rdfs_Resource))).
% 10.93/3.84 tff(c_86, plain, (iext(uri_rdfs_range, uri_rdf__2, uri_rdfs_Resource))).
% 10.93/3.84 tff(c_174, plain, (iext(uri_rdfs_range, uri_rdf_type, uri_rdfs_Class))).
% 10.93/3.84 tff(c_44, plain, (iext(uri_rdfs_domain, uri_rdfs_label, uri_rdfs_Resource))).
% 10.93/3.84 tff(c_110, plain, (iext(uri_rdfs_range, uri_rdfs_domain, uri_rdfs_Class))).
% 10.93/3.84 tff(c_48, plain, (iext(uri_rdfs_domain, uri_rdfs_seeAlso, uri_rdfs_Resource))).
% 10.93/3.84 tff(c_36, plain, (iext(uri_rdfs_range, uri_rdfs_comment, uri_rdfs_Literal))).
% 10.93/3.84 tff(c_76, plain, (iext(uri_rdfs_range, uri_rdfs_member, uri_rdfs_Resource))).
% 10.93/3.84 tff(c_46, plain, (iext(uri_rdfs_range, uri_rdfs_label, uri_rdfs_Literal))).
% 10.93/3.84 tff(c_138, plain, (iext(uri_rdfs_range, uri_rdf_predicate, uri_rdfs_Resource))).
% 10.93/3.84 tff(c_50, plain, (iext(uri_rdfs_range, uri_rdfs_seeAlso, uri_rdfs_Resource))).
% 10.93/3.84 tff(c_60, plain, (iext(uri_rdfs_range, uri_rdf_first, uri_rdfs_Resource))).
% 10.93/3.84 tff(c_38, plain, (iext(uri_rdfs_domain, uri_rdfs_isDefinedBy, uri_rdfs_Resource))).
% 10.93/3.84 tff(c_208, plain, (~iext(uri_rdf_type, uri_ex_harry, uri_ex_Eagle))).
% 10.93/3.84 tff(c_40, plain, (iext(uri_rdfs_range, uri_rdfs_isDefinedBy, uri_rdfs_Resource))).
% 10.93/3.84 tff(c_96, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Seq, uri_rdfs_Container))).
% 10.93/3.84 tff(c_182, plain, (iext(uri_rdf_rest, '#skF_3', uri_rdf_nil))).
% 10.93/3.84 tff(c_140, plain, (iext(uri_rdfs_domain, uri_rdf_subject, uri_rdfs_Statement))).
% 10.93/3.84 tff(c_124, plain, (iext(uri_rdf_type, uri_rdf_Property, uri_rdfs_Class))).
% 10.93/3.84 tff(c_20, plain, (iext(uri_rdf_type, uri_rdf_object, uri_rdf_Property))).
% 10.93/3.84 tff(c_196, plain, (iext(uri_rdf_type, uri_ex_Eagle, uri_ex_Species))).
% 10.93/3.84 tff(c_58, plain, (iext(uri_rdfs_domain, uri_rdf_first, uri_rdf_List))).
% 10.93/3.84 tff(c_84, plain, (iext(uri_rdfs_range, uri_rdf__1, uri_rdfs_Resource))).
% 10.93/3.84 tff(c_180, plain, (![BNODE_x_41]: (~iext(uri_rdf_type, BNODE_x_41, uri_ex_Species) | ~iext(uri_rdf_type, uri_ex_harry, BNODE_x_41)))).
% 10.93/3.84 tff(c_12, plain, (iext(uri_rdf_type, uri_rdf_rest, uri_rdf_Property))).
% 10.93/3.84 tff(c_178, plain, (iext(uri_rdfs_range, uri_rdf_value, uri_rdfs_Resource))).
% 10.93/3.84 tff(c_184, plain, (iext(uri_rdf_first, '#skF_3', uri_ex_Falcon))).
% 10.93/3.84 tff(c_8, plain, (iext(uri_rdf_type, uri_rdf_first, uri_rdf_Property))).
% 10.93/3.84 tff(c_190, plain, (iext(uri_owl_unionOf, '#skF_1', '#skF_2'))).
% 10.93/3.84 tff(c_104, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, uri_rdfs_Class))).
% 10.93/3.84 tff(c_152, plain, (iext(uri_rdfs_range, uri_rdfs_subClassOf, uri_rdfs_Class))).
% 10.93/3.84 tff(c_202, plain, (![X_17]: (icext(uri_rdfs_Resource, X_17)))).
% 10.93/3.84 tff(c_4, plain, (![X_4]: (ir(X_4)))).
% 10.93/3.84 % SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p
% 10.93/3.84
%------------------------------------------------------------------------------