%------------------------------------------------------------------------------ % File : Metis---2.4 % Problem : SWB009-10 : TPTP v8.1.0. Released v7.5.0. % Transfm : none % Format : tptp:raw % Command : metis --show proof --show saturation %s % Computer : n021.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 : 600s % DateTime : Tue Jul 19 19:15:18 EDT 2022 % Result : Satisfiable 0.92s 1.12s % Output : Saturation 1.02s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : SWB009-10 : TPTP v8.1.0. Released v7.5.0. % 0.03/0.13 % Command : metis --show proof --show saturation %s % 0.12/0.34 % Computer : n021.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 : 600 % 0.12/0.34 % DateTime : Wed Jun 1 04:58:30 EDT 2022 % 0.12/0.34 % CPUTime : % 0.12/0.34 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 0.92/1.12 % SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.92/1.12 % 0.92/1.12 SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.92/1.12 |- ifeq $A $A $B $C = $B % 0.92/1.12 |- ifeq (iext $P $S $O) true (ip $P) true = true % 0.92/1.12 |- ir $X = true % 0.92/1.12 |- ifeq (lv $X) true true true = true % 0.92/1.12 |- iext uri_rdf_type uri_rdf_first uri_rdf_Property = true % 0.92/1.12 |- iext uri_rdf_type uri_rdf_nil uri_rdf_List = true % 0.92/1.12 |- iext uri_rdf_type uri_rdf_rest uri_rdf_Property = true % 0.92/1.12 |- iext uri_rdf_type uri_rdf__1 uri_rdf_Property = true % 0.92/1.12 |- iext uri_rdf_type uri_rdf__2 uri_rdf_Property = true % 0.92/1.12 |- iext uri_rdf_type uri_rdf__3 uri_rdf_Property = true % 0.92/1.12 |- iext uri_rdf_type uri_rdf_object uri_rdf_Property = true % 0.92/1.12 |- iext uri_rdf_type uri_rdf_value uri_rdf_Property = true % 0.92/1.12 |- iext uri_rdf_type uri_rdf_subject uri_rdf_Property = true % 0.92/1.12 |- ifeq (ip $P) true (iext uri_rdf_type $P uri_rdf_Property) true = true % 0.92/1.12 |- ifeq (iext uri_rdf_type $P uri_rdf_Property) true (ip $P) true = true % 0.92/1.12 |- iext uri_rdf_type uri_rdf_type uri_rdf_Property = true % 0.92/1.12 |- iext uri_rdfs_domain uri_rdfs_comment uri_rdfs_Resource = true % 0.92/1.12 |- iext uri_rdfs_range uri_rdfs_comment uri_rdfs_Literal = true % 0.92/1.12 |- iext uri_rdfs_domain uri_rdfs_isDefinedBy uri_rdfs_Resource = true % 0.92/1.12 |- iext uri_rdfs_range uri_rdfs_isDefinedBy uri_rdfs_Resource = true % 0.92/1.12 |- iext uri_rdfs_subPropertyOf uri_rdfs_isDefinedBy uri_rdfs_seeAlso = true % 0.92/1.12 |- iext uri_rdfs_domain uri_rdfs_label uri_rdfs_Resource = true % 0.92/1.12 |- iext uri_rdfs_range uri_rdfs_label uri_rdfs_Literal = true % 0.92/1.12 |- iext uri_rdfs_domain uri_rdfs_seeAlso uri_rdfs_Resource = true % 0.92/1.12 |- iext uri_rdfs_range uri_rdfs_seeAlso uri_rdfs_Resource = true % 0.92/1.12 |- ifeq (icext $C $X) true (iext uri_rdf_type $X $C) true = true % 0.92/1.12 |- ifeq (iext uri_rdf_type $X $C) true (icext $C $X) true = true % 0.92/1.12 |- ifeq (ic $C) true (iext uri_rdfs_subClassOf $C uri_rdfs_Resource) true = % 0.92/1.12 true % 0.92/1.12 |- iext uri_rdfs_domain uri_rdf_first uri_rdf_List = true % 0.92/1.12 |- iext uri_rdfs_range uri_rdf_first uri_rdfs_Resource = true % 0.92/1.12 |- iext uri_rdfs_domain uri_rdf_rest uri_rdf_List = true % 0.92/1.12 |- iext uri_rdfs_range uri_rdf_rest uri_rdf_List = true % 0.92/1.12 |- iext uri_rdfs_subClassOf uri_rdf_Alt uri_rdfs_Container = true % 0.92/1.12 |- iext uri_rdfs_subClassOf uri_rdf_Bag uri_rdfs_Container = true % 0.92/1.12 |- ifeq (icext uri_rdfs_ContainerMembershipProperty $P) true % 0.92/1.12 (iext uri_rdfs_subPropertyOf $P uri_rdfs_member) true = true % 0.92/1.12 |- iext uri_rdfs_subClassOf uri_rdfs_ContainerMembershipProperty % 0.92/1.12 uri_rdf_Property = true % 0.92/1.12 |- iext uri_rdfs_domain uri_rdfs_member uri_rdfs_Resource = true % 0.92/1.12 |- iext uri_rdfs_range uri_rdfs_member uri_rdfs_Resource = true % 0.92/1.12 |- iext uri_rdfs_domain uri_rdf__1 uri_rdfs_Resource = true % 0.92/1.12 |- iext uri_rdfs_domain uri_rdf__2 uri_rdfs_Resource = true % 0.92/1.12 |- iext uri_rdfs_domain uri_rdf__3 uri_rdfs_Resource = true % 0.92/1.12 |- iext uri_rdfs_range uri_rdf__1 uri_rdfs_Resource = true % 0.92/1.12 |- iext uri_rdfs_range uri_rdf__2 uri_rdfs_Resource = true % 0.92/1.12 |- iext uri_rdfs_range uri_rdf__3 uri_rdfs_Resource = true % 0.92/1.12 |- iext uri_rdf_type uri_rdf__1 uri_rdfs_ContainerMembershipProperty = true % 0.92/1.12 |- iext uri_rdf_type uri_rdf__2 uri_rdfs_ContainerMembershipProperty = true % 0.92/1.12 |- iext uri_rdf_type uri_rdf__3 uri_rdfs_ContainerMembershipProperty = true % 0.92/1.12 |- iext uri_rdfs_subClassOf uri_rdfs_Seq uri_rdfs_Container = true % 0.92/1.12 |- iext uri_rdfs_subClassOf uri_rdf_XMLLiteral uri_rdfs_Literal = true % 0.92/1.12 |- iext uri_rdf_type uri_rdf_XMLLiteral uri_rdfs_Datatype = true % 0.92/1.12 |- ifeq (icext uri_rdfs_Datatype $D) true % 0.92/1.12 (iext uri_rdfs_subClassOf $D uri_rdfs_Literal) true = true % 0.92/1.12 |- iext uri_rdfs_subClassOf uri_rdfs_Datatype uri_rdfs_Class = true % 0.92/1.12 |- iext uri_rdfs_domain uri_rdfs_domain uri_rdf_Property = true % 0.92/1.12 |- ifeq (iext uri_rdfs_domain $P $C) true % 0.92/1.12 (ifeq (iext $P $X $Y) true (icext $C $X) true) true = true % 0.92/1.12 |- iext uri_rdfs_range uri_rdfs_domain uri_rdfs_Class = true % 0.92/1.12 |- ifeq (ic $X) true (icext uri_rdfs_Class $X) true = true % 0.92/1.12 |- ifeq (icext uri_rdfs_Class $X) true (ic $X) true = true % 0.92/1.12 |- icext uri_rdfs_Resource $X = true % 0.92/1.12 |- ifeq (icext uri_rdfs_Literal $X) true (lv $X) true = true % 0.92/1.12 |- ifeq (lv $X) true (icext uri_rdfs_Literal $X) true = true % 0.92/1.12 |- iext uri_rdf_type uri_rdf_Property uri_rdfs_Class = true % 0.92/1.12 |- iext uri_rdfs_domain uri_rdfs_range uri_rdf_Property = true % 0.92/1.12 |- ifeq (iext uri_rdfs_range $P $C) true % 0.92/1.12 (ifeq (iext $P $X $Y) true (icext $C $Y) true) true = true % 0.92/1.12 |- iext uri_rdfs_range uri_rdfs_range uri_rdfs_Class = true % 0.92/1.12 |- iext uri_rdfs_domain uri_rdf_object uri_rdfs_Statement = true % 0.92/1.12 |- iext uri_rdfs_range uri_rdf_predicate uri_rdfs_Resource = true % 0.92/1.12 |- iext uri_rdfs_domain uri_rdf_predicate uri_rdfs_Statement = true % 0.92/1.12 |- iext uri_rdfs_domain uri_rdf_subject uri_rdfs_Statement = true % 0.92/1.13 |- iext uri_rdfs_range uri_rdf_subject uri_rdfs_Resource = true % 0.92/1.13 |- iext uri_rdfs_domain uri_rdfs_subClassOf uri_rdfs_Class = true % 0.92/1.13 |- ifeq (icext $C $X) true % 0.92/1.13 (ifeq (iext uri_rdfs_subClassOf $C $D) true (icext $D $X) true) true = % 0.92/1.13 true % 0.92/1.13 |- ifeq (iext uri_rdfs_subClassOf $C $D) true (ic $D) true = true % 0.92/1.13 |- ifeq (iext uri_rdfs_subClassOf $C $D) true (ic $C) true = true % 0.92/1.13 |- iext uri_rdfs_range uri_rdfs_subClassOf uri_rdfs_Class = true % 0.92/1.13 |- ifeq (ic $C) true (iext uri_rdfs_subClassOf $C $C) true = true % 0.92/1.13 |- ifeq (iext uri_rdfs_subClassOf $D $E) true % 0.92/1.13 (ifeq (iext uri_rdfs_subClassOf $C $D) true % 0.92/1.13 (iext uri_rdfs_subClassOf $C $E) true) true = true % 0.92/1.13 |- iext uri_rdfs_domain uri_rdfs_subPropertyOf uri_rdf_Property = true % 0.92/1.13 |- ifeq (iext uri_rdfs_subPropertyOf $P $Q) true (ip $Q) true = true % 0.92/1.13 |- ifeq (iext uri_rdfs_subPropertyOf $P $Q) true (ip $P) true = true % 0.92/1.13 |- ifeq (iext uri_rdfs_subPropertyOf $P $Q) true % 0.92/1.13 (ifeq (iext $P $X $Y) true (iext $Q $X $Y) true) true = true % 0.92/1.13 |- iext uri_rdfs_range uri_rdfs_subPropertyOf uri_rdf_Property = true % 0.92/1.13 |- ifeq (ip $P) true (iext uri_rdfs_subPropertyOf $P $P) true = true % 0.92/1.13 |- ifeq (iext uri_rdfs_subPropertyOf $Q $R) true % 0.92/1.13 (ifeq (iext uri_rdfs_subPropertyOf $P $Q) true % 0.92/1.13 (iext uri_rdfs_subPropertyOf $P $R) true) true = true % 0.92/1.13 |- iext uri_rdfs_domain uri_rdf_type uri_rdfs_Resource = true % 0.92/1.13 |- iext uri_rdfs_range uri_rdf_type uri_rdfs_Class = true % 0.92/1.13 |- iext uri_rdfs_domain uri_rdf_value uri_rdfs_Resource = true % 0.92/1.13 |- iext uri_rdfs_range uri_rdf_value uri_rdfs_Resource = true % 0.92/1.13 |- iext uri_owl_someValuesFrom % 0.92/1.13 sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z % 0.92/1.13 uri_ex_c = true % 0.92/1.13 |- iext uri_owl_onProperty % 0.92/1.13 sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z % 0.92/1.13 uri_ex_p = true % 0.92/1.13 |- iext uri_rdf_type % 0.92/1.13 sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z % 0.92/1.13 uri_owl_Restriction = true % 0.92/1.13 |- iext uri_rdf_type uri_ex_c uri_owl_Class = true % 0.92/1.13 |- iext uri_rdf_type uri_ex_s % 0.92/1.13 sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z = % 0.92/1.13 true % 0.92/1.13 |- iext uri_rdf_type uri_ex_p uri_owl_ObjectProperty = true % 0.92/1.13 |- ~(tuple (iext uri_rdf_type $BNODE_x uri_ex_c) % 0.92/1.13 (iext uri_ex_p uri_ex_s $BNODE_x) = tuple true true) % 0.92/1.13 |- ip uri_rdf__1 = true % 0.92/1.13 |- ip uri_rdf__2 = true % 0.92/1.13 |- ip uri_rdf__3 = true % 0.92/1.13 |- ip uri_rdf_first = true % 0.92/1.13 |- ip uri_rdf_object = true % 0.92/1.13 |- ip uri_rdf_rest = true % 0.92/1.13 |- ip uri_rdf_subject = true % 0.92/1.13 |- ip uri_rdf_type = true % 0.92/1.13 |- ip uri_rdf_value = true % 0.92/1.13 |- iext uri_rdfs_subPropertyOf uri_rdf__1 uri_rdf__1 = true % 0.92/1.13 |- iext uri_rdfs_subPropertyOf uri_rdf__2 uri_rdf__2 = true % 0.92/1.13 |- iext uri_rdfs_subPropertyOf uri_rdf__3 uri_rdf__3 = true % 0.92/1.13 |- iext uri_rdfs_subPropertyOf uri_rdf_first uri_rdf_first = true % 0.92/1.13 |- iext uri_rdfs_subPropertyOf uri_rdf_object uri_rdf_object = true % 0.92/1.13 |- iext uri_rdfs_subPropertyOf uri_rdf_rest uri_rdf_rest = true % 0.92/1.13 |- iext uri_rdfs_subPropertyOf uri_rdf_subject uri_rdf_subject = true % 0.92/1.13 |- iext uri_rdfs_subPropertyOf uri_rdf_type uri_rdf_type = true % 0.92/1.13 |- iext uri_rdfs_subPropertyOf uri_rdf_value uri_rdf_value = true % 0.92/1.13 |- ic uri_rdfs_Container = true % 0.92/1.13 |- ic uri_rdfs_Literal = true % 0.92/1.13 |- ic uri_rdf_Property = true % 0.92/1.13 |- ic uri_rdfs_Class = true % 0.92/1.13 |- iext uri_rdfs_subClassOf uri_rdfs_Container uri_rdfs_Container = true % 0.92/1.13 |- iext uri_rdfs_subClassOf uri_rdfs_Container uri_rdfs_Resource = true % 0.92/1.13 |- icext uri_rdfs_Class uri_rdfs_Container = true % 0.92/1.13 |- iext uri_rdfs_subClassOf uri_rdfs_Literal uri_rdfs_Literal = true % 0.92/1.13 |- iext uri_rdfs_subClassOf uri_rdfs_Literal uri_rdfs_Resource = true % 0.92/1.13 |- icext uri_rdfs_Class uri_rdfs_Literal = true % 0.92/1.13 |- iext uri_rdfs_subClassOf uri_rdf_Property uri_rdf_Property = true % 0.92/1.13 |- iext uri_rdfs_subClassOf uri_rdf_Property uri_rdfs_Resource = true % 0.92/1.13 |- icext uri_rdfs_Class uri_rdf_Property = true % 0.92/1.13 |- iext uri_rdfs_subClassOf uri_rdfs_Class uri_rdfs_Class = true % 0.92/1.13 |- iext uri_rdfs_subClassOf uri_rdfs_Class uri_rdfs_Resource = true % 0.92/1.13 |- icext uri_rdfs_Class uri_rdfs_Class = true % 0.92/1.13 |- ic uri_rdfs_Resource = true % 0.92/1.13 |- iext uri_rdfs_subClassOf uri_rdfs_Resource uri_rdfs_Resource = true % 0.92/1.13 |- icext uri_rdfs_Class uri_rdfs_Resource = true % 0.92/1.13 |- ic uri_rdf_Alt = true % 0.92/1.13 |- ic uri_rdf_Bag = true % 0.92/1.13 |- ic uri_rdf_XMLLiteral = true % 0.92/1.13 |- ic uri_rdfs_ContainerMembershipProperty = true % 0.92/1.13 |- ic uri_rdfs_Datatype = true % 0.92/1.13 |- ic uri_rdfs_Seq = true % 0.92/1.13 |- iext uri_rdfs_subClassOf uri_rdf_Alt uri_rdf_Alt = true % 0.92/1.13 |- iext uri_rdfs_subClassOf uri_rdf_Alt uri_rdfs_Resource = true % 0.92/1.13 |- icext uri_rdfs_Class uri_rdf_Alt = true % 0.92/1.13 |- iext uri_rdfs_subClassOf uri_rdf_Bag uri_rdf_Bag = true % 0.92/1.13 |- iext uri_rdfs_subClassOf uri_rdf_Bag uri_rdfs_Resource = true % 0.92/1.13 |- icext uri_rdfs_Class uri_rdf_Bag = true % 0.92/1.13 |- iext uri_rdfs_subClassOf uri_rdf_XMLLiteral uri_rdf_XMLLiteral = true % 0.92/1.13 |- iext uri_rdfs_subClassOf uri_rdf_XMLLiteral uri_rdfs_Resource = true % 0.92/1.13 |- icext uri_rdfs_Class uri_rdf_XMLLiteral = true % 0.92/1.13 |- iext uri_rdfs_subClassOf uri_rdfs_ContainerMembershipProperty % 0.92/1.13 uri_rdfs_ContainerMembershipProperty = true % 0.92/1.13 |- iext uri_rdfs_subClassOf uri_rdfs_ContainerMembershipProperty % 0.92/1.13 uri_rdfs_Resource = true % 0.92/1.13 |- icext uri_rdfs_Class uri_rdfs_ContainerMembershipProperty = true % 0.92/1.13 |- iext uri_rdfs_subClassOf uri_rdfs_Datatype uri_rdfs_Datatype = true % 0.92/1.13 |- iext uri_rdfs_subClassOf uri_rdfs_Datatype uri_rdfs_Resource = true % 0.92/1.13 |- icext uri_rdfs_Class uri_rdfs_Datatype = true % 0.92/1.13 |- iext uri_rdfs_subClassOf uri_rdfs_Seq uri_rdfs_Seq = true % 0.92/1.13 |- iext uri_rdfs_subClassOf uri_rdfs_Seq uri_rdfs_Resource = true % 0.92/1.13 |- icext uri_rdfs_Class uri_rdfs_Seq = true % 0.92/1.13 |- ip uri_rdfs_seeAlso = true % 0.92/1.13 |- iext uri_rdfs_subPropertyOf uri_rdfs_seeAlso uri_rdfs_seeAlso = true % 0.92/1.13 |- iext uri_rdf_type uri_rdfs_seeAlso uri_rdf_Property = true % 0.92/1.13 |- ip uri_rdfs_isDefinedBy = true % 0.92/1.13 |- iext uri_rdfs_subPropertyOf uri_rdfs_isDefinedBy uri_rdfs_isDefinedBy = % 0.92/1.13 true % 0.92/1.13 |- iext uri_rdf_type uri_rdfs_isDefinedBy uri_rdf_Property = true % 0.92/1.13 |- icext uri_owl_Restriction % 0.92/1.13 sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z = % 0.92/1.13 true % 0.92/1.13 |- icext uri_owl_Class uri_ex_c = true % 0.92/1.13 |- icext uri_owl_ObjectProperty uri_ex_p = true % 0.92/1.13 |- icext % 0.92/1.13 sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z % 0.92/1.13 uri_ex_s = true % 0.92/1.13 |- icext uri_rdfs_Datatype uri_rdf_XMLLiteral = true % 0.92/1.13 |- icext uri_rdf_Property uri_rdf__1 = true % 0.92/1.13 |- icext uri_rdfs_ContainerMembershipProperty uri_rdf__1 = true % 0.92/1.13 |- icext uri_rdf_Property uri_rdf__2 = true % 0.92/1.13 |- icext uri_rdfs_ContainerMembershipProperty uri_rdf__2 = true % 0.92/1.13 |- icext uri_rdf_Property uri_rdf__3 = true % 0.92/1.13 |- icext uri_rdfs_ContainerMembershipProperty uri_rdf__3 = true % 0.92/1.13 |- icext uri_rdf_Property uri_rdf_first = true % 0.92/1.13 |- icext uri_rdf_List uri_rdf_nil = true % 0.92/1.13 |- icext uri_rdf_Property uri_rdf_object = true % 0.92/1.13 |- icext uri_rdf_Property uri_rdf_rest = true % 0.92/1.13 |- icext uri_rdf_Property uri_rdf_subject = true % 0.92/1.13 |- icext uri_rdf_Property uri_rdf_type = true % 0.92/1.13 |- icext uri_rdf_Property uri_rdf_value = true % 0.92/1.13 |- icext uri_rdf_Property uri_rdfs_isDefinedBy = true % 0.92/1.13 |- icext uri_rdf_Property uri_rdfs_seeAlso = true % 0.92/1.13 |- iext uri_rdfs_subPropertyOf uri_rdf__1 uri_rdfs_member = true % 0.92/1.13 |- iext uri_rdfs_subPropertyOf uri_rdf__2 uri_rdfs_member = true % 0.92/1.13 |- ip uri_rdfs_member = true % 0.92/1.13 |- iext uri_rdfs_subPropertyOf uri_rdfs_member uri_rdfs_member = true % 0.92/1.13 |- iext uri_rdf_type uri_rdfs_member uri_rdf_Property = true % 0.92/1.13 |- icext uri_rdf_Property uri_rdfs_member = true % 0.92/1.13 |- iext uri_rdfs_subPropertyOf uri_rdf__3 uri_rdfs_member = true % 0.92/1.13 |- iext uri_rdf_type uri_rdf_Alt uri_rdfs_Class = true % 0.92/1.13 |- iext uri_rdf_type uri_rdf_Bag uri_rdfs_Class = true % 0.92/1.14 |- iext uri_rdf_type uri_rdf_XMLLiteral uri_rdfs_Class = true % 0.92/1.14 |- iext uri_rdf_type uri_rdfs_Class uri_rdfs_Class = true % 0.92/1.14 |- iext uri_rdf_type uri_rdfs_Container uri_rdfs_Class = true % 0.92/1.14 |- iext uri_rdf_type uri_rdfs_ContainerMembershipProperty uri_rdfs_Class = % 0.92/1.14 true % 0.92/1.14 |- iext uri_rdf_type uri_rdfs_Datatype uri_rdfs_Class = true % 0.92/1.14 |- iext uri_rdf_type uri_rdfs_Literal uri_rdfs_Class = true % 0.92/1.14 |- iext uri_rdf_type uri_rdfs_Resource uri_rdfs_Class = true % 0.92/1.14 |- iext uri_rdf_type uri_rdfs_Seq uri_rdfs_Class = true % 0.92/1.14 |- iext uri_rdf_type $_58 uri_rdfs_Resource = true % 0.92/1.14 |- ifeq (iext uri_rdf__1 $_79 $_77) true true true = true % 0.92/1.14 |- ifeq (iext uri_rdf__2 $_79 $_77) true true true = true % 0.92/1.14 |- ifeq (iext uri_rdf__3 $_79 $_77) true true true = true % 0.92/1.14 |- ifeq (iext uri_rdf_first $_79 $_77) true true true = true % 0.92/1.14 |- ifeq (iext uri_rdf_object $_79 $_77) true true true = true % 0.92/1.14 |- ifeq (iext uri_rdf_rest $_79 $_77) true true true = true % 0.92/1.14 |- ifeq (iext uri_rdf_subject $_79 $_77) true true true = true % 0.92/1.14 |- ifeq (iext uri_rdf_type $_79 $_77) true true true = true % 0.92/1.14 |- ifeq (iext uri_rdf_value $_79 $_77) true true true = true % 0.92/1.14 |- ifeq (iext uri_rdfs_isDefinedBy $_79 $_77) true true true = true % 0.92/1.14 |- ifeq (iext uri_rdfs_member $_79 $_77) true true true = true % 0.92/1.14 |- ifeq (iext uri_rdfs_seeAlso $_79 $_77) true true true = true % 0.92/1.14 |- ip uri_owl_onProperty = true % 0.92/1.14 |- ip uri_owl_someValuesFrom = true % 0.92/1.14 |- ip uri_rdfs_domain = true % 0.92/1.14 |- ip uri_rdfs_range = true % 0.92/1.14 |- ip uri_rdfs_subClassOf = true % 0.92/1.14 |- ip uri_rdfs_subPropertyOf = true % 0.92/1.14 |- ifeq (iext uri_owl_onProperty $S $O) true true true = true % 0.92/1.14 |- iext uri_rdfs_subPropertyOf uri_owl_onProperty uri_owl_onProperty = true % 0.92/1.14 |- iext uri_rdf_type uri_owl_onProperty uri_rdf_Property = true % 0.92/1.14 |- ifeq (iext uri_owl_someValuesFrom $S $O) true true true = true % 0.92/1.14 |- iext uri_rdfs_subPropertyOf uri_owl_someValuesFrom % 0.92/1.14 uri_owl_someValuesFrom = true % 0.92/1.14 |- iext uri_rdf_type uri_owl_someValuesFrom uri_rdf_Property = true % 0.92/1.14 |- ifeq (iext uri_rdfs_domain $S $O) true true true = true % 0.92/1.14 |- iext uri_rdfs_subPropertyOf uri_rdfs_domain uri_rdfs_domain = true % 0.92/1.14 |- iext uri_rdf_type uri_rdfs_domain uri_rdf_Property = true % 0.92/1.14 |- ifeq (iext uri_rdfs_range $S $O) true true true = true % 0.92/1.14 |- iext uri_rdfs_subPropertyOf uri_rdfs_range uri_rdfs_range = true % 0.92/1.14 |- iext uri_rdf_type uri_rdfs_range uri_rdf_Property = true % 0.92/1.14 |- ifeq (iext uri_rdfs_subClassOf $S $O) true true true = true % 0.92/1.14 |- iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf uri_rdfs_subClassOf = % 0.92/1.14 true % 0.92/1.14 |- iext uri_rdf_type uri_rdfs_subClassOf uri_rdf_Property = true % 0.92/1.14 |- ifeq (iext uri_rdfs_subPropertyOf $S $O) true true true = true % 0.92/1.14 |- iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf % 0.92/1.14 uri_rdfs_subPropertyOf = true % 0.92/1.14 |- iext uri_rdf_type uri_rdfs_subPropertyOf uri_rdf_Property = true % 0.92/1.14 |- icext uri_rdf_Property uri_rdfs_subPropertyOf = true % 0.92/1.14 |- icext uri_rdf_Property uri_owl_onProperty = true % 0.92/1.14 |- icext uri_rdf_Property uri_owl_someValuesFrom = true % 0.92/1.14 |- icext uri_rdf_Property uri_rdfs_domain = true % 0.92/1.14 |- icext uri_rdf_Property uri_rdfs_range = true % 0.92/1.14 |- icext uri_rdf_Property uri_rdfs_subClassOf = true % 0.92/1.14 |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Container $_119) true % 0.92/1.14 (iext uri_rdfs_subClassOf uri_rdf_Alt $_119) true = true % 0.92/1.14 |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Resource $_119) true % 0.92/1.14 (iext uri_rdfs_subClassOf uri_rdf_Alt $_119) true = true % 0.92/1.14 |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Container $_119) true % 0.92/1.14 (iext uri_rdfs_subClassOf uri_rdf_Bag $_119) true = true % 0.92/1.14 |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Resource $_119) true % 0.92/1.14 (iext uri_rdfs_subClassOf uri_rdf_Bag $_119) true = true % 0.92/1.14 |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Resource $_119) true % 0.92/1.14 (iext uri_rdfs_subClassOf uri_rdf_Property $_119) true = true % 0.92/1.14 |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Literal $_119) true % 0.92/1.14 (iext uri_rdfs_subClassOf uri_rdf_XMLLiteral $_119) true = true % 0.92/1.14 |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Resource $_119) true % 0.92/1.14 (iext uri_rdfs_subClassOf uri_rdf_XMLLiteral $_119) true = true % 0.92/1.14 |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Resource $_119) true % 0.92/1.14 (iext uri_rdfs_subClassOf uri_rdfs_Class $_119) true = true % 0.92/1.14 |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Resource $_119) true % 0.92/1.14 (iext uri_rdfs_subClassOf uri_rdfs_Container $_119) true = true % 0.92/1.14 |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $_119) true % 0.92/1.14 (iext uri_rdfs_subClassOf uri_rdfs_ContainerMembershipProperty $_119) % 0.92/1.14 true = true % 0.92/1.14 |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Resource $_119) true % 0.92/1.14 (iext uri_rdfs_subClassOf uri_rdfs_ContainerMembershipProperty $_119) % 0.92/1.14 true = true % 0.92/1.14 |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Class $_119) true % 0.92/1.14 (iext uri_rdfs_subClassOf uri_rdfs_Datatype $_119) true = true % 0.92/1.14 |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Resource $_119) true % 0.92/1.14 (iext uri_rdfs_subClassOf uri_rdfs_Datatype $_119) true = true % 0.92/1.14 |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Resource $_119) true % 0.92/1.14 (iext uri_rdfs_subClassOf uri_rdfs_Literal $_119) true = true % 0.92/1.14 |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Container $_119) true % 0.92/1.14 (iext uri_rdfs_subClassOf uri_rdfs_Seq $_119) true = true % 0.92/1.14 |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Resource $_119) true % 0.92/1.14 (iext uri_rdfs_subClassOf uri_rdfs_Seq $_119) true = true % 0.92/1.14 |- ifeq (iext uri_rdfs_subClassOf $_117 uri_rdf_Alt) true % 0.92/1.14 (iext uri_rdfs_subClassOf $_117 uri_rdfs_Container) true = true % 0.92/1.14 |- ifeq (iext uri_rdfs_subClassOf $_117 uri_rdf_Alt) true % 0.92/1.14 (iext uri_rdfs_subClassOf $_117 uri_rdfs_Resource) true = true % 0.92/1.14 |- ifeq (iext uri_rdfs_subClassOf $_117 uri_rdf_Bag) true % 0.92/1.14 (iext uri_rdfs_subClassOf $_117 uri_rdfs_Container) true = true % 0.92/1.14 |- ifeq (iext uri_rdfs_subClassOf $_117 uri_rdf_Bag) true % 0.92/1.14 (iext uri_rdfs_subClassOf $_117 uri_rdfs_Resource) true = true % 0.92/1.14 |- ifeq (iext uri_rdfs_subClassOf $_117 uri_rdf_Property) true % 0.92/1.14 (iext uri_rdfs_subClassOf $_117 uri_rdfs_Resource) true = true % 0.92/1.14 |- ifeq (iext uri_rdfs_subClassOf $_117 uri_rdf_XMLLiteral) true % 0.92/1.14 (iext uri_rdfs_subClassOf $_117 uri_rdfs_Literal) true = true % 0.92/1.14 |- ifeq (iext uri_rdfs_subClassOf $_117 uri_rdf_XMLLiteral) true % 0.92/1.14 (iext uri_rdfs_subClassOf $_117 uri_rdfs_Resource) true = true % 0.92/1.14 |- ifeq (iext uri_rdfs_subClassOf $_117 uri_rdfs_Class) true % 0.92/1.14 (iext uri_rdfs_subClassOf $_117 uri_rdfs_Resource) true = true % 0.92/1.14 |- ifeq (iext uri_rdfs_subClassOf $_117 uri_rdfs_Container) true % 0.92/1.14 (iext uri_rdfs_subClassOf $_117 uri_rdfs_Resource) true = true % 0.92/1.14 |- ifeq % 0.92/1.14 (iext uri_rdfs_subClassOf $_117 uri_rdfs_ContainerMembershipProperty) % 0.92/1.14 true (iext uri_rdfs_subClassOf $_117 uri_rdf_Property) true = true % 0.92/1.14 |- ifeq % 0.92/1.14 (iext uri_rdfs_subClassOf $_117 uri_rdfs_ContainerMembershipProperty) % 0.92/1.14 true (iext uri_rdfs_subClassOf $_117 uri_rdfs_Resource) true = true % 0.92/1.14 |- ifeq (iext uri_rdfs_subClassOf $_117 uri_rdfs_Datatype) true % 0.92/1.14 (iext uri_rdfs_subClassOf $_117 uri_rdfs_Class) true = true % 0.92/1.14 |- ifeq (iext uri_rdfs_subClassOf $_117 uri_rdfs_Datatype) true % 0.92/1.14 (iext uri_rdfs_subClassOf $_117 uri_rdfs_Resource) true = true % 0.92/1.14 |- ifeq (iext uri_rdfs_subClassOf $_117 uri_rdfs_Literal) true % 0.92/1.14 (iext uri_rdfs_subClassOf $_117 uri_rdfs_Resource) true = true % 0.92/1.14 |- ifeq (iext uri_rdfs_subClassOf $_117 uri_rdfs_Seq) true % 0.92/1.14 (iext uri_rdfs_subClassOf $_117 uri_rdfs_Container) true = true % 0.92/1.14 |- ifeq (iext uri_rdfs_subClassOf $_117 uri_rdfs_Seq) true % 0.92/1.14 (iext uri_rdfs_subClassOf $_117 uri_rdfs_Resource) true = true % 0.92/1.14 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_member $_176) true % 0.92/1.14 (iext uri_rdfs_subPropertyOf uri_rdf__1 $_176) true = true % 0.92/1.14 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_member $_176) true % 0.92/1.14 (iext uri_rdfs_subPropertyOf uri_rdf__2 $_176) true = true % 0.92/1.14 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_member $_176) true % 0.92/1.14 (iext uri_rdfs_subPropertyOf uri_rdf__3 $_176) true = true % 0.92/1.14 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_seeAlso $_176) true % 0.92/1.14 (iext uri_rdfs_subPropertyOf uri_rdfs_isDefinedBy $_176) true = true % 0.92/1.14 |- ifeq (iext uri_rdfs_subPropertyOf $_174 uri_rdf__1) true % 0.92/1.14 (iext uri_rdfs_subPropertyOf $_174 uri_rdfs_member) true = true % 0.92/1.14 |- ifeq (iext uri_rdfs_subPropertyOf $_174 uri_rdf__2) true % 0.92/1.14 (iext uri_rdfs_subPropertyOf $_174 uri_rdfs_member) true = true % 0.92/1.14 |- ifeq (iext uri_rdfs_subPropertyOf $_174 uri_rdf__3) true % 0.92/1.14 (iext uri_rdfs_subPropertyOf $_174 uri_rdfs_member) true = true % 0.92/1.14 |- ifeq (iext uri_rdfs_subPropertyOf $_174 uri_rdfs_isDefinedBy) true % 0.92/1.14 (iext uri_rdfs_subPropertyOf $_174 uri_rdfs_seeAlso) true = true % 0.92/1.14 |- ifeq % 0.92/1.14 (iext uri_rdfs_domain $_222 % 0.92/1.14 sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z) % 0.92/1.14 true (ifeq (iext $_222 uri_ex_s $_224) true true true) true = true % 0.92/1.14 |- ifeq (iext uri_rdfs_domain $_222 uri_owl_Class) true % 0.92/1.14 (ifeq (iext $_222 uri_ex_c $_224) true true true) true = true % 0.92/1.14 |- ifeq (iext uri_rdfs_domain $_222 uri_owl_ObjectProperty) true % 0.92/1.14 (ifeq (iext $_222 uri_ex_p $_224) true true true) true = true % 0.92/1.14 |- ifeq (iext uri_rdfs_domain $_222 uri_owl_Restriction) true % 0.92/1.14 (ifeq % 0.92/1.14 (iext $_222 % 0.92/1.14 sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z % 0.92/1.14 $_224) true true true) true = true % 0.92/1.14 |- ifeq (iext uri_rdfs_domain $_222 uri_rdf_List) true % 0.92/1.14 (ifeq (iext $_222 uri_rdf_nil $_224) true true true) true = true % 0.92/1.14 |- ifeq (iext uri_rdfs_domain $_222 uri_rdf_Property) true % 0.92/1.14 (ifeq (iext $_222 uri_owl_onProperty $_224) true true true) true = % 0.92/1.14 true % 0.92/1.14 |- ifeq (iext uri_rdfs_domain $_222 uri_rdf_Property) true % 0.92/1.14 (ifeq (iext $_222 uri_owl_someValuesFrom $_224) true true true) true = % 0.92/1.14 true % 0.92/1.14 |- ifeq (iext uri_rdfs_domain $_222 uri_rdf_Property) true % 0.92/1.14 (ifeq (iext $_222 uri_rdf__1 $_224) true true true) true = true % 0.92/1.14 |- ifeq (iext uri_rdfs_domain $_222 uri_rdf_Property) true % 0.92/1.14 (ifeq (iext $_222 uri_rdf__2 $_224) true true true) true = true % 0.92/1.14 |- ifeq (iext uri_rdfs_domain $_222 uri_rdf_Property) true % 0.92/1.14 (ifeq (iext $_222 uri_rdf__3 $_224) true true true) true = true % 0.92/1.14 |- ifeq (iext uri_rdfs_domain $_222 uri_rdf_Property) true % 0.92/1.14 (ifeq (iext $_222 uri_rdf_first $_224) true true true) true = true % 0.92/1.14 |- ifeq (iext uri_rdfs_domain $_222 uri_rdf_Property) true % 0.92/1.14 (ifeq (iext $_222 uri_rdf_object $_224) true true true) true = true % 0.92/1.14 |- ifeq (iext uri_rdfs_domain $_222 uri_rdf_Property) true % 0.92/1.14 (ifeq (iext $_222 uri_rdf_rest $_224) true true true) true = true % 0.92/1.14 |- ifeq (iext uri_rdfs_domain $_222 uri_rdf_Property) true % 0.92/1.14 (ifeq (iext $_222 uri_rdf_subject $_224) true true true) true = true % 0.92/1.14 |- ifeq (iext uri_rdfs_domain $_222 uri_rdf_Property) true % 0.92/1.14 (ifeq (iext $_222 uri_rdf_type $_224) true true true) true = true % 0.92/1.14 |- ifeq (iext uri_rdfs_domain $_222 uri_rdf_Property) true % 0.92/1.14 (ifeq (iext $_222 uri_rdf_value $_224) true true true) true = true % 0.92/1.14 |- ifeq (iext uri_rdfs_domain $_222 uri_rdf_Property) true % 0.92/1.14 (ifeq (iext $_222 uri_rdfs_domain $_224) true true true) true = true % 0.92/1.14 |- ifeq (iext uri_rdfs_domain $_222 uri_rdf_Property) true % 0.92/1.14 (ifeq (iext $_222 uri_rdfs_isDefinedBy $_224) true true true) true = % 0.92/1.14 true % 0.92/1.14 |- ifeq (iext uri_rdfs_domain $_222 uri_rdf_Property) true % 0.92/1.14 (ifeq (iext $_222 uri_rdfs_member $_224) true true true) true = true % 0.92/1.14 |- ifeq (iext uri_rdfs_domain $_222 uri_rdf_Property) true % 0.92/1.14 (ifeq (iext $_222 uri_rdfs_range $_224) true true true) true = true % 0.92/1.14 |- ifeq (iext uri_rdfs_domain $_222 uri_rdf_Property) true % 0.92/1.14 (ifeq (iext $_222 uri_rdfs_seeAlso $_224) true true true) true = true % 0.92/1.14 |- ifeq (iext uri_rdfs_domain $_222 uri_rdf_Property) true % 0.92/1.14 (ifeq (iext $_222 uri_rdfs_subClassOf $_224) true true true) true = % 0.92/1.14 true % 0.92/1.14 |- ifeq (iext uri_rdfs_domain $_222 uri_rdf_Property) true % 0.92/1.14 (ifeq (iext $_222 uri_rdfs_subPropertyOf $_224) true true true) true = % 0.92/1.14 true % 0.92/1.14 |- ifeq (iext uri_rdfs_domain $_222 uri_rdfs_Class) true % 0.92/1.14 (ifeq (iext $_222 uri_rdf_Alt $_224) true true true) true = true % 0.92/1.14 |- ifeq (iext uri_rdfs_domain $_222 uri_rdfs_Class) true % 0.92/1.14 (ifeq (iext $_222 uri_rdf_Bag $_224) true true true) true = true % 0.92/1.14 |- ifeq (iext uri_rdfs_domain $_222 uri_rdfs_Class) true % 0.92/1.14 (ifeq (iext $_222 uri_rdf_Property $_224) true true true) true = true % 0.92/1.14 |- ifeq (iext uri_rdfs_domain $_222 uri_rdfs_Class) true % 0.92/1.14 (ifeq (iext $_222 uri_rdf_XMLLiteral $_224) true true true) true = % 0.92/1.14 true % 0.92/1.14 |- ifeq (iext uri_rdfs_domain $_222 uri_rdfs_Class) true % 0.92/1.14 (ifeq (iext $_222 uri_rdfs_Class $_224) true true true) true = true % 0.92/1.14 |- ifeq (iext uri_rdfs_domain $_222 uri_rdfs_Class) true % 0.92/1.14 (ifeq (iext $_222 uri_rdfs_Container $_224) true true true) true = % 0.92/1.14 true % 0.92/1.14 |- ifeq (iext uri_rdfs_domain $_222 uri_rdfs_Class) true % 0.92/1.14 (ifeq (iext $_222 uri_rdfs_ContainerMembershipProperty $_224) true % 0.92/1.14 true true) true = true % 0.92/1.14 |- ifeq (iext uri_rdfs_domain $_222 uri_rdfs_Class) true % 0.92/1.14 (ifeq (iext $_222 uri_rdfs_Datatype $_224) true true true) true = true % 0.92/1.14 |- ifeq (iext uri_rdfs_domain $_222 uri_rdfs_Class) true % 0.92/1.14 (ifeq (iext $_222 uri_rdfs_Literal $_224) true true true) true = true % 0.92/1.14 |- ifeq (iext uri_rdfs_domain $_222 uri_rdfs_Class) true % 0.92/1.14 (ifeq (iext $_222 uri_rdfs_Resource $_224) true true true) true = true % 0.92/1.14 |- ifeq (iext uri_rdfs_domain $_222 uri_rdfs_Class) true % 0.92/1.14 (ifeq (iext $_222 uri_rdfs_Seq $_224) true true true) true = true % 0.92/1.14 |- ifeq (iext uri_rdfs_domain $_222 uri_rdfs_ContainerMembershipProperty) % 0.92/1.14 true (ifeq (iext $_222 uri_rdf__1 $_224) true true true) true = true % 0.92/1.14 |- ifeq (iext uri_rdfs_domain $_222 uri_rdfs_ContainerMembershipProperty) % 0.92/1.14 true (ifeq (iext $_222 uri_rdf__2 $_224) true true true) true = true % 0.92/1.14 |- ifeq (iext uri_rdfs_domain $_222 uri_rdfs_ContainerMembershipProperty) % 0.92/1.14 true (ifeq (iext $_222 uri_rdf__3 $_224) true true true) true = true % 0.92/1.14 |- ifeq (iext uri_rdfs_domain $_222 uri_rdfs_Datatype) true % 0.92/1.14 (ifeq (iext $_222 uri_rdf_XMLLiteral $_224) true true true) true = % 0.92/1.14 true % 0.92/1.14 |- ifeq (iext uri_rdfs_domain $_222 uri_rdfs_Resource) true % 0.92/1.14 (ifeq (iext $_222 $_223 $_224) true true true) true = true % 0.92/1.14 |- ifeq (iext uri_rdfs_domain uri_owl_onProperty $_221) true % 0.92/1.14 (icext $_221 % 0.92/1.14 sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z) % 0.92/1.14 true = true % 0.92/1.14 |- ifeq (iext uri_rdfs_domain uri_owl_someValuesFrom $_221) true % 0.92/1.14 (icext $_221 % 0.92/1.14 sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z) % 0.92/1.14 true = true % 0.92/1.14 |- ifeq (iext uri_rdfs_domain uri_rdf_type $_221) true (icext $_221 $_223) % 0.92/1.14 true = true % 0.92/1.14 |- ifeq (iext uri_rdfs_domain uri_rdfs_domain $_221) true % 0.92/1.14 (icext $_221 uri_rdf__1) true = true % 0.92/1.14 |- ifeq (iext uri_rdfs_domain uri_rdfs_domain $_221) true % 0.92/1.14 (icext $_221 uri_rdf__2) true = true % 0.92/1.14 |- ifeq (iext uri_rdfs_domain uri_rdfs_domain $_221) true % 0.92/1.14 (icext $_221 uri_rdf__3) true = true % 0.92/1.14 |- ifeq (iext uri_rdfs_domain uri_rdfs_domain $_221) true % 0.92/1.14 (icext $_221 uri_rdf_first) true = true % 0.92/1.14 |- ifeq (iext uri_rdfs_domain uri_rdfs_domain $_221) true % 0.92/1.14 (icext $_221 uri_rdf_object) true = true % 0.92/1.14 |- ifeq (iext uri_rdfs_domain uri_rdfs_domain $_221) true % 0.92/1.14 (icext $_221 uri_rdf_predicate) true = true % 0.92/1.14 |- ifeq (iext uri_rdfs_domain uri_rdfs_domain $_221) true % 0.92/1.14 (icext $_221 uri_rdf_rest) true = true % 0.92/1.14 |- ifeq (iext uri_rdfs_domain uri_rdfs_domain $_221) true % 0.92/1.14 (icext $_221 uri_rdf_subject) true = true % 0.92/1.14 |- ifeq (iext uri_rdfs_domain uri_rdfs_domain $_221) true % 0.92/1.14 (icext $_221 uri_rdf_type) true = true % 0.92/1.14 |- ifeq (iext uri_rdfs_domain uri_rdfs_domain $_221) true % 0.92/1.14 (icext $_221 uri_rdf_value) true = true % 0.92/1.14 |- ifeq (iext uri_rdfs_domain uri_rdfs_domain $_221) true % 0.92/1.14 (icext $_221 uri_rdfs_comment) true = true % 0.92/1.14 |- ifeq (iext uri_rdfs_domain uri_rdfs_domain $_221) true % 0.92/1.14 (icext $_221 uri_rdfs_domain) true = true % 0.92/1.14 |- ifeq (iext uri_rdfs_domain uri_rdfs_domain $_221) true % 0.92/1.14 (icext $_221 uri_rdfs_isDefinedBy) true = true % 0.92/1.14 |- ifeq (iext uri_rdfs_domain uri_rdfs_domain $_221) true % 0.92/1.14 (icext $_221 uri_rdfs_label) true = true % 0.92/1.14 |- ifeq (iext uri_rdfs_domain uri_rdfs_domain $_221) true % 0.92/1.14 (icext $_221 uri_rdfs_member) true = true % 0.92/1.14 |- ifeq (iext uri_rdfs_domain uri_rdfs_domain $_221) true % 0.92/1.14 (icext $_221 uri_rdfs_range) true = true % 0.92/1.14 |- ifeq (iext uri_rdfs_domain uri_rdfs_domain $_221) true % 0.92/1.14 (icext $_221 uri_rdfs_seeAlso) true = true % 0.92/1.14 |- ifeq (iext uri_rdfs_domain uri_rdfs_domain $_221) true % 0.92/1.14 (icext $_221 uri_rdfs_subClassOf) true = true % 0.92/1.14 |- ifeq (iext uri_rdfs_domain uri_rdfs_domain $_221) true % 0.92/1.14 (icext $_221 uri_rdfs_subPropertyOf) true = true % 0.92/1.14 |- ifeq (iext uri_rdfs_domain uri_rdfs_range $_221) true % 0.92/1.14 (icext $_221 uri_rdf__1) true = true % 0.92/1.14 |- ifeq (iext uri_rdfs_domain uri_rdfs_range $_221) true % 0.92/1.14 (icext $_221 uri_rdf__2) true = true % 0.92/1.14 |- ifeq (iext uri_rdfs_domain uri_rdfs_range $_221) true % 0.92/1.14 (icext $_221 uri_rdf__3) true = true % 0.92/1.15 |- ifeq (iext uri_rdfs_domain uri_rdfs_range $_221) true % 0.92/1.15 (icext $_221 uri_rdf_first) true = true % 0.92/1.15 |- ifeq (iext uri_rdfs_domain uri_rdfs_range $_221) true % 0.92/1.15 (icext $_221 uri_rdf_predicate) true = true % 0.92/1.15 |- ifeq (iext uri_rdfs_domain uri_rdfs_range $_221) true % 0.92/1.15 (icext $_221 uri_rdf_rest) true = true % 0.92/1.15 |- ifeq (iext uri_rdfs_domain uri_rdfs_range $_221) true % 0.92/1.15 (icext $_221 uri_rdf_subject) true = true % 0.92/1.15 |- ifeq (iext uri_rdfs_domain uri_rdfs_range $_221) true % 0.92/1.15 (icext $_221 uri_rdf_type) true = true % 0.92/1.15 |- ifeq (iext uri_rdfs_domain uri_rdfs_range $_221) true % 0.92/1.15 (icext $_221 uri_rdf_value) true = true % 0.92/1.15 |- ifeq (iext uri_rdfs_domain uri_rdfs_range $_221) true % 0.92/1.15 (icext $_221 uri_rdfs_comment) true = true % 0.92/1.15 |- ifeq (iext uri_rdfs_domain uri_rdfs_range $_221) true % 0.92/1.15 (icext $_221 uri_rdfs_domain) true = true % 0.92/1.15 |- ifeq (iext uri_rdfs_domain uri_rdfs_range $_221) true % 0.92/1.15 (icext $_221 uri_rdfs_isDefinedBy) true = true % 0.92/1.15 |- ifeq (iext uri_rdfs_domain uri_rdfs_range $_221) true % 0.92/1.15 (icext $_221 uri_rdfs_label) true = true % 0.92/1.15 |- ifeq (iext uri_rdfs_domain uri_rdfs_range $_221) true % 0.92/1.15 (icext $_221 uri_rdfs_member) true = true % 0.92/1.15 |- ifeq (iext uri_rdfs_domain uri_rdfs_range $_221) true % 0.92/1.15 (icext $_221 uri_rdfs_range) true = true % 0.92/1.15 |- ifeq (iext uri_rdfs_domain uri_rdfs_range $_221) true % 0.92/1.15 (icext $_221 uri_rdfs_seeAlso) true = true % 0.92/1.15 |- ifeq (iext uri_rdfs_domain uri_rdfs_range $_221) true % 0.92/1.15 (icext $_221 uri_rdfs_subClassOf) true = true % 0.92/1.15 |- ifeq (iext uri_rdfs_domain uri_rdfs_range $_221) true % 0.92/1.15 (icext $_221 uri_rdfs_subPropertyOf) true = true % 0.92/1.15 |- ifeq (iext uri_rdfs_domain uri_rdfs_subClassOf $_221) true % 0.92/1.15 (icext $_221 uri_rdf_Alt) true = true % 0.92/1.15 |- ifeq (iext uri_rdfs_domain uri_rdfs_subClassOf $_221) true % 0.92/1.15 (icext $_221 uri_rdf_Bag) true = true % 0.92/1.15 |- ifeq (iext uri_rdfs_domain uri_rdfs_subClassOf $_221) true % 0.92/1.15 (icext $_221 uri_rdf_Property) true = true % 0.92/1.15 |- ifeq (iext uri_rdfs_domain uri_rdfs_subClassOf $_221) true % 0.92/1.15 (icext $_221 uri_rdf_XMLLiteral) true = true % 0.92/1.15 |- ifeq (iext uri_rdfs_domain uri_rdfs_subClassOf $_221) true % 0.92/1.15 (icext $_221 uri_rdfs_Class) true = true % 0.92/1.15 |- ifeq (iext uri_rdfs_domain uri_rdfs_subClassOf $_221) true % 0.92/1.15 (icext $_221 uri_rdfs_Container) true = true % 0.92/1.15 |- ifeq (iext uri_rdfs_domain uri_rdfs_subClassOf $_221) true % 0.92/1.15 (icext $_221 uri_rdfs_ContainerMembershipProperty) true = true % 0.92/1.15 |- ifeq (iext uri_rdfs_domain uri_rdfs_subClassOf $_221) true % 0.92/1.15 (icext $_221 uri_rdfs_Datatype) true = true % 0.92/1.15 |- ifeq (iext uri_rdfs_domain uri_rdfs_subClassOf $_221) true % 0.92/1.15 (icext $_221 uri_rdfs_Literal) true = true % 0.92/1.15 |- ifeq (iext uri_rdfs_domain uri_rdfs_subClassOf $_221) true % 0.92/1.15 (icext $_221 uri_rdfs_Resource) true = true % 0.92/1.15 |- ifeq (iext uri_rdfs_domain uri_rdfs_subClassOf $_221) true % 0.92/1.15 (icext $_221 uri_rdfs_Seq) true = true % 0.92/1.15 |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $_221) true % 0.92/1.15 (icext $_221 uri_owl_onProperty) true = true % 0.92/1.15 |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $_221) true % 0.92/1.15 (icext $_221 uri_owl_someValuesFrom) true = true % 0.92/1.15 |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $_221) true % 0.92/1.15 (icext $_221 uri_rdf__1) true = true % 0.92/1.15 |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $_221) true % 0.92/1.15 (icext $_221 uri_rdf__2) true = true % 0.92/1.15 |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $_221) true % 0.92/1.15 (icext $_221 uri_rdf__3) true = true % 0.92/1.15 |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $_221) true % 0.92/1.15 (icext $_221 uri_rdf_first) true = true % 0.92/1.15 |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $_221) true % 0.92/1.15 (icext $_221 uri_rdf_object) true = true % 0.92/1.15 |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $_221) true % 0.92/1.15 (icext $_221 uri_rdf_rest) true = true % 0.92/1.15 |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $_221) true % 0.92/1.15 (icext $_221 uri_rdf_subject) true = true % 0.92/1.15 |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $_221) true % 0.92/1.15 (icext $_221 uri_rdf_type) true = true % 0.92/1.15 |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $_221) true % 0.92/1.15 (icext $_221 uri_rdf_value) true = true % 0.92/1.15 |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $_221) true % 0.92/1.15 (icext $_221 uri_rdfs_domain) true = true % 0.92/1.15 |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $_221) true % 0.92/1.15 (icext $_221 uri_rdfs_isDefinedBy) true = true % 0.92/1.15 |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $_221) true % 0.92/1.15 (icext $_221 uri_rdfs_member) true = true % 0.92/1.15 |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $_221) true % 0.92/1.15 (icext $_221 uri_rdfs_range) true = true % 0.92/1.15 |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $_221) true % 0.92/1.15 (icext $_221 uri_rdfs_seeAlso) true = true % 0.92/1.15 |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $_221) true % 0.92/1.15 (icext $_221 uri_rdfs_subClassOf) true = true % 0.92/1.15 |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $_221) true % 0.92/1.15 (icext $_221 uri_rdfs_subPropertyOf) true = true % 0.92/1.15 |- ifeq (iext uri_rdf_first $_223 $_224) true (icext uri_rdf_List $_223) % 0.92/1.15 true = true % 0.92/1.15 |- ifeq (iext uri_rdf_object $_223 $_224) true % 0.92/1.15 (icext uri_rdfs_Statement $_223) true = true % 0.92/1.15 |- ifeq (iext uri_rdf_predicate $_223 $_224) true % 0.92/1.15 (icext uri_rdfs_Statement $_223) true = true % 0.92/1.15 |- ifeq (iext uri_rdf_rest $_223 $_224) true (icext uri_rdf_List $_223) % 0.92/1.15 true = true % 0.92/1.15 |- ifeq (iext uri_rdf_subject $_223 $_224) true % 0.92/1.15 (icext uri_rdfs_Statement $_223) true = true % 0.92/1.15 |- ifeq (iext uri_rdfs_comment $_223 $_224) true true true = true % 0.92/1.15 |- ifeq (iext uri_rdfs_domain $_223 $_224) true % 0.92/1.15 (icext uri_rdf_Property $_223) true = true % 0.92/1.15 |- ifeq (iext uri_rdfs_label $_223 $_224) true true true = true % 0.92/1.15 |- ifeq (iext uri_rdfs_range $_223 $_224) true % 0.92/1.15 (icext uri_rdf_Property $_223) true = true % 0.92/1.15 |- ifeq (iext uri_rdfs_subClassOf $_223 $_224) true % 0.92/1.15 (icext uri_rdfs_Class $_223) true = true % 0.92/1.15 |- ifeq (iext uri_rdfs_subPropertyOf $_223 $_224) true % 0.92/1.15 (icext uri_rdf_Property $_223) true = true % 0.92/1.15 |- icext uri_rdf_Property uri_rdf_predicate = true % 0.92/1.15 |- ifeq (iext uri_rdfs_domain $P uri_rdf_Property) true % 0.92/1.15 (ifeq (iext $P uri_rdf_predicate $Y) true true true) true = true % 0.92/1.15 |- iext uri_rdf_type uri_rdf_predicate uri_rdf_Property = true % 0.92/1.15 |- ip uri_rdf_predicate = true % 0.92/1.15 |- ifeq (iext uri_rdf_predicate $S $O) true true true = true % 0.92/1.15 |- iext uri_rdfs_subPropertyOf uri_rdf_predicate uri_rdf_predicate = true % 0.92/1.15 |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $C) true % 0.92/1.15 (icext $C uri_rdf_predicate) true = true % 0.92/1.15 |- icext uri_rdf_Property uri_rdfs_comment = true % 0.92/1.15 |- ifeq (iext uri_rdfs_domain $P uri_rdf_Property) true % 0.92/1.15 (ifeq (iext $P uri_rdfs_comment $Y) true true true) true = true % 0.92/1.15 |- iext uri_rdf_type uri_rdfs_comment uri_rdf_Property = true % 0.92/1.15 |- ip uri_rdfs_comment = true % 0.92/1.15 |- iext uri_rdfs_subPropertyOf uri_rdfs_comment uri_rdfs_comment = true % 0.92/1.15 |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $C) true % 0.92/1.15 (icext $C uri_rdfs_comment) true = true % 0.92/1.15 |- icext uri_rdf_Property uri_rdfs_label = true % 0.92/1.15 |- ifeq (iext uri_rdfs_domain $P uri_rdf_Property) true % 0.92/1.15 (ifeq (iext $P uri_rdfs_label $Y) true true true) true = true % 0.92/1.15 |- iext uri_rdf_type uri_rdfs_label uri_rdf_Property = true % 0.92/1.15 |- ip uri_rdfs_label = true % 0.92/1.15 |- iext uri_rdfs_subPropertyOf uri_rdfs_label uri_rdfs_label = true % 0.92/1.15 |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $C) true % 0.92/1.15 (icext $C uri_rdfs_label) true = true % 0.92/1.15 |- ifeq % 0.92/1.15 (iext uri_rdfs_range $_329 % 0.92/1.15 sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z) % 0.92/1.15 true (ifeq (iext $_329 $_330 uri_ex_s) true true true) true = true % 0.92/1.15 |- ifeq (iext uri_rdfs_range $_329 uri_owl_Class) true % 0.92/1.15 (ifeq (iext $_329 $_330 uri_ex_c) true true true) true = true % 0.92/1.15 |- ifeq (iext uri_rdfs_range $_329 uri_owl_ObjectProperty) true % 0.92/1.15 (ifeq (iext $_329 $_330 uri_ex_p) true true true) true = true % 0.92/1.15 |- ifeq (iext uri_rdfs_range $_329 uri_owl_Restriction) true % 0.92/1.15 (ifeq % 0.92/1.15 (iext $_329 $_330 % 0.92/1.15 sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z) % 0.92/1.15 true true true) true = true % 0.92/1.15 |- ifeq (iext uri_rdfs_range $_329 uri_rdf_List) true % 0.92/1.15 (ifeq (iext $_329 $_330 uri_rdf_nil) true true true) true = true % 0.92/1.15 |- ifeq (iext uri_rdfs_range $_329 uri_rdf_Property) true % 0.92/1.15 (ifeq (iext $_329 $_330 uri_owl_onProperty) true true true) true = % 0.92/1.15 true % 0.92/1.15 |- ifeq (iext uri_rdfs_range $_329 uri_rdf_Property) true % 0.92/1.15 (ifeq (iext $_329 $_330 uri_owl_someValuesFrom) true true true) true = % 0.92/1.15 true % 0.92/1.15 |- ifeq (iext uri_rdfs_range $_329 uri_rdf_Property) true % 0.92/1.15 (ifeq (iext $_329 $_330 uri_rdf__1) true true true) true = true % 0.92/1.15 |- ifeq (iext uri_rdfs_range $_329 uri_rdf_Property) true % 0.92/1.15 (ifeq (iext $_329 $_330 uri_rdf__2) true true true) true = true % 0.92/1.15 |- ifeq (iext uri_rdfs_range $_329 uri_rdf_Property) true % 0.92/1.15 (ifeq (iext $_329 $_330 uri_rdf__3) true true true) true = true % 0.92/1.15 |- ifeq (iext uri_rdfs_range $_329 uri_rdf_Property) true % 0.92/1.15 (ifeq (iext $_329 $_330 uri_rdf_first) true true true) true = true % 0.92/1.15 |- ifeq (iext uri_rdfs_range $_329 uri_rdf_Property) true % 0.92/1.15 (ifeq (iext $_329 $_330 uri_rdf_object) true true true) true = true % 0.92/1.15 |- ifeq (iext uri_rdfs_range $_329 uri_rdf_Property) true % 0.92/1.15 (ifeq (iext $_329 $_330 uri_rdf_predicate) true true true) true = true % 0.92/1.15 |- ifeq (iext uri_rdfs_range $_329 uri_rdf_Property) true % 0.92/1.15 (ifeq (iext $_329 $_330 uri_rdf_rest) true true true) true = true % 0.92/1.15 |- ifeq (iext uri_rdfs_range $_329 uri_rdf_Property) true % 0.92/1.15 (ifeq (iext $_329 $_330 uri_rdf_subject) true true true) true = true % 0.92/1.15 |- ifeq (iext uri_rdfs_range $_329 uri_rdf_Property) true % 0.92/1.15 (ifeq (iext $_329 $_330 uri_rdf_type) true true true) true = true % 0.92/1.15 |- ifeq (iext uri_rdfs_range $_329 uri_rdf_Property) true % 0.92/1.15 (ifeq (iext $_329 $_330 uri_rdf_value) true true true) true = true % 0.92/1.15 |- ifeq (iext uri_rdfs_range $_329 uri_rdf_Property) true % 0.92/1.15 (ifeq (iext $_329 $_330 uri_rdfs_comment) true true true) true = true % 0.92/1.15 |- ifeq (iext uri_rdfs_range $_329 uri_rdf_Property) true % 0.92/1.15 (ifeq (iext $_329 $_330 uri_rdfs_domain) true true true) true = true % 0.92/1.15 |- ifeq (iext uri_rdfs_range $_329 uri_rdf_Property) true % 0.92/1.15 (ifeq (iext $_329 $_330 uri_rdfs_isDefinedBy) true true true) true = % 0.92/1.15 true % 0.92/1.15 |- ifeq (iext uri_rdfs_range $_329 uri_rdf_Property) true % 0.92/1.15 (ifeq (iext $_329 $_330 uri_rdfs_label) true true true) true = true % 0.92/1.15 |- ifeq (iext uri_rdfs_range $_329 uri_rdf_Property) true % 0.92/1.15 (ifeq (iext $_329 $_330 uri_rdfs_member) true true true) true = true % 0.92/1.15 |- ifeq (iext uri_rdfs_range $_329 uri_rdf_Property) true % 0.92/1.15 (ifeq (iext $_329 $_330 uri_rdfs_range) true true true) true = true % 0.92/1.15 |- ifeq (iext uri_rdfs_range $_329 uri_rdf_Property) true % 0.92/1.15 (ifeq (iext $_329 $_330 uri_rdfs_seeAlso) true true true) true = true % 0.92/1.15 |- ifeq (iext uri_rdfs_range $_329 uri_rdf_Property) true % 0.92/1.15 (ifeq (iext $_329 $_330 uri_rdfs_subClassOf) true true true) true = % 0.92/1.15 true % 0.92/1.15 |- ifeq (iext uri_rdfs_range $_329 uri_rdf_Property) true % 0.92/1.15 (ifeq (iext $_329 $_330 uri_rdfs_subPropertyOf) true true true) true = % 0.92/1.15 true % 0.92/1.15 |- ifeq (iext uri_rdfs_range $_329 uri_rdfs_Class) true % 0.92/1.15 (ifeq (iext $_329 $_330 uri_rdf_Alt) true true true) true = true % 0.92/1.15 |- ifeq (iext uri_rdfs_range $_329 uri_rdfs_Class) true % 0.92/1.15 (ifeq (iext $_329 $_330 uri_rdf_Bag) true true true) true = true % 0.92/1.15 |- ifeq (iext uri_rdfs_range $_329 uri_rdfs_Class) true % 0.92/1.15 (ifeq (iext $_329 $_330 uri_rdf_Property) true true true) true = true % 0.92/1.15 |- ifeq (iext uri_rdfs_range $_329 uri_rdfs_Class) true % 0.92/1.15 (ifeq (iext $_329 $_330 uri_rdf_XMLLiteral) true true true) true = % 0.92/1.15 true % 0.92/1.15 |- ifeq (iext uri_rdfs_range $_329 uri_rdfs_Class) true % 0.92/1.15 (ifeq (iext $_329 $_330 uri_rdfs_Class) true true true) true = true % 0.92/1.15 |- ifeq (iext uri_rdfs_range $_329 uri_rdfs_Class) true % 0.92/1.15 (ifeq (iext $_329 $_330 uri_rdfs_Container) true true true) true = % 0.92/1.15 true % 0.92/1.15 |- ifeq (iext uri_rdfs_range $_329 uri_rdfs_Class) true % 0.92/1.15 (ifeq (iext $_329 $_330 uri_rdfs_ContainerMembershipProperty) true % 0.92/1.15 true true) true = true % 0.92/1.15 |- ifeq (iext uri_rdfs_range $_329 uri_rdfs_Class) true % 0.92/1.15 (ifeq (iext $_329 $_330 uri_rdfs_Datatype) true true true) true = true % 0.92/1.15 |- ifeq (iext uri_rdfs_range $_329 uri_rdfs_Class) true % 0.92/1.15 (ifeq (iext $_329 $_330 uri_rdfs_Literal) true true true) true = true % 0.92/1.15 |- ifeq (iext uri_rdfs_range $_329 uri_rdfs_Class) true % 0.92/1.15 (ifeq (iext $_329 $_330 uri_rdfs_Resource) true true true) true = true % 0.92/1.15 |- ifeq (iext uri_rdfs_range $_329 uri_rdfs_Class) true % 0.92/1.15 (ifeq (iext $_329 $_330 uri_rdfs_Seq) true true true) true = true % 0.92/1.15 |- ifeq (iext uri_rdfs_range $_329 uri_rdfs_ContainerMembershipProperty) % 0.92/1.15 true (ifeq (iext $_329 $_330 uri_rdf__1) true true true) true = true % 0.92/1.15 |- ifeq (iext uri_rdfs_range $_329 uri_rdfs_ContainerMembershipProperty) % 0.92/1.15 true (ifeq (iext $_329 $_330 uri_rdf__2) true true true) true = true % 0.92/1.15 |- ifeq (iext uri_rdfs_range $_329 uri_rdfs_ContainerMembershipProperty) % 0.92/1.15 true (ifeq (iext $_329 $_330 uri_rdf__3) true true true) true = true % 0.92/1.15 |- ifeq (iext uri_rdfs_range $_329 uri_rdfs_Datatype) true % 0.92/1.15 (ifeq (iext $_329 $_330 uri_rdf_XMLLiteral) true true true) true = % 0.92/1.15 true % 0.92/1.15 |- ifeq (iext uri_rdfs_range $_329 uri_rdfs_Resource) true % 0.92/1.15 (ifeq (iext $_329 $_330 $_331) true true true) true = true % 0.92/1.15 |- ifeq (iext uri_rdfs_range uri_owl_onProperty $_328) true % 0.92/1.15 (icext $_328 uri_ex_p) true = true % 0.92/1.15 |- ifeq (iext uri_rdfs_range uri_owl_someValuesFrom $_328) true % 0.92/1.15 (icext $_328 uri_ex_c) true = true % 0.92/1.15 |- ifeq (iext uri_rdfs_range uri_rdf_type $_328) true % 0.92/1.15 (icext $_328 uri_owl_Restriction) true = true % 0.92/1.15 |- ifeq (iext uri_rdfs_range uri_rdf_type $_328) true % 0.92/1.15 (icext $_328 uri_owl_Class) true = true % 0.92/1.15 |- ifeq (iext uri_rdfs_range uri_rdf_type $_328) true % 0.92/1.15 (icext $_328 uri_owl_ObjectProperty) true = true % 0.92/1.15 |- ifeq (iext uri_rdfs_range uri_rdf_type $_328) true % 0.92/1.15 (icext $_328 % 0.92/1.15 sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z) % 0.92/1.15 true = true % 0.92/1.15 |- ifeq (iext uri_rdfs_range uri_rdf_type $_328) true % 0.92/1.15 (icext $_328 uri_rdf_Property) true = true % 0.92/1.15 |- ifeq (iext uri_rdfs_range uri_rdf_type $_328) true % 0.92/1.15 (icext $_328 uri_rdfs_Class) true = true % 0.92/1.15 |- ifeq (iext uri_rdfs_range uri_rdf_type $_328) true % 0.92/1.15 (icext $_328 uri_rdfs_Datatype) true = true % 0.92/1.15 |- ifeq (iext uri_rdfs_range uri_rdf_type $_328) true % 0.92/1.15 (icext $_328 uri_rdfs_ContainerMembershipProperty) true = true % 0.92/1.15 |- ifeq (iext uri_rdfs_range uri_rdf_type $_328) true % 0.92/1.15 (icext $_328 uri_rdf_List) true = true % 0.92/1.15 |- ifeq (iext uri_rdfs_range uri_rdf_type $_328) true % 0.92/1.15 (icext $_328 uri_rdfs_Resource) true = true % 0.92/1.15 |- ifeq (iext uri_rdfs_range uri_rdfs_domain $_328) true % 0.92/1.15 (icext $_328 uri_rdfs_Resource) true = true % 0.92/1.15 |- ifeq (iext uri_rdfs_range uri_rdfs_domain $_328) true % 0.92/1.15 (icext $_328 uri_rdf_List) true = true % 0.92/1.15 |- ifeq (iext uri_rdfs_range uri_rdfs_domain $_328) true % 0.92/1.15 (icext $_328 uri_rdfs_Statement) true = true % 0.92/1.15 |- ifeq (iext uri_rdfs_range uri_rdfs_domain $_328) true % 0.92/1.15 (icext $_328 uri_rdf_Property) true = true % 0.92/1.15 |- ifeq (iext uri_rdfs_range uri_rdfs_domain $_328) true % 0.92/1.15 (icext $_328 uri_rdfs_Class) true = true % 0.92/1.15 |- ifeq (iext uri_rdfs_range uri_rdfs_range $_328) true % 0.92/1.15 (icext $_328 uri_rdfs_Resource) true = true % 0.92/1.15 |- ifeq (iext uri_rdfs_range uri_rdfs_range $_328) true % 0.92/1.15 (icext $_328 uri_rdf_List) true = true % 0.92/1.15 |- ifeq (iext uri_rdfs_range uri_rdfs_range $_328) true % 0.92/1.15 (icext $_328 uri_rdfs_Class) true = true % 0.92/1.15 |- ifeq (iext uri_rdfs_range uri_rdfs_range $_328) true % 0.92/1.15 (icext $_328 uri_rdfs_Literal) true = true % 0.92/1.15 |- ifeq (iext uri_rdfs_range uri_rdfs_range $_328) true % 0.92/1.15 (icext $_328 uri_rdf_Property) true = true % 0.92/1.15 |- ifeq (iext uri_rdfs_range uri_rdfs_subClassOf $_328) true % 0.92/1.15 (icext $_328 uri_rdf_Alt) true = true % 0.92/1.15 |- ifeq (iext uri_rdfs_range uri_rdfs_subClassOf $_328) true % 0.92/1.15 (icext $_328 uri_rdfs_Container) true = true % 0.92/1.15 |- ifeq (iext uri_rdfs_range uri_rdfs_subClassOf $_328) true % 0.92/1.15 (icext $_328 uri_rdfs_Resource) true = true % 0.92/1.15 |- ifeq (iext uri_rdfs_range uri_rdfs_subClassOf $_328) true % 0.92/1.15 (icext $_328 uri_rdf_Bag) true = true % 0.92/1.15 |- ifeq (iext uri_rdfs_range uri_rdfs_subClassOf $_328) true % 0.92/1.15 (icext $_328 uri_rdf_Property) true = true % 0.92/1.15 |- ifeq (iext uri_rdfs_range uri_rdfs_subClassOf $_328) true % 0.92/1.15 (icext $_328 uri_rdf_XMLLiteral) true = true % 0.92/1.15 |- ifeq (iext uri_rdfs_range uri_rdfs_subClassOf $_328) true % 0.92/1.15 (icext $_328 uri_rdfs_Literal) true = true % 0.92/1.15 |- ifeq (iext uri_rdfs_range uri_rdfs_subClassOf $_328) true % 0.92/1.15 (icext $_328 uri_rdfs_Class) true = true % 0.92/1.15 |- ifeq (iext uri_rdfs_range uri_rdfs_subClassOf $_328) true % 0.92/1.15 (icext $_328 uri_rdfs_ContainerMembershipProperty) true = true % 0.92/1.16 |- ifeq (iext uri_rdfs_range uri_rdfs_subClassOf $_328) true % 0.92/1.16 (icext $_328 uri_rdfs_Datatype) true = true % 0.92/1.16 |- ifeq (iext uri_rdfs_range uri_rdfs_subClassOf $_328) true % 0.92/1.16 (icext $_328 uri_rdfs_Seq) true = true % 0.92/1.16 |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_328) true % 0.92/1.16 (icext $_328 uri_owl_onProperty) true = true % 0.92/1.16 |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_328) true % 0.92/1.16 (icext $_328 uri_owl_someValuesFrom) true = true % 0.92/1.16 |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_328) true % 0.92/1.16 (icext $_328 uri_rdf__1) true = true % 0.92/1.16 |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_328) true % 0.92/1.16 (icext $_328 uri_rdfs_member) true = true % 0.92/1.16 |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_328) true % 0.92/1.16 (icext $_328 uri_rdf__2) true = true % 0.92/1.16 |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_328) true % 0.92/1.16 (icext $_328 uri_rdf__3) true = true % 0.92/1.16 |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_328) true % 0.92/1.16 (icext $_328 uri_rdf_first) true = true % 0.92/1.16 |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_328) true % 0.92/1.16 (icext $_328 uri_rdf_object) true = true % 0.92/1.16 |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_328) true % 0.92/1.16 (icext $_328 uri_rdf_predicate) true = true % 0.92/1.16 |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_328) true % 0.92/1.16 (icext $_328 uri_rdf_rest) true = true % 0.92/1.16 |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_328) true % 0.92/1.16 (icext $_328 uri_rdf_subject) true = true % 0.92/1.16 |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_328) true % 0.92/1.16 (icext $_328 uri_rdf_type) true = true % 0.92/1.16 |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_328) true % 0.92/1.16 (icext $_328 uri_rdf_value) true = true % 0.92/1.16 |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_328) true % 0.92/1.16 (icext $_328 uri_rdfs_comment) true = true % 0.92/1.16 |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_328) true % 0.92/1.16 (icext $_328 uri_rdfs_domain) true = true % 0.92/1.16 |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_328) true % 0.92/1.16 (icext $_328 uri_rdfs_isDefinedBy) true = true % 0.92/1.16 |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_328) true % 0.92/1.16 (icext $_328 uri_rdfs_seeAlso) true = true % 0.92/1.16 |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_328) true % 0.92/1.16 (icext $_328 uri_rdfs_label) true = true % 0.92/1.16 |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_328) true % 0.92/1.16 (icext $_328 uri_rdfs_range) true = true % 0.92/1.16 |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_328) true % 0.92/1.16 (icext $_328 uri_rdfs_subClassOf) true = true % 0.92/1.16 |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_328) true % 0.92/1.16 (icext $_328 uri_rdfs_subPropertyOf) true = true % 0.92/1.16 |- ifeq (iext uri_rdf_rest $_330 $_331) true (icext uri_rdf_List $_331) % 0.92/1.16 true = true % 0.92/1.16 |- ifeq (iext uri_rdf_type $_330 $_331) true (icext uri_rdfs_Class $_331) % 0.92/1.16 true = true % 0.92/1.16 |- ifeq (iext uri_rdfs_comment $_330 $_331) true % 0.92/1.16 (icext uri_rdfs_Literal $_331) true = true % 0.92/1.16 |- ifeq (iext uri_rdfs_domain $_330 $_331) true % 0.92/1.16 (icext uri_rdfs_Class $_331) true = true % 0.92/1.16 |- ifeq (iext uri_rdfs_label $_330 $_331) true % 0.92/1.16 (icext uri_rdfs_Literal $_331) true = true % 0.92/1.16 |- ifeq (iext uri_rdfs_range $_330 $_331) true (icext uri_rdfs_Class $_331) % 0.92/1.16 true = true % 0.92/1.16 |- ifeq (iext uri_rdfs_subClassOf $_330 $_331) true % 0.92/1.16 (icext uri_rdfs_Class $_331) true = true % 0.92/1.16 |- ifeq (iext uri_rdfs_subPropertyOf $_330 $_331) true % 0.92/1.16 (icext uri_rdf_Property $_331) true = true % 0.92/1.16 |- icext uri_rdfs_Class uri_owl_Restriction = true % 0.92/1.16 |- ifeq (iext uri_rdfs_range $P uri_rdfs_Class) true % 0.92/1.16 (ifeq (iext $P $X uri_owl_Restriction) true true true) true = true % 0.92/1.16 |- ifeq (iext uri_rdfs_domain $P uri_rdfs_Class) true % 0.92/1.16 (ifeq (iext $P uri_owl_Restriction $Y) true true true) true = true % 0.92/1.16 |- iext uri_rdf_type uri_owl_Restriction uri_rdfs_Class = true % 0.92/1.16 |- ic uri_owl_Restriction = true % 0.92/1.16 |- iext uri_rdfs_subClassOf uri_owl_Restriction uri_owl_Restriction = true % 0.92/1.16 |- iext uri_rdfs_subClassOf uri_owl_Restriction uri_rdfs_Resource = true % 0.92/1.16 |- ifeq (iext uri_rdfs_range uri_rdfs_subClassOf $C) true % 0.92/1.16 (icext $C uri_owl_Restriction) true = true % 0.92/1.16 |- ifeq (iext uri_rdfs_domain uri_rdfs_subClassOf $C) true % 0.92/1.16 (icext $C uri_owl_Restriction) true = true % 0.92/1.16 |- ifeq (iext uri_rdfs_subClassOf $C uri_owl_Restriction) true % 0.92/1.16 (iext uri_rdfs_subClassOf $C uri_rdfs_Resource) true = true % 0.92/1.16 |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Resource $E) true % 0.92/1.16 (iext uri_rdfs_subClassOf uri_owl_Restriction $E) true = true % 0.92/1.16 |- icext uri_rdfs_Class uri_owl_Class = true % 0.92/1.16 |- ifeq (iext uri_rdfs_range $P uri_rdfs_Class) true % 0.92/1.16 (ifeq (iext $P $X uri_owl_Class) true true true) true = true % 0.92/1.16 |- ifeq (iext uri_rdfs_domain $P uri_rdfs_Class) true % 0.92/1.16 (ifeq (iext $P uri_owl_Class $Y) true true true) true = true % 0.92/1.16 |- iext uri_rdf_type uri_owl_Class uri_rdfs_Class = true % 0.92/1.16 |- ic uri_owl_Class = true % 0.92/1.16 |- iext uri_rdfs_subClassOf uri_owl_Class uri_owl_Class = true % 0.92/1.16 |- iext uri_rdfs_subClassOf uri_owl_Class uri_rdfs_Resource = true % 0.92/1.16 |- ifeq (iext uri_rdfs_range uri_rdfs_subClassOf $C) true % 0.92/1.16 (icext $C uri_owl_Class) true = true % 0.92/1.16 |- ifeq (iext uri_rdfs_domain uri_rdfs_subClassOf $C) true % 0.92/1.16 (icext $C uri_owl_Class) true = true % 0.92/1.16 |- ifeq (iext uri_rdfs_subClassOf $C uri_owl_Class) true % 0.92/1.16 (iext uri_rdfs_subClassOf $C uri_rdfs_Resource) true = true % 0.92/1.16 |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Resource $E) true % 0.92/1.16 (iext uri_rdfs_subClassOf uri_owl_Class $E) true = true % 0.92/1.16 |- icext uri_rdfs_Class uri_owl_ObjectProperty = true % 0.92/1.16 |- ifeq (iext uri_rdfs_range $P uri_rdfs_Class) true % 0.92/1.16 (ifeq (iext $P $X uri_owl_ObjectProperty) true true true) true = true % 0.92/1.16 |- ifeq (iext uri_rdfs_domain $P uri_rdfs_Class) true % 0.92/1.16 (ifeq (iext $P uri_owl_ObjectProperty $Y) true true true) true = true % 0.92/1.16 |- iext uri_rdf_type uri_owl_ObjectProperty uri_rdfs_Class = true % 0.92/1.16 |- ic uri_owl_ObjectProperty = true % 0.92/1.16 |- iext uri_rdfs_subClassOf uri_owl_ObjectProperty uri_owl_ObjectProperty = % 0.92/1.16 true % 0.92/1.16 |- iext uri_rdfs_subClassOf uri_owl_ObjectProperty uri_rdfs_Resource = true % 0.92/1.16 |- ifeq (iext uri_rdfs_range uri_rdfs_subClassOf $C) true % 0.92/1.16 (icext $C uri_owl_ObjectProperty) true = true % 0.92/1.16 |- ifeq (iext uri_rdfs_domain uri_rdfs_subClassOf $C) true % 0.92/1.16 (icext $C uri_owl_ObjectProperty) true = true % 0.92/1.16 |- ifeq (iext uri_rdfs_subClassOf $C uri_owl_ObjectProperty) true % 0.92/1.16 (iext uri_rdfs_subClassOf $C uri_rdfs_Resource) true = true % 0.92/1.16 |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Resource $E) true % 0.92/1.16 (iext uri_rdfs_subClassOf uri_owl_ObjectProperty $E) true = true % 0.92/1.16 |- icext uri_rdfs_Class % 0.92/1.16 sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z = % 0.92/1.16 true % 0.92/1.16 |- ifeq (iext uri_rdfs_range $P uri_rdfs_Class) true % 0.92/1.16 (ifeq % 0.92/1.16 (iext $P $X % 0.92/1.16 sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z) % 0.92/1.16 true true true) true = true % 0.92/1.16 |- ifeq (iext uri_rdfs_domain $P uri_rdfs_Class) true % 0.92/1.16 (ifeq % 0.92/1.16 (iext $P % 0.92/1.16 sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z % 0.92/1.16 $Y) true true true) true = true % 0.92/1.16 |- iext uri_rdf_type % 0.92/1.16 sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z % 0.92/1.16 uri_rdfs_Class = true % 0.92/1.16 |- ic % 0.92/1.16 sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z = % 0.92/1.16 true % 0.92/1.16 |- iext uri_rdfs_subClassOf % 0.92/1.16 sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z % 0.92/1.16 sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z = % 0.92/1.16 true % 0.92/1.16 |- iext uri_rdfs_subClassOf % 0.92/1.16 sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z % 0.92/1.16 uri_rdfs_Resource = true % 0.92/1.16 |- ifeq (iext uri_rdfs_range uri_rdfs_subClassOf $C) true % 0.92/1.16 (icext $C % 0.92/1.16 sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z) % 0.92/1.16 true = true % 0.92/1.16 |- ifeq (iext uri_rdfs_domain uri_rdfs_subClassOf $C) true % 0.92/1.16 (icext $C % 0.92/1.16 sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z) % 0.92/1.16 true = true % 0.92/1.16 |- ifeq % 0.92/1.16 (iext uri_rdfs_subClassOf $C % 0.92/1.16 sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z) % 0.92/1.16 true (iext uri_rdfs_subClassOf $C uri_rdfs_Resource) true = true % 1.00/1.16 |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Resource $E) true % 1.00/1.16 (iext uri_rdfs_subClassOf % 1.00/1.16 sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z % 1.00/1.16 $E) true = true % 1.00/1.16 |- icext uri_rdfs_Class uri_rdf_List = true % 1.00/1.16 |- ifeq (iext uri_rdfs_range $P uri_rdfs_Class) true % 1.00/1.16 (ifeq (iext $P $X uri_rdf_List) true true true) true = true % 1.00/1.16 |- ifeq (iext uri_rdfs_domain $P uri_rdfs_Class) true % 1.00/1.16 (ifeq (iext $P uri_rdf_List $Y) true true true) true = true % 1.00/1.16 |- iext uri_rdf_type uri_rdf_List uri_rdfs_Class = true % 1.00/1.16 |- ic uri_rdf_List = true % 1.00/1.16 |- iext uri_rdfs_subClassOf uri_rdf_List uri_rdf_List = true % 1.00/1.16 |- iext uri_rdfs_subClassOf uri_rdf_List uri_rdfs_Resource = true % 1.00/1.16 |- ifeq (iext uri_rdfs_range uri_rdfs_subClassOf $C) true % 1.00/1.16 (icext $C uri_rdf_List) true = true % 1.00/1.16 |- ifeq (iext uri_rdfs_domain uri_rdfs_subClassOf $C) true % 1.00/1.16 (icext $C uri_rdf_List) true = true % 1.00/1.16 |- ifeq (iext uri_rdfs_subClassOf $C uri_rdf_List) true % 1.00/1.16 (iext uri_rdfs_subClassOf $C uri_rdfs_Resource) true = true % 1.00/1.16 |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Resource $E) true % 1.00/1.16 (iext uri_rdfs_subClassOf uri_rdf_List $E) true = true % 1.00/1.16 |- icext uri_rdfs_Class uri_rdfs_Statement = true % 1.00/1.16 |- ifeq (iext uri_rdfs_range $P uri_rdfs_Class) true % 1.00/1.16 (ifeq (iext $P $X uri_rdfs_Statement) true true true) true = true % 1.00/1.16 |- ifeq (iext uri_rdfs_domain $P uri_rdfs_Class) true % 1.00/1.16 (ifeq (iext $P uri_rdfs_Statement $Y) true true true) true = true % 1.00/1.16 |- iext uri_rdf_type uri_rdfs_Statement uri_rdfs_Class = true % 1.00/1.16 |- ic uri_rdfs_Statement = true % 1.00/1.16 |- iext uri_rdfs_subClassOf uri_rdfs_Statement uri_rdfs_Statement = true % 1.00/1.16 |- iext uri_rdfs_subClassOf uri_rdfs_Statement uri_rdfs_Resource = true % 1.00/1.16 |- ifeq (iext uri_rdfs_range uri_rdfs_subClassOf $C) true % 1.00/1.16 (icext $C uri_rdfs_Statement) true = true % 1.00/1.16 |- ifeq (iext uri_rdfs_domain uri_rdfs_subClassOf $C) true % 1.00/1.16 (icext $C uri_rdfs_Statement) true = true % 1.00/1.16 |- ifeq (iext uri_rdfs_subClassOf $C uri_rdfs_Statement) true % 1.00/1.16 (iext uri_rdfs_subClassOf $C uri_rdfs_Resource) true = true % 1.00/1.16 |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Resource $E) true % 1.00/1.16 (iext uri_rdfs_subClassOf uri_rdfs_Statement $E) true = true % 1.00/1.16 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_owl_onProperty) true % 1.00/1.16 (ifeq % 1.00/1.16 (iext $_438 % 1.00/1.16 sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z % 1.00/1.16 uri_ex_p) true true true) true = true % 1.00/1.16 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_owl_someValuesFrom) true % 1.00/1.16 (ifeq % 1.00/1.16 (iext $_438 % 1.00/1.16 sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z % 1.00/1.16 uri_ex_c) true true true) true = true % 1.00/1.16 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdf_type) true % 1.00/1.16 (ifeq % 1.00/1.16 (iext $_438 % 1.00/1.16 sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z % 1.00/1.16 uri_owl_Restriction) true true true) true = true % 1.00/1.16 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdf_type) true % 1.00/1.16 (ifeq % 1.00/1.16 (iext $_438 % 1.00/1.16 sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z % 1.00/1.16 uri_rdfs_Class) true true true) true = true % 1.00/1.16 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdf_type) true % 1.00/1.16 (ifeq (iext $_438 uri_ex_c uri_owl_Class) true true true) true = true % 1.00/1.16 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdf_type) true % 1.00/1.16 (ifeq (iext $_438 uri_ex_p uri_owl_ObjectProperty) true true true) % 1.00/1.16 true = true % 1.00/1.16 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdf_type) true % 1.00/1.16 (ifeq % 1.00/1.16 (iext $_438 uri_ex_s % 1.00/1.16 sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z) % 1.00/1.16 true true true) true = true % 1.00/1.16 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdf_type) true % 1.00/1.16 (ifeq (iext $_438 uri_owl_Class uri_rdfs_Class) true true true) true = % 1.00/1.16 true % 1.00/1.16 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdf_type) true % 1.00/1.16 (ifeq (iext $_438 uri_owl_ObjectProperty uri_rdfs_Class) true true % 1.00/1.16 true) true = true % 1.00/1.16 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdf_type) true % 1.00/1.16 (ifeq (iext $_438 uri_owl_Restriction uri_rdfs_Class) true true true) % 1.00/1.16 true = true % 1.00/1.16 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdf_type) true % 1.00/1.16 (ifeq (iext $_438 uri_owl_onProperty uri_rdf_Property) true true true) % 1.00/1.16 true = true % 1.00/1.16 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdf_type) true % 1.00/1.16 (ifeq (iext $_438 uri_owl_someValuesFrom uri_rdf_Property) true true % 1.00/1.16 true) true = true % 1.00/1.16 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdf_type) true % 1.00/1.16 (ifeq (iext $_438 uri_rdf_Alt uri_rdfs_Class) true true true) true = % 1.00/1.16 true % 1.00/1.16 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdf_type) true % 1.00/1.16 (ifeq (iext $_438 uri_rdf_Bag uri_rdfs_Class) true true true) true = % 1.00/1.16 true % 1.00/1.16 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdf_type) true % 1.00/1.16 (ifeq (iext $_438 uri_rdf_List uri_rdfs_Class) true true true) true = % 1.00/1.16 true % 1.00/1.16 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdf_type) true % 1.00/1.16 (ifeq (iext $_438 uri_rdf_Property uri_rdfs_Class) true true true) % 1.00/1.16 true = true % 1.00/1.16 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdf_type) true % 1.00/1.16 (ifeq (iext $_438 uri_rdf_XMLLiteral uri_rdfs_Class) true true true) % 1.00/1.16 true = true % 1.00/1.16 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdf_type) true % 1.00/1.16 (ifeq (iext $_438 uri_rdf_XMLLiteral uri_rdfs_Datatype) true true % 1.00/1.16 true) true = true % 1.00/1.16 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdf_type) true % 1.00/1.16 (ifeq (iext $_438 uri_rdf__1 uri_rdf_Property) true true true) true = % 1.00/1.16 true % 1.00/1.16 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdf_type) true % 1.00/1.16 (ifeq (iext $_438 uri_rdf__1 uri_rdfs_ContainerMembershipProperty) % 1.00/1.16 true true true) true = true % 1.00/1.16 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdf_type) true % 1.00/1.16 (ifeq (iext $_438 uri_rdf__2 uri_rdf_Property) true true true) true = % 1.00/1.16 true % 1.00/1.16 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdf_type) true % 1.00/1.16 (ifeq (iext $_438 uri_rdf__2 uri_rdfs_ContainerMembershipProperty) % 1.00/1.16 true true true) true = true % 1.00/1.16 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdf_type) true % 1.00/1.16 (ifeq (iext $_438 uri_rdf__3 uri_rdf_Property) true true true) true = % 1.00/1.16 true % 1.00/1.16 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdf_type) true % 1.00/1.16 (ifeq (iext $_438 uri_rdf__3 uri_rdfs_ContainerMembershipProperty) % 1.00/1.16 true true true) true = true % 1.00/1.16 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdf_type) true % 1.00/1.16 (ifeq (iext $_438 uri_rdf_first uri_rdf_Property) true true true) % 1.00/1.16 true = true % 1.00/1.16 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdf_type) true % 1.00/1.16 (ifeq (iext $_438 uri_rdf_nil uri_rdf_List) true true true) true = % 1.00/1.16 true % 1.00/1.16 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdf_type) true % 1.00/1.16 (ifeq (iext $_438 uri_rdf_object uri_rdf_Property) true true true) % 1.00/1.16 true = true % 1.00/1.16 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdf_type) true % 1.00/1.16 (ifeq (iext $_438 uri_rdf_predicate uri_rdf_Property) true true true) % 1.00/1.16 true = true % 1.00/1.16 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdf_type) true % 1.00/1.16 (ifeq (iext $_438 uri_rdf_rest uri_rdf_Property) true true true) % 1.00/1.16 true = true % 1.00/1.16 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdf_type) true % 1.00/1.16 (ifeq (iext $_438 uri_rdf_subject uri_rdf_Property) true true true) % 1.00/1.16 true = true % 1.00/1.16 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdf_type) true % 1.00/1.16 (ifeq (iext $_438 uri_rdf_type uri_rdf_Property) true true true) % 1.00/1.16 true = true % 1.00/1.16 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdf_type) true % 1.00/1.16 (ifeq (iext $_438 uri_rdf_value uri_rdf_Property) true true true) % 1.00/1.16 true = true % 1.00/1.16 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdf_type) true % 1.00/1.16 (ifeq (iext $_438 uri_rdfs_Class uri_rdfs_Class) true true true) % 1.00/1.16 true = true % 1.00/1.16 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdf_type) true % 1.00/1.16 (ifeq (iext $_438 uri_rdfs_Container uri_rdfs_Class) true true true) % 1.00/1.16 true = true % 1.00/1.16 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdf_type) true % 1.00/1.16 (ifeq (iext $_438 uri_rdfs_ContainerMembershipProperty uri_rdfs_Class) % 1.00/1.16 true true true) true = true % 1.00/1.16 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdf_type) true % 1.00/1.16 (ifeq (iext $_438 uri_rdfs_Datatype uri_rdfs_Class) true true true) % 1.00/1.16 true = true % 1.00/1.16 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdf_type) true % 1.00/1.16 (ifeq (iext $_438 uri_rdfs_Literal uri_rdfs_Class) true true true) % 1.00/1.16 true = true % 1.00/1.16 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdf_type) true % 1.00/1.16 (ifeq (iext $_438 uri_rdfs_Resource uri_rdfs_Class) true true true) % 1.00/1.16 true = true % 1.00/1.16 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdf_type) true % 1.00/1.16 (ifeq (iext $_438 uri_rdfs_Seq uri_rdfs_Class) true true true) true = % 1.00/1.16 true % 1.00/1.16 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdf_type) true % 1.00/1.16 (ifeq (iext $_438 uri_rdfs_Statement uri_rdfs_Class) true true true) % 1.00/1.16 true = true % 1.00/1.16 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdf_type) true % 1.00/1.16 (ifeq (iext $_438 uri_rdfs_comment uri_rdf_Property) true true true) % 1.00/1.16 true = true % 1.00/1.16 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdf_type) true % 1.00/1.16 (ifeq (iext $_438 uri_rdfs_domain uri_rdf_Property) true true true) % 1.00/1.16 true = true % 1.00/1.16 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdf_type) true % 1.00/1.16 (ifeq (iext $_438 uri_rdfs_isDefinedBy uri_rdf_Property) true true % 1.00/1.16 true) true = true % 1.00/1.16 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdf_type) true % 1.00/1.16 (ifeq (iext $_438 uri_rdfs_label uri_rdf_Property) true true true) % 1.00/1.16 true = true % 1.00/1.16 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdf_type) true % 1.00/1.16 (ifeq (iext $_438 uri_rdfs_member uri_rdf_Property) true true true) % 1.00/1.16 true = true % 1.00/1.16 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdf_type) true % 1.00/1.16 (ifeq (iext $_438 uri_rdfs_range uri_rdf_Property) true true true) % 1.00/1.16 true = true % 1.00/1.16 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdf_type) true % 1.00/1.16 (ifeq (iext $_438 uri_rdfs_seeAlso uri_rdf_Property) true true true) % 1.00/1.16 true = true % 1.00/1.16 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdf_type) true % 1.00/1.16 (ifeq (iext $_438 uri_rdfs_subClassOf uri_rdf_Property) true true % 1.00/1.16 true) true = true % 1.00/1.16 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdf_type) true % 1.00/1.16 (ifeq (iext $_438 uri_rdfs_subPropertyOf uri_rdf_Property) true true % 1.00/1.16 true) true = true % 1.00/1.16 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdf_type) true % 1.00/1.16 (ifeq (iext $_438 $_440 uri_rdfs_Resource) true true true) true = true % 1.00/1.16 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdfs_domain) true % 1.00/1.16 (ifeq (iext $_438 uri_rdf__1 uri_rdfs_Resource) true true true) true = % 1.00/1.16 true % 1.00/1.17 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdfs_domain) true % 1.00/1.17 (ifeq (iext $_438 uri_rdf__2 uri_rdfs_Resource) true true true) true = % 1.00/1.17 true % 1.00/1.17 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdfs_domain) true % 1.00/1.17 (ifeq (iext $_438 uri_rdf__3 uri_rdfs_Resource) true true true) true = % 1.00/1.17 true % 1.00/1.17 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdfs_domain) true % 1.00/1.17 (ifeq (iext $_438 uri_rdf_first uri_rdf_List) true true true) true = % 1.00/1.17 true % 1.00/1.17 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdfs_domain) true % 1.00/1.17 (ifeq (iext $_438 uri_rdf_object uri_rdfs_Statement) true true true) % 1.00/1.17 true = true % 1.00/1.17 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdfs_domain) true % 1.00/1.17 (ifeq (iext $_438 uri_rdf_predicate uri_rdfs_Statement) true true % 1.00/1.17 true) true = true % 1.00/1.17 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdfs_domain) true % 1.00/1.17 (ifeq (iext $_438 uri_rdf_rest uri_rdf_List) true true true) true = % 1.00/1.17 true % 1.00/1.17 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdfs_domain) true % 1.00/1.17 (ifeq (iext $_438 uri_rdf_subject uri_rdfs_Statement) true true true) % 1.00/1.17 true = true % 1.00/1.17 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdfs_domain) true % 1.00/1.17 (ifeq (iext $_438 uri_rdf_type uri_rdfs_Resource) true true true) % 1.00/1.17 true = true % 1.00/1.17 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdfs_domain) true % 1.00/1.17 (ifeq (iext $_438 uri_rdf_value uri_rdfs_Resource) true true true) % 1.00/1.17 true = true % 1.00/1.17 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdfs_domain) true % 1.00/1.17 (ifeq (iext $_438 uri_rdfs_comment uri_rdfs_Resource) true true true) % 1.00/1.17 true = true % 1.00/1.17 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdfs_domain) true % 1.00/1.17 (ifeq (iext $_438 uri_rdfs_domain uri_rdf_Property) true true true) % 1.00/1.17 true = true % 1.00/1.17 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdfs_domain) true % 1.00/1.17 (ifeq (iext $_438 uri_rdfs_isDefinedBy uri_rdfs_Resource) true true % 1.00/1.17 true) true = true % 1.00/1.17 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdfs_domain) true % 1.00/1.17 (ifeq (iext $_438 uri_rdfs_label uri_rdfs_Resource) true true true) % 1.00/1.17 true = true % 1.00/1.17 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdfs_domain) true % 1.00/1.17 (ifeq (iext $_438 uri_rdfs_member uri_rdfs_Resource) true true true) % 1.00/1.17 true = true % 1.00/1.17 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdfs_domain) true % 1.00/1.17 (ifeq (iext $_438 uri_rdfs_range uri_rdf_Property) true true true) % 1.00/1.17 true = true % 1.00/1.17 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdfs_domain) true % 1.00/1.17 (ifeq (iext $_438 uri_rdfs_seeAlso uri_rdfs_Resource) true true true) % 1.00/1.17 true = true % 1.00/1.17 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdfs_domain) true % 1.00/1.17 (ifeq (iext $_438 uri_rdfs_subClassOf uri_rdfs_Class) true true true) % 1.00/1.17 true = true % 1.00/1.17 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdfs_domain) true % 1.00/1.17 (ifeq (iext $_438 uri_rdfs_subPropertyOf uri_rdf_Property) true true % 1.00/1.17 true) true = true % 1.00/1.17 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdfs_range) true % 1.00/1.17 (ifeq (iext $_438 uri_rdf__1 uri_rdfs_Resource) true true true) true = % 1.00/1.17 true % 1.00/1.17 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdfs_range) true % 1.00/1.17 (ifeq (iext $_438 uri_rdf__2 uri_rdfs_Resource) true true true) true = % 1.00/1.17 true % 1.00/1.17 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdfs_range) true % 1.00/1.17 (ifeq (iext $_438 uri_rdf__3 uri_rdfs_Resource) true true true) true = % 1.00/1.17 true % 1.00/1.17 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdfs_range) true % 1.00/1.17 (ifeq (iext $_438 uri_rdf_first uri_rdfs_Resource) true true true) % 1.00/1.17 true = true % 1.00/1.17 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdfs_range) true % 1.00/1.17 (ifeq (iext $_438 uri_rdf_predicate uri_rdfs_Resource) true true true) % 1.00/1.17 true = true % 1.00/1.17 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdfs_range) true % 1.00/1.17 (ifeq (iext $_438 uri_rdf_rest uri_rdf_List) true true true) true = % 1.00/1.17 true % 1.00/1.17 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdfs_range) true % 1.00/1.17 (ifeq (iext $_438 uri_rdf_subject uri_rdfs_Resource) true true true) % 1.00/1.17 true = true % 1.00/1.17 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdfs_range) true % 1.00/1.17 (ifeq (iext $_438 uri_rdf_type uri_rdfs_Class) true true true) true = % 1.00/1.17 true % 1.00/1.17 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdfs_range) true % 1.00/1.17 (ifeq (iext $_438 uri_rdf_value uri_rdfs_Resource) true true true) % 1.00/1.17 true = true % 1.00/1.17 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdfs_range) true % 1.00/1.17 (ifeq (iext $_438 uri_rdfs_comment uri_rdfs_Literal) true true true) % 1.00/1.17 true = true % 1.00/1.17 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdfs_range) true % 1.00/1.17 (ifeq (iext $_438 uri_rdfs_domain uri_rdfs_Class) true true true) % 1.00/1.17 true = true % 1.00/1.17 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdfs_range) true % 1.00/1.17 (ifeq (iext $_438 uri_rdfs_isDefinedBy uri_rdfs_Resource) true true % 1.00/1.17 true) true = true % 1.00/1.17 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdfs_range) true % 1.00/1.17 (ifeq (iext $_438 uri_rdfs_label uri_rdfs_Literal) true true true) % 1.00/1.17 true = true % 1.00/1.17 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdfs_range) true % 1.00/1.17 (ifeq (iext $_438 uri_rdfs_member uri_rdfs_Resource) true true true) % 1.00/1.17 true = true % 1.00/1.17 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdfs_range) true % 1.00/1.17 (ifeq (iext $_438 uri_rdfs_range uri_rdfs_Class) true true true) % 1.00/1.17 true = true % 1.00/1.17 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdfs_range) true % 1.00/1.17 (ifeq (iext $_438 uri_rdfs_seeAlso uri_rdfs_Resource) true true true) % 1.00/1.17 true = true % 1.00/1.17 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdfs_range) true % 1.00/1.17 (ifeq (iext $_438 uri_rdfs_subClassOf uri_rdfs_Class) true true true) % 1.00/1.17 true = true % 1.00/1.17 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdfs_range) true % 1.00/1.17 (ifeq (iext $_438 uri_rdfs_subPropertyOf uri_rdf_Property) true true % 1.00/1.17 true) true = true % 1.00/1.17 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdfs_subClassOf) true % 1.00/1.17 (ifeq % 1.00/1.17 (iext $_438 % 1.00/1.17 sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z % 1.00/1.17 sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z) % 1.00/1.17 true true true) true = true % 1.00/1.17 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdfs_subClassOf) true % 1.00/1.17 (ifeq % 1.00/1.17 (iext $_438 % 1.00/1.17 sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z % 1.00/1.17 uri_rdfs_Resource) true true true) true = true % 1.00/1.17 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdfs_subClassOf) true % 1.00/1.17 (ifeq (iext $_438 uri_owl_Class uri_owl_Class) true true true) true = % 1.00/1.17 true % 1.00/1.17 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdfs_subClassOf) true % 1.00/1.17 (ifeq (iext $_438 uri_owl_Class uri_rdfs_Resource) true true true) % 1.00/1.17 true = true % 1.00/1.17 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdfs_subClassOf) true % 1.00/1.17 (ifeq (iext $_438 uri_owl_ObjectProperty uri_owl_ObjectProperty) true % 1.00/1.17 true true) true = true % 1.00/1.17 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdfs_subClassOf) true % 1.00/1.17 (ifeq (iext $_438 uri_owl_ObjectProperty uri_rdfs_Resource) true true % 1.00/1.17 true) true = true % 1.00/1.17 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdfs_subClassOf) true % 1.00/1.17 (ifeq (iext $_438 uri_owl_Restriction uri_owl_Restriction) true true % 1.00/1.17 true) true = true % 1.00/1.17 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdfs_subClassOf) true % 1.00/1.17 (ifeq (iext $_438 uri_owl_Restriction uri_rdfs_Resource) true true % 1.00/1.17 true) true = true % 1.00/1.17 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdfs_subClassOf) true % 1.00/1.17 (ifeq (iext $_438 uri_rdf_Alt uri_rdf_Alt) true true true) true = true % 1.00/1.17 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdfs_subClassOf) true % 1.00/1.17 (ifeq (iext $_438 uri_rdf_Alt uri_rdfs_Container) true true true) % 1.00/1.17 true = true % 1.00/1.17 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdfs_subClassOf) true % 1.00/1.17 (ifeq (iext $_438 uri_rdf_Alt uri_rdfs_Resource) true true true) % 1.00/1.17 true = true % 1.00/1.17 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdfs_subClassOf) true % 1.00/1.17 (ifeq (iext $_438 uri_rdf_Bag uri_rdf_Bag) true true true) true = true % 1.00/1.17 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdfs_subClassOf) true % 1.00/1.17 (ifeq (iext $_438 uri_rdf_Bag uri_rdfs_Container) true true true) % 1.00/1.17 true = true % 1.00/1.17 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdfs_subClassOf) true % 1.00/1.17 (ifeq (iext $_438 uri_rdf_Bag uri_rdfs_Resource) true true true) % 1.00/1.17 true = true % 1.00/1.17 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdfs_subClassOf) true % 1.00/1.17 (ifeq (iext $_438 uri_rdf_List uri_rdf_List) true true true) true = % 1.00/1.17 true % 1.00/1.17 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdfs_subClassOf) true % 1.00/1.17 (ifeq (iext $_438 uri_rdf_List uri_rdfs_Resource) true true true) % 1.00/1.17 true = true % 1.00/1.17 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdfs_subClassOf) true % 1.00/1.17 (ifeq (iext $_438 uri_rdf_Property uri_rdf_Property) true true true) % 1.00/1.17 true = true % 1.00/1.17 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdfs_subClassOf) true % 1.00/1.17 (ifeq (iext $_438 uri_rdf_Property uri_rdfs_Resource) true true true) % 1.00/1.17 true = true % 1.00/1.17 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdfs_subClassOf) true % 1.00/1.17 (ifeq (iext $_438 uri_rdf_XMLLiteral uri_rdf_XMLLiteral) true true % 1.00/1.17 true) true = true % 1.00/1.17 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdfs_subClassOf) true % 1.00/1.17 (ifeq (iext $_438 uri_rdf_XMLLiteral uri_rdfs_Literal) true true true) % 1.00/1.17 true = true % 1.00/1.17 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdfs_subClassOf) true % 1.00/1.17 (ifeq (iext $_438 uri_rdf_XMLLiteral uri_rdfs_Resource) true true % 1.00/1.17 true) true = true % 1.00/1.17 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdfs_subClassOf) true % 1.00/1.17 (ifeq (iext $_438 uri_rdfs_Class uri_rdfs_Class) true true true) % 1.00/1.17 true = true % 1.00/1.17 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdfs_subClassOf) true % 1.00/1.17 (ifeq (iext $_438 uri_rdfs_Class uri_rdfs_Resource) true true true) % 1.00/1.17 true = true % 1.00/1.17 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdfs_subClassOf) true % 1.00/1.17 (ifeq (iext $_438 uri_rdfs_Container uri_rdfs_Container) true true % 1.00/1.17 true) true = true % 1.00/1.17 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdfs_subClassOf) true % 1.00/1.17 (ifeq (iext $_438 uri_rdfs_Container uri_rdfs_Resource) true true % 1.00/1.17 true) true = true % 1.00/1.17 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdfs_subClassOf) true % 1.00/1.17 (ifeq % 1.00/1.17 (iext $_438 uri_rdfs_ContainerMembershipProperty uri_rdf_Property) % 1.00/1.17 true true true) true = true % 1.00/1.17 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdfs_subClassOf) true % 1.00/1.17 (ifeq % 1.00/1.17 (iext $_438 uri_rdfs_ContainerMembershipProperty % 1.00/1.17 uri_rdfs_ContainerMembershipProperty) true true true) true = % 1.00/1.17 true % 1.00/1.17 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdfs_subClassOf) true % 1.00/1.17 (ifeq % 1.00/1.17 (iext $_438 uri_rdfs_ContainerMembershipProperty uri_rdfs_Resource) % 1.00/1.17 true true true) true = true % 1.00/1.17 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdfs_subClassOf) true % 1.00/1.17 (ifeq (iext $_438 uri_rdfs_Datatype uri_rdfs_Class) true true true) % 1.00/1.17 true = true % 1.00/1.17 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdfs_subClassOf) true % 1.00/1.17 (ifeq (iext $_438 uri_rdfs_Datatype uri_rdfs_Datatype) true true true) % 1.00/1.17 true = true % 1.00/1.17 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdfs_subClassOf) true % 1.00/1.17 (ifeq (iext $_438 uri_rdfs_Datatype uri_rdfs_Resource) true true true) % 1.00/1.17 true = true % 1.00/1.17 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdfs_subClassOf) true % 1.00/1.17 (ifeq (iext $_438 uri_rdfs_Literal uri_rdfs_Literal) true true true) % 1.00/1.17 true = true % 1.00/1.17 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdfs_subClassOf) true % 1.00/1.17 (ifeq (iext $_438 uri_rdfs_Literal uri_rdfs_Resource) true true true) % 1.00/1.17 true = true % 1.00/1.17 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdfs_subClassOf) true % 1.00/1.17 (ifeq (iext $_438 uri_rdfs_Resource uri_rdfs_Resource) true true true) % 1.00/1.17 true = true % 1.00/1.17 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdfs_subClassOf) true % 1.00/1.17 (ifeq (iext $_438 uri_rdfs_Seq uri_rdfs_Container) true true true) % 1.00/1.17 true = true % 1.00/1.17 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdfs_subClassOf) true % 1.00/1.17 (ifeq (iext $_438 uri_rdfs_Seq uri_rdfs_Resource) true true true) % 1.00/1.17 true = true % 1.00/1.17 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdfs_subClassOf) true % 1.00/1.17 (ifeq (iext $_438 uri_rdfs_Seq uri_rdfs_Seq) true true true) true = % 1.00/1.17 true % 1.00/1.17 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdfs_subClassOf) true % 1.00/1.17 (ifeq (iext $_438 uri_rdfs_Statement uri_rdfs_Resource) true true % 1.00/1.17 true) true = true % 1.00/1.17 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdfs_subClassOf) true % 1.00/1.17 (ifeq (iext $_438 uri_rdfs_Statement uri_rdfs_Statement) true true % 1.00/1.17 true) true = true % 1.00/1.17 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdfs_subPropertyOf) true % 1.00/1.17 (ifeq (iext $_438 uri_owl_onProperty uri_owl_onProperty) true true % 1.00/1.17 true) true = true % 1.00/1.17 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdfs_subPropertyOf) true % 1.00/1.17 (ifeq (iext $_438 uri_owl_someValuesFrom uri_owl_someValuesFrom) true % 1.00/1.17 true true) true = true % 1.00/1.17 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdfs_subPropertyOf) true % 1.00/1.17 (ifeq (iext $_438 uri_rdf__1 uri_rdf__1) true true true) true = true % 1.00/1.17 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdfs_subPropertyOf) true % 1.00/1.17 (ifeq (iext $_438 uri_rdf__1 uri_rdfs_member) true true true) true = % 1.00/1.17 true % 1.00/1.17 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdfs_subPropertyOf) true % 1.00/1.17 (ifeq (iext $_438 uri_rdf__2 uri_rdf__2) true true true) true = true % 1.00/1.17 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdfs_subPropertyOf) true % 1.00/1.17 (ifeq (iext $_438 uri_rdf__2 uri_rdfs_member) true true true) true = % 1.00/1.17 true % 1.00/1.17 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdfs_subPropertyOf) true % 1.00/1.17 (ifeq (iext $_438 uri_rdf__3 uri_rdf__3) true true true) true = true % 1.00/1.17 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdfs_subPropertyOf) true % 1.00/1.17 (ifeq (iext $_438 uri_rdf__3 uri_rdfs_member) true true true) true = % 1.00/1.17 true % 1.00/1.17 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdfs_subPropertyOf) true % 1.00/1.17 (ifeq (iext $_438 uri_rdf_first uri_rdf_first) true true true) true = % 1.00/1.17 true % 1.00/1.17 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdfs_subPropertyOf) true % 1.00/1.17 (ifeq (iext $_438 uri_rdf_object uri_rdf_object) true true true) % 1.00/1.17 true = true % 1.00/1.17 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdfs_subPropertyOf) true % 1.00/1.17 (ifeq (iext $_438 uri_rdf_predicate uri_rdf_predicate) true true true) % 1.00/1.17 true = true % 1.00/1.17 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdfs_subPropertyOf) true % 1.00/1.17 (ifeq (iext $_438 uri_rdf_rest uri_rdf_rest) true true true) true = % 1.00/1.17 true % 1.00/1.17 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdfs_subPropertyOf) true % 1.00/1.17 (ifeq (iext $_438 uri_rdf_subject uri_rdf_subject) true true true) % 1.00/1.17 true = true % 1.00/1.17 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdfs_subPropertyOf) true % 1.00/1.17 (ifeq (iext $_438 uri_rdf_type uri_rdf_type) true true true) true = % 1.00/1.17 true % 1.00/1.17 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdfs_subPropertyOf) true % 1.00/1.17 (ifeq (iext $_438 uri_rdf_value uri_rdf_value) true true true) true = % 1.00/1.17 true % 1.00/1.17 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdfs_subPropertyOf) true % 1.00/1.17 (ifeq (iext $_438 uri_rdfs_comment uri_rdfs_comment) true true true) % 1.00/1.17 true = true % 1.00/1.17 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdfs_subPropertyOf) true % 1.00/1.17 (ifeq (iext $_438 uri_rdfs_domain uri_rdfs_domain) true true true) % 1.00/1.17 true = true % 1.00/1.17 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdfs_subPropertyOf) true % 1.00/1.17 (ifeq (iext $_438 uri_rdfs_isDefinedBy uri_rdfs_isDefinedBy) true true % 1.00/1.17 true) true = true % 1.00/1.17 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdfs_subPropertyOf) true % 1.00/1.17 (ifeq (iext $_438 uri_rdfs_isDefinedBy uri_rdfs_seeAlso) true true % 1.00/1.17 true) true = true % 1.00/1.17 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdfs_subPropertyOf) true % 1.00/1.17 (ifeq (iext $_438 uri_rdfs_label uri_rdfs_label) true true true) % 1.00/1.17 true = true % 1.00/1.17 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdfs_subPropertyOf) true % 1.00/1.17 (ifeq (iext $_438 uri_rdfs_member uri_rdfs_member) true true true) % 1.00/1.17 true = true % 1.00/1.17 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdfs_subPropertyOf) true % 1.00/1.17 (ifeq (iext $_438 uri_rdfs_range uri_rdfs_range) true true true) % 1.00/1.17 true = true % 1.00/1.17 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdfs_subPropertyOf) true % 1.00/1.17 (ifeq (iext $_438 uri_rdfs_seeAlso uri_rdfs_seeAlso) true true true) % 1.00/1.17 true = true % 1.00/1.17 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdfs_subPropertyOf) true % 1.00/1.17 (ifeq (iext $_438 uri_rdfs_subClassOf uri_rdfs_subClassOf) true true % 1.00/1.17 true) true = true % 1.00/1.17 |- ifeq (iext uri_rdfs_subPropertyOf $_438 uri_rdfs_subPropertyOf) true % 1.00/1.17 (ifeq (iext $_438 uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf) true % 1.00/1.17 true true) true = true % 1.00/1.17 |- ifeq (iext uri_rdfs_subPropertyOf uri_owl_onProperty $_439) true % 1.00/1.17 (iext $_439 % 1.00/1.17 sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z % 1.00/1.17 uri_ex_p) true = true % 1.00/1.17 |- ifeq (iext uri_rdfs_subPropertyOf uri_owl_someValuesFrom $_439) true % 1.00/1.17 (iext $_439 % 1.00/1.17 sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z % 1.00/1.17 uri_ex_c) true = true % 1.00/1.17 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_439) true % 1.00/1.17 (iext $_439 % 1.00/1.17 sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z % 1.00/1.17 uri_owl_Restriction) true = true % 1.00/1.17 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_439) true % 1.00/1.17 (iext $_439 % 1.00/1.17 sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z % 1.00/1.17 uri_rdfs_Class) true = true % 1.00/1.17 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_439) true % 1.00/1.17 (iext $_439 uri_ex_c uri_owl_Class) true = true % 1.00/1.17 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_439) true % 1.00/1.17 (iext $_439 uri_ex_p uri_owl_ObjectProperty) true = true % 1.00/1.17 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_439) true % 1.00/1.17 (iext $_439 uri_ex_s % 1.00/1.17 sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z) % 1.00/1.17 true = true % 1.00/1.17 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_439) true % 1.00/1.17 (iext $_439 uri_owl_Class uri_rdfs_Class) true = true % 1.00/1.17 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_439) true % 1.00/1.17 (iext $_439 uri_owl_ObjectProperty uri_rdfs_Class) true = true % 1.00/1.17 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_439) true % 1.00/1.17 (iext $_439 uri_owl_Restriction uri_rdfs_Class) true = true % 1.00/1.17 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_439) true % 1.00/1.17 (iext $_439 uri_owl_onProperty uri_rdf_Property) true = true % 1.00/1.17 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_439) true % 1.00/1.17 (iext $_439 uri_owl_someValuesFrom uri_rdf_Property) true = true % 1.00/1.17 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_439) true % 1.00/1.17 (iext $_439 uri_rdf_Alt uri_rdfs_Class) true = true % 1.00/1.17 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_439) true % 1.00/1.17 (iext $_439 uri_rdf_Bag uri_rdfs_Class) true = true % 1.00/1.17 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_439) true % 1.00/1.17 (iext $_439 uri_rdf_List uri_rdfs_Class) true = true % 1.00/1.17 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_439) true % 1.00/1.17 (iext $_439 uri_rdf_Property uri_rdfs_Class) true = true % 1.00/1.17 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_439) true % 1.00/1.17 (iext $_439 uri_rdf_XMLLiteral uri_rdfs_Class) true = true % 1.00/1.17 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_439) true % 1.00/1.17 (iext $_439 uri_rdf_XMLLiteral uri_rdfs_Datatype) true = true % 1.00/1.17 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_439) true % 1.00/1.17 (iext $_439 uri_rdf__1 uri_rdf_Property) true = true % 1.00/1.17 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_439) true % 1.00/1.17 (iext $_439 uri_rdf__1 uri_rdfs_ContainerMembershipProperty) true = % 1.00/1.17 true % 1.00/1.17 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_439) true % 1.00/1.17 (iext $_439 uri_rdf__2 uri_rdf_Property) true = true % 1.00/1.17 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_439) true % 1.00/1.17 (iext $_439 uri_rdf__2 uri_rdfs_ContainerMembershipProperty) true = % 1.00/1.17 true % 1.00/1.17 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_439) true % 1.00/1.17 (iext $_439 uri_rdf__3 uri_rdf_Property) true = true % 1.00/1.17 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_439) true % 1.00/1.17 (iext $_439 uri_rdf__3 uri_rdfs_ContainerMembershipProperty) true = % 1.00/1.17 true % 1.00/1.17 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_439) true % 1.00/1.17 (iext $_439 uri_rdf_first uri_rdf_Property) true = true % 1.00/1.17 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_439) true % 1.00/1.17 (iext $_439 uri_rdf_nil uri_rdf_List) true = true % 1.00/1.17 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_439) true % 1.00/1.17 (iext $_439 uri_rdf_object uri_rdf_Property) true = true % 1.00/1.17 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_439) true % 1.00/1.17 (iext $_439 uri_rdf_predicate uri_rdf_Property) true = true % 1.00/1.17 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_439) true % 1.00/1.17 (iext $_439 uri_rdf_rest uri_rdf_Property) true = true % 1.00/1.17 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_439) true % 1.00/1.17 (iext $_439 uri_rdf_subject uri_rdf_Property) true = true % 1.00/1.17 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_439) true % 1.00/1.17 (iext $_439 uri_rdf_type uri_rdf_Property) true = true % 1.00/1.17 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_439) true % 1.00/1.17 (iext $_439 uri_rdf_value uri_rdf_Property) true = true % 1.00/1.17 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_439) true % 1.00/1.17 (iext $_439 uri_rdfs_Class uri_rdfs_Class) true = true % 1.00/1.17 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_439) true % 1.00/1.17 (iext $_439 uri_rdfs_Container uri_rdfs_Class) true = true % 1.00/1.17 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_439) true % 1.00/1.17 (iext $_439 uri_rdfs_ContainerMembershipProperty uri_rdfs_Class) % 1.00/1.17 true = true % 1.00/1.18 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_439) true % 1.00/1.18 (iext $_439 uri_rdfs_Datatype uri_rdfs_Class) true = true % 1.00/1.18 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_439) true % 1.00/1.18 (iext $_439 uri_rdfs_Literal uri_rdfs_Class) true = true % 1.00/1.18 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_439) true % 1.00/1.18 (iext $_439 uri_rdfs_Resource uri_rdfs_Class) true = true % 1.00/1.18 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_439) true % 1.00/1.18 (iext $_439 uri_rdfs_Seq uri_rdfs_Class) true = true % 1.00/1.18 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_439) true % 1.00/1.18 (iext $_439 uri_rdfs_Statement uri_rdfs_Class) true = true % 1.00/1.18 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_439) true % 1.00/1.18 (iext $_439 uri_rdfs_comment uri_rdf_Property) true = true % 1.00/1.18 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_439) true % 1.00/1.18 (iext $_439 uri_rdfs_domain uri_rdf_Property) true = true % 1.00/1.18 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_439) true % 1.00/1.18 (iext $_439 uri_rdfs_isDefinedBy uri_rdf_Property) true = true % 1.00/1.18 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_439) true % 1.00/1.18 (iext $_439 uri_rdfs_label uri_rdf_Property) true = true % 1.00/1.18 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_439) true % 1.00/1.18 (iext $_439 uri_rdfs_member uri_rdf_Property) true = true % 1.00/1.18 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_439) true % 1.00/1.18 (iext $_439 uri_rdfs_range uri_rdf_Property) true = true % 1.00/1.18 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_439) true % 1.00/1.18 (iext $_439 uri_rdfs_seeAlso uri_rdf_Property) true = true % 1.00/1.18 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_439) true % 1.00/1.18 (iext $_439 uri_rdfs_subClassOf uri_rdf_Property) true = true % 1.00/1.18 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_439) true % 1.00/1.18 (iext $_439 uri_rdfs_subPropertyOf uri_rdf_Property) true = true % 1.00/1.18 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_439) true % 1.00/1.18 (iext $_439 $_440 uri_rdfs_Resource) true = true % 1.00/1.18 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_domain $_439) true % 1.00/1.18 (iext $_439 uri_rdf__1 uri_rdfs_Resource) true = true % 1.00/1.18 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_domain $_439) true % 1.00/1.18 (iext $_439 uri_rdf__2 uri_rdfs_Resource) true = true % 1.00/1.18 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_domain $_439) true % 1.00/1.18 (iext $_439 uri_rdf__3 uri_rdfs_Resource) true = true % 1.00/1.18 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_domain $_439) true % 1.00/1.18 (iext $_439 uri_rdf_first uri_rdf_List) true = true % 1.00/1.18 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_domain $_439) true % 1.00/1.18 (iext $_439 uri_rdf_object uri_rdfs_Statement) true = true % 1.00/1.18 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_domain $_439) true % 1.00/1.18 (iext $_439 uri_rdf_predicate uri_rdfs_Statement) true = true % 1.00/1.18 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_domain $_439) true % 1.00/1.18 (iext $_439 uri_rdf_rest uri_rdf_List) true = true % 1.00/1.18 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_domain $_439) true % 1.00/1.18 (iext $_439 uri_rdf_subject uri_rdfs_Statement) true = true % 1.00/1.18 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_domain $_439) true % 1.00/1.18 (iext $_439 uri_rdf_type uri_rdfs_Resource) true = true % 1.00/1.18 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_domain $_439) true % 1.00/1.18 (iext $_439 uri_rdf_value uri_rdfs_Resource) true = true % 1.00/1.18 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_domain $_439) true % 1.00/1.18 (iext $_439 uri_rdfs_comment uri_rdfs_Resource) true = true % 1.00/1.18 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_domain $_439) true % 1.00/1.18 (iext $_439 uri_rdfs_domain uri_rdf_Property) true = true % 1.00/1.18 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_domain $_439) true % 1.00/1.18 (iext $_439 uri_rdfs_isDefinedBy uri_rdfs_Resource) true = true % 1.00/1.18 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_domain $_439) true % 1.00/1.18 (iext $_439 uri_rdfs_label uri_rdfs_Resource) true = true % 1.00/1.18 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_domain $_439) true % 1.00/1.18 (iext $_439 uri_rdfs_member uri_rdfs_Resource) true = true % 1.00/1.18 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_domain $_439) true % 1.00/1.18 (iext $_439 uri_rdfs_range uri_rdf_Property) true = true % 1.00/1.18 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_domain $_439) true % 1.00/1.18 (iext $_439 uri_rdfs_seeAlso uri_rdfs_Resource) true = true % 1.00/1.18 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_domain $_439) true % 1.00/1.18 (iext $_439 uri_rdfs_subClassOf uri_rdfs_Class) true = true % 1.00/1.18 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_domain $_439) true % 1.00/1.18 (iext $_439 uri_rdfs_subPropertyOf uri_rdf_Property) true = true % 1.00/1.18 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_range $_439) true % 1.00/1.18 (iext $_439 uri_rdf__1 uri_rdfs_Resource) true = true % 1.00/1.18 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_range $_439) true % 1.00/1.18 (iext $_439 uri_rdf__2 uri_rdfs_Resource) true = true % 1.00/1.18 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_range $_439) true % 1.00/1.18 (iext $_439 uri_rdf__3 uri_rdfs_Resource) true = true % 1.00/1.18 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_range $_439) true % 1.00/1.18 (iext $_439 uri_rdf_first uri_rdfs_Resource) true = true % 1.00/1.18 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_range $_439) true % 1.00/1.18 (iext $_439 uri_rdf_predicate uri_rdfs_Resource) true = true % 1.00/1.18 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_range $_439) true % 1.00/1.18 (iext $_439 uri_rdf_rest uri_rdf_List) true = true % 1.00/1.18 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_range $_439) true % 1.00/1.18 (iext $_439 uri_rdf_subject uri_rdfs_Resource) true = true % 1.00/1.18 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_range $_439) true % 1.00/1.18 (iext $_439 uri_rdf_type uri_rdfs_Class) true = true % 1.00/1.18 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_range $_439) true % 1.00/1.18 (iext $_439 uri_rdf_value uri_rdfs_Resource) true = true % 1.00/1.18 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_range $_439) true % 1.00/1.18 (iext $_439 uri_rdfs_comment uri_rdfs_Literal) true = true % 1.00/1.18 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_range $_439) true % 1.00/1.18 (iext $_439 uri_rdfs_domain uri_rdfs_Class) true = true % 1.00/1.18 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_range $_439) true % 1.00/1.18 (iext $_439 uri_rdfs_isDefinedBy uri_rdfs_Resource) true = true % 1.00/1.18 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_range $_439) true % 1.00/1.18 (iext $_439 uri_rdfs_label uri_rdfs_Literal) true = true % 1.00/1.18 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_range $_439) true % 1.00/1.18 (iext $_439 uri_rdfs_member uri_rdfs_Resource) true = true % 1.00/1.18 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_range $_439) true % 1.00/1.18 (iext $_439 uri_rdfs_range uri_rdfs_Class) true = true % 1.00/1.18 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_range $_439) true % 1.00/1.18 (iext $_439 uri_rdfs_seeAlso uri_rdfs_Resource) true = true % 1.00/1.18 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_range $_439) true % 1.00/1.18 (iext $_439 uri_rdfs_subClassOf uri_rdfs_Class) true = true % 1.00/1.18 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_range $_439) true % 1.00/1.18 (iext $_439 uri_rdfs_subPropertyOf uri_rdf_Property) true = true % 1.00/1.18 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_439) true % 1.00/1.18 (iext $_439 % 1.00/1.18 sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z % 1.00/1.18 sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z) % 1.00/1.18 true = true % 1.00/1.18 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_439) true % 1.00/1.18 (iext $_439 % 1.00/1.18 sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z % 1.00/1.18 uri_rdfs_Resource) true = true % 1.00/1.18 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_439) true % 1.00/1.18 (iext $_439 uri_owl_Class uri_owl_Class) true = true % 1.00/1.18 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_439) true % 1.00/1.18 (iext $_439 uri_owl_Class uri_rdfs_Resource) true = true % 1.00/1.18 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_439) true % 1.00/1.18 (iext $_439 uri_owl_ObjectProperty uri_owl_ObjectProperty) true = true % 1.00/1.18 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_439) true % 1.00/1.18 (iext $_439 uri_owl_ObjectProperty uri_rdfs_Resource) true = true % 1.00/1.18 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_439) true % 1.00/1.18 (iext $_439 uri_owl_Restriction uri_owl_Restriction) true = true % 1.00/1.18 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_439) true % 1.00/1.18 (iext $_439 uri_owl_Restriction uri_rdfs_Resource) true = true % 1.00/1.18 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_439) true % 1.00/1.18 (iext $_439 uri_rdf_Alt uri_rdf_Alt) true = true % 1.00/1.18 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_439) true % 1.00/1.18 (iext $_439 uri_rdf_Alt uri_rdfs_Container) true = true % 1.00/1.18 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_439) true % 1.00/1.18 (iext $_439 uri_rdf_Alt uri_rdfs_Resource) true = true % 1.00/1.18 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_439) true % 1.00/1.18 (iext $_439 uri_rdf_Bag uri_rdf_Bag) true = true % 1.00/1.18 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_439) true % 1.00/1.18 (iext $_439 uri_rdf_Bag uri_rdfs_Container) true = true % 1.00/1.18 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_439) true % 1.00/1.18 (iext $_439 uri_rdf_Bag uri_rdfs_Resource) true = true % 1.00/1.18 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_439) true % 1.00/1.18 (iext $_439 uri_rdf_List uri_rdf_List) true = true % 1.00/1.18 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_439) true % 1.00/1.18 (iext $_439 uri_rdf_List uri_rdfs_Resource) true = true % 1.00/1.18 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_439) true % 1.00/1.18 (iext $_439 uri_rdf_Property uri_rdf_Property) true = true % 1.00/1.18 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_439) true % 1.00/1.18 (iext $_439 uri_rdf_Property uri_rdfs_Resource) true = true % 1.00/1.18 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_439) true % 1.00/1.18 (iext $_439 uri_rdf_XMLLiteral uri_rdf_XMLLiteral) true = true % 1.00/1.18 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_439) true % 1.00/1.18 (iext $_439 uri_rdf_XMLLiteral uri_rdfs_Literal) true = true % 1.00/1.18 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_439) true % 1.00/1.18 (iext $_439 uri_rdf_XMLLiteral uri_rdfs_Resource) true = true % 1.00/1.18 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_439) true % 1.00/1.18 (iext $_439 uri_rdfs_Class uri_rdfs_Class) true = true % 1.00/1.18 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_439) true % 1.00/1.18 (iext $_439 uri_rdfs_Class uri_rdfs_Resource) true = true % 1.00/1.18 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_439) true % 1.00/1.18 (iext $_439 uri_rdfs_Container uri_rdfs_Container) true = true % 1.00/1.18 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_439) true % 1.00/1.18 (iext $_439 uri_rdfs_Container uri_rdfs_Resource) true = true % 1.00/1.18 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_439) true % 1.00/1.18 (iext $_439 uri_rdfs_ContainerMembershipProperty uri_rdf_Property) % 1.00/1.18 true = true % 1.00/1.18 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_439) true % 1.00/1.18 (iext $_439 uri_rdfs_ContainerMembershipProperty % 1.00/1.18 uri_rdfs_ContainerMembershipProperty) true = true % 1.00/1.18 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_439) true % 1.00/1.18 (iext $_439 uri_rdfs_ContainerMembershipProperty uri_rdfs_Resource) % 1.00/1.18 true = true % 1.00/1.18 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_439) true % 1.00/1.18 (iext $_439 uri_rdfs_Datatype uri_rdfs_Class) true = true % 1.00/1.18 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_439) true % 1.00/1.18 (iext $_439 uri_rdfs_Datatype uri_rdfs_Datatype) true = true % 1.00/1.18 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_439) true % 1.00/1.18 (iext $_439 uri_rdfs_Datatype uri_rdfs_Resource) true = true % 1.00/1.18 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_439) true % 1.00/1.18 (iext $_439 uri_rdfs_Literal uri_rdfs_Literal) true = true % 1.00/1.18 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_439) true % 1.00/1.18 (iext $_439 uri_rdfs_Literal uri_rdfs_Resource) true = true % 1.00/1.18 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_439) true % 1.00/1.18 (iext $_439 uri_rdfs_Resource uri_rdfs_Resource) true = true % 1.00/1.18 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_439) true % 1.00/1.18 (iext $_439 uri_rdfs_Seq uri_rdfs_Container) true = true % 1.00/1.18 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_439) true % 1.00/1.18 (iext $_439 uri_rdfs_Seq uri_rdfs_Resource) true = true % 1.00/1.18 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_439) true % 1.00/1.18 (iext $_439 uri_rdfs_Seq uri_rdfs_Seq) true = true % 1.00/1.18 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_439) true % 1.00/1.18 (iext $_439 uri_rdfs_Statement uri_rdfs_Resource) true = true % 1.00/1.18 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_439) true % 1.00/1.18 (iext $_439 uri_rdfs_Statement uri_rdfs_Statement) true = true % 1.00/1.18 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_439) true % 1.00/1.18 (iext $_439 uri_owl_onProperty uri_owl_onProperty) true = true % 1.00/1.18 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_439) true % 1.00/1.18 (iext $_439 uri_owl_someValuesFrom uri_owl_someValuesFrom) true = true % 1.00/1.18 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_439) true % 1.00/1.18 (iext $_439 uri_rdf__1 uri_rdf__1) true = true % 1.00/1.18 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_439) true % 1.00/1.18 (iext $_439 uri_rdf__1 uri_rdfs_member) true = true % 1.00/1.18 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_439) true % 1.00/1.18 (iext $_439 uri_rdf__2 uri_rdf__2) true = true % 1.00/1.18 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_439) true % 1.00/1.18 (iext $_439 uri_rdf__2 uri_rdfs_member) true = true % 1.00/1.18 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_439) true % 1.00/1.18 (iext $_439 uri_rdf__3 uri_rdf__3) true = true % 1.00/1.18 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_439) true % 1.00/1.18 (iext $_439 uri_rdf__3 uri_rdfs_member) true = true % 1.00/1.18 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_439) true % 1.00/1.18 (iext $_439 uri_rdf_first uri_rdf_first) true = true % 1.00/1.18 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_439) true % 1.00/1.18 (iext $_439 uri_rdf_object uri_rdf_object) true = true % 1.00/1.18 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_439) true % 1.00/1.18 (iext $_439 uri_rdf_predicate uri_rdf_predicate) true = true % 1.00/1.18 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_439) true % 1.00/1.18 (iext $_439 uri_rdf_rest uri_rdf_rest) true = true % 1.00/1.18 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_439) true % 1.00/1.18 (iext $_439 uri_rdf_subject uri_rdf_subject) true = true % 1.00/1.18 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_439) true % 1.00/1.18 (iext $_439 uri_rdf_type uri_rdf_type) true = true % 1.00/1.18 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_439) true % 1.00/1.18 (iext $_439 uri_rdf_value uri_rdf_value) true = true % 1.00/1.18 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_439) true % 1.00/1.18 (iext $_439 uri_rdfs_comment uri_rdfs_comment) true = true % 1.00/1.18 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_439) true % 1.00/1.18 (iext $_439 uri_rdfs_domain uri_rdfs_domain) true = true % 1.00/1.18 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_439) true % 1.00/1.18 (iext $_439 uri_rdfs_isDefinedBy uri_rdfs_isDefinedBy) true = true % 1.00/1.18 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_439) true % 1.00/1.18 (iext $_439 uri_rdfs_isDefinedBy uri_rdfs_seeAlso) true = true % 1.00/1.18 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_439) true % 1.00/1.18 (iext $_439 uri_rdfs_label uri_rdfs_label) true = true % 1.00/1.18 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_439) true % 1.00/1.18 (iext $_439 uri_rdfs_member uri_rdfs_member) true = true % 1.00/1.18 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_439) true % 1.00/1.18 (iext $_439 uri_rdfs_range uri_rdfs_range) true = true % 1.00/1.18 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_439) true % 1.00/1.18 (iext $_439 uri_rdfs_seeAlso uri_rdfs_seeAlso) true = true % 1.00/1.18 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_439) true % 1.00/1.18 (iext $_439 uri_rdfs_subClassOf uri_rdfs_subClassOf) true = true % 1.00/1.18 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_439) true % 1.00/1.18 (iext $_439 uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf) true = true % 1.00/1.18 |- ifeq (iext uri_owl_onProperty $_440 $_441) true % 1.00/1.18 (iext uri_owl_onProperty $_440 $_441) true = true % 1.00/1.18 |- ifeq (iext uri_owl_someValuesFrom $_440 $_441) true % 1.00/1.18 (iext uri_owl_someValuesFrom $_440 $_441) true = true % 1.00/1.18 |- ifeq (iext uri_rdf__1 $_440 $_441) true (iext uri_rdf__1 $_440 $_441) % 1.00/1.18 true = true % 1.00/1.18 |- ifeq (iext uri_rdf__1 $_440 $_441) true % 1.00/1.18 (iext uri_rdfs_member $_440 $_441) true = true % 1.00/1.18 |- ifeq (iext uri_rdf__2 $_440 $_441) true (iext uri_rdf__2 $_440 $_441) % 1.00/1.18 true = true % 1.00/1.18 |- ifeq (iext uri_rdf__2 $_440 $_441) true % 1.00/1.18 (iext uri_rdfs_member $_440 $_441) true = true % 1.00/1.18 |- ifeq (iext uri_rdf__3 $_440 $_441) true (iext uri_rdf__3 $_440 $_441) % 1.00/1.18 true = true % 1.00/1.18 |- ifeq (iext uri_rdf__3 $_440 $_441) true % 1.00/1.18 (iext uri_rdfs_member $_440 $_441) true = true % 1.00/1.18 |- ifeq (iext uri_rdf_first $_440 $_441) true % 1.00/1.18 (iext uri_rdf_first $_440 $_441) true = true % 1.00/1.18 |- ifeq (iext uri_rdf_object $_440 $_441) true % 1.00/1.18 (iext uri_rdf_object $_440 $_441) true = true % 1.00/1.18 |- ifeq (iext uri_rdf_predicate $_440 $_441) true % 1.00/1.18 (iext uri_rdf_predicate $_440 $_441) true = true % 1.00/1.18 |- ifeq (iext uri_rdf_rest $_440 $_441) true % 1.00/1.18 (iext uri_rdf_rest $_440 $_441) true = true % 1.00/1.18 |- ifeq (iext uri_rdf_subject $_440 $_441) true % 1.00/1.18 (iext uri_rdf_subject $_440 $_441) true = true % 1.00/1.18 |- ifeq (iext uri_rdf_type $_440 $_441) true % 1.00/1.18 (iext uri_rdf_type $_440 $_441) true = true % 1.00/1.18 |- ifeq (iext uri_rdf_value $_440 $_441) true % 1.00/1.18 (iext uri_rdf_value $_440 $_441) true = true % 1.00/1.18 |- ifeq (iext uri_rdfs_comment $_440 $_441) true % 1.00/1.18 (iext uri_rdfs_comment $_440 $_441) true = true % 1.00/1.18 |- ifeq (iext uri_rdfs_domain $_440 $_441) true % 1.00/1.18 (iext uri_rdfs_domain $_440 $_441) true = true % 1.00/1.18 |- ifeq (iext uri_rdfs_isDefinedBy $_440 $_441) true % 1.00/1.18 (iext uri_rdfs_isDefinedBy $_440 $_441) true = true % 1.00/1.18 |- ifeq (iext uri_rdfs_isDefinedBy $_440 $_441) true % 1.00/1.18 (iext uri_rdfs_seeAlso $_440 $_441) true = true % 1.00/1.18 |- ifeq (iext uri_rdfs_label $_440 $_441) true % 1.00/1.18 (iext uri_rdfs_label $_440 $_441) true = true % 1.00/1.18 |- ifeq (iext uri_rdfs_member $_440 $_441) true % 1.00/1.18 (iext uri_rdfs_member $_440 $_441) true = true % 1.00/1.18 |- ifeq (iext uri_rdfs_range $_440 $_441) true % 1.00/1.18 (iext uri_rdfs_range $_440 $_441) true = true % 1.00/1.18 |- ifeq (iext uri_rdfs_seeAlso $_440 $_441) true % 1.00/1.18 (iext uri_rdfs_seeAlso $_440 $_441) true = true % 1.00/1.18 |- ifeq (iext uri_rdfs_subClassOf $_440 $_441) true % 1.00/1.18 (iext uri_rdfs_subClassOf $_440 $_441) true = true % 1.00/1.18 |- ifeq (iext uri_rdfs_subPropertyOf $_440 $_441) true % 1.00/1.18 (iext uri_rdfs_subPropertyOf $_440 $_441) true = true % 1.00/1.18 |- ifeq (icext $_978 $_980) true true true = true % 1.00/1.18 |- ifeq % 1.00/1.18 (icext % 1.00/1.18 sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z % 1.00/1.18 $_980) true % 1.00/1.18 (icext % 1.00/1.18 sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z % 1.00/1.18 $_980) true = true % 1.00/1.18 |- ifeq (icext uri_owl_Class $_980) true (icext uri_owl_Class $_980) true = % 1.00/1.18 true % 1.00/1.18 |- ifeq (icext uri_owl_ObjectProperty $_980) true % 1.00/1.18 (icext uri_owl_ObjectProperty $_980) true = true % 1.00/1.18 |- ifeq (icext uri_owl_Restriction $_980) true % 1.00/1.18 (icext uri_owl_Restriction $_980) true = true % 1.00/1.18 |- ifeq (icext uri_rdf_Alt $_980) true (icext uri_rdf_Alt $_980) true = % 1.00/1.18 true % 1.00/1.18 |- ifeq (icext uri_rdf_Alt $_980) true (icext uri_rdfs_Container $_980) % 1.00/1.18 true = true % 1.00/1.18 |- ifeq (icext uri_rdf_Bag $_980) true (icext uri_rdf_Bag $_980) true = % 1.00/1.18 true % 1.00/1.18 |- ifeq (icext uri_rdf_Bag $_980) true (icext uri_rdfs_Container $_980) % 1.00/1.18 true = true % 1.00/1.18 |- ifeq (icext uri_rdf_List $_980) true (icext uri_rdf_List $_980) true = % 1.00/1.18 true % 1.00/1.18 |- ifeq (icext uri_rdf_Property $_980) true (icext uri_rdf_Property $_980) % 1.00/1.18 true = true % 1.00/1.18 |- ifeq (icext uri_rdf_XMLLiteral $_980) true % 1.00/1.18 (icext uri_rdf_XMLLiteral $_980) true = true % 1.00/1.18 |- ifeq (icext uri_rdf_XMLLiteral $_980) true % 1.00/1.18 (icext uri_rdfs_Literal $_980) true = true % 1.00/1.18 |- ifeq (icext uri_rdfs_Class $_980) true (icext uri_rdfs_Class $_980) % 1.00/1.18 true = true % 1.00/1.18 |- ifeq (icext uri_rdfs_Container $_980) true % 1.00/1.18 (icext uri_rdfs_Container $_980) true = true % 1.00/1.18 |- ifeq (icext uri_rdfs_ContainerMembershipProperty $_980) true % 1.00/1.18 (icext uri_rdf_Property $_980) true = true % 1.00/1.18 |- ifeq (icext uri_rdfs_ContainerMembershipProperty $_980) true % 1.00/1.18 (icext uri_rdfs_ContainerMembershipProperty $_980) true = true % 1.00/1.18 |- ifeq (icext uri_rdfs_Datatype $_980) true (icext uri_rdfs_Class $_980) % 1.00/1.18 true = true % 1.00/1.18 |- ifeq (icext uri_rdfs_Datatype $_980) true % 1.00/1.18 (icext uri_rdfs_Datatype $_980) true = true % 1.00/1.18 |- ifeq (icext uri_rdfs_Literal $_980) true (icext uri_rdfs_Literal $_980) % 1.00/1.18 true = true % 1.00/1.18 |- ifeq (icext uri_rdfs_Seq $_980) true (icext uri_rdfs_Container $_980) % 1.00/1.18 true = true % 1.00/1.18 |- ifeq (icext uri_rdfs_Seq $_980) true (icext uri_rdfs_Seq $_980) true = % 1.00/1.18 true % 1.00/1.18 |- ifeq (icext uri_rdfs_Statement $_980) true % 1.00/1.18 (icext uri_rdfs_Statement $_980) true = true % 1.00/1.18 |- ifeq % 1.00/1.18 (iext uri_rdfs_subClassOf % 1.00/1.18 sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z % 1.00/1.18 $_979) true (icext $_979 uri_ex_s) true = true % 1.00/1.18 |- ifeq (iext uri_rdfs_subClassOf uri_owl_Class $_979) true % 1.00/1.18 (icext $_979 uri_ex_c) true = true % 1.00/1.18 |- ifeq (iext uri_rdfs_subClassOf uri_owl_ObjectProperty $_979) true % 1.00/1.18 (icext $_979 uri_ex_p) true = true % 1.00/1.19 |- ifeq (iext uri_rdfs_subClassOf uri_owl_Restriction $_979) true % 1.00/1.19 (icext $_979 % 1.00/1.19 sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z) % 1.00/1.19 true = true % 1.00/1.19 |- ifeq (iext uri_rdfs_subClassOf uri_rdf_List $_979) true % 1.00/1.19 (icext $_979 uri_rdf_nil) true = true % 1.00/1.19 |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $_979) true % 1.00/1.19 (icext $_979 uri_owl_onProperty) true = true % 1.00/1.19 |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $_979) true % 1.00/1.19 (icext $_979 uri_owl_someValuesFrom) true = true % 1.00/1.19 |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $_979) true % 1.00/1.19 (icext $_979 uri_rdf__1) true = true % 1.00/1.19 |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $_979) true % 1.00/1.19 (icext $_979 uri_rdf__2) true = true % 1.00/1.19 |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $_979) true % 1.00/1.19 (icext $_979 uri_rdf__3) true = true % 1.00/1.19 |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $_979) true % 1.00/1.19 (icext $_979 uri_rdf_first) true = true % 1.00/1.19 |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $_979) true % 1.00/1.19 (icext $_979 uri_rdf_object) true = true % 1.00/1.19 |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $_979) true % 1.00/1.19 (icext $_979 uri_rdf_predicate) true = true % 1.00/1.19 |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $_979) true % 1.00/1.19 (icext $_979 uri_rdf_rest) true = true % 1.00/1.19 |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $_979) true % 1.00/1.19 (icext $_979 uri_rdf_subject) true = true % 1.00/1.19 |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $_979) true % 1.00/1.19 (icext $_979 uri_rdf_type) true = true % 1.00/1.19 |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $_979) true % 1.00/1.19 (icext $_979 uri_rdf_value) true = true % 1.00/1.19 |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $_979) true % 1.00/1.19 (icext $_979 uri_rdfs_comment) true = true % 1.00/1.19 |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $_979) true % 1.00/1.19 (icext $_979 uri_rdfs_domain) true = true % 1.00/1.19 |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $_979) true % 1.00/1.19 (icext $_979 uri_rdfs_isDefinedBy) true = true % 1.00/1.19 |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $_979) true % 1.00/1.19 (icext $_979 uri_rdfs_label) true = true % 1.00/1.19 |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $_979) true % 1.00/1.19 (icext $_979 uri_rdfs_member) true = true % 1.00/1.19 |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $_979) true % 1.00/1.19 (icext $_979 uri_rdfs_range) true = true % 1.00/1.19 |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $_979) true % 1.00/1.19 (icext $_979 uri_rdfs_seeAlso) true = true % 1.00/1.19 |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $_979) true % 1.00/1.19 (icext $_979 uri_rdfs_subClassOf) true = true % 1.00/1.19 |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $_979) true % 1.00/1.19 (icext $_979 uri_rdfs_subPropertyOf) true = true % 1.00/1.19 |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Class $_979) true % 1.00/1.19 (icext $_979 % 1.00/1.19 sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z) % 1.00/1.19 true = true % 1.00/1.19 |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Class $_979) true % 1.00/1.19 (icext $_979 uri_owl_Class) true = true % 1.00/1.19 |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Class $_979) true % 1.00/1.19 (icext $_979 uri_owl_ObjectProperty) true = true % 1.00/1.19 |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Class $_979) true % 1.00/1.19 (icext $_979 uri_owl_Restriction) true = true % 1.00/1.19 |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Class $_979) true % 1.00/1.19 (icext $_979 uri_rdf_Alt) true = true % 1.02/1.19 |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Class $_979) true % 1.02/1.19 (icext $_979 uri_rdf_Bag) true = true % 1.02/1.19 |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Class $_979) true % 1.02/1.19 (icext $_979 uri_rdf_List) true = true % 1.02/1.19 |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Class $_979) true % 1.02/1.19 (icext $_979 uri_rdf_Property) true = true % 1.02/1.19 |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Class $_979) true % 1.02/1.19 (icext $_979 uri_rdf_XMLLiteral) true = true % 1.02/1.19 |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Class $_979) true % 1.02/1.19 (icext $_979 uri_rdfs_Class) true = true % 1.02/1.19 |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Class $_979) true % 1.02/1.19 (icext $_979 uri_rdfs_Container) true = true % 1.02/1.19 |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Class $_979) true % 1.02/1.19 (icext $_979 uri_rdfs_ContainerMembershipProperty) true = true % 1.02/1.19 |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Class $_979) true % 1.02/1.19 (icext $_979 uri_rdfs_Datatype) true = true % 1.02/1.19 |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Class $_979) true % 1.02/1.19 (icext $_979 uri_rdfs_Literal) true = true % 1.02/1.19 |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Class $_979) true % 1.02/1.19 (icext $_979 uri_rdfs_Resource) true = true % 1.02/1.19 |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Class $_979) true % 1.02/1.19 (icext $_979 uri_rdfs_Seq) true = true % 1.02/1.19 |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Class $_979) true % 1.02/1.19 (icext $_979 uri_rdfs_Statement) true = true % 1.02/1.19 |- ifeq % 1.02/1.19 (iext uri_rdfs_subClassOf uri_rdfs_ContainerMembershipProperty $_979) % 1.02/1.19 true (icext $_979 uri_rdf__1) true = true % 1.02/1.19 |- ifeq % 1.02/1.19 (iext uri_rdfs_subClassOf uri_rdfs_ContainerMembershipProperty $_979) % 1.02/1.19 true (icext $_979 uri_rdf__2) true = true % 1.02/1.19 |- ifeq % 1.02/1.19 (iext uri_rdfs_subClassOf uri_rdfs_ContainerMembershipProperty $_979) % 1.02/1.19 true (icext $_979 uri_rdf__3) true = true % 1.02/1.19 |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Datatype $_979) true % 1.02/1.19 (icext $_979 uri_rdf_XMLLiteral) true = true % 1.02/1.19 |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Resource $_979) true % 1.02/1.19 (icext $_979 $_980) true = true % 1.02/1.19 SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 1.02/1.19 %------------------------------------------------------------------------------