%------------------------------------------------------------------------------ % File : Beagle---0.9.52 % Problem : SWB005+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 : n029.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:45 PM UTC 2025 % Result : CounterSatisfiable 11.36s 3.75s % Output : Assurance 0s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SWB005+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/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 : n029.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:52:19 EDT 2025 % 0.20/0.34 % CPUTime : % 11.36/3.75 % 11.36/3.75 % SZS status CounterSatisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 11.36/3.75 % 11.36/3.75 % SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 11.36/3.76 %$ 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_Thing > uri_owl_ObjectProperty > uri_ex_s > uri_ex_p > uri_ex_o % 11.36/3.76 % 11.36/3.76 %Foreground sorts: % 11.36/3.76 % 11.36/3.76 % 11.36/3.76 %Background operators: % 11.36/3.76 % 11.36/3.76 % 11.36/3.76 %Foreground operators: % 11.36/3.76 tff(uri_rdfs_Datatype, type, uri_rdfs_Datatype: $i). % 11.36/3.76 tff(uri_rdfs_ContainerMembershipProperty, type, uri_rdfs_ContainerMembershipProperty: $i). % 11.36/3.76 tff(uri_rdfs_Resource, type, uri_rdfs_Resource: $i). % 11.36/3.76 tff(uri_rdf_Property, type, uri_rdf_Property: $i). % 11.36/3.76 tff(uri_rdf_subject, type, uri_rdf_subject: $i). % 11.36/3.76 tff(uri_rdf_type, type, uri_rdf_type: $i). % 11.36/3.76 tff(uri_rdfs_subPropertyOf, type, uri_rdfs_subPropertyOf: $i). % 11.36/3.76 tff(uri_rdfs_seeAlso, type, uri_rdfs_seeAlso: $i). % 11.36/3.76 tff(uri_rdfs_range, type, uri_rdfs_range: $i). % 11.36/3.76 tff(uri_rdf_XMLLiteral, type, uri_rdf_XMLLiteral: $i). % 11.36/3.76 tff(uri_rdf_List, type, uri_rdf_List: $i). % 11.36/3.76 tff(uri_ex_s, type, uri_ex_s: $i). % 11.36/3.76 tff(uri_rdf_first, type, uri_rdf_first: $i). % 11.36/3.76 tff(uri_rdf_predicate, type, uri_rdf_predicate: $i). % 11.36/3.76 tff(uri_owl_Thing, type, uri_owl_Thing: $i). % 11.36/3.76 tff(uri_rdf__3, type, uri_rdf__3: $i). % 11.36/3.76 tff(icext, type, icext: ($i * $i) > $o). % 11.36/3.76 tff(uri_rdf_value, type, uri_rdf_value: $i). % 11.36/3.76 tff(ip, type, ip: $i > $o). % 11.36/3.76 tff(uri_rdfs_Statement, type, uri_rdfs_Statement: $i). % 11.36/3.76 tff(uri_ex_p, type, uri_ex_p: $i). % 11.36/3.76 tff(uri_rdf__1, type, uri_rdf__1: $i). % 11.36/3.76 tff(lv, type, lv: $i > $o). % 11.36/3.76 tff(ir, type, ir: $i > $o). % 11.36/3.76 tff(uri_rdf_rest, type, uri_rdf_rest: $i). % 11.36/3.76 tff(uri_rdfs_label, type, uri_rdfs_label: $i). % 11.36/3.76 tff(uri_rdfs_Container, type, uri_rdfs_Container: $i). % 11.36/3.76 tff(ic, type, ic: $i > $o). % 11.36/3.76 tff(uri_owl_ObjectProperty, type, uri_owl_ObjectProperty: $i). % 11.36/3.76 tff(uri_rdfs_subClassOf, type, uri_rdfs_subClassOf: $i). % 11.36/3.76 tff(uri_rdf_object, type, uri_rdf_object: $i). % 11.36/3.76 tff(uri_rdfs_Class, type, uri_rdfs_Class: $i). % 11.36/3.76 tff(uri_rdfs_Seq, type, uri_rdfs_Seq: $i). % 11.36/3.76 tff(iext, type, iext: ($i * $i * $i) > $o). % 11.36/3.76 tff(uri_rdfs_member, type, uri_rdfs_member: $i). % 11.36/3.76 tff(uri_rdf_Bag, type, uri_rdf_Bag: $i). % 11.36/3.76 tff(uri_rdf__2, type, uri_rdf__2: $i). % 11.36/3.76 tff(uri_rdfs_comment, type, uri_rdfs_comment: $i). % 11.36/3.76 tff(uri_rdfs_Literal, type, uri_rdfs_Literal: $i). % 11.36/3.76 tff(uri_rdf_Alt, type, uri_rdf_Alt: $i). % 11.36/3.76 tff(uri_rdf_nil, type, uri_rdf_nil: $i). % 11.36/3.76 tff(uri_ex_o, type, uri_ex_o: $i). % 11.36/3.76 tff(uri_rdfs_isDefinedBy, type, uri_rdfs_isDefinedBy: $i). % 11.36/3.76 tff(uri_rdfs_domain, type, uri_rdfs_domain: $i). % 11.36/3.76 % 11.36/3.76 %Saturated clause set: % 11.36/3.76 tff(c_7198, 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)))). % 11.36/3.76 tff(c_7571, 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)))). % 11.36/3.77 tff(c_7199, 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)))). % 11.36/3.77 tff(c_7572, 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)))). % 11.36/3.77 tff(c_6316, 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_XMLLiteral)))). % 11.36/3.77 tff(c_6880, 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_Bag)))). % 11.36/3.77 tff(c_6590, plain, (![C_28, C_352]: (iext(uri_rdfs_subClassOf, C_28, uri_rdfs_Resource) | ~iext(uri_rdfs_subClassOf, C_28, C_352) | ~iext(uri_rdfs_subClassOf, C_352, uri_rdf_Alt)))). % 11.36/3.77 tff(c_6317, 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_XMLLiteral)))). % 11.36/3.77 tff(c_6591, plain, (![Q_32, C_352]: (iext(Q_32, C_352, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_32) | ~iext(uri_rdfs_subClassOf, C_352, uri_rdf_Alt)))). % 11.36/3.77 tff(c_6879, 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_Bag)))). % 11.36/3.77 tff(c_3970, 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_Alt)))). % 11.36/3.77 tff(c_8017, plain, (~iext(uri_rdfs_subClassOf, uri_rdfs_Container, uri_rdf_XMLLiteral))). % 11.36/3.77 tff(c_4432, plain, (![C_28, C_271]: (iext(uri_rdfs_subClassOf, C_28, uri_rdfs_Literal) | ~iext(uri_rdfs_subClassOf, C_28, C_271) | ~iext(uri_rdfs_subClassOf, C_271, uri_rdf_XMLLiteral)))). % 11.36/3.77 tff(c_4433, plain, (![Q_32, C_271]: (iext(Q_32, C_271, uri_rdfs_Literal) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_32) | ~iext(uri_rdfs_subClassOf, C_271, uri_rdf_XMLLiteral)))). % 11.36/3.77 tff(c_7926, plain, (~iext(uri_rdfs_subPropertyOf, uri_rdfs_member, uri_rdfs_isDefinedBy))). % 11.36/3.77 tff(c_4670, plain, (![P_38, P_277]: (iext(uri_rdfs_subPropertyOf, P_38, uri_rdfs_seeAlso) | ~iext(uri_rdfs_subPropertyOf, P_38, P_277) | ~iext(uri_rdfs_subPropertyOf, P_277, uri_rdfs_isDefinedBy)))). % 11.36/3.77 tff(c_4672, plain, (![Q_32, P_277]: (iext(Q_32, P_277, uri_rdfs_seeAlso) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_32) | ~iext(uri_rdfs_subPropertyOf, P_277, uri_rdfs_isDefinedBy)))). % 11.36/3.77 tff(c_4201, plain, (![C_28, C_269]: (iext(uri_rdfs_subClassOf, C_28, uri_rdfs_Container) | ~iext(uri_rdfs_subClassOf, C_28, C_269) | ~iext(uri_rdfs_subClassOf, C_269, uri_rdf_Bag)))). % 11.36/3.77 tff(c_3969, 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_Alt)))). % 11.36/3.77 tff(c_4202, plain, (![Q_32, C_269]: (iext(Q_32, C_269, uri_rdfs_Container) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_32) | ~iext(uri_rdfs_subClassOf, C_269, uri_rdf_Bag)))). % 11.36/3.77 tff(c_6043, 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)))). % 11.36/3.77 tff(c_6042, 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)))). % 11.36/3.77 tff(c_7623, plain, (~icext(uri_rdfs_ContainerMembershipProperty, uri_rdfs_seeAlso))). % 11.36/3.77 tff(c_1928, plain, (![P_113, P_10]: (iext(uri_rdfs_subPropertyOf, P_113, uri_rdfs_member) | ~iext(uri_rdfs_subPropertyOf, P_113, P_10) | ~icext(uri_rdfs_ContainerMembershipProperty, P_10)))). % 11.36/3.77 tff(c_1781, plain, (![Q_105, D_11]: (iext(Q_105, D_11, uri_rdfs_Literal) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_105) | ~icext(uri_rdfs_Datatype, D_11)))). % 11.36/3.77 tff(c_5620, plain, (![Q_32]: (iext(Q_32, uri_rdf_XMLLiteral, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_32)))). % 11.36/3.77 tff(c_5572, plain, (![C_28]: (iext(uri_rdfs_subClassOf, C_28, uri_rdfs_Resource) | ~iext(uri_rdfs_subClassOf, C_28, uri_rdfs_ContainerMembershipProperty)))). % 11.36/3.77 tff(c_5768, plain, (![Q_32]: (iext(Q_32, uri_rdfs_Seq, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_32)))). % 11.36/3.77 tff(c_7287, plain, (~icext(uri_rdfs_Datatype, uri_rdfs_Container))). % 11.36/3.77 tff(c_1884, plain, (![C_110, D_11]: (iext(uri_rdfs_subClassOf, C_110, uri_rdfs_Literal) | ~iext(uri_rdfs_subClassOf, C_110, D_11) | ~icext(uri_rdfs_Datatype, D_11)))). % 11.36/3.77 tff(c_5767, plain, (![C_28]: (iext(uri_rdfs_subClassOf, C_28, uri_rdfs_Resource) | ~iext(uri_rdfs_subClassOf, C_28, uri_rdfs_Seq)))). % 11.36/3.77 tff(c_5735, plain, (![C_28]: (iext(uri_rdfs_subClassOf, C_28, uri_rdfs_Resource) | ~iext(uri_rdfs_subClassOf, C_28, uri_rdfs_Datatype)))). % 11.36/3.77 tff(c_5736, plain, (![Q_32]: (iext(Q_32, uri_rdfs_Datatype, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_32)))). % 11.36/3.77 tff(c_5573, plain, (![Q_32]: (iext(Q_32, uri_rdfs_ContainerMembershipProperty, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_32)))). % 11.36/3.77 tff(c_5684, plain, (![Q_32]: (iext(Q_32, uri_rdf_Alt, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_32)))). % 11.36/3.77 tff(c_5506, plain, (![C_110]: (iext(uri_rdfs_subClassOf, C_110, uri_rdfs_Resource) | ~iext(uri_rdfs_subClassOf, C_110, uri_rdf_Bag)))). % 11.36/3.77 tff(c_1780, plain, (![Q_105, P_10]: (iext(Q_105, P_10, uri_rdfs_member) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_105) | ~icext(uri_rdfs_ContainerMembershipProperty, P_10)))). % 11.36/3.77 tff(c_5509, plain, (![C_110]: (iext(uri_rdfs_subClassOf, C_110, uri_rdfs_Resource) | ~iext(uri_rdfs_subClassOf, C_110, uri_rdf_Alt)))). % 11.36/3.77 tff(c_5503, plain, (![C_110]: (iext(uri_rdfs_subClassOf, C_110, uri_rdfs_Resource) | ~iext(uri_rdfs_subClassOf, C_110, uri_rdf_XMLLiteral)))). % 11.36/3.77 tff(c_5512, plain, (![D_11]: (iext(uri_rdfs_subClassOf, D_11, uri_rdfs_Resource) | ~icext(uri_rdfs_Datatype, D_11)))). % 11.36/3.77 tff(c_5534, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Seq, uri_rdfs_Resource))). % 11.36/3.77 tff(c_5522, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, uri_rdfs_Resource))). % 11.36/3.77 tff(c_5652, plain, (![Q_32]: (iext(Q_32, uri_rdf_Bag, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_32)))). % 11.36/3.77 tff(c_5525, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Alt, uri_rdfs_Resource))). % 11.36/3.77 tff(c_5528, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Bag, uri_rdfs_Resource))). % 11.36/3.77 tff(c_5531, plain, (iext(uri_rdfs_subClassOf, uri_rdf_XMLLiteral, uri_rdfs_Resource))). % 11.36/3.77 tff(c_1779, plain, (![Q_105, X_7, C_8]: (iext(Q_105, X_7, C_8) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_105) | ~icext(C_8, X_7)))). % 11.36/3.77 tff(c_5519, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, uri_rdfs_Resource))). % 11.36/3.77 tff(c_1885, plain, (![C_110, C_9]: (iext(uri_rdfs_subClassOf, C_110, uri_rdfs_Resource) | ~iext(uri_rdfs_subClassOf, C_110, C_9) | ~ic(C_9)))). % 11.36/3.77 tff(c_1782, plain, (![Q_105, P_6]: (iext(Q_105, P_6, uri_rdf_Property) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_105) | ~ip(P_6)))). % 11.36/3.77 tff(c_5434, plain, (![C_100]: (icext(C_100, uri_rdfs_member) | ~iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_100)))). % 11.36/3.77 tff(c_5438, plain, (![P_339]: (icext(uri_rdf_Property, P_339) | ~icext(uri_rdfs_ContainerMembershipProperty, P_339)))). % 11.36/3.77 tff(c_1346, plain, (![C_95, P_10]: (icext(C_95, P_10) | ~iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_95) | ~icext(uri_rdfs_ContainerMembershipProperty, P_10)))). % 11.36/3.77 tff(c_5422, plain, (![D_336]: (icext(uri_rdfs_Class, D_336) | ~icext(uri_rdfs_Datatype, D_336)))). % 11.36/3.77 tff(c_1347, plain, (![C_95, D_11]: (icext(C_95, D_11) | ~iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_95) | ~icext(uri_rdfs_Datatype, D_11)))). % 11.36/3.77 tff(c_5418, plain, (~iext(uri_rdfs_subClassOf, uri_rdfs_Literal, uri_rdf_Bag))). % 11.36/3.77 tff(c_5252, plain, (![C_331, X_332]: (icext(uri_rdfs_Class, C_331) | ~icext(C_331, X_332)))). % 11.36/3.78 tff(c_5248, plain, (~iext(uri_rdfs_subClassOf, uri_rdfs_Literal, uri_rdf_Alt))). % 11.36/3.78 tff(c_1563, plain, (![C_100, C_8, X_7]: (icext(C_100, C_8) | ~iext(uri_rdfs_range, uri_rdf_type, C_100) | ~icext(C_8, X_7)))). % 11.36/3.78 tff(c_1785, plain, (![Q_105, C_27]: (iext(Q_105, C_27, C_27) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_105) | ~ic(C_27)))). % 11.36/3.78 tff(c_5232, plain, (~iext(uri_rdfs_subPropertyOf, uri_ex_p, uri_rdfs_isDefinedBy))). % 11.36/3.78 tff(c_1783, plain, (![Q_105, P_37]: (iext(Q_105, P_37, P_37) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_105) | ~ip(P_37)))). % 11.36/3.78 tff(c_1345, plain, (![C_95, X_7, C_8]: (icext(C_95, X_7) | ~iext(uri_rdfs_domain, uri_rdf_type, C_95) | ~icext(C_8, X_7)))). % 11.36/3.78 tff(c_1996, plain, (![D_24, P_117]: (icext(D_24, P_117) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24) | ~ip(P_117)))). % 11.36/3.78 tff(c_1784, plain, (![Q_105, C_9]: (iext(Q_105, C_9, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_105) | ~ic(C_9)))). % 11.36/3.78 tff(c_1348, plain, (![C_95, P_6]: (icext(C_95, P_6) | ~iext(uri_rdfs_domain, uri_rdf_type, C_95) | ~ip(P_6)))). % 11.36/3.78 tff(c_5156, plain, (![C_100]: (icext(C_100, uri_rdfs_Resource) | ~iext(uri_rdfs_range, uri_rdfs_subClassOf, C_100)))). % 11.36/3.78 tff(c_5136, plain, (~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, uri_rdfs_isDefinedBy))). % 11.36/3.78 tff(c_1567, plain, (![C_100, P_37]: (icext(C_100, P_37) | ~iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_100) | ~ip(P_37)))). % 11.36/3.78 tff(c_1197, plain, (![D_92, X_18]: (icext(D_92, X_18) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Literal, D_92) | ~lv(X_18)))). % 11.36/3.78 tff(c_1569, plain, (![C_100, C_27]: (icext(C_100, C_27) | ~iext(uri_rdfs_range, uri_rdfs_subClassOf, C_100) | ~ic(C_27)))). % 11.36/3.78 tff(c_5098, plain, (~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, uri_rdfs_isDefinedBy))). % 11.36/3.78 tff(c_1198, plain, (![D_92, X_16]: (icext(D_92, X_16) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_92) | ~ic(X_16)))). % 11.36/3.78 tff(c_5064, plain, (~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, uri_rdfs_isDefinedBy))). % 11.36/3.78 tff(c_1350, plain, (![C_95, C_9]: (icext(C_95, C_9) | ~iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_95) | ~ic(C_9)))). % 11.36/3.78 tff(c_5063, plain, (~iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, uri_rdfs_isDefinedBy))). % 11.36/3.78 tff(c_1349, plain, (![C_95, P_37]: (icext(C_95, P_37) | ~iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_95) | ~ip(P_37)))). % 11.36/3.78 tff(c_1818, plain, (![Q_105]: (iext(Q_105, uri_rdfs_ContainerMembershipProperty, uri_rdf_Property) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_105)))). % 11.36/3.78 tff(c_1814, plain, (![Q_105]: (iext(Q_105, uri_rdf__2, uri_rdf_Property) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_105)))). % 11.36/3.78 tff(c_1892, plain, (![C_110]: (iext(uri_rdfs_subClassOf, C_110, uri_rdfs_Container) | ~iext(uri_rdfs_subClassOf, C_110, uri_rdfs_Seq)))). % 11.36/3.78 tff(c_1797, plain, (![Q_105]: (iext(Q_105, uri_rdf__3, uri_rdfs_ContainerMembershipProperty) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_105)))). % 11.36/3.78 tff(c_1844, plain, (![Q_105]: (iext(Q_105, uri_rdf_first, uri_rdf_Property) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_105)))). % 11.36/3.78 tff(c_1794, plain, (![Q_105]: (iext(Q_105, uri_rdf__1, uri_rdf_Property) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_105)))). % 11.36/3.78 tff(c_1829, plain, (![Q_105]: (iext(Q_105, uri_rdf_rest, uri_rdf_List) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_105)))). % 11.36/3.78 tff(c_1843, plain, (![Q_105]: (iext(Q_105, uri_rdf_nil, uri_rdf_List) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_105)))). % 11.36/3.78 tff(c_1824, plain, (![Q_105]: (iext(Q_105, uri_rdf_XMLLiteral, uri_rdfs_Datatype) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_105)))). % 11.36/3.78 tff(c_1786, plain, (![Q_105]: (iext(Q_105, uri_rdf_type, uri_rdf_Property) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_105)))). % 11.36/3.78 tff(c_1846, plain, (![Q_105]: (iext(Q_105, uri_rdfs_Seq, uri_rdfs_Container) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_105)))). % 11.36/3.78 tff(c_1833, plain, (![Q_105]: (iext(Q_105, uri_rdf_object, uri_rdf_Property) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_105)))). % 11.36/3.78 tff(c_1827, plain, (![Q_105]: (iext(Q_105, uri_rdf_subject, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_105)))). % 11.36/3.78 tff(c_1799, plain, (![Q_105]: (iext(Q_105, uri_rdf_value, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_105)))). % 11.36/3.78 tff(c_1837, plain, (![Q_105]: (iext(Q_105, uri_rdf_Bag, uri_rdfs_Container) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_105)))). % 11.36/3.78 tff(c_1791, plain, (![Q_105]: (iext(Q_105, uri_rdf__1, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_105)))). % 11.36/3.78 tff(c_1813, plain, (![Q_105]: (iext(Q_105, uri_rdf_Property, uri_rdfs_Class) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_105)))). % 11.36/3.78 tff(c_1793, plain, (![Q_105]: (iext(Q_105, uri_rdf_predicate, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_105)))). % 11.36/3.78 tff(c_1798, plain, (![Q_105]: (iext(Q_105, uri_rdf_subject, uri_rdfs_Statement) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_105)))). % 11.36/3.78 tff(c_1831, plain, (![Q_105]: (iext(Q_105, uri_rdfs_domain, uri_rdfs_Class) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_105)))). % 11.36/3.78 tff(c_1801, plain, (![Q_105]: (iext(Q_105, uri_rdfs_subClassOf, uri_rdfs_Class) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_105)))). % 11.36/3.78 tff(c_1787, plain, (![Q_105]: (iext(Q_105, uri_rdfs_isDefinedBy, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_105)))). % 11.36/3.78 tff(c_1788, plain, (![Q_105]: (iext(Q_105, uri_rdf_first, uri_rdf_List) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_105)))). % 11.36/3.78 tff(c_1888, plain, (![C_110]: (iext(uri_rdfs_subClassOf, C_110, uri_rdfs_Class) | ~iext(uri_rdfs_subClassOf, C_110, uri_rdfs_Datatype)))). % 11.36/3.78 tff(c_4712, plain, (~icext(uri_rdfs_ContainerMembershipProperty, uri_rdfs_subPropertyOf))). % 11.36/3.78 tff(c_1826, plain, (![Q_105]: (iext(Q_105, uri_rdfs_isDefinedBy, uri_rdfs_seeAlso) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subPropertyOf, Q_105)))). % 11.36/3.78 tff(c_1828, plain, (![Q_105]: (iext(Q_105, uri_rdfs_isDefinedBy, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_105)))). % 11.36/3.78 tff(c_4681, plain, (~iext(uri_rdfs_subClassOf, uri_rdf_List, uri_rdf_Bag))). % 11.36/3.78 tff(c_4680, plain, (~iext(uri_rdfs_subPropertyOf, uri_rdf_type, uri_rdfs_isDefinedBy))). % 11.36/3.78 tff(c_1930, plain, (![P_113]: (iext(uri_rdfs_subPropertyOf, P_113, uri_rdfs_seeAlso) | ~iext(uri_rdfs_subPropertyOf, P_113, uri_rdfs_isDefinedBy)))). % 11.36/3.78 tff(c_4493, plain, (~iext(uri_rdfs_subClassOf, uri_rdf_List, uri_rdf_XMLLiteral))). % 11.36/3.78 tff(c_1795, plain, (![Q_105]: (iext(Q_105, uri_rdf__1, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_105)))). % 11.36/3.78 tff(c_1800, plain, (![Q_105]: (iext(Q_105, uri_rdf_rest, uri_rdf_Property) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_105)))). % 11.36/3.78 tff(c_4481, plain, (~iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, uri_rdf_XMLLiteral))). % 11.36/3.78 tff(c_4480, plain, (~icext(uri_rdfs_ContainerMembershipProperty, uri_ex_p))). % 11.36/3.78 tff(c_1819, plain, (![Q_105]: (iext(Q_105, uri_ex_s, uri_ex_o) | ~iext(uri_rdfs_subPropertyOf, uri_ex_p, Q_105)))). % 11.36/3.78 tff(c_4468, plain, (~iext(uri_rdfs_subClassOf, uri_rdf_Property, uri_rdf_Bag))). % 11.36/3.78 tff(c_1845, plain, (![Q_105]: (iext(Q_105, uri_rdf_XMLLiteral, uri_rdfs_Literal) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_105)))). % 11.36/3.78 tff(c_4456, plain, (~iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, uri_rdf_XMLLiteral))). % 11.36/3.78 tff(c_4455, plain, (~iext(uri_rdfs_subClassOf, uri_rdfs_Class, uri_rdf_XMLLiteral))). % 11.36/3.78 tff(c_4443, plain, (~iext(uri_rdfs_subClassOf, uri_rdf_Property, uri_rdf_XMLLiteral))). % 11.36/3.78 tff(c_1815, plain, (![Q_105]: (iext(Q_105, uri_rdf_subject, uri_rdf_Property) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_105)))). % 11.36/3.78 tff(c_4442, plain, (~iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, uri_rdf_Bag))). % 11.36/3.78 tff(c_4441, plain, (~iext(uri_rdfs_subClassOf, uri_rdfs_Resource, uri_rdf_XMLLiteral))). % 11.36/3.78 tff(c_1891, plain, (![C_110]: (iext(uri_rdfs_subClassOf, C_110, uri_rdfs_Literal) | ~iext(uri_rdfs_subClassOf, C_110, uri_rdf_XMLLiteral)))). % 11.36/3.78 tff(c_4224, plain, (~iext(uri_rdfs_subClassOf, uri_rdf_List, uri_rdf_Alt))). % 11.36/3.79 tff(c_1808, plain, (![Q_105]: (iext(Q_105, uri_rdfs_subClassOf, uri_rdfs_Class) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_105)))). % 11.36/3.79 tff(c_4212, plain, (~iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, uri_rdf_Bag))). % 11.36/3.79 tff(c_4211, plain, (~iext(uri_rdfs_subClassOf, uri_rdfs_Class, uri_rdf_Bag))). % 11.36/3.79 tff(c_4210, plain, (~iext(uri_rdfs_subClassOf, uri_rdfs_Resource, uri_rdf_Bag))). % 11.36/3.79 tff(c_1890, plain, (![C_110]: (iext(uri_rdfs_subClassOf, C_110, uri_rdfs_Container) | ~iext(uri_rdfs_subClassOf, C_110, uri_rdf_Bag)))). % 11.36/3.79 tff(c_3993, plain, (~iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, uri_rdf_Alt))). % 11.36/3.79 tff(c_3992, plain, (~iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, uri_rdf_Alt))). % 11.36/3.79 tff(c_3991, plain, (~iext(uri_rdfs_subClassOf, uri_rdfs_Class, uri_rdf_Alt))). % 11.36/3.79 tff(c_1810, plain, (![Q_105]: (iext(Q_105, uri_rdf_value, uri_rdf_Property) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_105)))). % 11.36/3.79 tff(c_3979, plain, (~iext(uri_rdfs_subClassOf, uri_rdf_Property, uri_rdf_Alt))). % 11.36/3.79 tff(c_3978, plain, (~iext(uri_rdfs_subClassOf, uri_rdfs_Resource, uri_rdf_Alt))). % 11.36/3.79 tff(c_1889, plain, (![C_110]: (iext(uri_rdfs_subClassOf, C_110, uri_rdfs_Container) | ~iext(uri_rdfs_subClassOf, C_110, uri_rdf_Alt)))). % 11.36/3.79 tff(c_1832, plain, (![Q_105]: (iext(Q_105, uri_rdfs_range, uri_rdfs_Class) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_105)))). % 11.36/3.79 tff(c_1811, plain, (![Q_105]: (iext(Q_105, uri_rdfs_seeAlso, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_105)))). % 11.36/3.79 tff(c_1842, plain, (![Q_105]: (iext(Q_105, uri_rdfs_range, uri_rdf_Property) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_105)))). % 11.36/3.79 tff(c_1806, plain, (![Q_105]: (iext(Q_105, uri_rdf__3, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_105)))). % 11.36/3.79 tff(c_1830, plain, (![Q_105]: (iext(Q_105, uri_rdf_Alt, uri_rdfs_Container) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_105)))). % 11.36/3.79 tff(c_1822, plain, (![Q_105]: (iext(Q_105, uri_rdf_first, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_105)))). % 11.36/3.79 tff(c_1796, plain, (![Q_105]: (iext(Q_105, uri_rdf__2, uri_rdfs_ContainerMembershipProperty) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_105)))). % 11.36/3.79 tff(c_1790, plain, (![Q_105]: (iext(Q_105, uri_rdf_rest, uri_rdf_List) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_105)))). % 11.36/3.79 tff(c_1812, plain, (![Q_105]: (iext(Q_105, uri_rdfs_seeAlso, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_105)))). % 11.36/3.79 tff(c_3651, plain, (~icext(uri_rdfs_ContainerMembershipProperty, uri_rdfs_subClassOf))). % 11.36/3.79 tff(c_1816, plain, (![Q_105]: (iext(Q_105, uri_rdf__2, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_105)))). % 11.36/3.79 tff(c_1820, plain, (![Q_105]: (iext(Q_105, uri_rdfs_Datatype, uri_rdfs_Class) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_subClassOf, Q_105)))). % 11.36/3.79 tff(c_1840, plain, (![Q_105]: (iext(Q_105, uri_rdfs_comment, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_105)))). % 11.36/3.79 tff(c_1836, plain, (![Q_105]: (iext(Q_105, uri_rdf__3, uri_rdf_Property) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_105)))). % 11.36/3.79 tff(c_1789, plain, (![Q_105]: (iext(Q_105, uri_rdf_type, uri_rdfs_Class) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_105)))). % 11.36/3.79 tff(c_1841, plain, (![Q_105]: (iext(Q_105, uri_rdfs_domain, uri_rdf_Property) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_105)))). % 11.36/3.79 tff(c_1805, plain, (![Q_105]: (iext(Q_105, uri_rdfs_label, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_105)))). % 11.36/3.79 tff(c_1792, plain, (![Q_105]: (iext(Q_105, uri_rdf__2, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_105)))). % 11.36/3.79 tff(c_1809, plain, (![Q_105]: (iext(Q_105, uri_rdf__3, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_105)))). % 11.36/3.79 tff(c_1803, plain, (![Q_105]: (iext(Q_105, uri_rdf__1, uri_rdfs_ContainerMembershipProperty) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_105)))). % 11.36/3.79 tff(c_1835, plain, (![Q_105]: (iext(Q_105, uri_rdf_object, uri_rdfs_Statement) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_105)))). % 11.36/3.79 tff(c_1802, plain, (![Q_105]: (iext(Q_105, uri_rdf_type, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_105)))). % 11.36/3.79 tff(c_1834, plain, (![Q_105]: (iext(Q_105, uri_rdfs_member, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_105)))). % 11.36/3.79 tff(c_1821, plain, (![Q_105]: (iext(Q_105, uri_rdfs_label, uri_rdfs_Literal) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_105)))). % 11.36/3.79 tff(c_1839, plain, (![Q_105]: (iext(Q_105, uri_rdfs_subPropertyOf, uri_rdf_Property) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_105)))). % 11.36/3.79 tff(c_1825, plain, (![Q_105]: (iext(Q_105, uri_rdf_value, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_105)))). % 11.36/3.79 tff(c_2086, plain, (![D_24]: (icext(D_24, uri_rdfs_ContainerMembershipProperty) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_24)))). % 11.36/3.79 tff(c_2262, plain, (![D_24]: (icext(D_24, uri_rdfs_isDefinedBy) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))). % 11.36/3.79 tff(c_2105, plain, (![D_24]: (icext(D_24, uri_rdf_Alt) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_24)))). % 11.36/3.79 tff(c_2305, plain, (![D_24]: (icext(D_24, uri_rdfs_member) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))). % 11.36/3.79 tff(c_2175, plain, (![D_24]: (icext(D_24, uri_rdf_predicate) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))). % 11.36/3.79 tff(c_2188, plain, (![D_24]: (icext(D_24, uri_rdfs_subClassOf) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))). % 11.36/3.79 tff(c_2335, plain, (![D_24]: (icext(D_24, uri_rdf_List) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_24)))). % 11.36/3.79 tff(c_1817, plain, (![Q_105]: (iext(Q_105, uri_rdf_predicate, uri_rdfs_Statement) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_105)))). % 11.36/3.79 tff(c_2273, plain, (![D_24]: (icext(D_24, uri_rdfs_Statement) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_24)))). % 11.36/3.79 tff(c_2374, plain, (![D_24]: (icext(D_24, uri_rdfs_comment) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))). % 11.36/3.79 tff(c_2347, plain, (![D_24]: (icext(D_24, uri_rdfs_Container) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_24)))). % 11.36/3.79 tff(c_2168, plain, (![D_24]: (icext(D_24, uri_rdfs_label) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))). % 11.36/3.79 tff(c_2360, plain, (![D_24]: (icext(D_24, uri_rdf_XMLLiteral) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_24)))). % 11.36/3.79 tff(c_2137, plain, (![D_24]: (icext(D_24, uri_rdfs_Literal) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_24)))). % 11.36/3.79 tff(c_2241, plain, (![D_24]: (icext(D_24, uri_rdfs_Class) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_24)))). % 11.36/3.79 tff(c_2324, plain, (![D_24]: (icext(D_24, uri_rdfs_seeAlso) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))). % 11.36/3.79 tff(c_2613, plain, (![D_24]: (icext(D_24, uri_rdfs_Seq) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_24)))). % 11.36/3.79 tff(c_1887, plain, (![C_110]: (iext(uri_rdfs_subClassOf, C_110, uri_rdf_Property) | ~iext(uri_rdfs_subClassOf, C_110, uri_rdfs_ContainerMembershipProperty)))). % 11.36/3.79 tff(c_2387, plain, (![D_24]: (icext(D_24, uri_rdfs_range) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))). % 11.36/3.79 tff(c_2477, plain, (![D_24]: (icext(D_24, uri_rdf_Bag) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_24)))). % 11.36/3.79 tff(c_2428, plain, (![D_24]: (icext(D_24, uri_rdfs_Datatype) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_24)))). % 11.36/3.79 tff(c_2577, plain, (![D_24]: (icext(D_24, uri_rdfs_domain) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))). % 11.36/3.79 tff(c_3046, plain, (~icext(uri_rdfs_Datatype, uri_rdf_List))). % 11.36/3.79 tff(c_2126, plain, (![D_24]: (icext(D_24, uri_rdfs_subPropertyOf) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))). % 11.36/3.79 tff(c_1933, plain, (![D_24]: (icext(D_24, uri_rdf_nil) | ~iext(uri_rdfs_subClassOf, uri_rdf_List, D_24)))). % 11.36/3.79 tff(c_1920, plain, (![D_24]: (icext(D_24, uri_rdf__2) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))). % 11.36/3.79 tff(c_1804, plain, (![Q_105]: (iext(Q_105, uri_rdfs_comment, uri_rdfs_Literal) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_105)))). % 11.36/3.79 tff(c_1917, plain, (![D_24]: (icext(D_24, uri_rdf_rest) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))). % 11.36/3.79 tff(c_1946, plain, (![D_24]: (icext(D_24, uri_rdf_subject) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))). % 11.36/3.79 tff(c_2954, plain, (~icext(uri_rdfs_ContainerMembershipProperty, uri_rdfs_domain))). % 11.36/3.79 tff(c_2933, plain, (~icext(uri_rdfs_ContainerMembershipProperty, uri_rdfs_range))). % 11.36/3.79 tff(c_1906, plain, (![D_24]: (icext(D_24, uri_rdf_type) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))). % 11.36/3.79 tff(c_1955, plain, (![D_24]: (icext(D_24, uri_rdf__2) | ~iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, D_24)))). % 11.36/3.79 tff(c_1961, plain, (![D_24]: (icext(D_24, uri_rdf_object) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))). % 11.36/3.79 tff(c_1807, plain, (![Q_105]: (iext(Q_105, uri_rdfs_subPropertyOf, uri_rdf_Property) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_domain, Q_105)))). % 11.36/3.79 tff(c_1936, plain, (![D_24]: (icext(D_24, uri_rdf_value) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))). % 11.36/3.79 tff(c_1949, plain, (![D_24]: (icext(D_24, uri_rdf__1) | ~iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, D_24)))). % 11.36/3.79 tff(c_1958, plain, (![D_24]: (icext(D_24, uri_rdf_first) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))). % 11.36/3.79 tff(c_1939, plain, (![D_24]: (icext(D_24, uri_rdf__1) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))). % 11.36/3.79 tff(c_2791, plain, (~icext(uri_rdfs_Datatype, uri_rdf_Property))). % 11.36/3.79 tff(c_1943, plain, (![D_24]: (icext(D_24, uri_rdf__3) | ~iext(uri_rdfs_subClassOf, uri_rdf_Property, D_24)))). % 11.36/3.79 tff(c_2770, plain, (~icext(uri_rdfs_Datatype, uri_rdfs_ContainerMembershipProperty))). % 11.36/3.79 tff(c_1823, plain, (![Q_105]: (iext(Q_105, uri_rdfs_member, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdfs_range, Q_105)))). % 11.36/3.80 tff(c_1964, plain, (![D_24]: (icext(D_24, uri_rdf__3) | ~iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, D_24)))). % 11.36/3.80 tff(c_1912, plain, (![D_24]: (icext(D_24, uri_rdf_Property) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_24)))). % 11.36/3.80 tff(c_2713, plain, (~icext(uri_rdfs_Datatype, uri_rdfs_Datatype))). % 11.36/3.80 tff(c_1952, plain, (![D_24]: (icext(D_24, uri_rdf_XMLLiteral) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, D_24)))). % 11.36/3.80 tff(c_1379, plain, (![C_95]: (icext(C_95, uri_rdf_Property) | ~iext(uri_rdfs_domain, uri_rdf_type, C_95)))). % 11.36/3.80 tff(c_1390, plain, (![C_95]: (icext(C_95, uri_rdf_XMLLiteral) | ~iext(uri_rdfs_domain, uri_rdf_type, C_95)))). % 11.36/3.80 tff(c_1623, plain, (![C_100]: (icext(C_100, uri_rdf_Property) | ~iext(uri_rdfs_range, uri_rdfs_range, C_100)))). % 11.36/3.80 tff(c_1397, plain, (![C_95]: (icext(C_95, uri_rdfs_domain) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_95)))). % 11.36/3.80 tff(c_1597, plain, (![C_100]: (icext(C_100, uri_rdfs_Class) | ~iext(uri_rdfs_range, uri_rdf_type, C_100)))). % 11.36/3.80 tff(c_1602, plain, (![C_100]: (icext(C_100, uri_rdf_Property) | ~iext(uri_rdfs_range, uri_rdfs_subClassOf, C_100)))). % 11.36/3.80 tff(c_1610, plain, (![C_100]: (icext(C_100, uri_rdfs_seeAlso) | ~iext(uri_rdfs_range, uri_rdfs_subPropertyOf, C_100)))). % 11.36/3.80 tff(c_1367, plain, (![C_95]: (icext(C_95, uri_rdfs_subClassOf) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_95)))). % 11.36/3.80 tff(c_1377, plain, (![C_95]: (icext(C_95, uri_rdfs_seeAlso) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_95)))). % 11.36/3.80 tff(c_1406, plain, (![C_95]: (icext(C_95, uri_rdfs_comment) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_95)))). % 11.36/3.80 tff(c_1362, plain, (![C_95]: (icext(C_95, uri_rdf__2) | ~iext(uri_rdfs_domain, uri_rdf_type, C_95)))). % 11.36/3.80 tff(c_1387, plain, (![C_95]: (icext(C_95, uri_rdfs_label) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_95)))). % 11.36/3.80 tff(c_2607, plain, (icext(uri_rdfs_Class, uri_rdfs_Seq))). % 11.36/3.80 tff(c_1412, plain, (![C_95]: (icext(C_95, uri_rdfs_Seq) | ~iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_95)))). % 11.36/3.80 tff(c_1400, plain, (![C_95]: (icext(C_95, uri_rdfs_member) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_95)))). % 11.36/3.80 tff(c_1604, plain, (![C_100]: (icext(C_100, uri_rdfs_Class) | ~iext(uri_rdfs_range, uri_rdfs_subClassOf, C_100)))). % 11.36/3.80 tff(c_1372, plain, (![C_95]: (icext(C_95, uri_rdf__3) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_95)))). % 11.36/3.80 tff(c_1375, plain, (![C_95]: (icext(C_95, uri_rdf__3) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_95)))). % 11.36/3.80 tff(c_1603, plain, (![C_100]: (icext(C_100, uri_ex_o) | ~iext(uri_rdfs_range, uri_ex_p, C_100)))). % 11.36/3.80 tff(c_2569, plain, (icext(uri_rdf_Property, uri_rdfs_domain))). % 11.36/3.80 tff(c_1407, plain, (![C_95]: (icext(C_95, uri_rdfs_domain) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_95)))). % 11.36/3.80 tff(c_1395, plain, (![C_95]: (icext(C_95, uri_rdf_rest) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_95)))). % 11.36/3.80 tff(c_1360, plain, (![C_95]: (icext(C_95, uri_rdf__1) | ~iext(uri_rdfs_domain, uri_rdf_type, C_95)))). % 11.36/3.80 tff(c_1386, plain, (![C_95]: (icext(C_95, uri_rdfs_Datatype) | ~iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_95)))). % 11.36/3.80 tff(c_1366, plain, (![C_95]: (icext(C_95, uri_rdf_rest) | ~iext(uri_rdfs_domain, uri_rdf_type, C_95)))). % 11.36/3.80 tff(c_1388, plain, (![C_95]: (icext(C_95, uri_rdf_first) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_95)))). % 11.36/3.80 tff(c_1399, plain, (![C_95]: (icext(C_95, uri_rdf_object) | ~iext(uri_rdfs_domain, uri_rdf_type, C_95)))). % 11.36/3.80 tff(c_1358, plain, (![C_95]: (icext(C_95, uri_rdf__2) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_95)))). % 11.36/3.80 tff(c_1384, plain, (![C_95]: (icext(C_95, uri_rdfs_ContainerMembershipProperty) | ~iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_95)))). % 11.36/3.80 tff(c_1383, plain, (![C_95]: (icext(C_95, uri_rdf_predicate) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_95)))). % 11.36/3.80 tff(c_1409, plain, (![C_95]: (icext(C_95, uri_rdf_nil) | ~iext(uri_rdfs_domain, uri_rdf_type, C_95)))). % 11.36/3.80 tff(c_1394, plain, (![C_95]: (icext(C_95, uri_rdfs_isDefinedBy) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_95)))). % 11.36/3.80 tff(c_1376, plain, (![C_95]: (icext(C_95, uri_rdf_value) | ~iext(uri_rdfs_domain, uri_rdf_type, C_95)))). % 11.36/3.80 tff(c_1385, plain, (![C_95]: (icext(C_95, uri_ex_s) | ~iext(uri_rdfs_domain, uri_ex_p, C_95)))). % 11.36/3.80 tff(c_1392, plain, (![C_95]: (icext(C_95, uri_rdfs_isDefinedBy) | ~iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, C_95)))). % 11.36/3.80 tff(c_1357, plain, (![C_95]: (icext(C_95, uri_rdf__1) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_95)))). % 11.36/3.80 tff(c_2471, plain, (icext(uri_rdfs_Class, uri_rdf_Bag))). % 11.36/3.80 tff(c_1403, plain, (![C_95]: (icext(C_95, uri_rdf_Bag) | ~iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_95)))). % 11.36/3.80 tff(c_1629, plain, (![C_100]: (icext(C_100, uri_rdfs_Literal) | ~iext(uri_rdfs_range, uri_rdfs_subClassOf, C_100)))). % 11.36/3.80 tff(c_1352, plain, (![C_95]: (icext(C_95, uri_rdf_type) | ~iext(uri_rdfs_domain, uri_rdf_type, C_95)))). % 11.36/3.80 tff(c_1401, plain, (![C_95]: (icext(C_95, uri_rdf_object) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_95)))). % 11.36/3.80 tff(c_1354, plain, (![C_95]: (icext(C_95, uri_rdf_first) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_95)))). % 11.36/3.80 tff(c_1572, plain, (![C_100]: (icext(C_100, uri_rdf_List) | ~iext(uri_rdfs_range, uri_rdfs_domain, C_100)))). % 11.36/3.80 tff(c_1627, plain, (![C_100]: (icext(C_100, uri_rdf_List) | ~iext(uri_rdfs_range, uri_rdf_type, C_100)))). % 11.36/3.80 tff(c_2422, plain, (icext(uri_rdfs_Class, uri_rdfs_Datatype))). % 11.36/3.80 tff(c_1608, plain, (![C_100]: (icext(C_100, uri_rdfs_Datatype) | ~iext(uri_rdfs_range, uri_rdf_type, C_100)))). % 11.36/3.80 tff(c_1393, plain, (![C_95]: (icext(C_95, uri_rdf_subject) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_95)))). % 11.36/3.80 tff(c_1408, plain, (![C_95]: (icext(C_95, uri_rdfs_range) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_95)))). % 11.36/3.80 tff(c_1361, plain, (![C_95]: (icext(C_95, uri_rdf__1) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_95)))). % 11.36/3.80 tff(c_1365, plain, (![C_95]: (icext(C_95, uri_rdf_value) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_95)))). % 11.36/3.80 tff(c_1585, plain, (![C_100]: (icext(C_100, uri_rdfs_Class) | ~iext(uri_rdfs_range, uri_rdfs_domain, C_100)))). % 11.36/3.80 tff(c_2379, plain, (icext(uri_rdf_Property, uri_rdfs_range))). % 11.36/3.80 tff(c_1398, plain, (![C_95]: (icext(C_95, uri_rdfs_range) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_95)))). % 11.36/3.80 tff(c_2373, plain, (ip(uri_rdfs_comment))). % 11.36/3.80 tff(c_2367, plain, (icext(uri_rdf_Property, uri_rdfs_comment))). % 11.36/3.80 tff(c_1370, plain, (![C_95]: (icext(C_95, uri_rdfs_comment) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_95)))). % 11.36/3.80 tff(c_2354, plain, (icext(uri_rdfs_Class, uri_rdf_XMLLiteral))). % 11.36/3.80 tff(c_1411, plain, (![C_95]: (icext(C_95, uri_rdf_XMLLiteral) | ~iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_95)))). % 11.36/3.80 tff(c_2341, plain, (icext(uri_rdfs_Class, uri_rdfs_Container))). % 11.36/3.80 tff(c_1621, plain, (![C_100]: (icext(C_100, uri_rdfs_Container) | ~iext(uri_rdfs_range, uri_rdfs_subClassOf, C_100)))). % 11.36/3.80 tff(c_2336, plain, (ic(uri_rdf_List))). % 11.36/3.80 tff(c_2329, plain, (icext(uri_rdfs_Class, uri_rdf_List))). % 11.36/3.80 tff(c_1613, plain, (![C_100]: (icext(C_100, uri_rdf_List) | ~iext(uri_rdfs_range, uri_rdfs_range, C_100)))). % 11.36/3.80 tff(c_2316, plain, (icext(uri_rdf_Property, uri_rdfs_seeAlso))). % 11.36/3.80 tff(c_1378, plain, (![C_95]: (icext(C_95, uri_rdfs_seeAlso) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_95)))). % 11.36/3.80 tff(c_1405, plain, (![C_95]: (icext(C_95, uri_rdfs_subPropertyOf) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_95)))). % 11.36/3.80 tff(c_2297, plain, (icext(uri_rdf_Property, uri_rdfs_member))). % 11.36/3.80 tff(c_1389, plain, (![C_95]: (icext(C_95, uri_rdfs_member) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_95)))). % 11.36/3.80 tff(c_1368, plain, (![C_95]: (icext(C_95, uri_rdf_type) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_95)))). % 11.36/3.80 tff(c_1382, plain, (![C_95]: (icext(C_95, uri_rdf__2) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_95)))). % 11.36/3.80 tff(c_1410, plain, (![C_95]: (icext(C_95, uri_rdf_first) | ~iext(uri_rdfs_domain, uri_rdf_type, C_95)))). % 11.36/3.80 tff(c_2274, plain, (ic(uri_rdfs_Statement))). % 11.36/3.80 tff(c_2267, plain, (icext(uri_rdfs_Class, uri_rdfs_Statement))). % 11.36/3.80 tff(c_1601, plain, (![C_100]: (icext(C_100, uri_rdfs_Statement) | ~iext(uri_rdfs_range, uri_rdfs_domain, C_100)))). % 11.36/3.80 tff(c_2254, plain, (icext(uri_rdf_Property, uri_rdfs_isDefinedBy))). % 11.36/3.80 tff(c_1353, plain, (![C_95]: (icext(C_95, uri_rdfs_isDefinedBy) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_95)))). % 11.36/3.80 tff(c_1391, plain, (![C_95]: (icext(C_95, uri_rdf_value) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_95)))). % 11.36/3.80 tff(c_2235, plain, (icext(uri_rdfs_Class, uri_rdfs_Class))). % 11.36/3.80 tff(c_1592, plain, (![C_100]: (icext(C_100, uri_rdfs_Class) | ~iext(uri_rdfs_range, uri_rdfs_range, C_100)))). % 11.36/3.80 tff(c_1355, plain, (![C_95]: (icext(C_95, uri_rdf_type) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_95)))). % 11.36/3.80 tff(c_2224, plain, (~icext(uri_rdfs_Datatype, uri_rdfs_Resource))). % 11.36/3.80 tff(c_1199, plain, (![D_92, X_17]: (icext(D_92, X_17) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Resource, D_92)))). % 11.36/3.80 tff(c_1381, plain, (![C_95]: (icext(C_95, uri_rdf_subject) | ~iext(uri_rdfs_domain, uri_rdf_type, C_95)))). % 11.36/3.80 tff(c_1364, plain, (![C_95]: (icext(C_95, uri_rdf_subject) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_95)))). % 11.36/3.80 tff(c_1402, plain, (![C_95]: (icext(C_95, uri_rdf__3) | ~iext(uri_rdfs_domain, uri_rdf_type, C_95)))). % 11.36/3.80 tff(c_2180, plain, (icext(uri_rdf_Property, uri_rdfs_subClassOf))). % 11.36/3.80 tff(c_2174, plain, (ip(uri_rdf_predicate))). % 11.36/3.80 tff(c_1374, plain, (![C_95]: (icext(C_95, uri_rdfs_subClassOf) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_95)))). % 11.36/3.80 tff(c_2161, plain, (icext(uri_rdf_Property, uri_rdf_predicate))). % 11.36/3.80 tff(c_2167, plain, (ip(uri_rdfs_label))). % 11.36/3.80 tff(c_2156, plain, (icext(uri_rdf_Property, uri_rdfs_label))). % 11.36/3.80 tff(c_1359, plain, (![C_95]: (icext(C_95, uri_rdf_predicate) | ~iext(uri_rdfs_domain, uri_rdfs_range, C_95)))). % 11.36/3.80 tff(c_1371, plain, (![C_95]: (icext(C_95, uri_rdfs_label) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_95)))). % 11.36/3.80 tff(c_1590, plain, (![C_100]: (icext(C_100, uri_rdfs_Resource) | ~iext(uri_rdfs_range, uri_rdfs_range, C_100)))). % 11.36/3.80 tff(c_1612, plain, (![C_100]: (icext(C_100, uri_rdfs_Resource) | ~iext(uri_rdfs_range, uri_rdfs_domain, C_100)))). % 11.36/3.80 tff(c_2131, plain, (icext(uri_rdfs_Class, uri_rdfs_Literal))). % 11.36/3.80 tff(c_1605, plain, (![C_100]: (icext(C_100, uri_rdfs_Literal) | ~iext(uri_rdfs_range, uri_rdfs_range, C_100)))). % 11.36/3.80 tff(c_2118, plain, (icext(uri_rdf_Property, uri_rdfs_subPropertyOf))). % 11.36/3.80 tff(c_1373, plain, (![C_95]: (icext(C_95, uri_rdfs_subPropertyOf) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_95)))). % 11.36/3.80 tff(c_1620, plain, (![C_100]: (icext(C_100, uri_rdf_Property) | ~iext(uri_rdfs_range, uri_rdf_type, C_100)))). % 11.36/3.80 tff(c_2099, plain, (icext(uri_rdfs_Class, uri_rdf_Alt))). % 11.36/3.80 tff(c_1396, plain, (![C_95]: (icext(C_95, uri_rdf_Alt) | ~iext(uri_rdfs_domain, uri_rdfs_subClassOf, C_95)))). % 11.36/3.80 tff(c_1625, plain, (![C_100]: (icext(C_100, uri_rdf_Property) | ~iext(uri_rdfs_range, uri_rdfs_domain, C_100)))). % 11.36/3.80 tff(c_2080, plain, (icext(uri_rdfs_Class, uri_rdfs_ContainerMembershipProperty))). % 11.36/3.80 tff(c_1587, plain, (![C_100]: (icext(C_100, uri_rdfs_ContainerMembershipProperty) | ~iext(uri_rdfs_range, uri_rdf_type, C_100)))). % 11.36/3.81 tff(c_1356, plain, (![C_95]: (icext(C_95, uri_rdf_rest) | ~iext(uri_rdfs_domain, uri_rdfs_domain, C_95)))). % 11.36/3.81 tff(c_2069, plain, (~icext(uri_rdfs_Datatype, uri_rdfs_Class))). % 11.36/3.81 tff(c_1183, plain, (![X_90]: (ip(X_90) | ~icext(uri_rdf_Property, X_90)))). % 11.36/3.81 tff(c_1084, plain, (![P_87]: (ip(P_87) | ~icext(uri_rdfs_ContainerMembershipProperty, P_87)))). % 11.36/3.81 tff(c_1067, plain, (![D_86]: (ic(D_86) | ~icext(uri_rdfs_Datatype, D_86)))). % 11.36/3.81 tff(c_1145, plain, (![P_6]: (icext(uri_rdf_Property, P_6) | ~ip(P_6)))). % 11.36/3.81 tff(c_1992, plain, (ip(uri_rdfs_member))). % 11.36/3.81 tff(c_1901, plain, (![D_24]: (icext(D_24, uri_rdfs_Resource) | ~iext(uri_rdfs_subClassOf, uri_rdfs_Class, D_24)))). % 11.36/3.81 tff(c_1940, plain, (~icext(uri_rdfs_ContainerMembershipProperty, uri_rdf_type))). % 11.36/3.81 tff(c_1149, plain, (icext(uri_rdfs_ContainerMembershipProperty, uri_rdf__3))). % 11.36/3.81 tff(c_1157, plain, (icext(uri_rdf_Property, uri_rdf_object))). % 11.36/3.81 tff(c_1162, plain, (icext(uri_rdf_Property, uri_rdf_first))). % 11.36/3.81 tff(c_1148, plain, (icext(uri_rdfs_ContainerMembershipProperty, uri_rdf__2))). % 11.36/3.81 tff(c_1156, plain, (icext(uri_rdfs_Datatype, uri_rdf_XMLLiteral))). % 11.36/3.81 tff(c_1151, plain, (icext(uri_rdfs_ContainerMembershipProperty, uri_rdf__1))). % 11.36/3.81 tff(c_1155, plain, (icext(uri_rdf_Property, uri_rdf_subject))). % 11.36/3.81 tff(c_1158, plain, (icext(uri_rdf_Property, uri_rdf__3))). % 11.36/3.81 tff(c_1147, plain, (icext(uri_rdf_Property, uri_rdf__1))). % 11.36/3.81 tff(c_1152, plain, (icext(uri_rdf_Property, uri_rdf_value))). % 11.36/3.81 tff(c_1161, plain, (icext(uri_rdf_List, uri_rdf_nil))). % 11.36/3.81 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)))). % 11.36/3.81 tff(c_1154, plain, (icext(uri_rdf_Property, uri_rdf__2))). % 11.36/3.81 tff(c_1150, plain, (icext(uri_rdf_Property, uri_rdf_rest))). % 11.36/3.81 tff(c_1153, plain, (icext(uri_rdfs_Class, uri_rdf_Property))). % 11.36/3.81 tff(c_1146, plain, (icext(uri_rdf_Property, uri_rdf_type))). % 11.36/3.81 tff(c_1053, plain, (ic(uri_rdf_XMLLiteral))). % 11.36/3.81 tff(c_1638, plain, (icext(uri_rdfs_Class, uri_rdfs_Resource))). % 11.36/3.81 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)))). % 11.36/3.81 tff(c_1051, plain, (ic(uri_rdf_Alt))). % 11.36/3.81 tff(c_1838, plain, (![Q_105]: (iext(Q_105, uri_ex_s, uri_rdfs_Resource) | ~iext(uri_rdfs_subPropertyOf, uri_rdf_type, Q_105)))). % 11.36/3.81 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)))). % 11.36/3.81 tff(c_726, plain, (ip(uri_rdf_value))). % 11.36/3.81 tff(c_1050, plain, (ic(uri_rdfs_Datatype))). % 11.36/3.81 tff(c_1622, plain, (![C_100]: (icext(C_100, uri_rdfs_Resource) | ~iext(uri_rdfs_range, uri_rdf_type, C_100)))). % 11.36/3.81 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)))). % 11.36/3.81 tff(c_1404, plain, (![C_95]: (icext(C_95, uri_ex_s) | ~iext(uri_rdfs_domain, uri_rdf_type, C_95)))). % 11.36/3.81 tff(c_727, plain, (ip(uri_rdf__2))). % 11.36/3.81 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)))). % 11.36/3.81 tff(c_1184, plain, (~icext(uri_owl_Thing, uri_ex_o))). % 11.36/3.81 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)))). % 11.36/3.81 tff(c_54, plain, (![X_7, C_8]: (iext(uri_rdf_type, X_7, C_8) | ~icext(C_8, X_7)))). % 11.36/3.81 tff(c_52, plain, (![C_8, X_7]: (icext(C_8, X_7) | ~iext(uri_rdf_type, X_7, C_8)))). % 11.36/3.81 tff(c_70, plain, (![P_10]: (iext(uri_rdfs_subPropertyOf, P_10, uri_rdfs_member) | ~icext(uri_rdfs_ContainerMembershipProperty, P_10)))). % 11.36/3.81 tff(c_1049, plain, (ic(uri_rdfs_ContainerMembershipProperty))). % 11.36/3.81 tff(c_102, plain, (![D_11]: (iext(uri_rdfs_subClassOf, D_11, uri_rdfs_Literal) | ~icext(uri_rdfs_Datatype, D_11)))). % 11.36/3.81 tff(c_725, plain, (ip(uri_rdf_rest))). % 11.36/3.81 tff(c_1052, plain, (ic(uri_rdf_Bag))). % 11.36/3.81 tff(c_1054, plain, (ic(uri_rdfs_Seq))). % 11.36/3.81 tff(c_150, plain, (![C_23, D_24]: (ic(C_23) | ~iext(uri_rdfs_subClassOf, C_23, D_24)))). % 11.36/3.81 tff(c_957, plain, (ip(uri_ex_p))). % 11.36/3.81 tff(c_28, plain, (![P_6]: (iext(uri_rdf_type, P_6, uri_rdf_Property) | ~ip(P_6)))). % 11.36/3.81 tff(c_730, plain, (ip(uri_rdf__3))). % 11.36/3.81 tff(c_1006, plain, (ip(uri_rdfs_isDefinedBy))). % 11.36/3.81 tff(c_164, plain, (![P_31, Q_32]: (ip(P_31) | ~iext(uri_rdfs_subPropertyOf, P_31, Q_32)))). % 11.36/3.81 tff(c_729, plain, (ip(uri_rdf_object))). % 11.36/3.81 tff(c_943, plain, (ip(uri_rdfs_domain))). % 11.36/3.81 tff(c_168, plain, (![P_37]: (iext(uri_rdfs_subPropertyOf, P_37, P_37) | ~ip(P_37)))). % 11.36/3.81 tff(c_728, plain, (ip(uri_rdf_subject))). % 11.36/3.81 tff(c_964, plain, (ip(uri_rdfs_subPropertyOf))). % 11.36/3.81 tff(c_965, plain, (ip(uri_rdfs_range))). % 11.36/3.81 tff(c_724, plain, (ip(uri_rdf__1))). % 11.36/3.81 tff(c_976, plain, (ip(uri_rdf_type))). % 11.36/3.81 tff(c_984, plain, (ip(uri_rdfs_subClassOf))). % 11.36/3.81 tff(c_731, plain, (ip(uri_rdf_first))). % 11.36/3.81 tff(c_2, plain, (![P_2, S_1, O_3]: (ip(P_2) | ~iext(P_2, S_1, O_3)))). % 11.36/3.81 tff(c_26, plain, (![P_6]: (ip(P_6) | ~iext(uri_rdf_type, P_6, uri_rdf_Property)))). % 11.36/3.81 tff(c_694, plain, (ic(uri_rdfs_Resource))). % 11.36/3.81 tff(c_56, plain, (![C_9]: (iext(uri_rdfs_subClassOf, C_9, uri_rdfs_Resource) | ~ic(C_9)))). % 11.36/3.81 tff(c_154, plain, (![C_27]: (iext(uri_rdfs_subClassOf, C_27, C_27) | ~ic(C_27)))). % 11.36/3.81 tff(c_674, plain, (ip(uri_rdfs_seeAlso))). % 11.36/3.81 tff(c_667, plain, (ic(uri_rdfs_Literal))). % 11.36/3.81 tff(c_162, plain, (![Q_32, P_31]: (ip(Q_32) | ~iext(uri_rdfs_subPropertyOf, P_31, Q_32)))). % 11.36/3.81 tff(c_665, plain, (ic(uri_rdfs_Container))). % 11.36/3.81 tff(c_664, plain, (ic(uri_rdfs_Class))). % 11.36/3.81 tff(c_663, plain, (ic(uri_rdf_Property))). % 11.36/3.81 tff(c_148, plain, (![D_24, C_23]: (ic(D_24) | ~iext(uri_rdfs_subClassOf, C_23, D_24)))). % 11.36/3.81 tff(c_120, plain, (![X_18]: (icext(uri_rdfs_Literal, X_18) | ~lv(X_18)))). % 11.36/3.81 tff(c_114, plain, (![X_16]: (ic(X_16) | ~icext(uri_rdfs_Class, X_16)))). % 11.36/3.81 tff(c_112, plain, (![X_16]: (icext(uri_rdfs_Class, X_16) | ~ic(X_16)))). % 11.36/3.81 tff(c_122, plain, (![X_18]: (lv(X_18) | ~icext(uri_rdfs_Literal, X_18)))). % 11.36/3.81 tff(c_32, plain, (iext(uri_rdf_type, uri_rdf_type, uri_rdf_Property))). % 11.36/3.81 tff(c_40, plain, (iext(uri_rdfs_range, uri_rdfs_isDefinedBy, uri_rdfs_Resource))). % 11.36/3.81 tff(c_58, plain, (iext(uri_rdfs_domain, uri_rdf_first, uri_rdf_List))). % 11.36/3.81 tff(c_174, plain, (iext(uri_rdfs_range, uri_rdf_type, uri_rdfs_Class))). % 11.36/3.81 tff(c_62, plain, (iext(uri_rdfs_domain, uri_rdf_rest, uri_rdf_List))). % 11.36/3.81 tff(c_78, plain, (iext(uri_rdfs_domain, uri_rdf__1, uri_rdfs_Resource))). % 11.36/3.81 tff(c_80, plain, (iext(uri_rdfs_domain, uri_rdf__2, uri_rdfs_Resource))). % 11.36/3.81 tff(c_138, plain, (iext(uri_rdfs_range, uri_rdf_predicate, uri_rdfs_Resource))). % 11.36/3.81 tff(c_14, plain, (iext(uri_rdf_type, uri_rdf__1, uri_rdf_Property))). % 11.36/3.81 tff(c_84, plain, (iext(uri_rdfs_range, uri_rdf__1, uri_rdfs_Resource))). % 11.36/3.81 tff(c_92, plain, (iext(uri_rdf_type, uri_rdf__2, uri_rdfs_ContainerMembershipProperty))). % 11.36/3.81 tff(c_94, plain, (iext(uri_rdf_type, uri_rdf__3, uri_rdfs_ContainerMembershipProperty))). % 11.36/3.81 tff(c_140, plain, (iext(uri_rdfs_domain, uri_rdf_subject, uri_rdfs_Statement))). % 11.36/3.81 tff(c_178, plain, (iext(uri_rdfs_range, uri_rdf_value, uri_rdfs_Resource))). % 11.36/3.81 tff(c_12, plain, (iext(uri_rdf_type, uri_rdf_rest, uri_rdf_Property))). % 11.36/3.81 tff(c_144, plain, (iext(uri_rdfs_domain, uri_rdfs_subClassOf, uri_rdfs_Class))). % 11.36/3.81 tff(c_172, plain, (iext(uri_rdfs_domain, uri_rdf_type, uri_rdfs_Resource))). % 11.36/3.81 tff(c_90, plain, (iext(uri_rdf_type, uri_rdf__1, uri_rdfs_ContainerMembershipProperty))). % 11.36/3.81 tff(c_36, plain, (iext(uri_rdfs_range, uri_rdfs_comment, uri_rdfs_Literal))). % 11.36/3.81 tff(c_44, plain, (iext(uri_rdfs_domain, uri_rdfs_label, uri_rdfs_Resource))). % 11.36/3.81 tff(c_88, plain, (iext(uri_rdfs_range, uri_rdf__3, uri_rdfs_Resource))). % 11.36/3.81 tff(c_158, plain, (iext(uri_rdfs_domain, uri_rdfs_subPropertyOf, uri_rdf_Property))). % 11.36/3.81 tff(c_152, plain, (iext(uri_rdfs_range, uri_rdfs_subClassOf, uri_rdfs_Class))). % 11.36/3.81 tff(c_82, plain, (iext(uri_rdfs_domain, uri_rdf__3, uri_rdfs_Resource))). % 11.36/3.81 tff(c_22, plain, (iext(uri_rdf_type, uri_rdf_value, uri_rdf_Property))). % 11.36/3.81 tff(c_50, plain, (iext(uri_rdfs_range, uri_rdfs_seeAlso, uri_rdfs_Resource))). % 11.36/3.81 tff(c_48, plain, (iext(uri_rdfs_domain, uri_rdfs_seeAlso, uri_rdfs_Resource))). % 11.36/3.81 tff(c_124, plain, (iext(uri_rdf_type, uri_rdf_Property, uri_rdfs_Class))). % 11.36/3.81 tff(c_16, plain, (iext(uri_rdf_type, uri_rdf__2, uri_rdf_Property))). % 11.36/3.81 tff(c_24, plain, (iext(uri_rdf_type, uri_rdf_subject, uri_rdf_Property))). % 11.36/3.81 tff(c_86, plain, (iext(uri_rdfs_range, uri_rdf__2, uri_rdfs_Resource))). % 11.36/3.81 tff(c_136, plain, (iext(uri_rdfs_domain, uri_rdf_predicate, uri_rdfs_Statement))). % 11.36/3.81 tff(c_72, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_ContainerMembershipProperty, uri_rdf_Property))). % 11.36/3.81 tff(c_182, plain, (iext(uri_ex_p, uri_ex_s, uri_ex_o))). % 11.36/3.81 tff(c_104, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Datatype, uri_rdfs_Class))). % 11.36/3.81 tff(c_46, plain, (iext(uri_rdfs_range, uri_rdfs_label, uri_rdfs_Literal))). % 11.36/3.81 tff(c_631, plain, (~iext(uri_rdf_type, uri_ex_o, uri_owl_Thing))). % 11.36/3.81 tff(c_60, plain, (iext(uri_rdfs_range, uri_rdf_first, uri_rdfs_Resource))). % 11.36/3.81 tff(c_76, plain, (iext(uri_rdfs_range, uri_rdfs_member, uri_rdfs_Resource))). % 11.36/3.81 tff(c_100, plain, (iext(uri_rdf_type, uri_rdf_XMLLiteral, uri_rdfs_Datatype))). % 11.36/3.81 tff(c_176, plain, (iext(uri_rdfs_domain, uri_rdf_value, uri_rdfs_Resource))). % 11.36/3.81 tff(c_42, plain, (iext(uri_rdfs_subPropertyOf, uri_rdfs_isDefinedBy, uri_rdfs_seeAlso))). % 11.36/3.81 tff(c_142, plain, (iext(uri_rdfs_range, uri_rdf_subject, uri_rdfs_Resource))). % 11.36/3.81 tff(c_38, plain, (iext(uri_rdfs_domain, uri_rdfs_isDefinedBy, uri_rdfs_Resource))). % 11.36/3.81 tff(c_64, plain, (iext(uri_rdfs_range, uri_rdf_rest, uri_rdf_List))). % 11.36/3.81 tff(c_66, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Alt, uri_rdfs_Container))). % 11.36/3.81 tff(c_110, plain, (iext(uri_rdfs_range, uri_rdfs_domain, uri_rdfs_Class))). % 11.36/3.81 tff(c_130, plain, (iext(uri_rdfs_range, uri_rdfs_range, uri_rdfs_Class))). % 11.36/3.81 tff(c_20, plain, (iext(uri_rdf_type, uri_rdf_object, uri_rdf_Property))). % 11.36/3.81 tff(c_74, plain, (iext(uri_rdfs_domain, uri_rdfs_member, uri_rdfs_Resource))). % 11.36/3.81 tff(c_132, plain, (iext(uri_rdfs_domain, uri_rdf_object, uri_rdfs_Statement))). % 11.36/3.81 tff(c_18, plain, (iext(uri_rdf_type, uri_rdf__3, uri_rdf_Property))). % 11.36/3.81 tff(c_68, plain, (iext(uri_rdfs_subClassOf, uri_rdf_Bag, uri_rdfs_Container))). % 11.36/3.81 tff(c_630, plain, (iext(uri_rdf_type, uri_ex_s, uri_rdfs_Resource))). % 11.36/3.81 tff(c_166, plain, (iext(uri_rdfs_range, uri_rdfs_subPropertyOf, uri_rdf_Property))). % 11.36/3.81 tff(c_34, plain, (iext(uri_rdfs_domain, uri_rdfs_comment, uri_rdfs_Resource))). % 11.36/3.82 tff(c_106, plain, (iext(uri_rdfs_domain, uri_rdfs_domain, uri_rdf_Property))). % 11.36/3.82 tff(c_126, plain, (iext(uri_rdfs_domain, uri_rdfs_range, uri_rdf_Property))). % 11.36/3.82 tff(c_10, plain, (iext(uri_rdf_type, uri_rdf_nil, uri_rdf_List))). % 11.36/3.82 tff(c_8, plain, (iext(uri_rdf_type, uri_rdf_first, uri_rdf_Property))). % 11.36/3.82 tff(c_98, plain, (iext(uri_rdfs_subClassOf, uri_rdf_XMLLiteral, uri_rdfs_Literal))). % 11.36/3.82 tff(c_96, plain, (iext(uri_rdfs_subClassOf, uri_rdfs_Seq, uri_rdfs_Container))). % 11.36/3.82 tff(c_186, plain, (![X_17]: (icext(uri_rdfs_Resource, X_17)))). % 11.36/3.82 tff(c_4, plain, (![X_4]: (ir(X_4)))). % 11.36/3.82 % SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 11.36/3.82 %------------------------------------------------------------------------------