%------------------------------------------------------------------------------ % File : ZenonModulo---0.5.0 % Problem : SWB009-10 : TPTP v8.2.0. Released v7.5.0. % Transfm : none % Format : tptp:raw % Command : run_zenon_modulo %d %s % Computer : n016.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 300s % DateTime : Tue Jun 25 02:13:24 EDT 2024 % Result : Unknown 4.26s 4.42s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.12/0.12 % Problem : SWB009-10 : TPTP v8.2.0. Released v7.5.0. % 0.12/0.12 % Command : run_zenon_modulo %d %s % 0.12/0.33 % Computer : n016.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 300 % 0.12/0.33 % DateTime : Thu Jun 20 16:26:09 EDT 2024 % 0.12/0.33 % CPUTime : % 4.24/4.40 Zenon error: exhausted search space without finding a proof % 4.24/4.40 (* Current branch: % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_Restriction)) != (iext (uri_rdf_type) (uri_rdf_type) (uri_rdf_Property))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Literal)) != (iext (uri_rdfs_domain) (uri_rdfs_member) (uri_rdfs_Resource))) % 4.24/4.40 ((uri_rdfs_Class) != (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z)) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_Restriction)) != (iext (uri_rdf_type) (uri_rdf__3) (uri_rdf_Property))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_ex_p)) != (iext (uri_rdf_type) (uri_rdf_subject) (uri_rdf_Property))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_ex_p)) != (iext (uri_rdf_type) (uri_ex_c) (uri_owl_Class))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) zenon_X0) != (iext (uri_rdfs_range) (uri_rdfs_comment) (uri_rdfs_Literal))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_ex_c)) != (iext (uri_rdf_type) (uri_rdf_Property) (uri_rdfs_Class))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_ContainerMembershipProperty)) != (iext (uri_rdfs_range) (uri_rdfs_label) (uri_rdfs_Literal))) % 4.24/4.40 ((uri_rdfs_Resource) != (uri_rdfs_Container)) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z)) != (iext (uri_rdf_type) (uri_rdf__1) (uri_rdfs_ContainerMembershipProperty))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Statement)) != (iext (uri_rdfs_range) (uri_rdf_subject) (uri_rdfs_Resource))) % 4.24/4.40 ((uri_ex_s) != (uri_rdf_predicate)) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_Restriction)) != (iext (uri_rdfs_subClassOf) (uri_rdf_Alt) (uri_rdfs_Container))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_Restriction)) != (iext (uri_rdf_type) (uri_ex_p) (uri_owl_ObjectProperty))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Class)) != (iext (uri_rdfs_subClassOf) (uri_rdfs_Seq) (uri_rdfs_Container))) % 4.24/4.40 ((iext (uri_rdfs_subClassOf) (uri_rdfs_Seq) (uri_rdfs_Container)) = (true)) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Datatype)) != (iext (uri_rdf_type) (uri_rdf__3) (uri_rdf_Property))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_rdf_List)) != (iext (uri_rdfs_domain) (uri_rdfs_comment) (uri_rdfs_Resource))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Class)) != (iext (uri_rdf_type) (uri_ex_p) (uri_owl_ObjectProperty))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z)) != (iext (uri_rdfs_range) (uri_rdf_type) (uri_rdfs_Class))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_ex_c)) != (iext (uri_rdfs_domain) (uri_rdfs_member) (uri_rdfs_Resource))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Literal)) != (iext (uri_rdfs_domain) (uri_rdf_type) (uri_rdfs_Resource))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_seeAlso)) != (iext (uri_rdfs_domain) (uri_rdf__2) (uri_rdfs_Resource))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Statement)) != (iext (uri_owl_onProperty) (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z) (uri_ex_p))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_rdf_Property)) != (iext (uri_rdfs_range) (uri_rdfs_comment) (uri_rdfs_Literal))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Literal)) != (iext (uri_rdfs_domain) (uri_rdfs_subClassOf) (uri_rdfs_Class))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_Class)) != (iext (uri_rdfs_range) (uri_rdfs_member) (uri_rdfs_Resource))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_Class)) != (iext (uri_rdfs_subClassOf) (uri_rdfs_ContainerMembershipProperty) (uri_rdf_Property))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) zenon_X0) != (iext (uri_rdfs_domain) (uri_rdfs_subClassOf) (uri_rdfs_Class))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_rdf_List)) != (iext (uri_rdfs_domain) (uri_rdf_value) (uri_rdfs_Resource))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Literal)) != (iext (uri_rdfs_domain) (uri_rdf__3) (uri_rdfs_Resource))) % 4.24/4.40 ((uri_ex_s) != (uri_rdf_object)) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z)) != (iext (uri_rdfs_range) (uri_rdfs_isDefinedBy) (uri_rdfs_Resource))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_ObjectProperty)) != (iext (uri_rdfs_range) (uri_rdf__2) (uri_rdfs_Resource))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Literal)) != (iext (uri_rdf_type) (uri_rdf__1) (uri_rdfs_ContainerMembershipProperty))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Literal)) != (iext (uri_owl_onProperty) (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z) (uri_ex_p))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Resource)) != (iext (uri_rdf_type) (uri_rdf_type) (uri_rdf_Property))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Statement)) != (iext (uri_rdfs_range) (uri_rdf_first) (uri_rdfs_Resource))) % 4.24/4.40 ((uri_rdfs_Literal) != (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z)) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z)) != (iext (uri_rdf_type) (uri_ex_p) (uri_owl_ObjectProperty))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_ContainerMembershipProperty)) != (iext (uri_rdf_type) (uri_rdf_rest) (uri_rdf_Property))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_ex_c)) != (iext (uri_rdfs_range) (uri_rdf_value) (uri_rdfs_Resource))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_Restriction)) != (iext (uri_rdfs_range) (uri_rdfs_isDefinedBy) (uri_rdfs_Resource))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_seeAlso)) != (iext (uri_rdfs_domain) (uri_rdf_value) (uri_rdfs_Resource))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_ObjectProperty)) != (iext (uri_rdfs_range) (uri_rdf__1) (uri_rdfs_Resource))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_ex_c)) != (iext (uri_rdfs_domain) (uri_rdfs_domain) (uri_rdf_Property))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Class)) != (iext (uri_rdfs_subPropertyOf) (uri_rdfs_isDefinedBy) (uri_rdfs_seeAlso))) % 4.24/4.40 ((uri_ex_s) != (uri_rdf_type)) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z)) != (iext (uri_rdfs_range) (uri_rdf__2) (uri_rdfs_Resource))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Datatype)) != (iext (uri_rdfs_domain) (uri_rdfs_subPropertyOf) (uri_rdf_Property))) % 4.24/4.40 ((uri_rdfs_Literal) != (uri_rdfs_Class)) % 4.24/4.40 ((uri_rdfs_Literal) != (uri_ex_c)) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Resource)) != (iext (uri_rdfs_domain) (uri_rdf__3) (uri_rdfs_Resource))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Container)) != (iext (uri_rdfs_domain) (uri_rdf_rest) (uri_rdf_List))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_ContainerMembershipProperty)) != (iext (uri_rdfs_domain) (uri_rdfs_domain) (uri_rdf_Property))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Literal)) != (iext (uri_rdfs_domain) (uri_rdfs_isDefinedBy) (uri_rdfs_Resource))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Class)) != (iext (uri_rdfs_domain) (uri_rdf__2) (uri_rdfs_Resource))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_rdf_List)) != (iext (uri_rdf_type) (uri_ex_s) (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) zenon_X0) != (iext (uri_rdf_type) (uri_ex_c) (uri_owl_Class))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Datatype)) != (iext (uri_rdf_type) (uri_ex_c) (uri_owl_Class))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_ContainerMembershipProperty)) != (iext (uri_rdfs_domain) (uri_rdf_value) (uri_rdfs_Resource))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_ex_p)) != (iext (uri_rdfs_domain) (uri_rdfs_isDefinedBy) (uri_rdfs_Resource))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_rdf_Property)) != (iext (uri_rdfs_subClassOf) (uri_rdfs_Seq) (uri_rdfs_Container))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_rdf_Property)) != (iext (uri_rdf_type) (uri_ex_c) (uri_owl_Class))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_rdf_Property)) != (iext (uri_rdfs_range) (uri_rdfs_member) (uri_rdfs_Resource))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Datatype)) != (iext (uri_rdfs_range) (uri_rdf_subject) (uri_rdfs_Resource))) % 4.24/4.40 ((uri_rdfs_seeAlso) != (uri_ex_p)) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_Class)) != (iext (uri_rdfs_domain) (uri_rdfs_domain) (uri_rdf_Property))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Literal)) != (iext (uri_rdfs_domain) (uri_rdf_first) (uri_rdf_List))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Resource)) != (iext (uri_rdf_type) (uri_rdf__1) (uri_rdfs_ContainerMembershipProperty))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_seeAlso)) != (iext (uri_rdfs_subClassOf) (uri_rdf_XMLLiteral) (uri_rdfs_Literal))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Statement)) != (iext (uri_rdfs_domain) (uri_rdf__3) (uri_rdfs_Resource))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Statement)) != (iext (uri_rdfs_domain) (uri_rdfs_domain) (uri_rdf_Property))) % 4.24/4.40 ((uri_ex_s) != (uri_rdf_Bag)) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Container)) != (iext (uri_rdfs_range) (uri_rdf__2) (uri_rdfs_Resource))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_seeAlso)) != (iext (uri_rdf_type) (uri_rdf__2) (uri_rdfs_ContainerMembershipProperty))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_ObjectProperty)) != (iext (uri_rdfs_range) (uri_rdfs_domain) (uri_rdfs_Class))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_ContainerMembershipProperty)) != (iext (uri_rdfs_domain) (uri_rdf__1) (uri_rdfs_Resource))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_rdf_List)) != (iext (uri_rdf_type) (uri_rdf_type) (uri_rdf_Property))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_ContainerMembershipProperty)) != (iext (uri_rdf_type) (uri_ex_c) (uri_owl_Class))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_Class)) != (iext (uri_rdfs_domain) (uri_rdf__1) (uri_rdfs_Resource))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_Class)) != (iext (uri_rdfs_range) (uri_rdfs_comment) (uri_rdfs_Literal))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_rdf_Property)) != (iext (uri_rdf_type) (uri_ex_s) (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Literal)) != (iext (uri_rdf_type) (uri_rdf_Property) (uri_rdfs_Class))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_ObjectProperty)) != (iext (uri_rdfs_subClassOf) (uri_rdfs_ContainerMembershipProperty) (uri_rdf_Property))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Class)) != (iext (uri_owl_onProperty) (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z) (uri_ex_p))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) zenon_X0) != (iext (uri_owl_onProperty) (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z) (uri_ex_p))) % 4.24/4.40 ((iext (uri_rdfs_subClassOf) (uri_rdf_XMLLiteral) (uri_rdfs_Literal)) = (true)) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_rdf_Property)) != (iext (uri_rdfs_range) (uri_rdfs_label) (uri_rdfs_Literal))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) zenon_X0) != (iext (uri_rdf_type) (uri_rdf__1) (uri_rdf_Property))) % 4.24/4.40 ((tuple (iext (uri_rdf_type) (uri_rdfs_Resource) (uri_ex_c)) (iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Resource))) != (tuple (true) (true))) % 4.24/4.40 ((uri_rdf_Property) != (uri_rdfs_seeAlso)) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_rdf_List)) != (iext (uri_rdfs_range) (uri_rdfs_isDefinedBy) (uri_rdfs_Resource))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Class)) != (iext (uri_rdf_type) (uri_rdf_type) (uri_rdf_Property))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Datatype)) != (iext (uri_rdfs_domain) (uri_rdfs_subClassOf) (uri_rdfs_Class))) % 4.24/4.40 ((uri_rdf_List) != (uri_rdfs_Resource)) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_rdf_Property)) != (iext (uri_rdfs_range) (uri_rdf_rest) (uri_rdf_List))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Container)) != (iext (uri_rdfs_range) (uri_rdf__3) (uri_rdfs_Resource))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_Restriction)) != (iext (uri_rdf_type) (uri_rdf_first) (uri_rdf_Property))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_ex_p)) != (iext (uri_rdfs_range) (uri_rdf_predicate) (uri_rdfs_Resource))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_seeAlso)) != (iext (uri_rdfs_domain) (uri_rdf_rest) (uri_rdf_List))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z)) != (iext (uri_rdfs_subPropertyOf) (uri_rdfs_isDefinedBy) (uri_rdfs_seeAlso))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_ContainerMembershipProperty)) != (iext (uri_rdf_type) (uri_ex_p) (uri_owl_ObjectProperty))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_rdf_List)) != (iext (uri_rdfs_subPropertyOf) (uri_rdfs_isDefinedBy) (uri_rdfs_seeAlso))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_seeAlso)) != (iext (uri_rdfs_domain) (uri_rdfs_member) (uri_rdfs_Resource))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_rdf_Property)) != (iext (uri_rdfs_range) (uri_rdf_value) (uri_rdfs_Resource))) % 4.24/4.40 ((iext (uri_rdf_type) (uri_ex_p) (uri_owl_ObjectProperty)) = (true)) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_ex_p)) != (iext (uri_rdfs_domain) (uri_rdf_rest) (uri_rdf_List))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Container)) != (iext (uri_rdf_type) (uri_ex_c) (uri_owl_Class))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_seeAlso)) != (iext (uri_rdfs_range) (uri_rdf_value) (uri_rdfs_Resource))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Datatype)) != (iext (uri_rdfs_range) (uri_rdfs_subClassOf) (uri_rdfs_Class))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Container)) != (iext (uri_rdfs_subClassOf) (uri_rdf_Alt) (uri_rdfs_Container))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_rdf_Property)) != (iext (uri_rdfs_domain) (uri_rdfs_comment) (uri_rdfs_Resource))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_rdf_List)) != (iext (uri_rdfs_domain) (uri_rdfs_range) (uri_rdf_Property))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Literal)) != (iext (uri_rdf_type) (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z) (uri_owl_Restriction))) % 4.24/4.40 ((uri_rdf_List) != (uri_ex_c)) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Statement)) != (iext (uri_rdfs_range) (uri_rdfs_comment) (uri_rdfs_Literal))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z)) != (iext (uri_rdfs_domain) (uri_rdfs_range) (uri_rdf_Property))) % 4.24/4.40 (zenon_X0 != (uri_rdfs_Datatype)) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Container)) != (iext (uri_rdf_type) (uri_rdf_XMLLiteral) (uri_rdfs_Datatype))) % 4.24/4.40 (zenon_X0 != (uri_rdfs_Statement)) % 4.24/4.40 ((uri_ex_s) != (uri_rdfs_isDefinedBy)) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) zenon_X0) != (iext (uri_rdf_type) (uri_rdf_subject) (uri_rdf_Property))) % 4.24/4.40 ((uri_rdf_Property) != (uri_rdfs_Resource)) % 4.24/4.40 ((uri_rdf_Property) != (uri_rdfs_Class)) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Literal)) != (iext (uri_owl_someValuesFrom) (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z) (uri_ex_c))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Statement)) != (iext (uri_rdfs_domain) (uri_rdf_subject) (uri_rdfs_Statement))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_ex_c)) != (iext (uri_rdfs_domain) (uri_rdf__1) (uri_rdfs_Resource))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_ObjectProperty)) != (iext (uri_rdf_type) (uri_rdf_Property) (uri_rdfs_Class))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_ex_c)) != (iext (uri_rdf_type) (uri_rdf__2) (uri_rdf_Property))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Statement)) != (iext (uri_rdf_type) (uri_rdf_first) (uri_rdf_Property))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_ContainerMembershipProperty)) != (iext (uri_rdfs_range) (uri_rdf__1) (uri_rdfs_Resource))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_Class)) != (iext (uri_rdfs_range) (uri_rdf_value) (uri_rdfs_Resource))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Resource)) != (iext (uri_rdf_type) (uri_rdf_XMLLiteral) (uri_rdfs_Datatype))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Container)) != (iext (uri_rdfs_domain) (uri_rdfs_range) (uri_rdf_Property))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_rdf_List)) != (iext (uri_rdf_type) (uri_rdf_object) (uri_rdf_Property))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_ContainerMembershipProperty)) != (iext (uri_rdfs_domain) (uri_rdf__2) (uri_rdfs_Resource))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Statement)) != (iext (uri_rdf_type) (uri_rdf_nil) (uri_rdf_List))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Class)) != (iext (uri_rdf_type) (uri_rdf_first) (uri_rdf_Property))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Literal)) != (iext (uri_rdfs_subClassOf) (uri_rdf_Alt) (uri_rdfs_Container))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Literal)) != (iext (uri_rdfs_range) (uri_rdf_predicate) (uri_rdfs_Resource))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_ContainerMembershipProperty)) != (iext (uri_rdfs_subClassOf) (uri_rdf_Alt) (uri_rdfs_Container))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_ex_c)) != (iext (uri_rdfs_domain) (uri_rdfs_range) (uri_rdf_Property))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_ex_c)) != (iext (uri_rdfs_domain) (uri_rdf__3) (uri_rdfs_Resource))) % 4.24/4.40 ((uri_rdfs_Literal) != (uri_rdfs_Container)) % 4.24/4.40 ((uri_rdfs_Resource) != (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z)) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Container)) != (iext (uri_rdf_type) (uri_ex_p) (uri_owl_ObjectProperty))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_Restriction)) != (iext (uri_rdf_type) (uri_rdf_value) (uri_rdf_Property))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z)) != (iext (uri_rdfs_range) (uri_rdfs_label) (uri_rdfs_Literal))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_ex_c)) != (iext (uri_rdfs_range) (uri_rdfs_label) (uri_rdfs_Literal))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Literal)) != (iext (uri_rdfs_range) (uri_rdfs_comment) (uri_rdfs_Literal))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Resource)) != (iext (uri_rdfs_range) (uri_rdfs_range) (uri_rdfs_Class))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_ContainerMembershipProperty)) != (iext (uri_rdf_type) (uri_rdf_XMLLiteral) (uri_rdfs_Datatype))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_seeAlso)) != (iext (uri_rdfs_domain) (uri_rdf_type) (uri_rdfs_Resource))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Statement)) != (iext (uri_rdfs_subPropertyOf) (uri_rdfs_isDefinedBy) (uri_rdfs_seeAlso))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Resource)) != (true)) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_ex_c)) != (iext (uri_rdfs_domain) (uri_rdfs_label) (uri_rdfs_Resource))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Container)) != (iext (uri_rdf_type) (uri_rdf__3) (uri_rdf_Property))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_rdf_Property)) != (iext (uri_owl_someValuesFrom) (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z) (uri_ex_c))) % 4.24/4.40 ((uri_rdfs_Resource) != (uri_owl_Class)) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Literal)) != (iext (uri_rdfs_domain) (uri_rdf_rest) (uri_rdf_List))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_Restriction)) != (iext (uri_rdfs_subClassOf) (uri_rdfs_Datatype) (uri_rdfs_Class))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Statement)) != (iext (uri_rdfs_domain) (uri_rdf_value) (uri_rdfs_Resource))) % 4.24/4.40 ((iext (uri_rdf_type) (uri_rdf__2) (uri_rdfs_ContainerMembershipProperty)) = (true)) % 4.24/4.40 ((uri_rdfs_Datatype) != (uri_rdfs_Class)) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Class)) != (iext (uri_rdfs_domain) (uri_rdfs_member) (uri_rdfs_Resource))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_ObjectProperty)) != (iext (uri_rdf_type) (uri_rdf_rest) (uri_rdf_Property))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) zenon_X0) != (iext (uri_rdfs_range) (uri_rdfs_domain) (uri_rdfs_Class))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Resource)) != (iext (uri_rdf_type) (uri_rdf__2) (uri_rdfs_ContainerMembershipProperty))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_ContainerMembershipProperty)) != (iext (uri_rdf_type) (uri_rdf_object) (uri_rdf_Property))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_rdf_List)) != (iext (uri_rdf_type) (uri_rdf_subject) (uri_rdf_Property))) % 4.24/4.40 ((uri_rdfs_Container) != (uri_ex_p)) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_ex_c)) != (iext (uri_rdfs_subClassOf) (uri_rdf_Alt) (uri_rdfs_Container))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_ex_p)) != (iext (uri_rdfs_subClassOf) (uri_rdf_Bag) (uri_rdfs_Container))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_rdf_List)) != (iext (uri_rdf_type) (uri_rdf_nil) (uri_rdf_List))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Container)) != (iext (uri_rdfs_range) (uri_rdfs_range) (uri_rdfs_Class))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Container)) != (iext (uri_rdfs_range) (uri_rdfs_subClassOf) (uri_rdfs_Class))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_Restriction)) != (iext (uri_rdfs_domain) (uri_rdfs_member) (uri_rdfs_Resource))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_ObjectProperty)) != (iext (uri_rdf_type) (uri_rdf_XMLLiteral) (uri_rdfs_Datatype))) % 4.24/4.40 ((iext (uri_rdfs_domain) (uri_rdfs_member) (uri_rdfs_Resource)) = (true)) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_Restriction)) != (iext (uri_rdfs_range) (uri_rdf__1) (uri_rdfs_Resource))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Datatype)) != (iext (uri_rdfs_range) (uri_rdf__2) (uri_rdfs_Resource))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_ex_c)) != (iext (uri_rdf_type) (uri_rdf_nil) (uri_rdf_List))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_rdf_Property)) != (iext (uri_rdf_type) (uri_rdf__1) (uri_rdfs_ContainerMembershipProperty))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_rdf_List)) != (iext (uri_rdf_type) (uri_rdf__3) (uri_rdf_Property))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_rdf_List)) != (iext (uri_owl_onProperty) (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z) (uri_ex_p))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z)) != (iext (uri_rdf_type) (uri_rdf_object) (uri_rdf_Property))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z)) != (iext (uri_rdfs_range) (uri_rdfs_comment) (uri_rdfs_Literal))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_ObjectProperty)) != (iext (uri_rdf_type) (uri_rdf_subject) (uri_rdf_Property))) % 4.24/4.40 ((iext (uri_rdf_type) (uri_rdf_value) (uri_rdf_Property)) = (true)) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Literal)) != (iext (uri_rdf_type) (uri_rdf_XMLLiteral) (uri_rdfs_Datatype))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Datatype)) != (iext (uri_rdfs_range) (uri_rdf__1) (uri_rdfs_Resource))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_ObjectProperty)) != (iext (uri_rdfs_range) (uri_rdf_rest) (uri_rdf_List))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Class)) != (iext (uri_rdf_type) (uri_ex_s) (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Statement)) != (iext (uri_rdf_type) (uri_rdf_object) (uri_rdf_Property))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_Class)) != (iext (uri_rdfs_range) (uri_rdf_predicate) (uri_rdfs_Resource))) % 4.24/4.40 ((uri_ex_s) != (uri_rdf_XMLLiteral)) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Literal)) != (iext (uri_rdfs_range) (uri_rdf_type) (uri_rdfs_Class))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Class)) != (iext (uri_rdf_type) (uri_rdf_nil) (uri_rdf_List))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Statement)) != (iext (uri_rdfs_domain) (uri_rdfs_seeAlso) (uri_rdfs_Resource))) % 4.24/4.40 ((uri_rdfs_Statement) != (uri_owl_Class)) % 4.24/4.40 ((iext (uri_rdfs_range) (uri_rdf_subject) (uri_rdfs_Resource)) = (true)) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_rdf_Property)) != (iext (uri_rdfs_range) (uri_rdfs_subPropertyOf) (uri_rdf_Property))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_ex_c)) != (iext (uri_rdfs_domain) (uri_rdf_first) (uri_rdf_List))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_Class)) != (iext (uri_rdf_type) (uri_rdf__3) (uri_rdfs_ContainerMembershipProperty))) % 4.24/4.40 ((tuple (iext (uri_rdf_type) (uri_rdfs_Container) (uri_ex_c)) (iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Container))) != (tuple (true) (true))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_ContainerMembershipProperty)) != (iext (uri_rdfs_domain) (uri_rdfs_comment) (uri_rdfs_Resource))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) zenon_X0) != (iext (uri_rdfs_range) (uri_rdfs_isDefinedBy) (uri_rdfs_Resource))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Literal)) != (iext (uri_rdf_type) (uri_rdf__3) (uri_rdfs_ContainerMembershipProperty))) % 4.24/4.40 ((uri_rdfs_Statement) != (uri_owl_ObjectProperty)) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_Restriction)) != (iext (uri_rdfs_domain) (uri_rdf_predicate) (uri_rdfs_Statement))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_ObjectProperty)) != (iext (uri_rdf_type) (uri_rdf_nil) (uri_rdf_List))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_ObjectProperty)) != (iext (uri_rdfs_subClassOf) (uri_rdfs_Datatype) (uri_rdfs_Class))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_Class)) != (iext (uri_rdfs_subClassOf) (uri_rdfs_Seq) (uri_rdfs_Container))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_ex_c)) != (iext (uri_rdfs_domain) (uri_rdfs_subClassOf) (uri_rdfs_Class))) % 4.24/4.40 (zenon_X0 != (uri_rdfs_ContainerMembershipProperty)) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) zenon_X0) != (iext (uri_rdf_type) (uri_rdf_first) (uri_rdf_Property))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Container)) != (iext (uri_rdfs_range) (uri_rdfs_label) (uri_rdfs_Literal))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z)) != (iext (uri_rdfs_range) (uri_rdfs_seeAlso) (uri_rdfs_Resource))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_ex_c)) != (iext (uri_rdf_type) (uri_rdf_value) (uri_rdf_Property))) % 4.24/4.40 ((iext (uri_ex_p) (uri_ex_s) (uri_ex_c)) != (iext (uri_rdfs_domain) (uri_rdf__2) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Resource)) != (iext (uri_owl_someValuesFrom) (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z) (uri_ex_c))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Container)) != (iext (uri_rdfs_domain) (uri_rdf_predicate) (uri_rdfs_Statement))) % 4.24/4.41 ((sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z) != (uri_owl_Class)) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdf_List)) != (iext (uri_rdf_type) (uri_rdf__1) (uri_rdf_Property))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Datatype)) != (iext (uri_rdfs_range) (uri_rdf_predicate) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_seeAlso)) != (iext (uri_rdfs_domain) (uri_rdfs_label) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_ObjectProperty)) != (iext (uri_rdfs_subClassOf) (uri_rdfs_Seq) (uri_rdfs_Container))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdf_Property)) != (iext (uri_rdfs_range) (uri_rdf__2) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z)) != (iext (uri_rdfs_range) (uri_rdf__3) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_ContainerMembershipProperty)) != (iext (uri_rdfs_range) (uri_rdf__3) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_ContainerMembershipProperty)) != (iext (uri_rdfs_range) (uri_rdf_predicate) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Resource)) != (iext (uri_rdfs_range) (uri_rdf_first) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_seeAlso)) != (iext (uri_rdf_type) (uri_rdf_value) (uri_rdf_Property))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_ex_p)) != (iext (uri_rdfs_domain) (uri_rdfs_subPropertyOf) (uri_rdf_Property))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_ex_c)) != (iext (uri_rdf_type) (uri_rdf__2) (uri_rdfs_ContainerMembershipProperty))) % 4.24/4.41 ((tuple (iext (uri_rdf_type) (uri_ex_c) (uri_ex_c)) (iext (uri_ex_p) (uri_ex_s) (uri_ex_c))) != (tuple (true) (true))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_ex_c)) != (iext (uri_rdfs_range) (uri_rdfs_subClassOf) (uri_rdfs_Class))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Literal)) != (iext (uri_rdf_type) (uri_rdf__2) (uri_rdf_Property))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdf_List)) != (iext (uri_rdfs_domain) (uri_rdf__2) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Literal)) != (iext (uri_rdf_type) (uri_rdf__1) (uri_rdf_Property))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z)) != (iext (uri_rdfs_domain) (uri_rdf_rest) (uri_rdf_List))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_Class)) != (iext (uri_rdfs_domain) (uri_rdfs_label) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_seeAlso)) != (iext (uri_rdfs_range) (uri_rdf__1) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_ContainerMembershipProperty)) != (iext (uri_rdfs_domain) (uri_rdfs_seeAlso) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_ObjectProperty)) != (iext (uri_rdfs_domain) (uri_rdfs_domain) (uri_rdf_Property))) % 4.24/4.41 ((iext (uri_owl_onProperty) (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z) (uri_ex_p)) = (true)) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Datatype)) != (iext (uri_rdf_type) (uri_rdf__1) (uri_rdfs_ContainerMembershipProperty))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Resource)) != (iext (uri_rdfs_range) (uri_rdfs_subClassOf) (uri_rdfs_Class))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Container)) != (iext (uri_rdf_type) (uri_ex_s) (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z)) != (iext (uri_rdfs_domain) (uri_rdf__3) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_rdfs_domain) (uri_rdf_rest) (uri_rdf_List)) = (true)) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Literal)) != (iext (uri_rdfs_subClassOf) (uri_rdfs_ContainerMembershipProperty) (uri_rdf_Property))) % 4.24/4.41 ((uri_rdf_Property) != (uri_ex_c)) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Class)) != (iext (uri_rdfs_domain) (uri_rdf_predicate) (uri_rdfs_Statement))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Resource)) != (iext (uri_rdf_type) (uri_ex_p) (uri_owl_ObjectProperty))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Statement)) != (iext (uri_rdfs_subClassOf) (uri_rdf_Bag) (uri_rdfs_Container))) % 4.24/4.41 (zenon_X0 != (uri_rdf_List)) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdf_List)) != (iext (uri_rdf_type) (uri_rdf__1) (uri_rdfs_ContainerMembershipProperty))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_ContainerMembershipProperty)) != (iext (uri_rdfs_range) (uri_rdfs_domain) (uri_rdfs_Class))) % 4.24/4.41 ((uri_rdfs_seeAlso) != (uri_owl_Restriction)) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_ex_c)) != (iext (uri_rdfs_range) (uri_rdf_type) (uri_rdfs_Class))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdf_List)) != (iext (uri_rdf_type) (uri_rdf_Property) (uri_rdfs_Class))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Container)) != (iext (uri_rdf_type) (uri_rdf_subject) (uri_rdf_Property))) % 4.24/4.41 ((tuple (iext (uri_rdf_type) (uri_owl_Class) (uri_ex_c)) (iext (uri_ex_p) (uri_ex_s) (uri_owl_Class))) != (tuple (true) (true))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdf_Property)) != (iext (uri_rdf_type) (uri_rdf_object) (uri_rdf_Property))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_ContainerMembershipProperty)) != (iext (uri_rdfs_domain) (uri_rdfs_isDefinedBy) (uri_rdfs_Resource))) % 4.24/4.41 ((uri_rdf_List) != (uri_rdfs_Class)) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_Restriction)) != (iext (uri_rdfs_domain) (uri_rdf_subject) (uri_rdfs_Statement))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_ContainerMembershipProperty)) != (iext (uri_rdf_type) (uri_rdf__3) (uri_rdf_Property))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) zenon_X0) != (iext (uri_rdfs_domain) (uri_rdf_predicate) (uri_rdfs_Statement))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_Restriction)) != (iext (uri_rdfs_range) (uri_rdf_value) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_Restriction)) != (iext (uri_rdfs_domain) (uri_rdf__2) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Statement)) != (iext (uri_rdfs_range) (uri_rdf__1) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_Class)) != (iext (uri_rdfs_range) (uri_rdfs_seeAlso) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_rdfs_domain) (uri_rdf_predicate) (uri_rdfs_Statement)) = (true)) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdf_Property)) != (iext (uri_rdf_type) (uri_rdf__2) (uri_rdf_Property))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_ObjectProperty)) != (iext (uri_rdfs_range) (uri_rdfs_subPropertyOf) (uri_rdf_Property))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_ex_p)) != (iext (uri_rdfs_domain) (uri_rdfs_label) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Resource)) != (iext (uri_rdfs_domain) (uri_rdf__2) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdf_Property)) != (iext (uri_rdfs_domain) (uri_rdfs_seeAlso) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_seeAlso)) != (iext (uri_rdf_type) (uri_ex_s) (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_seeAlso)) != (iext (uri_rdfs_domain) (uri_rdf_first) (uri_rdf_List))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) zenon_X0) != (iext (uri_rdf_type) (uri_rdf_object) (uri_rdf_Property))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Datatype)) != (iext (uri_rdfs_domain) (uri_rdf__1) (uri_rdfs_Resource))) % 4.24/4.41 ((uri_rdfs_seeAlso) != (uri_owl_Class)) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_Restriction)) != (iext (uri_rdf_type) (uri_rdf_Property) (uri_rdfs_Class))) % 4.24/4.41 ((uri_rdf_List) != (uri_rdfs_Literal)) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Class)) != (iext (uri_rdfs_range) (uri_rdf_first) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_Class)) != (iext (uri_rdfs_domain) (uri_rdf_object) (uri_rdfs_Statement))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdf_List)) != (iext (uri_rdfs_range) (uri_rdfs_member) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Container)) != (iext (uri_rdf_type) (uri_rdf__1) (uri_rdfs_ContainerMembershipProperty))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Literal)) != (iext (uri_rdfs_range) (uri_rdfs_isDefinedBy) (uri_rdfs_Resource))) % 4.24/4.41 ((uri_rdf_Property) != (uri_rdfs_Container)) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Class)) != (iext (uri_rdfs_range) (uri_rdfs_domain) (uri_rdfs_Class))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Statement)) != (iext (uri_rdfs_domain) (uri_rdfs_subClassOf) (uri_rdfs_Class))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Datatype)) != (iext (uri_rdf_type) (uri_rdf_Property) (uri_rdfs_Class))) % 4.24/4.41 ((tuple (iext (uri_rdf_type) (uri_ex_p) (uri_ex_c)) (iext (uri_ex_p) (uri_ex_s) (uri_ex_p))) != (tuple (true) (true))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_Restriction)) != (iext (uri_rdf_type) (uri_ex_s) (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdf_List)) != (iext (uri_rdfs_range) (uri_rdf__2) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_ContainerMembershipProperty)) != (iext (uri_rdfs_range) (uri_rdf_rest) (uri_rdf_List))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_seeAlso)) != (iext (uri_rdfs_range) (uri_rdfs_subClassOf) (uri_rdfs_Class))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Class)) != (iext (uri_rdfs_domain) (uri_rdfs_subPropertyOf) (uri_rdf_Property))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Statement)) != (iext (uri_rdfs_subClassOf) (uri_rdf_XMLLiteral) (uri_rdfs_Literal))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_ex_c)) != (iext (uri_rdfs_subClassOf) (uri_rdf_XMLLiteral) (uri_rdfs_Literal))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdf_List)) != (iext (uri_rdfs_subClassOf) (uri_rdf_Alt) (uri_rdfs_Container))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Container)) != (iext (uri_rdfs_range) (uri_rdf__1) (uri_rdfs_Resource))) % 4.24/4.41 ((uri_rdfs_Datatype) != (uri_ex_p)) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdf_List)) != (iext (uri_owl_someValuesFrom) (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z) (uri_ex_c))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_ContainerMembershipProperty)) != (iext (uri_rdfs_subClassOf) (uri_rdfs_ContainerMembershipProperty) (uri_rdf_Property))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_Class)) != (iext (uri_rdfs_range) (uri_rdfs_label) (uri_rdfs_Literal))) % 4.24/4.41 ((uri_rdf_List) != (uri_rdfs_seeAlso)) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_Restriction)) != (iext (uri_rdfs_domain) (uri_rdfs_subClassOf) (uri_rdfs_Class))) % 4.24/4.41 ((uri_ex_s) != (uri_rdf_first)) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdf_Property)) != (iext (uri_rdfs_subPropertyOf) (uri_rdfs_isDefinedBy) (uri_rdfs_seeAlso))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdf_Property)) != (iext (uri_rdf_type) (uri_rdf_Property) (uri_rdfs_Class))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_Class)) != (iext (uri_rdfs_range) (uri_rdfs_range) (uri_rdfs_Class))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_ex_c)) != (true)) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdf_List)) != (iext (uri_rdfs_domain) (uri_rdf__1) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Resource)) != (iext (uri_rdf_type) (uri_rdf__3) (uri_rdfs_ContainerMembershipProperty))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_Restriction)) != (iext (uri_rdfs_range) (uri_rdf_type) (uri_rdfs_Class))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_ex_c)) != (iext (uri_rdf_type) (uri_rdf__1) (uri_rdfs_ContainerMembershipProperty))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_ex_p)) != (iext (uri_rdf_type) (uri_rdf_type) (uri_rdf_Property))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_Class)) != (iext (uri_rdfs_domain) (uri_rdf_rest) (uri_rdf_List))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Class)) != (true)) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z)) != (iext (uri_rdfs_domain) (uri_rdf_first) (uri_rdf_List))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_Class)) != (iext (uri_rdfs_range) (uri_rdf__1) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z)) != (iext (uri_rdfs_domain) (uri_rdf_type) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_Restriction)) != (iext (uri_rdfs_subClassOf) (uri_rdfs_Seq) (uri_rdfs_Container))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_Class)) != (iext (uri_rdfs_range) (uri_rdf__2) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_ex_c)) != (iext (uri_rdfs_range) (uri_rdfs_subPropertyOf) (uri_rdf_Property))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Container)) != (iext (uri_rdfs_domain) (uri_rdf__3) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_ex_c)) != (iext (uri_rdf_type) (uri_ex_p) (uri_owl_ObjectProperty))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Datatype)) != (iext (uri_rdf_type) (uri_rdf__2) (uri_rdfs_ContainerMembershipProperty))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_Class)) != (iext (uri_rdf_type) (uri_rdf__1) (uri_rdf_Property))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_ex_c)) != (iext (uri_rdfs_domain) (uri_rdf_type) (uri_rdfs_Resource))) % 4.24/4.41 ((uri_rdfs_seeAlso) != (uri_ex_c)) % 4.24/4.41 ((uri_rdfs_Datatype) != (uri_owl_ObjectProperty)) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_Class)) != (iext (uri_rdfs_domain) (uri_rdfs_subPropertyOf) (uri_rdf_Property))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Container)) != (iext (uri_rdfs_domain) (uri_rdfs_domain) (uri_rdf_Property))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_ex_p)) != (iext (uri_rdfs_range) (uri_rdfs_label) (uri_rdfs_Literal))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_ex_c)) != (iext (uri_rdfs_domain) (uri_rdf_predicate) (uri_rdfs_Statement))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_ex_p)) != (iext (uri_rdfs_domain) (uri_rdf_first) (uri_rdf_List))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Container)) != (iext (uri_rdfs_subClassOf) (uri_rdfs_ContainerMembershipProperty) (uri_rdf_Property))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Class)) != (iext (uri_rdfs_domain) (uri_rdfs_seeAlso) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdf_Property)) != (iext (uri_rdf_type) (uri_rdf__3) (uri_rdfs_ContainerMembershipProperty))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdf_Property)) != (iext (uri_rdfs_domain) (uri_rdfs_range) (uri_rdf_Property))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Statement)) != (iext (uri_rdf_type) (uri_rdf__1) (uri_rdf_Property))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Statement)) != (iext (uri_rdfs_range) (uri_rdf__3) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Statement)) != (iext (uri_rdfs_domain) (uri_rdf_rest) (uri_rdf_List))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_Class)) != (iext (uri_rdf_type) (uri_ex_c) (uri_owl_Class))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_ex_p)) != (iext (uri_owl_someValuesFrom) (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z) (uri_ex_c))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_ContainerMembershipProperty)) != (iext (uri_rdf_type) (uri_rdf_Property) (uri_rdfs_Class))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_ex_p)) != (iext (uri_rdf_type) (uri_rdf__3) (uri_rdfs_ContainerMembershipProperty))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_seeAlso)) != (iext (uri_rdfs_range) (uri_rdf_type) (uri_rdfs_Class))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Datatype)) != (iext (uri_rdf_type) (uri_ex_p) (uri_owl_ObjectProperty))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_Restriction)) != (iext (uri_rdfs_domain) (uri_rdf_object) (uri_rdfs_Statement))) % 4.24/4.41 ((iext (uri_rdfs_range) (uri_rdfs_subClassOf) (uri_rdfs_Class)) = (true)) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_Restriction)) != (iext (uri_rdfs_domain) (uri_rdfs_seeAlso) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_ObjectProperty)) != (iext (uri_rdfs_domain) (uri_rdf__1) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) zenon_X0) != (iext (uri_rdfs_subClassOf) (uri_rdfs_Datatype) (uri_rdfs_Class))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdf_List)) != (iext (uri_rdfs_domain) (uri_rdfs_subPropertyOf) (uri_rdf_Property))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) zenon_X0) != (iext (uri_rdfs_domain) (uri_rdf_first) (uri_rdf_List))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Datatype)) != (iext (uri_rdfs_subClassOf) (uri_rdf_Bag) (uri_rdfs_Container))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Datatype)) != (iext (uri_rdfs_range) (uri_rdfs_domain) (uri_rdfs_Class))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_ContainerMembershipProperty)) != (iext (uri_rdfs_subPropertyOf) (uri_rdfs_isDefinedBy) (uri_rdfs_seeAlso))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdf_Property)) != (iext (uri_rdf_type) (uri_rdf_rest) (uri_rdf_Property))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) zenon_X0) != (iext (uri_rdfs_range) (uri_rdfs_subClassOf) (uri_rdfs_Class))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_ObjectProperty)) != (true)) % 4.24/4.41 ((uri_rdf_Property) != (uri_rdfs_Statement)) % 4.24/4.41 ((iext (uri_rdf_type) (uri_ex_s) (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z)) = (true)) % 4.24/4.41 (zenon_X0 != (uri_rdfs_Container)) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) zenon_X0) != (iext (uri_rdfs_domain) (uri_rdf__1) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Datatype)) != (iext (uri_owl_onProperty) (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z) (uri_ex_p))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_Class)) != (iext (uri_rdf_type) (uri_rdf_type) (uri_rdf_Property))) % 4.24/4.41 ((tuple (iext (uri_rdf_type) (uri_rdfs_Class) (uri_ex_c)) (iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Class))) != (tuple (true) (true))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdf_List)) != (iext (uri_rdfs_range) (uri_rdf_first) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_seeAlso)) != (iext (uri_rdfs_subClassOf) (uri_rdf_Bag) (uri_rdfs_Container))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_seeAlso)) != (iext (uri_owl_someValuesFrom) (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z) (uri_ex_c))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Class)) != (iext (uri_rdfs_range) (uri_rdf_rest) (uri_rdf_List))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_ex_c)) != (iext (uri_rdf_type) (uri_rdf_first) (uri_rdf_Property))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_ex_p)) != (iext (uri_rdf_type) (uri_rdf_value) (uri_rdf_Property))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Container)) != (true)) % 4.24/4.41 ((tuple (iext (uri_rdf_type) (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z) (uri_ex_c)) (iext (uri_ex_p) (uri_ex_s) (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z))) != (tuple (true) (true))) % 4.24/4.41 ((iext (uri_rdfs_subPropertyOf) (uri_rdfs_isDefinedBy) (uri_rdfs_seeAlso)) = (true)) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_Restriction)) != (true)) % 4.24/4.41 (zenon_X0 != (uri_ex_p)) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_seeAlso)) != (iext (uri_rdfs_domain) (uri_rdf_predicate) (uri_rdfs_Statement))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_ex_p)) != (iext (uri_rdfs_domain) (uri_rdfs_subClassOf) (uri_rdfs_Class))) % 4.24/4.41 ((uri_ex_s) != (uri_rdfs_domain)) % 4.24/4.41 ((tuple (iext (uri_rdf_type) (uri_owl_ObjectProperty) (uri_ex_c)) (iext (uri_ex_p) (uri_ex_s) (uri_owl_ObjectProperty))) != (tuple (true) (true))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_seeAlso)) != (iext (uri_rdf_type) (uri_rdf_XMLLiteral) (uri_rdfs_Datatype))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_Restriction)) != (iext (uri_rdfs_domain) (uri_rdfs_isDefinedBy) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Resource)) != (iext (uri_rdfs_domain) (uri_rdfs_domain) (uri_rdf_Property))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Class)) != (iext (uri_rdfs_subClassOf) (uri_rdf_XMLLiteral) (uri_rdfs_Literal))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) zenon_X0) != (iext (uri_rdfs_subPropertyOf) (uri_rdfs_isDefinedBy) (uri_rdfs_seeAlso))) % 4.24/4.41 ((uri_rdfs_Literal) != (uri_ex_p)) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Resource)) != (iext (uri_rdfs_domain) (uri_rdfs_seeAlso) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_seeAlso)) != (iext (uri_rdfs_domain) (uri_rdfs_isDefinedBy) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) zenon_X0) != (iext (uri_rdfs_domain) (uri_rdf_subject) (uri_rdfs_Statement))) % 4.24/4.41 ((uri_ex_s) != (uri_rdf__2)) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Resource)) != (iext (uri_rdf_type) (uri_rdf_rest) (uri_rdf_Property))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Container)) != (iext (uri_rdf_type) (uri_rdf_first) (uri_rdf_Property))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_Restriction)) != (iext (uri_rdfs_range) (uri_rdfs_label) (uri_rdfs_Literal))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdf_Property)) != (iext (uri_rdf_type) (uri_rdf__1) (uri_rdf_Property))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Statement)) != (iext (uri_rdf_type) (uri_rdf__1) (uri_rdfs_ContainerMembershipProperty))) % 4.24/4.41 ((tuple (iext (uri_rdf_type) (uri_rdfs_Statement) (uri_ex_c)) (iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Statement))) != (tuple (true) (true))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdf_List)) != (true)) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdf_List)) != (iext (uri_rdf_type) (uri_ex_c) (uri_owl_Class))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Datatype)) != (iext (uri_rdfs_range) (uri_rdfs_comment) (uri_rdfs_Literal))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Class)) != (iext (uri_rdfs_domain) (uri_rdf_type) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Class)) != (iext (uri_rdfs_subClassOf) (uri_rdf_Bag) (uri_rdfs_Container))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) zenon_X0) != (iext (uri_rdfs_range) (uri_rdf_value) (uri_rdfs_Resource))) % 4.24/4.41 ((uri_rdfs_Resource) != (uri_ex_c)) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Class)) != (iext (uri_rdfs_domain) (uri_rdf__1) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_ObjectProperty)) != (iext (uri_rdfs_domain) (uri_rdfs_isDefinedBy) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Resource)) != (iext (uri_rdfs_domain) (uri_rdf_object) (uri_rdfs_Statement))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_ex_c)) != (iext (uri_owl_someValuesFrom) (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z) (uri_ex_c))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdf_Property)) != (iext (uri_rdfs_domain) (uri_rdfs_subPropertyOf) (uri_rdf_Property))) % 4.24/4.41 ((uri_rdfs_Literal) != (uri_rdfs_Statement)) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Datatype)) != (iext (uri_rdfs_range) (uri_rdfs_range) (uri_rdfs_Class))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_Restriction)) != (iext (uri_rdfs_range) (uri_rdf_predicate) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Statement)) != (iext (uri_rdfs_domain) (uri_rdfs_range) (uri_rdf_Property))) % 4.24/4.41 ((uri_ex_s) != (uri_rdfs_range)) % 4.24/4.41 ((iext (uri_rdf_type) (uri_rdf__3) (uri_rdf_Property)) = (true)) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Resource)) != (iext (uri_rdfs_range) (uri_rdf_value) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_ex_p)) != (iext (uri_rdf_type) (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z) (uri_owl_Restriction))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Resource)) != (iext (uri_rdf_type) (uri_rdf__1) (uri_rdf_Property))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_Class)) != (iext (uri_rdf_type) (uri_rdf__1) (uri_rdfs_ContainerMembershipProperty))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) zenon_X0) != (iext (uri_rdfs_subClassOf) (uri_rdfs_Seq) (uri_rdfs_Container))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_ContainerMembershipProperty)) != (iext (uri_rdfs_subClassOf) (uri_rdfs_Datatype) (uri_rdfs_Class))) % 4.24/4.41 ((uri_rdf_List) != (uri_rdfs_Statement)) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Statement)) != (iext (uri_rdfs_domain) (uri_rdfs_subPropertyOf) (uri_rdf_Property))) % 4.24/4.41 ((tuple (iext (uri_rdf_type) (uri_rdf_List) (uri_ex_c)) (iext (uri_ex_p) (uri_ex_s) (uri_rdf_List))) != (tuple (true) (true))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Resource)) != (iext (uri_rdfs_range) (uri_rdfs_isDefinedBy) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_Class)) != (iext (uri_rdfs_domain) (uri_rdf__3) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_rdfs_domain) (uri_rdfs_label) (uri_rdfs_Resource)) = (true)) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Datatype)) != (iext (uri_rdf_type) (uri_rdf_XMLLiteral) (uri_rdfs_Datatype))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_ContainerMembershipProperty)) != (iext (uri_rdfs_range) (uri_rdf_subject) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_ex_p)) != (iext (uri_rdf_type) (uri_rdf_rest) (uri_rdf_Property))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z)) != (iext (uri_rdf_type) (uri_rdf_subject) (uri_rdf_Property))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_Class)) != (iext (uri_rdfs_range) (uri_rdfs_subClassOf) (uri_rdfs_Class))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_ex_p)) != (iext (uri_rdfs_domain) (uri_rdf_type) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) zenon_X0) != (iext (uri_rdfs_domain) (uri_rdfs_range) (uri_rdf_Property))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_Restriction)) != (iext (uri_rdfs_subPropertyOf) (uri_rdfs_isDefinedBy) (uri_rdfs_seeAlso))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Statement)) != (iext (uri_rdfs_domain) (uri_rdf_type) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Statement)) != (iext (uri_rdf_type) (uri_rdf__2) (uri_rdfs_ContainerMembershipProperty))) % 4.24/4.41 ((iext (uri_rdfs_domain) (uri_rdf_object) (uri_rdfs_Statement)) = (true)) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_Class)) != (iext (uri_rdfs_range) (uri_rdfs_domain) (uri_rdfs_Class))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) zenon_X0) != (iext (uri_rdf_type) (uri_rdf_rest) (uri_rdf_Property))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Literal)) != (iext (uri_rdfs_domain) (uri_rdfs_seeAlso) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Datatype)) != (iext (uri_rdf_type) (uri_rdf_object) (uri_rdf_Property))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Statement)) != (iext (uri_rdfs_range) (uri_rdfs_member) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_Class)) != (iext (uri_rdf_type) (uri_rdf_Property) (uri_rdfs_Class))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_seeAlso)) != (iext (uri_rdfs_domain) (uri_rdf_object) (uri_rdfs_Statement))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdf_List)) != (iext (uri_rdfs_domain) (uri_rdf_object) (uri_rdfs_Statement))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_seeAlso)) != (iext (uri_rdfs_domain) (uri_rdf__1) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z)) != (iext (uri_rdf_type) (uri_rdf_Property) (uri_rdfs_Class))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_ContainerMembershipProperty)) != (iext (uri_rdfs_range) (uri_rdf_value) (uri_rdfs_Resource))) % 4.24/4.41 ((uri_rdf_List) != (uri_owl_ObjectProperty)) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Class)) != (iext (uri_rdfs_subClassOf) (uri_rdfs_Datatype) (uri_rdfs_Class))) % 4.24/4.41 ((uri_ex_s) != (uri_rdf_Alt)) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z)) != (iext (uri_rdfs_range) (uri_rdfs_domain) (uri_rdfs_Class))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdf_List)) != (iext (uri_rdfs_range) (uri_rdfs_seeAlso) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_ObjectProperty)) != (iext (uri_rdfs_domain) (uri_rdf_rest) (uri_rdf_List))) % 4.24/4.41 (zenon_X0 != (uri_owl_ObjectProperty)) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_Class)) != (iext (uri_rdfs_range) (uri_rdfs_isDefinedBy) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdf_Property)) != (iext (uri_rdfs_subClassOf) (uri_rdfs_ContainerMembershipProperty) (uri_rdf_Property))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Class)) != (iext (uri_rdf_type) (uri_rdf_value) (uri_rdf_Property))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_ex_c)) != (iext (uri_rdfs_subClassOf) (uri_rdfs_Datatype) (uri_rdfs_Class))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdf_List)) != (iext (uri_rdfs_domain) (uri_rdfs_label) (uri_rdfs_Resource))) % 4.24/4.41 ((uri_rdfs_seeAlso) != (uri_rdfs_Container)) % 4.24/4.41 ((uri_rdfs_Class) != (uri_owl_Class)) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_Restriction)) != (iext (uri_rdfs_range) (uri_rdf_subject) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Statement)) != (iext (uri_rdf_type) (uri_rdf__2) (uri_rdf_Property))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z)) != (iext (uri_rdf_type) (uri_rdf_value) (uri_rdf_Property))) % 4.24/4.41 ((iext (uri_rdfs_range) (uri_rdf__2) (uri_rdfs_Resource)) = (true)) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_ContainerMembershipProperty)) != (iext (uri_rdfs_range) (uri_rdfs_member) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_ex_p)) != (iext (uri_rdfs_domain) (uri_rdfs_member) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_rdfs_subClassOf) (uri_rdf_Alt) (uri_rdfs_Container)) = (true)) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) zenon_X0) != (iext (uri_rdfs_range) (uri_rdf_type) (uri_rdfs_Class))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdf_List)) != (iext (uri_rdf_type) (uri_rdf_value) (uri_rdf_Property))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdf_List)) != (iext (uri_rdfs_range) (uri_rdf__1) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_seeAlso)) != (iext (uri_rdfs_range) (uri_rdfs_comment) (uri_rdfs_Literal))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_seeAlso)) != (iext (uri_rdfs_domain) (uri_rdfs_subClassOf) (uri_rdfs_Class))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_seeAlso)) != (iext (uri_rdfs_range) (uri_rdfs_seeAlso) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_ObjectProperty)) != (iext (uri_rdfs_domain) (uri_rdf_object) (uri_rdfs_Statement))) % 4.24/4.41 ((iext (uri_rdf_type) (uri_rdf_nil) (uri_rdf_List)) = (true)) % 4.24/4.41 ((iext (uri_rdf_type) (uri_rdf_type) (uri_rdf_Property)) = (true)) % 4.24/4.41 ((tuple (iext (uri_rdf_type) (uri_rdfs_Datatype) (uri_ex_c)) (iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Datatype))) != (tuple (true) (true))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z)) != (iext (uri_rdfs_range) (uri_rdf_subject) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_ex_c)) != (iext (uri_rdfs_range) (uri_rdfs_domain) (uri_rdfs_Class))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_ex_c)) != (iext (uri_rdfs_domain) (uri_rdf_subject) (uri_rdfs_Statement))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Literal)) != (true)) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Class)) != (iext (uri_rdfs_domain) (uri_rdfs_subClassOf) (uri_rdfs_Class))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_ObjectProperty)) != (iext (uri_rdf_type) (uri_rdf__2) (uri_rdf_Property))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdf_Property)) != (iext (uri_rdfs_range) (uri_rdf_subject) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_ex_c)) != (iext (uri_rdfs_subPropertyOf) (uri_rdfs_isDefinedBy) (uri_rdfs_seeAlso))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_seeAlso)) != (iext (uri_rdfs_subPropertyOf) (uri_rdfs_isDefinedBy) (uri_rdfs_seeAlso))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_ex_p)) != (iext (uri_rdfs_range) (uri_rdf__3) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_Restriction)) != (iext (uri_rdfs_domain) (uri_rdf_first) (uri_rdf_List))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Resource)) != (iext (uri_rdfs_range) (uri_rdfs_comment) (uri_rdfs_Literal))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Datatype)) != (iext (uri_rdfs_range) (uri_rdfs_label) (uri_rdfs_Literal))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z)) != (iext (uri_rdf_type) (uri_rdf_nil) (uri_rdf_List))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_ObjectProperty)) != (iext (uri_rdfs_domain) (uri_rdfs_subPropertyOf) (uri_rdf_Property))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_ObjectProperty)) != (iext (uri_rdf_type) (uri_ex_s) (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) zenon_X0) != (iext (uri_rdfs_domain) (uri_rdfs_subPropertyOf) (uri_rdf_Property))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_ObjectProperty)) != (iext (uri_owl_onProperty) (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z) (uri_ex_p))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_Class)) != (iext (uri_rdf_type) (uri_rdf_value) (uri_rdf_Property))) % 4.24/4.41 ((uri_rdfs_Literal) != (uri_rdfs_seeAlso)) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Statement)) != (iext (uri_rdfs_subClassOf) (uri_rdfs_ContainerMembershipProperty) (uri_rdf_Property))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Statement)) != (iext (uri_rdf_type) (uri_ex_c) (uri_owl_Class))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Statement)) != (iext (uri_rdfs_range) (uri_rdf_type) (uri_rdfs_Class))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdf_List)) != (iext (uri_rdfs_domain) (uri_rdf_type) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z)) != (iext (uri_rdfs_subClassOf) (uri_rdfs_Seq) (uri_rdfs_Container))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_ex_c)) != (iext (uri_rdfs_range) (uri_rdfs_comment) (uri_rdfs_Literal))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_ex_p)) != (iext (uri_rdfs_range) (uri_rdf__1) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) zenon_X0) != (iext (uri_owl_someValuesFrom) (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z) (uri_ex_c))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Class)) != (iext (uri_rdfs_range) (uri_rdf_value) (uri_rdfs_Resource))) % 4.24/4.41 ((uri_rdfs_Class) != (uri_ex_c)) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Class)) != (iext (uri_rdfs_range) (uri_rdfs_comment) (uri_rdfs_Literal))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_ex_p)) != (iext (uri_owl_onProperty) (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z) (uri_ex_p))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Container)) != (iext (uri_owl_someValuesFrom) (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z) (uri_ex_c))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_ex_p)) != (iext (uri_rdfs_domain) (uri_rdfs_range) (uri_rdf_Property))) % 4.24/4.41 ((iext (uri_rdf_type) (uri_rdf_subject) (uri_rdf_Property)) = (true)) % 4.24/4.41 ((uri_rdf_List) != (uri_rdfs_Container)) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_Restriction)) != (iext (uri_rdfs_domain) (uri_rdfs_domain) (uri_rdf_Property))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_ex_c)) != (iext (uri_rdfs_domain) (uri_rdfs_seeAlso) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_Restriction)) != (iext (uri_rdfs_range) (uri_rdf_first) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdf_Property)) != (iext (uri_rdf_type) (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z) (uri_owl_Restriction))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdf_Property)) != (iext (uri_rdfs_domain) (uri_rdf__3) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Datatype)) != (iext (uri_rdf_type) (uri_rdf_subject) (uri_rdf_Property))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Class)) != (iext (uri_rdfs_domain) (uri_rdfs_label) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_ContainerMembershipProperty)) != (iext (uri_rdfs_range) (uri_rdfs_subPropertyOf) (uri_rdf_Property))) % 4.24/4.41 ((iext (uri_rdfs_range) (uri_rdf_predicate) (uri_rdfs_Resource)) = (true)) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z)) != (iext (uri_rdfs_domain) (uri_rdf__2) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_ex_p)) != (iext (uri_rdfs_domain) (uri_rdf_value) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Class)) != (iext (uri_rdfs_range) (uri_rdfs_member) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_Class)) != (iext (uri_rdfs_range) (uri_rdf_first) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_rdfs_range) (uri_rdf__3) (uri_rdfs_Resource)) = (true)) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdf_List)) != (iext (uri_rdfs_domain) (uri_rdf__3) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Datatype)) != (iext (uri_rdfs_range) (uri_rdfs_isDefinedBy) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Datatype)) != (iext (uri_rdfs_domain) (uri_rdfs_comment) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) zenon_X0) != (iext (uri_rdfs_domain) (uri_rdfs_seeAlso) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) zenon_X0) != (iext (uri_rdfs_subClassOf) (uri_rdfs_ContainerMembershipProperty) (uri_rdf_Property))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdf_Property)) != (iext (uri_rdfs_domain) (uri_rdf__1) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_seeAlso)) != (iext (uri_rdf_type) (uri_rdf__3) (uri_rdf_Property))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_seeAlso)) != (iext (uri_rdfs_domain) (uri_rdfs_comment) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Literal)) != (iext (uri_rdf_type) (uri_rdf_first) (uri_rdf_Property))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_Class)) != (iext (uri_rdf_type) (uri_rdf__2) (uri_rdfs_ContainerMembershipProperty))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) zenon_X0) != (iext (uri_rdf_type) (uri_rdf_value) (uri_rdf_Property))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdf_List)) != (iext (uri_rdfs_range) (uri_rdf_type) (uri_rdfs_Class))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_ex_p)) != (iext (uri_rdfs_subClassOf) (uri_rdfs_ContainerMembershipProperty) (uri_rdf_Property))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_seeAlso)) != (iext (uri_rdf_type) (uri_rdf__1) (uri_rdf_Property))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) zenon_X0) != (iext (uri_rdfs_range) (uri_rdfs_label) (uri_rdfs_Literal))) % 4.24/4.41 ((iext (uri_rdfs_range) (uri_rdfs_label) (uri_rdfs_Literal)) = (true)) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdf_Property)) != (iext (uri_rdf_type) (uri_rdf_type) (uri_rdf_Property))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Datatype)) != (iext (uri_rdfs_subClassOf) (uri_rdf_Alt) (uri_rdfs_Container))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Container)) != (iext (uri_rdfs_subClassOf) (uri_rdf_XMLLiteral) (uri_rdfs_Literal))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Datatype)) != (iext (uri_rdf_type) (uri_rdf_nil) (uri_rdf_List))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_Restriction)) != (iext (uri_rdfs_range) (uri_rdfs_seeAlso) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdf_Property)) != (iext (uri_rdfs_range) (uri_rdfs_domain) (uri_rdfs_Class))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Class)) != (iext (uri_rdfs_range) (uri_rdfs_range) (uri_rdfs_Class))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_ex_p)) != (iext (uri_rdfs_range) (uri_rdf_subject) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Literal)) != (iext (uri_rdfs_domain) (uri_rdf_object) (uri_rdfs_Statement))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Class)) != (iext (uri_rdfs_domain) (uri_rdf__3) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Resource)) != (iext (uri_rdfs_domain) (uri_rdf__1) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_seeAlso)) != (iext (uri_rdf_type) (uri_rdf_Property) (uri_rdfs_Class))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Statement)) != (iext (uri_rdf_type) (uri_rdf_value) (uri_rdf_Property))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Resource)) != (iext (uri_owl_onProperty) (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z) (uri_ex_p))) % 4.24/4.41 ((iext (uri_rdfs_domain) (uri_rdf__1) (uri_rdfs_Resource)) = (true)) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z)) != (iext (uri_rdfs_domain) (uri_rdfs_isDefinedBy) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdf_Property)) != (iext (uri_rdfs_subClassOf) (uri_rdf_XMLLiteral) (uri_rdfs_Literal))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Literal)) != (iext (uri_rdf_type) (uri_ex_p) (uri_owl_ObjectProperty))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdf_Property)) != (iext (uri_rdfs_domain) (uri_rdf_rest) (uri_rdf_List))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z)) != (iext (uri_rdfs_domain) (uri_rdf_predicate) (uri_rdfs_Statement))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_Class)) != (iext (uri_rdf_type) (uri_rdf__3) (uri_rdf_Property))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdf_Property)) != (iext (uri_rdfs_subClassOf) (uri_rdf_Alt) (uri_rdfs_Container))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Datatype)) != (iext (uri_rdfs_domain) (uri_rdfs_label) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_Restriction)) != (iext (uri_rdf_type) (uri_rdf_XMLLiteral) (uri_rdfs_Datatype))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z)) != (iext (uri_rdf_type) (uri_rdf__2) (uri_rdf_Property))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) zenon_X0) != (iext (uri_rdfs_range) (uri_rdfs_subPropertyOf) (uri_rdf_Property))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_seeAlso)) != (true)) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Container)) != (iext (uri_rdfs_domain) (uri_rdfs_subClassOf) (uri_rdfs_Class))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Statement)) != (iext (uri_rdf_type) (uri_rdf_rest) (uri_rdf_Property))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Container)) != (iext (uri_rdfs_range) (uri_rdfs_member) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_Restriction)) != (iext (uri_rdfs_range) (uri_rdfs_subClassOf) (uri_rdfs_Class))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Literal)) != (iext (uri_rdfs_subClassOf) (uri_rdf_XMLLiteral) (uri_rdfs_Literal))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_Class)) != (iext (uri_rdfs_subClassOf) (uri_rdfs_Datatype) (uri_rdfs_Class))) % 4.24/4.41 ((uri_ex_s) != (uri_rdf_nil)) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdf_List)) != (iext (uri_rdfs_domain) (uri_rdfs_domain) (uri_rdf_Property))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdf_List)) != (iext (uri_rdfs_range) (uri_rdfs_domain) (uri_rdfs_Class))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Datatype)) != (iext (uri_rdfs_domain) (uri_rdf_type) (uri_rdfs_Resource))) % 4.24/4.41 ((uri_rdfs_seeAlso) != (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z)) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Class)) != (iext (uri_rdfs_domain) (uri_rdfs_range) (uri_rdf_Property))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Resource)) != (iext (uri_rdfs_range) (uri_rdfs_domain) (uri_rdfs_Class))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Class)) != (iext (uri_rdf_type) (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z) (uri_owl_Restriction))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_ContainerMembershipProperty)) != (iext (uri_rdf_type) (uri_rdf_type) (uri_rdf_Property))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_ObjectProperty)) != (iext (uri_rdfs_subClassOf) (uri_rdf_XMLLiteral) (uri_rdfs_Literal))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Container)) != (iext (uri_rdf_type) (uri_rdf_Property) (uri_rdfs_Class))) % 4.24/4.41 ((uri_rdf_Property) != (uri_owl_ObjectProperty)) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Container)) != (iext (uri_rdfs_subClassOf) (uri_rdfs_Datatype) (uri_rdfs_Class))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Class)) != (iext (uri_rdfs_range) (uri_rdfs_seeAlso) (uri_rdfs_Resource))) % 4.24/4.41 (zenon_X0 != (uri_owl_Class)) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Literal)) != (iext (uri_rdfs_range) (uri_rdf__2) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Literal)) != (iext (uri_rdfs_subClassOf) (uri_rdfs_Datatype) (uri_rdfs_Class))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z)) != (iext (uri_rdfs_range) (uri_rdfs_subClassOf) (uri_rdfs_Class))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_Class)) != (iext (uri_rdfs_domain) (uri_rdf_first) (uri_rdf_List))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_ex_c)) != (iext (uri_rdfs_range) (uri_rdf_subject) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdf_Property)) != (true)) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_seeAlso)) != (iext (uri_rdfs_range) (uri_rdf_subject) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Class)) != (iext (uri_rdf_type) (uri_rdf__3) (uri_rdf_Property))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z)) != (iext (uri_rdf_type) (uri_rdf__1) (uri_rdf_Property))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_ContainerMembershipProperty)) != (iext (uri_rdf_type) (uri_rdf_first) (uri_rdf_Property))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_Restriction)) != (iext (uri_rdfs_range) (uri_rdf__2) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdf_Property)) != (iext (uri_rdfs_range) (uri_rdf_type) (uri_rdfs_Class))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_ObjectProperty)) != (iext (uri_rdfs_domain) (uri_rdfs_range) (uri_rdf_Property))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_Class)) != (iext (uri_rdf_type) (uri_rdf_first) (uri_rdf_Property))) % 4.24/4.41 ((iext (uri_rdfs_domain) (uri_rdfs_comment) (uri_rdfs_Resource)) = (true)) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Literal)) != (iext (uri_rdfs_subPropertyOf) (uri_rdfs_isDefinedBy) (uri_rdfs_seeAlso))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Class)) != (iext (uri_rdfs_range) (uri_rdfs_subClassOf) (uri_rdfs_Class))) % 4.24/4.41 ((iext (uri_rdfs_domain) (uri_rdfs_subPropertyOf) (uri_rdf_Property)) = (true)) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_Restriction)) != (iext (uri_rdfs_domain) (uri_rdf_type) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z)) != (iext (uri_rdfs_range) (uri_rdfs_member) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Datatype)) != (iext (uri_rdfs_domain) (uri_rdfs_isDefinedBy) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z)) != (iext (uri_rdfs_domain) (uri_rdfs_domain) (uri_rdf_Property))) % 4.24/4.41 ((uri_rdfs_Resource) != (uri_owl_Restriction)) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z)) != (iext (uri_rdfs_range) (uri_rdf_rest) (uri_rdf_List))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Datatype)) != (iext (uri_rdfs_range) (uri_rdf_type) (uri_rdfs_Class))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdf_Property)) != (iext (uri_rdf_type) (uri_rdf_XMLLiteral) (uri_rdfs_Datatype))) % 4.24/4.41 (zenon_X0 != (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z)) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_Restriction)) != (iext (uri_rdf_type) (uri_rdf__2) (uri_rdfs_ContainerMembershipProperty))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_ObjectProperty)) != (iext (uri_rdfs_range) (uri_rdf_predicate) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_rdfs_subClassOf) (uri_rdfs_Datatype) (uri_rdfs_Class)) = (true)) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Resource)) != (iext (uri_rdfs_domain) (uri_rdf_rest) (uri_rdf_List))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_ObjectProperty)) != (iext (uri_rdfs_domain) (uri_rdf_predicate) (uri_rdfs_Statement))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_ex_p)) != (iext (uri_rdfs_subClassOf) (uri_rdf_Alt) (uri_rdfs_Container))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Class)) != (iext (uri_rdfs_range) (uri_rdf__3) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Container)) != (iext (uri_rdfs_range) (uri_rdfs_domain) (uri_rdfs_Class))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_ex_c)) != (iext (uri_rdfs_range) (uri_rdfs_member) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_ex_p)) != (iext (uri_rdfs_range) (uri_rdfs_range) (uri_rdfs_Class))) % 4.24/4.41 ((iext (uri_rdf_type) (uri_rdf_object) (uri_rdf_Property)) = (true)) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z)) != (iext (uri_owl_onProperty) (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z) (uri_ex_p))) % 4.24/4.41 ((iext (uri_rdf_type) (uri_rdf__2) (uri_rdf_Property)) = (true)) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_seeAlso)) != (iext (uri_rdfs_range) (uri_rdf__3) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdf_List)) != (iext (uri_rdfs_range) (uri_rdf_predicate) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z)) != (iext (uri_owl_someValuesFrom) (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z) (uri_ex_c))) % 4.24/4.41 ((iext (uri_rdfs_domain) (uri_rdf__3) (uri_rdfs_Resource)) = (true)) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Class)) != (iext (uri_owl_someValuesFrom) (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z) (uri_ex_c))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Container)) != (iext (uri_rdfs_range) (uri_rdfs_subPropertyOf) (uri_rdf_Property))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_ex_c)) != (iext (uri_rdfs_domain) (uri_rdfs_isDefinedBy) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Resource)) != (iext (uri_rdf_type) (uri_rdf__3) (uri_rdf_Property))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_ObjectProperty)) != (iext (uri_rdf_type) (uri_ex_c) (uri_owl_Class))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_ObjectProperty)) != (iext (uri_rdfs_range) (uri_rdf_subject) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) zenon_X0) != (iext (uri_rdf_type) (uri_ex_p) (uri_owl_ObjectProperty))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Class)) != (iext (uri_rdfs_range) (uri_rdf_subject) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_rdfs_range) (uri_rdf_value) (uri_rdfs_Resource)) = (true)) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_ContainerMembershipProperty)) != (iext (uri_rdfs_domain) (uri_rdfs_label) (uri_rdfs_Resource))) % 4.24/4.41 ((uri_rdfs_Resource) != (uri_rdfs_Class)) % 4.24/4.41 ((uri_rdfs_seeAlso) != (uri_rdfs_Class)) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Class)) != (iext (uri_rdf_type) (uri_rdf_rest) (uri_rdf_Property))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_seeAlso)) != (iext (uri_rdf_type) (uri_rdf_subject) (uri_rdf_Property))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Container)) != (iext (uri_rdfs_domain) (uri_rdf_first) (uri_rdf_List))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Literal)) != (iext (uri_rdfs_range) (uri_rdf__1) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) zenon_X0) != (iext (uri_rdfs_range) (uri_rdfs_range) (uri_rdfs_Class))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_ContainerMembershipProperty)) != (iext (uri_rdfs_subClassOf) (uri_rdf_Bag) (uri_rdfs_Container))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) zenon_X0) != (iext (uri_rdf_type) (uri_rdf__3) (uri_rdf_Property))) % 4.24/4.41 ((uri_ex_s) != (uri_rdf_Property)) % 4.24/4.41 ((uri_owl_Restriction) != (uri_owl_ObjectProperty)) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) zenon_X0) != (iext (uri_rdfs_range) (uri_rdfs_member) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Literal)) != (iext (uri_rdf_type) (uri_rdf_subject) (uri_rdf_Property))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Statement)) != (iext (uri_rdf_type) (uri_ex_p) (uri_owl_ObjectProperty))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z)) != (iext (uri_rdfs_range) (uri_rdf_predicate) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_ex_p)) != (iext (uri_rdfs_subPropertyOf) (uri_rdfs_isDefinedBy) (uri_rdfs_seeAlso))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Datatype)) != (iext (uri_rdfs_domain) (uri_rdf_first) (uri_rdf_List))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_ContainerMembershipProperty)) != (iext (uri_rdf_type) (uri_rdf__2) (uri_rdf_Property))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_ObjectProperty)) != (iext (uri_rdfs_domain) (uri_rdf__2) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_ObjectProperty)) != (iext (uri_rdf_type) (uri_rdf__1) (uri_rdfs_ContainerMembershipProperty))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Literal)) != (iext (uri_rdfs_domain) (uri_rdfs_comment) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_Class)) != (iext (uri_rdf_type) (uri_ex_s) (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z))) % 4.24/4.41 ((uri_rdf_Property) != (uri_owl_Restriction)) % 4.24/4.41 ((uri_rdfs_Literal) != (uri_rdfs_Resource)) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdf_Property)) != (iext (uri_rdfs_range) (uri_rdfs_isDefinedBy) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_ContainerMembershipProperty)) != (iext (uri_rdfs_domain) (uri_rdf_object) (uri_rdfs_Statement))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Resource)) != (iext (uri_rdfs_range) (uri_rdf_type) (uri_rdfs_Class))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Datatype)) != (iext (uri_rdf_type) (uri_rdf__2) (uri_rdf_Property))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_Restriction)) != (iext (uri_rdf_type) (uri_rdf__2) (uri_rdf_Property))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Class)) != (iext (uri_rdf_type) (uri_rdf__1) (uri_rdfs_ContainerMembershipProperty))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Statement)) != (iext (uri_rdfs_range) (uri_rdfs_subPropertyOf) (uri_rdf_Property))) % 4.24/4.41 ((iext (uri_rdfs_range) (uri_rdf__1) (uri_rdfs_Resource)) = (true)) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) zenon_X0) != (iext (uri_rdfs_domain) (uri_rdf__2) (uri_rdfs_Resource))) % 4.24/4.41 ((uri_rdf_Property) != (uri_rdf_List)) % 4.24/4.41 ((uri_rdfs_Literal) != (uri_owl_Restriction)) % 4.24/4.41 ((uri_ex_s) != (uri_rdf_rest)) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_Restriction)) != (iext (uri_rdfs_subClassOf) (uri_rdf_XMLLiteral) (uri_rdfs_Literal))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_ObjectProperty)) != (iext (uri_rdfs_domain) (uri_rdfs_member) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_rdf_type) (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z) (uri_owl_Restriction)) = (true)) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Resource)) != (iext (uri_rdfs_domain) (uri_rdfs_isDefinedBy) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Container)) != (iext (uri_rdfs_subClassOf) (uri_rdfs_Seq) (uri_rdfs_Container))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Resource)) != (iext (uri_rdfs_range) (uri_rdfs_seeAlso) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_ex_c)) != (iext (uri_rdfs_range) (uri_rdf__3) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_ex_p)) != (iext (uri_rdf_type) (uri_rdf__2) (uri_rdfs_ContainerMembershipProperty))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_ex_c)) != (iext (uri_rdfs_subClassOf) (uri_rdf_Bag) (uri_rdfs_Container))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Resource)) != (iext (uri_rdfs_range) (uri_rdf__1) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdf_List)) != (iext (uri_rdfs_subClassOf) (uri_rdfs_ContainerMembershipProperty) (uri_rdf_Property))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Literal)) != (iext (uri_rdf_type) (uri_rdf_nil) (uri_rdf_List))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Class)) != (iext (uri_rdfs_range) (uri_rdf_type) (uri_rdfs_Class))) % 4.24/4.41 (zenon_X0 != (uri_rdfs_Resource)) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Container)) != (iext (uri_rdfs_domain) (uri_rdfs_comment) (uri_rdfs_Resource))) % 4.24/4.41 ((uri_owl_Restriction) != (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z)) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_Class)) != (iext (uri_rdfs_domain) (uri_rdfs_seeAlso) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Literal)) != (iext (uri_rdfs_domain) (uri_rdf__1) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_Class)) != (iext (uri_rdfs_domain) (uri_rdfs_comment) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdf_List)) != (iext (uri_rdfs_domain) (uri_rdf_rest) (uri_rdf_List))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) zenon_X0) != (iext (uri_rdfs_range) (uri_rdf__3) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdf_Property)) != (iext (uri_rdfs_subClassOf) (uri_rdf_Bag) (uri_rdfs_Container))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdf_Property)) != (iext (uri_rdfs_range) (uri_rdfs_range) (uri_rdfs_Class))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Statement)) != (iext (uri_rdfs_subClassOf) (uri_rdfs_Seq) (uri_rdfs_Container))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z)) != (iext (uri_rdfs_domain) (uri_rdfs_label) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_ex_p)) != (iext (uri_rdf_type) (uri_ex_p) (uri_owl_ObjectProperty))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_Class)) != (iext (uri_rdf_type) (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z) (uri_owl_Restriction))) % 4.24/4.41 ((iext (uri_rdf_type) (uri_rdf_rest) (uri_rdf_Property)) = (true)) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Resource)) != (iext (uri_rdf_type) (uri_rdf_nil) (uri_rdf_List))) % 4.24/4.41 ((iext (uri_owl_someValuesFrom) (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z) (uri_ex_c)) = (true)) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_ContainerMembershipProperty)) != (iext (uri_rdf_type) (uri_rdf__1) (uri_rdfs_ContainerMembershipProperty))) % 4.24/4.41 ((iext (uri_rdfs_range) (uri_rdf_first) (uri_rdfs_Resource)) = (true)) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Statement)) != (iext (uri_rdfs_range) (uri_rdf_value) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_ObjectProperty)) != (iext (uri_rdfs_domain) (uri_rdfs_comment) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z)) != (iext (uri_rdfs_domain) (uri_rdf_value) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Datatype)) != (iext (uri_rdf_type) (uri_rdf_type) (uri_rdf_Property))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Container)) != (iext (uri_rdfs_domain) (uri_rdfs_subPropertyOf) (uri_rdf_Property))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) zenon_X0) != (iext (uri_rdf_type) (uri_rdf_type) (uri_rdf_Property))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) zenon_X0) != (iext (uri_rdf_type) (uri_rdf__2) (uri_rdfs_ContainerMembershipProperty))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Class)) != (iext (uri_rdfs_range) (uri_rdfs_isDefinedBy) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) zenon_X0) != (iext (uri_rdf_type) (uri_ex_s) (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Container)) != (iext (uri_rdf_type) (uri_rdf_object) (uri_rdf_Property))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_ex_p)) != (iext (uri_rdfs_domain) (uri_rdf_object) (uri_rdfs_Statement))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Resource)) != (iext (uri_rdfs_subClassOf) (uri_rdfs_ContainerMembershipProperty) (uri_rdf_Property))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Class)) != (iext (uri_rdfs_domain) (uri_rdf_value) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Statement)) != (iext (uri_rdfs_domain) (uri_rdfs_comment) (uri_rdfs_Resource))) % 4.24/4.41 (zenon_X0 != (uri_rdfs_seeAlso)) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_ContainerMembershipProperty)) != (iext (uri_rdfs_domain) (uri_rdfs_range) (uri_rdf_Property))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_ex_c)) != (iext (uri_owl_onProperty) (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z) (uri_ex_p))) % 4.24/4.41 ((uri_rdf_List) != (uri_ex_p)) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_ContainerMembershipProperty)) != (iext (uri_rdfs_range) (uri_rdf_type) (uri_rdfs_Class))) % 4.24/4.41 ((uri_ex_s) != (uri_rdf__1)) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Container)) != (iext (uri_rdfs_domain) (uri_rdfs_label) (uri_rdfs_Resource))) % 4.24/4.41 ((uri_rdfs_Class) != (uri_owl_ObjectProperty)) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_ContainerMembershipProperty)) != (true)) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z)) != (iext (uri_rdfs_domain) (uri_rdf_subject) (uri_rdfs_Statement))) % 4.24/4.41 ((iext (uri_rdfs_range) (uri_rdf_type) (uri_rdfs_Class)) = (true)) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Resource)) != (iext (uri_rdfs_subClassOf) (uri_rdfs_Seq) (uri_rdfs_Container))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Statement)) != (iext (uri_rdfs_range) (uri_rdfs_seeAlso) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) zenon_X0) != (iext (uri_rdfs_subClassOf) (uri_rdf_XMLLiteral) (uri_rdfs_Literal))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Datatype)) != (iext (uri_rdfs_domain) (uri_rdf__3) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_seeAlso)) != (iext (uri_rdf_type) (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z) (uri_owl_Restriction))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_ContainerMembershipProperty)) != (iext (uri_rdf_type) (uri_ex_s) (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_Restriction)) != (iext (uri_rdfs_domain) (uri_rdf__3) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Container)) != (iext (uri_rdf_type) (uri_rdf_value) (uri_rdf_Property))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_ex_p)) != (iext (uri_rdfs_range) (uri_rdfs_isDefinedBy) (uri_rdfs_Resource))) % 4.24/4.41 ((uri_rdf_Property) != (uri_ex_p)) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Resource)) != (iext (uri_rdfs_range) (uri_rdfs_member) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdf_Property)) != (iext (uri_rdfs_domain) (uri_rdf_first) (uri_rdf_List))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) zenon_X0) != (iext (uri_rdf_type) (uri_rdf_XMLLiteral) (uri_rdfs_Datatype))) % 4.24/4.41 ((uri_ex_s) != (uri_rdfs_Datatype)) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdf_List)) != (iext (uri_rdfs_domain) (uri_rdfs_isDefinedBy) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdf_List)) != (iext (uri_rdfs_subClassOf) (uri_rdf_Bag) (uri_rdfs_Container))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Resource)) != (iext (uri_rdfs_domain) (uri_rdfs_label) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_ex_c)) != (iext (uri_rdf_type) (uri_rdf_XMLLiteral) (uri_rdfs_Datatype))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_ex_c)) != (iext (uri_rdf_type) (uri_ex_s) (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_ex_p)) != (iext (uri_rdf_type) (uri_rdf_object) (uri_rdf_Property))) % 4.24/4.41 ((uri_rdfs_Literal) != (uri_owl_Class)) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) zenon_X0) != (iext (uri_rdfs_domain) (uri_rdfs_member) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_ex_p)) != (iext (uri_rdfs_range) (uri_rdf_type) (uri_rdfs_Class))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Statement)) != (iext (uri_rdfs_domain) (uri_rdf__2) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z)) != (iext (uri_rdf_type) (uri_rdf__3) (uri_rdfs_ContainerMembershipProperty))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_ContainerMembershipProperty)) != (iext (uri_rdfs_domain) (uri_rdfs_subPropertyOf) (uri_rdf_Property))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_seeAlso)) != (iext (uri_rdfs_domain) (uri_rdf__3) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_ContainerMembershipProperty)) != (iext (uri_rdf_type) (uri_rdf_subject) (uri_rdf_Property))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_Class)) != (iext (uri_rdf_type) (uri_rdf_subject) (uri_rdf_Property))) % 4.24/4.41 ((iext (uri_rdfs_range) (uri_rdf_rest) (uri_rdf_List)) = (true)) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_ex_c)) != (iext (uri_rdfs_domain) (uri_rdf_rest) (uri_rdf_List))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) zenon_X0) != (iext (uri_rdfs_subClassOf) (uri_rdf_Bag) (uri_rdfs_Container))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_seeAlso)) != (iext (uri_rdf_type) (uri_rdf_object) (uri_rdf_Property))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Class)) != (iext (uri_rdfs_range) (uri_rdfs_label) (uri_rdfs_Literal))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) zenon_X0) != (iext (uri_rdfs_range) (uri_rdf_predicate) (uri_rdfs_Resource))) % 4.24/4.41 (zenon_X0 != (uri_ex_c)) % 4.24/4.41 ((uri_ex_s) != (uri_rdf__3)) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Statement)) != (iext (uri_rdfs_range) (uri_rdf_predicate) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z)) != (iext (uri_rdf_type) (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z) (uri_owl_Restriction))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_ObjectProperty)) != (iext (uri_rdfs_range) (uri_rdf__3) (uri_rdfs_Resource))) % 4.24/4.41 ((uri_ex_s) != (uri_rdfs_ContainerMembershipProperty)) % 4.24/4.41 ((uri_rdfs_Datatype) != (uri_rdfs_Container)) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_ex_p)) != (iext (uri_rdf_type) (uri_ex_s) (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_Class)) != (iext (uri_rdfs_domain) (uri_rdf_type) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) zenon_X0) != (iext (uri_rdfs_domain) (uri_rdf_type) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Class)) != (iext (uri_rdf_type) (uri_ex_c) (uri_owl_Class))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Datatype)) != (iext (uri_owl_someValuesFrom) (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z) (uri_ex_c))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Datatype)) != (iext (uri_rdfs_domain) (uri_rdfs_member) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z)) != (iext (uri_rdfs_domain) (uri_rdfs_member) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_ContainerMembershipProperty)) != (iext (uri_rdfs_domain) (uri_rdfs_member) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_ContainerMembershipProperty)) != (iext (uri_owl_onProperty) (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z) (uri_ex_p))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_ObjectProperty)) != (iext (uri_rdfs_range) (uri_rdfs_label) (uri_rdfs_Literal))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) zenon_X0) != (true)) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdf_List)) != (iext (uri_rdfs_range) (uri_rdf__3) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_seeAlso)) != (iext (uri_rdfs_range) (uri_rdfs_member) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdf_Property)) != (iext (uri_rdfs_domain) (uri_rdfs_subClassOf) (uri_rdfs_Class))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_ex_p)) != (iext (uri_rdfs_range) (uri_rdfs_comment) (uri_rdfs_Literal))) % 4.24/4.41 ((uri_ex_s) != (uri_rdf_value)) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z)) != (iext (uri_rdfs_domain) (uri_rdfs_subClassOf) (uri_rdfs_Class))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_Restriction)) != (iext (uri_owl_someValuesFrom) (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z) (uri_ex_c))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_ex_p)) != (iext (uri_rdfs_range) (uri_rdf_rest) (uri_rdf_List))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Literal)) != (iext (uri_rdf_type) (uri_rdf_object) (uri_rdf_Property))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Container)) != (iext (uri_rdfs_subClassOf) (uri_rdf_Bag) (uri_rdfs_Container))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_Restriction)) != (iext (uri_rdfs_domain) (uri_rdfs_range) (uri_rdf_Property))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) zenon_X0) != (iext (uri_rdfs_domain) (uri_rdfs_comment) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Literal)) != (iext (uri_rdfs_range) (uri_rdf_subject) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_Restriction)) != (iext (uri_rdf_type) (uri_rdf_rest) (uri_rdf_Property))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_ObjectProperty)) != (iext (uri_rdf_type) (uri_ex_p) (uri_owl_ObjectProperty))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Statement)) != (iext (uri_rdf_type) (uri_rdf__3) (uri_rdf_Property))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_Class)) != (iext (uri_rdfs_subClassOf) (uri_rdf_Bag) (uri_rdfs_Container))) % 4.24/4.41 ((iext (uri_rdfs_domain) (uri_rdf_type) (uri_rdfs_Resource)) = (true)) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Resource)) != (iext (uri_rdfs_range) (uri_rdf__2) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Class)) != (iext (uri_rdf_type) (uri_rdf_object) (uri_rdf_Property))) % 4.24/4.41 ((uri_rdf_List) != (uri_owl_Class)) % 4.24/4.41 ((uri_rdf_Property) != (uri_rdfs_Literal)) % 4.24/4.41 ((uri_rdf_Property) != (uri_owl_Class)) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Datatype)) != (iext (uri_rdfs_range) (uri_rdfs_member) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_ContainerMembershipProperty)) != (iext (uri_rdfs_range) (uri_rdf__2) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_ObjectProperty)) != (iext (uri_rdf_type) (uri_rdf_value) (uri_rdf_Property))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) zenon_X0) != (iext (uri_rdf_type) (uri_rdf__3) (uri_rdfs_ContainerMembershipProperty))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_seeAlso)) != (iext (uri_rdfs_domain) (uri_rdfs_seeAlso) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z)) != (iext (uri_rdf_type) (uri_ex_c) (uri_owl_Class))) % 4.24/4.41 ((uri_rdfs_Resource) != (uri_ex_p)) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Container)) != (iext (uri_rdf_type) (uri_rdf_nil) (uri_rdf_List))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Datatype)) != (iext (uri_rdfs_range) (uri_rdf_value) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_Restriction)) != (iext (uri_rdf_type) (uri_rdf__1) (uri_rdf_Property))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdf_Property)) != (iext (uri_rdfs_range) (uri_rdfs_subClassOf) (uri_rdfs_Class))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_ObjectProperty)) != (iext (uri_rdfs_range) (uri_rdf_first) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdf_List)) != (iext (uri_rdf_type) (uri_rdf__3) (uri_rdfs_ContainerMembershipProperty))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z)) != (iext (uri_rdfs_range) (uri_rdf_first) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Resource)) != (iext (uri_rdf_type) (uri_rdf_value) (uri_rdf_Property))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_Restriction)) != (iext (uri_rdf_type) (uri_rdf__3) (uri_rdfs_ContainerMembershipProperty))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdf_Property)) != (iext (uri_rdf_type) (uri_rdf__2) (uri_rdfs_ContainerMembershipProperty))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdf_Property)) != (iext (uri_owl_onProperty) (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z) (uri_ex_p))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Datatype)) != (iext (uri_rdfs_range) (uri_rdf_first) (uri_rdfs_Resource))) % 4.24/4.41 ((uri_owl_Restriction) != (uri_owl_Class)) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_ObjectProperty)) != (iext (uri_rdf_type) (uri_rdf_first) (uri_rdf_Property))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Literal)) != (iext (uri_rdfs_range) (uri_rdf_value) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_ContainerMembershipProperty)) != (iext (uri_rdfs_range) (uri_rdfs_subClassOf) (uri_rdfs_Class))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_ObjectProperty)) != (iext (uri_rdfs_range) (uri_rdfs_range) (uri_rdfs_Class))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Container)) != (iext (uri_rdf_type) (uri_rdf__1) (uri_rdf_Property))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_ex_p)) != (iext (uri_rdfs_subClassOf) (uri_rdfs_Datatype) (uri_rdfs_Class))) % 4.24/4.41 ((iext (uri_rdfs_range) (uri_rdfs_subPropertyOf) (uri_rdf_Property)) = (true)) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Statement)) != (iext (uri_rdf_type) (uri_rdf_type) (uri_rdf_Property))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_ObjectProperty)) != (iext (uri_rdfs_domain) (uri_rdf_type) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_ex_c)) != (iext (uri_rdfs_subClassOf) (uri_rdfs_Seq) (uri_rdfs_Container))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_ex_p)) != (iext (uri_rdfs_range) (uri_rdfs_subClassOf) (uri_rdfs_Class))) % 4.24/4.41 ((uri_ex_s) != (uri_rdfs_subClassOf)) % 4.24/4.41 ((uri_ex_s) != (uri_rdfs_member)) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_ex_p)) != (iext (uri_rdf_type) (uri_rdf_XMLLiteral) (uri_rdfs_Datatype))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Datatype)) != (iext (uri_rdf_type) (uri_rdf_first) (uri_rdf_Property))) % 4.24/4.41 ((iext (uri_rdf_type) (uri_rdf_XMLLiteral) (uri_rdfs_Datatype)) = (true)) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_Class)) != (iext (uri_rdfs_domain) (uri_rdfs_isDefinedBy) (uri_rdfs_Resource))) % 4.24/4.41 ((tuple (iext (uri_rdf_type) zenon_X0 (uri_ex_c)) (iext (uri_ex_p) (uri_ex_s) zenon_X0)) != (tuple (true) (true))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Statement)) != (iext (uri_rdf_type) (uri_rdf__3) (uri_rdfs_ContainerMembershipProperty))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdf_List)) != (iext (uri_rdfs_subClassOf) (uri_rdfs_Datatype) (uri_rdfs_Class))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_seeAlso)) != (iext (uri_rdf_type) (uri_rdf_type) (uri_rdf_Property))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_ObjectProperty)) != (iext (uri_rdfs_range) (uri_rdf_type) (uri_rdfs_Class))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Resource)) != (iext (uri_rdfs_range) (uri_rdfs_subPropertyOf) (uri_rdf_Property))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Container)) != (iext (uri_rdfs_domain) (uri_rdfs_seeAlso) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z)) != (iext (uri_rdfs_subClassOf) (uri_rdf_Bag) (uri_rdfs_Container))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Literal)) != (iext (uri_rdfs_domain) (uri_rdfs_domain) (uri_rdf_Property))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_seeAlso)) != (iext (uri_rdf_type) (uri_rdf_first) (uri_rdf_Property))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_Class)) != (iext (uri_rdfs_domain) (uri_rdfs_member) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_Restriction)) != (iext (uri_rdfs_domain) (uri_rdfs_subPropertyOf) (uri_rdf_Property))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_ObjectProperty)) != (iext (uri_rdf_type) (uri_rdf_type) (uri_rdf_Property))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_ObjectProperty)) != (iext (uri_rdf_type) (uri_rdf__2) (uri_rdfs_ContainerMembershipProperty))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Statement)) != (iext (uri_rdf_type) (uri_ex_s) (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_seeAlso)) != (iext (uri_rdfs_range) (uri_rdfs_range) (uri_rdfs_Class))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) zenon_X0) != (iext (uri_rdf_type) (uri_rdf_Property) (uri_rdfs_Class))) % 4.24/4.41 ((uri_ex_s) != (uri_rdfs_subPropertyOf)) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Container)) != (iext (uri_rdfs_domain) (uri_rdf_object) (uri_rdfs_Statement))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_seeAlso)) != (iext (uri_rdf_type) (uri_rdf__3) (uri_rdfs_ContainerMembershipProperty))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_seeAlso)) != (iext (uri_owl_onProperty) (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z) (uri_ex_p))) % 4.24/4.41 ((iext (uri_rdfs_domain) (uri_rdf_first) (uri_rdf_List)) = (true)) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) zenon_X0) != (iext (uri_rdfs_range) (uri_rdf_first) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Container)) != (iext (uri_rdfs_range) (uri_rdf_subject) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z)) != (iext (uri_rdfs_range) (uri_rdfs_subPropertyOf) (uri_rdf_Property))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_ContainerMembershipProperty)) != (iext (uri_rdfs_domain) (uri_rdf_rest) (uri_rdf_List))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_ObjectProperty)) != (iext (uri_rdfs_range) (uri_rdfs_isDefinedBy) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) zenon_X0) != (iext (uri_rdf_type) (uri_rdf_nil) (uri_rdf_List))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_ObjectProperty)) != (iext (uri_rdfs_range) (uri_rdfs_subClassOf) (uri_rdfs_Class))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_Class)) != (iext (uri_rdfs_domain) (uri_rdf_predicate) (uri_rdfs_Statement))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdf_Property)) != (iext (uri_rdf_type) (uri_rdf_value) (uri_rdf_Property))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_ex_p)) != (iext (uri_rdfs_subClassOf) (uri_rdfs_Seq) (uri_rdfs_Container))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Datatype)) != (iext (uri_rdf_type) (uri_rdf_rest) (uri_rdf_Property))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdf_Property)) != (iext (uri_rdfs_range) (uri_rdf_predicate) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Statement)) != (iext (uri_rdfs_domain) (uri_rdf__1) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_ContainerMembershipProperty)) != (iext (uri_rdfs_domain) (uri_rdf__3) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_rdfs_subClassOf) (uri_rdfs_ContainerMembershipProperty) (uri_rdf_Property)) = (true)) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Literal)) != (iext (uri_rdfs_range) (uri_rdfs_member) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_ex_c)) != (iext (uri_rdfs_range) (uri_rdf_rest) (uri_rdf_List))) % 4.24/4.41 ((tuple (iext (uri_rdf_type) (uri_rdfs_Literal) (uri_ex_c)) (iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Literal))) != (tuple (true) (true))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdf_Property)) != (iext (uri_rdf_type) (uri_rdf_nil) (uri_rdf_List))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdf_List)) != (iext (uri_rdfs_domain) (uri_rdfs_seeAlso) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Statement)) != (iext (uri_rdfs_domain) (uri_rdfs_label) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_ex_p)) != (iext (uri_rdfs_domain) (uri_rdfs_comment) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Class)) != (iext (uri_rdf_type) (uri_rdf__3) (uri_rdfs_ContainerMembershipProperty))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z)) != (iext (uri_rdfs_subClassOf) (uri_rdfs_Datatype) (uri_rdfs_Class))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Resource)) != (iext (uri_rdf_type) (uri_rdf_Property) (uri_rdfs_Class))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Datatype)) != (iext (uri_rdfs_subClassOf) (uri_rdfs_Datatype) (uri_rdfs_Class))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Class)) != (iext (uri_rdf_type) (uri_rdf__2) (uri_rdfs_ContainerMembershipProperty))) % 4.24/4.41 ((uri_rdfs_Container) != (uri_owl_Restriction)) % 4.24/4.41 ((uri_rdfs_Container) != (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z)) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_ObjectProperty)) != (iext (uri_owl_someValuesFrom) (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z) (uri_ex_c))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_ex_c)) != (iext (uri_rdfs_domain) (uri_rdfs_comment) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_Restriction)) != (iext (uri_rdfs_range) (uri_rdfs_domain) (uri_rdfs_Class))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Statement)) != (iext (uri_rdfs_range) (uri_rdfs_label) (uri_rdfs_Literal))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_ContainerMembershipProperty)) != (iext (uri_rdfs_range) (uri_rdfs_range) (uri_rdfs_Class))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdf_List)) != (iext (uri_rdf_type) (uri_rdf_XMLLiteral) (uri_rdfs_Datatype))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Container)) != (iext (uri_rdfs_domain) (uri_rdfs_member) (uri_rdfs_Resource))) % 4.24/4.41 ((uri_rdfs_Literal) != (uri_owl_ObjectProperty)) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Container)) != (iext (uri_rdfs_range) (uri_rdfs_comment) (uri_rdfs_Literal))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Resource)) != (iext (uri_rdfs_domain) (uri_rdfs_member) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Statement)) != (iext (uri_rdfs_range) (uri_rdf_rest) (uri_rdf_List))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z)) != (iext (uri_rdf_type) (uri_rdf_rest) (uri_rdf_Property))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Datatype)) != (iext (uri_rdfs_domain) (uri_rdf_subject) (uri_rdfs_Statement))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_Class)) != (iext (uri_rdf_type) (uri_rdf__2) (uri_rdf_Property))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdf_Property)) != (iext (uri_rdfs_domain) (uri_rdfs_member) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdf_List)) != (iext (uri_rdfs_subClassOf) (uri_rdf_XMLLiteral) (uri_rdfs_Literal))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Resource)) != (iext (uri_rdf_type) (uri_rdf_object) (uri_rdf_Property))) % 4.24/4.41 ((uri_owl_Restriction) != (uri_ex_p)) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdf_Property)) != (iext (uri_rdfs_range) (uri_rdf__1) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Class)) != (iext (uri_rdfs_domain) (uri_rdfs_comment) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Statement)) != (iext (uri_owl_someValuesFrom) (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z) (uri_ex_c))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_ex_p)) != (iext (uri_rdfs_domain) (uri_rdf__3) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) zenon_X0) != (iext (uri_rdfs_subClassOf) (uri_rdf_Alt) (uri_rdfs_Container))) % 4.24/4.41 ((uri_owl_Restriction) != (uri_ex_c)) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_ContainerMembershipProperty)) != (iext (uri_rdfs_range) (uri_rdfs_seeAlso) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_Class)) != (iext (uri_rdfs_range) (uri_rdfs_subPropertyOf) (uri_rdf_Property))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_ObjectProperty)) != (iext (uri_rdf_type) (uri_rdf__1) (uri_rdf_Property))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Resource)) != (iext (uri_rdfs_domain) (uri_rdfs_subPropertyOf) (uri_rdf_Property))) % 4.24/4.41 ((uri_rdfs_Statement) != (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z)) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_ex_c)) != (iext (uri_rdfs_range) (uri_rdf__1) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Datatype)) != (iext (uri_rdfs_domain) (uri_rdfs_seeAlso) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Datatype)) != (iext (uri_rdfs_domain) (uri_rdf_value) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_ex_p)) != (iext (uri_rdf_type) (uri_rdf_first) (uri_rdf_Property))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_ObjectProperty)) != (iext (uri_rdfs_domain) (uri_rdfs_seeAlso) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_ex_c)) != (iext (uri_rdfs_domain) (uri_rdf_value) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_Class)) != (iext (uri_rdfs_subClassOf) (uri_rdf_Alt) (uri_rdfs_Container))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_Class)) != (true)) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Resource)) != (iext (uri_rdfs_range) (uri_rdf_subject) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_Class)) != (iext (uri_rdfs_range) (uri_rdf_subject) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_rdfs_domain) (uri_rdf__2) (uri_rdfs_Resource)) = (true)) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_ex_c)) != (iext (uri_rdfs_range) (uri_rdfs_range) (uri_rdfs_Class))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_ObjectProperty)) != (iext (uri_rdfs_domain) (uri_rdf_subject) (uri_rdfs_Statement))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_ContainerMembershipProperty)) != (iext (uri_rdf_type) (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z) (uri_owl_Restriction))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_ex_c)) != (iext (uri_rdfs_range) (uri_rdf_predicate) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdf_Property)) != (iext (uri_rdfs_range) (uri_rdfs_seeAlso) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Class)) != (iext (uri_rdf_type) (uri_rdf_Property) (uri_rdfs_Class))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_Restriction)) != (iext (uri_rdfs_domain) (uri_rdf_rest) (uri_rdf_List))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_Restriction)) != (iext (uri_rdf_type) (uri_rdf_object) (uri_rdf_Property))) % 4.24/4.41 ((uri_rdf_List) != (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z)) % 4.24/4.41 ((iext (uri_rdf_type) (uri_rdf__3) (uri_rdfs_ContainerMembershipProperty)) = (true)) % 4.24/4.41 ((uri_rdfs_Datatype) != (uri_ex_c)) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_ex_p)) != (iext (uri_rdf_type) (uri_rdf__1) (uri_rdf_Property))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Literal)) != (iext (uri_rdfs_subClassOf) (uri_rdfs_Seq) (uri_rdfs_Container))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Resource)) != (iext (uri_rdfs_domain) (uri_rdf_value) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdf_Property)) != (iext (uri_rdfs_subClassOf) (uri_rdfs_Datatype) (uri_rdfs_Class))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_ex_p)) != (iext (uri_rdf_type) (uri_rdf__3) (uri_rdf_Property))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) zenon_X0) != (iext (uri_rdf_type) (uri_rdf__2) (uri_rdf_Property))) % 4.24/4.41 ((iext (uri_rdfs_domain) (uri_rdfs_seeAlso) (uri_rdfs_Resource)) = (true)) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Datatype)) != (iext (uri_rdfs_subClassOf) (uri_rdfs_Seq) (uri_rdfs_Container))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Literal)) != (iext (uri_rdfs_domain) (uri_rdfs_label) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_ContainerMembershipProperty)) != (iext (uri_rdf_type) (uri_rdf_value) (uri_rdf_Property))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Container)) != (iext (uri_rdfs_domain) (uri_rdf__2) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z)) != (iext (uri_rdfs_range) (uri_rdfs_range) (uri_rdfs_Class))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_ex_c)) != (iext (uri_rdfs_range) (uri_rdf__2) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Statement)) != (iext (uri_rdfs_domain) (uri_rdfs_member) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdf_List)) != (iext (uri_rdfs_domain) (uri_rdfs_subClassOf) (uri_rdfs_Class))) % 4.24/4.41 ((uri_rdfs_Resource) != (uri_owl_ObjectProperty)) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Container)) != (iext (uri_rdf_type) (uri_rdf_rest) (uri_rdf_Property))) % 4.24/4.41 ((uri_rdfs_Container) != (uri_owl_ObjectProperty)) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Literal)) != (iext (uri_rdfs_range) (uri_rdf_first) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Resource)) != (iext (uri_rdfs_domain) (uri_rdfs_subClassOf) (uri_rdfs_Class))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdf_Property)) != (iext (uri_rdfs_domain) (uri_rdfs_label) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Literal)) != (iext (uri_rdf_type) (uri_rdf__2) (uri_rdfs_ContainerMembershipProperty))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z)) != (iext (uri_rdfs_domain) (uri_rdfs_comment) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_ObjectProperty)) != (iext (uri_rdfs_range) (uri_rdf_value) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Resource)) != (iext (uri_rdfs_range) (uri_rdf_predicate) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdf_List)) != (iext (uri_rdfs_range) (uri_rdfs_subClassOf) (uri_rdfs_Class))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdf_List)) != (iext (uri_rdfs_range) (uri_rdfs_subPropertyOf) (uri_rdf_Property))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_ex_p)) != (iext (uri_rdfs_subClassOf) (uri_rdf_XMLLiteral) (uri_rdfs_Literal))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdf_Property)) != (iext (uri_rdfs_range) (uri_rdf_first) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Datatype)) != (iext (uri_rdfs_subClassOf) (uri_rdfs_ContainerMembershipProperty) (uri_rdf_Property))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_ObjectProperty)) != (iext (uri_rdfs_subPropertyOf) (uri_rdfs_isDefinedBy) (uri_rdfs_seeAlso))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) zenon_X0) != (iext (uri_rdfs_domain) (uri_rdfs_domain) (uri_rdf_Property))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdf_Property)) != (iext (uri_rdf_type) (uri_rdf__3) (uri_rdf_Property))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_seeAlso)) != (iext (uri_rdfs_domain) (uri_rdfs_domain) (uri_rdf_Property))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_ContainerMembershipProperty)) != (iext (uri_rdf_type) (uri_rdf__3) (uri_rdfs_ContainerMembershipProperty))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_ObjectProperty)) != (iext (uri_rdf_type) (uri_rdf_object) (uri_rdf_Property))) % 4.24/4.41 ((iext (uri_rdfs_range) (uri_rdfs_isDefinedBy) (uri_rdfs_Resource)) = (true)) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Literal)) != (iext (uri_rdf_type) (uri_ex_c) (uri_owl_Class))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_Class)) != (iext (uri_rdfs_range) (uri_rdf__3) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdf_Property)) != (iext (uri_rdfs_domain) (uri_rdf_object) (uri_rdfs_Statement))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Statement)) != (iext (uri_rdfs_range) (uri_rdfs_domain) (uri_rdfs_Class))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_ex_c)) != (iext (uri_rdf_type) (uri_rdf__3) (uri_rdfs_ContainerMembershipProperty))) % 4.24/4.41 ((uri_rdf_Property) != (uri_rdfs_Datatype)) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z)) != (iext (uri_rdfs_domain) (uri_rdf__1) (uri_rdfs_Resource))) % 4.24/4.41 (zenon_X0 != (uri_owl_Restriction)) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdf_Property)) != (iext (uri_rdfs_range) (uri_rdf__3) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Datatype)) != (iext (uri_rdf_type) (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z) (uri_owl_Restriction))) % 4.24/4.41 ((uri_rdfs_Class) != (uri_ex_p)) % 4.24/4.41 ((uri_ex_p) != (uri_rdf_type)) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_ex_p)) != (iext (uri_rdf_type) (uri_rdf_Property) (uri_rdfs_Class))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_Class)) != (iext (uri_rdf_type) (uri_rdf_rest) (uri_rdf_Property))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Literal)) != (iext (uri_rdf_type) (uri_rdf_type) (uri_rdf_Property))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_Restriction)) != (iext (uri_rdfs_range) (uri_rdf_rest) (uri_rdf_List))) % 4.24/4.41 ((iext (uri_rdf_type) (uri_rdf__1) (uri_rdf_Property)) = (true)) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_ContainerMembershipProperty)) != (iext (uri_owl_someValuesFrom) (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z) (uri_ex_c))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Literal)) != (iext (uri_rdfs_range) (uri_rdf_rest) (uri_rdf_List))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_seeAlso)) != (iext (uri_rdfs_subClassOf) (uri_rdf_Alt) (uri_rdfs_Container))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Class)) != (iext (uri_rdf_type) (uri_rdf__2) (uri_rdf_Property))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_seeAlso)) != (iext (uri_rdfs_subClassOf) (uri_rdfs_Datatype) (uri_rdfs_Class))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Container)) != (iext (uri_rdfs_range) (uri_rdf_predicate) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Class)) != (iext (uri_rdfs_range) (uri_rdf__2) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_ObjectProperty)) != (iext (uri_rdfs_domain) (uri_rdfs_subClassOf) (uri_rdfs_Class))) % 4.24/4.41 ((iext (uri_rdfs_domain) (uri_rdfs_range) (uri_rdf_Property)) = (true)) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_ex_p)) != (iext (uri_rdfs_domain) (uri_rdfs_domain) (uri_rdf_Property))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_ex_p)) != (iext (uri_rdfs_domain) (uri_rdf_subject) (uri_rdfs_Statement))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Resource)) != (iext (uri_rdf_type) (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z) (uri_owl_Restriction))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Resource)) != (iext (uri_rdfs_subClassOf) (uri_rdf_XMLLiteral) (uri_rdfs_Literal))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_ObjectProperty)) != (iext (uri_rdfs_range) (uri_rdfs_seeAlso) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdf_List)) != (iext (uri_rdf_type) (uri_rdf_first) (uri_rdf_Property))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) zenon_X0) != (iext (uri_rdfs_range) (uri_rdfs_seeAlso) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_ex_c)) != (iext (uri_rdf_type) (uri_rdf_object) (uri_rdf_Property))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Statement)) != (iext (uri_rdfs_domain) (uri_rdf_predicate) (uri_rdfs_Statement))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Resource)) != (iext (uri_rdfs_range) (uri_rdf__3) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_rdfs_domain) (uri_rdfs_domain) (uri_rdf_Property)) = (true)) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_Restriction)) != (iext (uri_rdfs_subClassOf) (uri_rdf_Bag) (uri_rdfs_Container))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Container)) != (iext (uri_rdf_type) (uri_rdf__3) (uri_rdfs_ContainerMembershipProperty))) % 4.24/4.41 ((iext (uri_rdf_type) (uri_ex_c) (uri_owl_Class)) = (true)) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Container)) != (iext (uri_rdfs_domain) (uri_rdf_type) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_Class)) != (iext (uri_rdf_type) (uri_rdf_nil) (uri_rdf_List))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_Class)) != (iext (uri_rdfs_domain) (uri_rdf_subject) (uri_rdfs_Statement))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Statement)) != (true)) % 4.24/4.41 ((uri_rdfs_Datatype) != (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z)) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Statement)) != (iext (uri_rdf_type) (uri_rdf_subject) (uri_rdf_Property))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Resource)) != (iext (uri_rdfs_range) (uri_rdfs_label) (uri_rdfs_Literal))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdf_Property)) != (iext (uri_rdfs_domain) (uri_rdf_predicate) (uri_rdfs_Statement))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Class)) != (iext (uri_rdfs_range) (uri_rdf__1) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_rdfs_range) (uri_rdfs_comment) (uri_rdfs_Literal)) = (true)) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_ContainerMembershipProperty)) != (iext (uri_rdfs_range) (uri_rdfs_comment) (uri_rdfs_Literal))) % 4.24/4.41 ((iext (uri_rdfs_domain) (uri_rdfs_isDefinedBy) (uri_rdfs_Resource)) = (true)) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Datatype)) != (iext (uri_rdfs_domain) (uri_rdfs_range) (uri_rdf_Property))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_Restriction)) != (iext (uri_rdfs_domain) (uri_rdf__1) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_ex_c)) != (iext (uri_rdfs_range) (uri_rdf_first) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_ObjectProperty)) != (iext (uri_rdfs_domain) (uri_rdf_first) (uri_rdf_List))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdf_List)) != (iext (uri_rdfs_range) (uri_rdf_rest) (uri_rdf_List))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdf_List)) != (iext (uri_rdfs_domain) (uri_rdf_subject) (uri_rdfs_Statement))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Class)) != (iext (uri_rdfs_domain) (uri_rdf_object) (uri_rdfs_Statement))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_Restriction)) != (iext (uri_rdfs_range) (uri_rdf__3) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_ex_c)) != (iext (uri_rdfs_domain) (uri_rdf_object) (uri_rdfs_Statement))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdf_Property)) != (iext (uri_rdf_type) (uri_rdf_first) (uri_rdf_Property))) % 4.24/4.41 ((uri_rdf_List) != (uri_owl_Restriction)) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Datatype)) != (iext (uri_rdfs_range) (uri_rdf_rest) (uri_rdf_List))) % 4.24/4.41 ((uri_ex_s) != (uri_rdfs_Seq)) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Statement)) != (iext (uri_rdfs_range) (uri_rdfs_range) (uri_rdfs_Class))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_Class)) != (iext (uri_rdfs_domain) (uri_rdfs_subClassOf) (uri_rdfs_Class))) % 4.24/4.41 ((uri_rdfs_Class) != (uri_rdfs_Container)) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Class)) != (iext (uri_rdfs_range) (uri_rdfs_subPropertyOf) (uri_rdf_Property))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_seeAlso)) != (iext (uri_rdf_type) (uri_rdf_nil) (uri_rdf_List))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_seeAlso)) != (iext (uri_rdfs_range) (uri_rdfs_domain) (uri_rdfs_Class))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdf_Property)) != (iext (uri_rdfs_domain) (uri_rdf_type) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_ex_p)) != (iext (uri_rdfs_range) (uri_rdf_first) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_ex_p)) != (iext (uri_rdfs_domain) (uri_rdf_predicate) (uri_rdfs_Statement))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_ex_p)) != (iext (uri_rdfs_range) (uri_rdf__2) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_rdf_type) (uri_rdf_first) (uri_rdf_Property)) = (true)) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z)) != (iext (uri_rdfs_domain) (uri_rdfs_subPropertyOf) (uri_rdf_Property))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Datatype)) != (iext (uri_rdfs_range) (uri_rdfs_seeAlso) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z)) != (iext (uri_rdfs_subClassOf) (uri_rdfs_ContainerMembershipProperty) (uri_rdf_Property))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Container)) != (iext (uri_rdfs_range) (uri_rdf_value) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdf_List)) != (iext (uri_rdfs_domain) (uri_rdf_first) (uri_rdf_List))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdf_List)) != (iext (uri_rdf_type) (uri_ex_p) (uri_owl_ObjectProperty))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdf_List)) != (iext (uri_rdf_type) (uri_rdf__2) (uri_rdf_Property))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Resource)) != (iext (uri_rdf_type) (uri_ex_c) (uri_owl_Class))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Literal)) != (iext (uri_rdfs_range) (uri_rdfs_label) (uri_rdfs_Literal))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdf_List)) != (iext (uri_rdfs_subClassOf) (uri_rdfs_Seq) (uri_rdfs_Container))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Resource)) != (iext (uri_rdf_type) (uri_ex_s) (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_Restriction)) != (iext (uri_rdfs_domain) (uri_rdfs_label) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Class)) != (iext (uri_rdf_type) (uri_rdf_XMLLiteral) (uri_rdfs_Datatype))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Class)) != (iext (uri_rdfs_domain) (uri_rdf_subject) (uri_rdfs_Statement))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_ContainerMembershipProperty)) != (iext (uri_rdfs_range) (uri_rdfs_isDefinedBy) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) zenon_X0) != (iext (uri_rdfs_range) (uri_rdf__1) (uri_rdfs_Resource))) % 4.24/4.41 ((uri_rdfs_Class) != (uri_owl_Restriction)) % 4.24/4.41 ((iext (uri_rdfs_domain) (uri_rdfs_subClassOf) (uri_rdfs_Class)) = (true)) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Container)) != (iext (uri_rdfs_subPropertyOf) (uri_rdfs_isDefinedBy) (uri_rdfs_seeAlso))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_ContainerMembershipProperty)) != (iext (uri_rdf_type) (uri_rdf__2) (uri_rdfs_ContainerMembershipProperty))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_ObjectProperty)) != (iext (uri_rdf_type) (uri_rdf__3) (uri_rdf_Property))) % 4.24/4.41 ((uri_rdfs_Container) != (uri_ex_c)) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_Class)) != (iext (uri_rdfs_domain) (uri_rdfs_range) (uri_rdf_Property))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdf_List)) != (iext (uri_rdfs_domain) (uri_rdf_predicate) (uri_rdfs_Statement))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_ex_c)) != (iext (uri_rdfs_domain) (uri_rdfs_subPropertyOf) (uri_rdf_Property))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_ex_p)) != (iext (uri_rdfs_domain) (uri_rdfs_seeAlso) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Class)) != (iext (uri_rdfs_subClassOf) (uri_rdfs_ContainerMembershipProperty) (uri_rdf_Property))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_ex_c)) != (iext (uri_rdfs_range) (uri_rdfs_seeAlso) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) zenon_X0) != (iext (uri_rdfs_domain) (uri_rdf_rest) (uri_rdf_List))) % 4.24/4.41 ((tuple (iext (uri_rdf_type) (uri_rdfs_ContainerMembershipProperty) (uri_ex_c)) (iext (uri_ex_p) (uri_ex_s) (uri_rdfs_ContainerMembershipProperty))) != (tuple (true) (true))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdf_List)) != (iext (uri_rdfs_range) (uri_rdfs_range) (uri_rdfs_Class))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Container)) != (iext (uri_owl_onProperty) (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z) (uri_ex_p))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Class)) != (iext (uri_rdf_type) (uri_rdf__1) (uri_rdf_Property))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_Restriction)) != (iext (uri_rdfs_subClassOf) (uri_rdfs_ContainerMembershipProperty) (uri_rdf_Property))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Datatype)) != (iext (uri_rdf_type) (uri_rdf__1) (uri_rdf_Property))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_Class)) != (iext (uri_rdf_type) (uri_rdf_XMLLiteral) (uri_rdfs_Datatype))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z)) != (iext (uri_rdf_type) (uri_rdf_XMLLiteral) (uri_rdfs_Datatype))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_ObjectProperty)) != (iext (uri_rdfs_range) (uri_rdfs_comment) (uri_rdfs_Literal))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Literal)) != (iext (uri_rdfs_range) (uri_rdfs_range) (uri_rdfs_Class))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_ex_p)) != (iext (uri_rdfs_domain) (uri_rdf__1) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Resource)) != (iext (uri_rdf_type) (uri_rdf_first) (uri_rdf_Property))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_ex_p)) != (iext (uri_rdf_type) (uri_rdf__2) (uri_rdf_Property))) % 4.24/4.41 (zenon_X0 != (uri_rdf_Property)) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_seeAlso)) != (iext (uri_rdfs_domain) (uri_rdf_subject) (uri_rdfs_Statement))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_ContainerMembershipProperty)) != (iext (uri_rdfs_subClassOf) (uri_rdf_XMLLiteral) (uri_rdfs_Literal))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_Class)) != (iext (uri_rdfs_subClassOf) (uri_rdf_XMLLiteral) (uri_rdfs_Literal))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Literal)) != (iext (uri_rdfs_range) (uri_rdfs_domain) (uri_rdfs_Class))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Resource)) != (iext (uri_rdfs_subPropertyOf) (uri_rdfs_isDefinedBy) (uri_rdfs_seeAlso))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Resource)) != (iext (uri_rdfs_range) (uri_rdf_rest) (uri_rdf_List))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_ex_c)) != (iext (uri_rdf_type) (uri_ex_c) (uri_owl_Class))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_seeAlso)) != (iext (uri_rdfs_range) (uri_rdf_predicate) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_ContainerMembershipProperty)) != (iext (uri_rdfs_domain) (uri_rdf_first) (uri_rdf_List))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_ex_p)) != (iext (uri_rdfs_range) (uri_rdfs_member) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Datatype)) != (iext (uri_rdfs_domain) (uri_rdf__2) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_Class)) != (iext (uri_rdfs_range) (uri_rdf_rest) (uri_rdf_List))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z)) != (iext (uri_rdf_type) (uri_rdf__3) (uri_rdf_Property))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_ex_p)) != (iext (uri_rdf_type) (uri_rdf_nil) (uri_rdf_List))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Resource)) != (iext (uri_rdf_type) (uri_rdf__2) (uri_rdf_Property))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Datatype)) != (iext (uri_rdfs_subPropertyOf) (uri_rdfs_isDefinedBy) (uri_rdfs_seeAlso))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_seeAlso)) != (iext (uri_rdf_type) (uri_ex_p) (uri_owl_ObjectProperty))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdf_Property)) != (iext (uri_rdfs_domain) (uri_rdfs_domain) (uri_rdf_Property))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Statement)) != (iext (uri_rdfs_subClassOf) (uri_rdf_Alt) (uri_rdfs_Container))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_Class)) != (iext (uri_rdfs_domain) (uri_rdf__2) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Literal)) != (iext (uri_rdfs_range) (uri_rdfs_seeAlso) (uri_rdfs_Resource))) % 4.24/4.41 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Class)) != (iext (uri_rdfs_domain) (uri_rdf_first) (uri_rdf_List))) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_Restriction)) != (iext (uri_rdf_type) (uri_rdf__1) (uri_rdfs_ContainerMembershipProperty))) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Statement)) != (iext (uri_rdf_type) (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z) (uri_owl_Restriction))) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Resource)) != (iext (uri_rdfs_domain) (uri_rdf_predicate) (uri_rdfs_Statement))) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Datatype)) != (iext (uri_rdfs_domain) (uri_rdfs_domain) (uri_rdf_Property))) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_seeAlso)) != (iext (uri_rdf_type) (uri_rdf__2) (uri_rdf_Property))) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (uri_ex_c)) != (iext (uri_rdfs_subClassOf) (uri_rdfs_ContainerMembershipProperty) (uri_rdf_Property))) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (uri_rdf_List)) != (iext (uri_rdfs_domain) (uri_rdfs_member) (uri_rdfs_Resource))) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z)) != (iext (uri_rdfs_subClassOf) (uri_rdf_XMLLiteral) (uri_rdfs_Literal))) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (uri_ex_p)) != (iext (uri_rdfs_domain) (uri_rdf__2) (uri_rdfs_Resource))) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Literal)) != (iext (uri_rdfs_domain) (uri_rdf_predicate) (uri_rdfs_Statement))) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Datatype)) != (iext (uri_rdf_type) (uri_rdf_value) (uri_rdf_Property))) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Container)) != (iext (uri_rdf_type) (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z) (uri_owl_Restriction))) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Literal)) != (iext (uri_rdf_type) (uri_rdf_rest) (uri_rdf_Property))) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_Class)) != (iext (uri_rdf_type) (uri_ex_p) (uri_owl_ObjectProperty))) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (uri_ex_c)) != (iext (uri_rdf_type) (uri_rdf_rest) (uri_rdf_Property))) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Literal)) != (iext (uri_rdf_type) (uri_rdf__3) (uri_rdf_Property))) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (uri_ex_p)) != (iext (uri_rdf_type) (uri_rdf__1) (uri_rdfs_ContainerMembershipProperty))) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Resource)) != (iext (uri_rdfs_domain) (uri_rdfs_range) (uri_rdf_Property))) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_seeAlso)) != (iext (uri_rdfs_domain) (uri_rdfs_range) (uri_rdf_Property))) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Container)) != (iext (uri_rdfs_range) (uri_rdfs_seeAlso) (uri_rdfs_Resource))) % 4.26/4.42 ((tuple (iext (uri_rdf_type) (uri_rdfs_seeAlso) (uri_ex_c)) (iext (uri_ex_p) (uri_ex_s) (uri_rdfs_seeAlso))) != (tuple (true) (true))) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Container)) != (iext (uri_rdfs_range) (uri_rdfs_isDefinedBy) (uri_rdfs_Resource))) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (uri_rdf_Property)) != (iext (uri_rdfs_domain) (uri_rdf_value) (uri_rdfs_Resource))) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_Restriction)) != (iext (uri_rdfs_range) (uri_rdfs_range) (uri_rdfs_Class))) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) zenon_X0) != (iext (uri_rdfs_range) (uri_rdf__2) (uri_rdfs_Resource))) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Resource)) != (iext (uri_rdf_type) (uri_rdf_subject) (uri_rdf_Property))) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Datatype)) != (iext (uri_rdfs_range) (uri_rdfs_subPropertyOf) (uri_rdf_Property))) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_Restriction)) != (iext (uri_rdf_type) (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z) (uri_owl_Restriction))) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Class)) != (iext (uri_rdfs_domain) (uri_rdf_rest) (uri_rdf_List))) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Container)) != (iext (uri_rdfs_domain) (uri_rdf_subject) (uri_rdfs_Statement))) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) zenon_X0) != (iext (uri_rdf_type) (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z) (uri_owl_Restriction))) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_ObjectProperty)) != (iext (uri_rdfs_domain) (uri_rdf__3) (uri_rdfs_Resource))) % 4.26/4.42 ((iext (uri_rdfs_range) (uri_rdfs_member) (uri_rdfs_Resource)) = (true)) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (uri_rdf_List)) != (iext (uri_rdfs_range) (uri_rdf_subject) (uri_rdfs_Resource))) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Literal)) != (iext (uri_rdfs_domain) (uri_rdfs_range) (uri_rdf_Property))) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_seeAlso)) != (iext (uri_rdfs_subClassOf) (uri_rdfs_ContainerMembershipProperty) (uri_rdf_Property))) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z)) != (iext (uri_rdfs_subClassOf) (uri_rdf_Alt) (uri_rdfs_Container))) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (uri_ex_c)) != (iext (uri_rdf_type) (uri_rdf__3) (uri_rdf_Property))) % 4.26/4.42 ((iext (uri_rdfs_range) (uri_rdfs_seeAlso) (uri_rdfs_Resource)) = (true)) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (uri_rdf_List)) != (iext (uri_rdf_type) (uri_rdf__2) (uri_rdfs_ContainerMembershipProperty))) % 4.26/4.42 ((uri_ex_s) != (uri_rdfs_label)) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Container)) != (iext (uri_rdfs_range) (uri_rdf_first) (uri_rdfs_Resource))) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_Restriction)) != (iext (uri_rdfs_domain) (uri_rdfs_comment) (uri_rdfs_Resource))) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (uri_ex_c)) != (iext (uri_rdf_type) (uri_rdf_subject) (uri_rdf_Property))) % 4.26/4.42 ((iext (uri_rdf_type) (uri_rdf_Property) (uri_rdfs_Class)) = (true)) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Container)) != (iext (uri_rdfs_domain) (uri_rdfs_isDefinedBy) (uri_rdfs_Resource))) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z)) != (true)) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (uri_rdf_Property)) != (iext (uri_rdfs_domain) (uri_rdfs_isDefinedBy) (uri_rdfs_Resource))) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z)) != (iext (uri_rdf_type) (uri_ex_s) (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z))) % 4.26/4.42 ((uri_rdfs_Container) != (uri_owl_Class)) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_ContainerMembershipProperty)) != (iext (uri_rdfs_range) (uri_rdf_first) (uri_rdfs_Resource))) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_ObjectProperty)) != (iext (uri_rdf_type) (uri_rdf__3) (uri_rdfs_ContainerMembershipProperty))) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Literal)) != (iext (uri_rdfs_range) (uri_rdfs_subClassOf) (uri_rdfs_Class))) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Statement)) != (iext (uri_rdfs_domain) (uri_rdf_object) (uri_rdfs_Statement))) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z)) != (iext (uri_rdf_type) (uri_rdf_type) (uri_rdf_Property))) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (uri_rdf_List)) != (iext (uri_rdfs_range) (uri_rdf_value) (uri_rdfs_Resource))) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Literal)) != (iext (uri_rdfs_subClassOf) (uri_rdf_Bag) (uri_rdfs_Container))) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (uri_ex_c)) != (iext (uri_rdf_type) (uri_rdf__1) (uri_rdf_Property))) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Statement)) != (iext (uri_rdfs_subClassOf) (uri_rdfs_Datatype) (uri_rdfs_Class))) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_ObjectProperty)) != (iext (uri_rdfs_domain) (uri_rdfs_label) (uri_rdfs_Resource))) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_seeAlso)) != (iext (uri_rdfs_range) (uri_rdf_rest) (uri_rdf_List))) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Statement)) != (iext (uri_rdfs_range) (uri_rdfs_isDefinedBy) (uri_rdfs_Resource))) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Literal)) != (iext (uri_rdfs_range) (uri_rdf__3) (uri_rdfs_Resource))) % 4.26/4.42 ((iext (uri_rdfs_range) (uri_rdfs_domain) (uri_rdfs_Class)) = (true)) % 4.26/4.42 (zenon_X0 != (uri_rdfs_Class)) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (uri_rdf_List)) != (iext (uri_rdf_type) (uri_rdf_rest) (uri_rdf_Property))) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z)) != (iext (uri_rdf_type) (uri_rdf_first) (uri_rdf_Property))) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) zenon_X0) != (iext (uri_rdfs_domain) (uri_rdf_object) (uri_rdfs_Statement))) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Datatype)) != (iext (uri_rdfs_domain) (uri_rdf_object) (uri_rdfs_Statement))) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (uri_ex_c)) != (iext (uri_rdf_type) (uri_rdf_type) (uri_rdf_Property))) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) zenon_X0) != (iext (uri_rdfs_range) (uri_rdf_subject) (uri_rdfs_Resource))) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_seeAlso)) != (iext (uri_rdfs_range) (uri_rdf_first) (uri_rdfs_Resource))) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Statement)) != (iext (uri_rdfs_domain) (uri_rdf_first) (uri_rdf_List))) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_seeAlso)) != (iext (uri_rdfs_range) (uri_rdfs_label) (uri_rdfs_Literal))) % 4.26/4.42 ((uri_rdfs_Datatype) != (uri_owl_Restriction)) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Container)) != (iext (uri_rdfs_range) (uri_rdf_type) (uri_rdfs_Class))) % 4.26/4.42 ((iext (uri_rdf_type) (uri_rdf__1) (uri_rdfs_ContainerMembershipProperty)) = (true)) % 4.26/4.42 ((uri_ex_s) != (uri_rdf_subject)) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_seeAlso)) != (iext (uri_rdfs_range) (uri_rdfs_isDefinedBy) (uri_rdfs_Resource))) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_seeAlso)) != (iext (uri_rdfs_domain) (uri_rdfs_subPropertyOf) (uri_rdf_Property))) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_Class)) != (iext (uri_rdfs_range) (uri_rdf_type) (uri_rdfs_Class))) % 4.26/4.42 ((uri_rdfs_seeAlso) != (uri_owl_ObjectProperty)) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Resource)) != (iext (uri_rdfs_domain) (uri_rdf_first) (uri_rdf_List))) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Resource)) != (iext (uri_rdfs_domain) (uri_rdf_type) (uri_rdfs_Resource))) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z)) != (iext (uri_rdfs_domain) (uri_rdfs_seeAlso) (uri_rdfs_Resource))) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (uri_ex_c)) != (iext (uri_rdfs_range) (uri_rdfs_isDefinedBy) (uri_rdfs_Resource))) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Statement)) != (iext (uri_rdfs_range) (uri_rdfs_subClassOf) (uri_rdfs_Class))) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (uri_ex_p)) != (iext (uri_rdfs_range) (uri_rdfs_subPropertyOf) (uri_rdf_Property))) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Resource)) != (iext (uri_rdfs_subClassOf) (uri_rdf_Bag) (uri_rdfs_Container))) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Container)) != (iext (uri_rdfs_domain) (uri_rdf_value) (uri_rdfs_Resource))) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Statement)) != (iext (uri_rdfs_domain) (uri_rdfs_isDefinedBy) (uri_rdfs_Resource))) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Statement)) != (iext (uri_rdf_type) (uri_rdf_Property) (uri_rdfs_Class))) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Literal)) != (iext (uri_rdfs_domain) (uri_rdf_value) (uri_rdfs_Resource))) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_Restriction)) != (iext (uri_rdfs_range) (uri_rdfs_subPropertyOf) (uri_rdf_Property))) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Class)) != (iext (uri_rdf_type) (uri_rdf_subject) (uri_rdf_Property))) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) zenon_X0) != (iext (uri_rdfs_domain) (uri_rdf_value) (uri_rdfs_Resource))) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_Restriction)) != (iext (uri_rdf_type) (uri_rdf_nil) (uri_rdf_List))) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Class)) != (iext (uri_rdfs_domain) (uri_rdfs_domain) (uri_rdf_Property))) % 4.26/4.42 ((iext (uri_rdfs_domain) (uri_rdf_value) (uri_rdfs_Resource)) = (true)) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_ContainerMembershipProperty)) != (iext (uri_rdfs_domain) (uri_rdfs_subClassOf) (uri_rdfs_Class))) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_ObjectProperty)) != (iext (uri_rdfs_domain) (uri_rdf_value) (uri_rdfs_Resource))) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (uri_rdf_Property)) != (iext (uri_rdfs_domain) (uri_rdf_subject) (uri_rdfs_Statement))) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Literal)) != (iext (uri_rdfs_domain) (uri_rdf_subject) (uri_rdfs_Statement))) % 4.26/4.42 ((uri_rdf_List) != (uri_rdfs_Datatype)) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Statement)) != (iext (uri_rdf_type) (uri_rdf_XMLLiteral) (uri_rdfs_Datatype))) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (uri_ex_p)) != (true)) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z)) != (iext (uri_rdfs_range) (uri_rdf_value) (uri_rdfs_Resource))) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_ContainerMembershipProperty)) != (iext (uri_rdfs_domain) (uri_rdf_subject) (uri_rdfs_Statement))) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (uri_ex_p)) != (iext (uri_rdfs_range) (uri_rdfs_domain) (uri_rdfs_Class))) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (uri_ex_p)) != (iext (uri_rdfs_range) (uri_rdf_value) (uri_rdfs_Resource))) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_seeAlso)) != (iext (uri_rdf_type) (uri_ex_c) (uri_owl_Class))) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (uri_rdf_List)) != (iext (uri_rdfs_range) (uri_rdfs_comment) (uri_rdfs_Literal))) % 4.26/4.42 ((uri_ex_s) != (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z)) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_ContainerMembershipProperty)) != (iext (uri_rdfs_domain) (uri_rdf_predicate) (uri_rdfs_Statement))) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) zenon_X0) != (iext (uri_rdfs_range) (uri_rdf_rest) (uri_rdf_List))) % 4.26/4.42 ((uri_ex_s) != (uri_rdfs_seeAlso)) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_seeAlso)) != (iext (uri_rdf_type) (uri_rdf__1) (uri_rdfs_ContainerMembershipProperty))) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Datatype)) != (iext (uri_rdfs_subClassOf) (uri_rdf_XMLLiteral) (uri_rdfs_Literal))) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_Class)) != (iext (uri_rdf_type) (uri_rdf_object) (uri_rdf_Property))) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Statement)) != (iext (uri_rdfs_range) (uri_rdf__2) (uri_rdfs_Resource))) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Class)) != (iext (uri_rdfs_subClassOf) (uri_rdf_Alt) (uri_rdfs_Container))) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Container)) != (iext (uri_rdfs_range) (uri_rdf_rest) (uri_rdf_List))) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z)) != (iext (uri_rdf_type) (uri_rdf__2) (uri_rdfs_ContainerMembershipProperty))) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_ObjectProperty)) != (iext (uri_rdfs_range) (uri_rdfs_member) (uri_rdfs_Resource))) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_Class)) != (iext (uri_rdfs_subPropertyOf) (uri_rdfs_isDefinedBy) (uri_rdfs_seeAlso))) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (uri_ex_p)) != (iext (uri_rdfs_range) (uri_rdfs_seeAlso) (uri_rdfs_Resource))) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Container)) != (iext (uri_rdfs_domain) (uri_rdf__1) (uri_rdfs_Resource))) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_ObjectProperty)) != (iext (uri_rdf_type) (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z) (uri_owl_Restriction))) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_Class)) != (iext (uri_owl_someValuesFrom) (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z) (uri_ex_c))) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Datatype)) != (iext (uri_rdf_type) (uri_rdf__3) (uri_rdfs_ContainerMembershipProperty))) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_Restriction)) != (iext (uri_rdf_type) (uri_rdf_subject) (uri_rdf_Property))) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) zenon_X0) != (iext (uri_rdfs_domain) (uri_rdfs_isDefinedBy) (uri_rdfs_Resource))) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Datatype)) != (iext (uri_rdfs_domain) (uri_rdf_rest) (uri_rdf_List))) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_Restriction)) != (iext (uri_rdfs_domain) (uri_rdf_value) (uri_rdfs_Resource))) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_ObjectProperty)) != (iext (uri_rdfs_subClassOf) (uri_rdf_Bag) (uri_rdfs_Container))) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) zenon_X0) != (iext (uri_rdf_type) (uri_rdf__1) (uri_rdfs_ContainerMembershipProperty))) % 4.26/4.42 ((uri_rdfs_Datatype) != (uri_owl_Class)) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_Restriction)) != (iext (uri_rdf_type) (uri_ex_c) (uri_owl_Class))) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_ContainerMembershipProperty)) != (iext (uri_rdfs_domain) (uri_rdf_type) (uri_rdfs_Resource))) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Datatype)) != (iext (uri_rdfs_range) (uri_rdf__3) (uri_rdfs_Resource))) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Container)) != (iext (uri_rdf_type) (uri_rdf__2) (uri_rdf_Property))) % 4.26/4.42 ((iext (uri_rdfs_domain) (uri_rdf_subject) (uri_rdfs_Statement)) = (true)) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) zenon_X0) != (iext (uri_rdfs_domain) (uri_rdfs_label) (uri_rdfs_Resource))) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (uri_ex_c)) != (iext (uri_rdf_type) (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z) (uri_owl_Restriction))) % 4.26/4.42 ((tuple (iext (uri_rdf_type) (uri_owl_Restriction) (uri_ex_c)) (iext (uri_ex_p) (uri_ex_s) (uri_owl_Restriction))) != (tuple (true) (true))) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_ObjectProperty)) != (iext (uri_rdfs_subClassOf) (uri_rdf_Alt) (uri_rdfs_Container))) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Class)) != (iext (uri_rdfs_range) (uri_rdf_predicate) (uri_rdfs_Resource))) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Literal)) != (iext (uri_rdf_type) (uri_ex_s) (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z))) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Resource)) != (iext (uri_rdfs_domain) (uri_rdfs_comment) (uri_rdfs_Resource))) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (uri_rdf_List)) != (iext (uri_rdfs_range) (uri_rdfs_label) (uri_rdfs_Literal))) % 4.26/4.42 ((uri_ex_s) != (uri_rdfs_comment)) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Resource)) != (iext (uri_rdfs_subClassOf) (uri_rdf_Alt) (uri_rdfs_Container))) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Datatype)) != (iext (uri_rdf_type) (uri_ex_s) (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z))) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Container)) != (iext (uri_rdf_type) (uri_rdf__2) (uri_rdfs_ContainerMembershipProperty))) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_seeAlso)) != (iext (uri_rdfs_range) (uri_rdfs_subPropertyOf) (uri_rdf_Property))) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Container)) != (iext (uri_rdf_type) (uri_rdf_type) (uri_rdf_Property))) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (uri_rdf_Property)) != (iext (uri_rdf_type) (uri_rdf_subject) (uri_rdf_Property))) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (uri_rdf_Property)) != (iext (uri_rdf_type) (uri_ex_p) (uri_owl_ObjectProperty))) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_Restriction)) != (iext (uri_rdfs_range) (uri_rdfs_member) (uri_rdfs_Resource))) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Resource)) != (iext (uri_rdfs_subClassOf) (uri_rdfs_Datatype) (uri_rdfs_Class))) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (uri_rdf_Property)) != (iext (uri_rdfs_domain) (uri_rdf__2) (uri_rdfs_Resource))) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_seeAlso)) != (iext (uri_rdfs_subClassOf) (uri_rdfs_Seq) (uri_rdfs_Container))) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Literal)) != (iext (uri_rdfs_domain) (uri_rdfs_subPropertyOf) (uri_rdf_Property))) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_ContainerMembershipProperty)) != (iext (uri_rdf_type) (uri_rdf__1) (uri_rdf_Property))) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z)) != (iext (uri_rdfs_domain) (uri_rdf_object) (uri_rdfs_Statement))) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Resource)) != (iext (uri_rdfs_domain) (uri_rdf_subject) (uri_rdfs_Statement))) % 4.26/4.42 ((iext (uri_rdfs_subClassOf) (uri_rdf_Bag) (uri_rdfs_Container)) = (true)) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Datatype)) != (iext (uri_rdfs_domain) (uri_rdf_predicate) (uri_rdfs_Statement))) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_seeAlso)) != (iext (uri_rdfs_range) (uri_rdf__2) (uri_rdfs_Resource))) % 4.26/4.42 (zenon_X0 != (uri_rdfs_Literal)) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_ContainerMembershipProperty)) != (iext (uri_rdf_type) (uri_rdf_nil) (uri_rdf_List))) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_Class)) != (iext (uri_rdfs_domain) (uri_rdf_value) (uri_rdfs_Resource))) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_Class)) != (iext (uri_owl_onProperty) (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z) (uri_ex_p))) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Class)) != (iext (uri_rdfs_domain) (uri_rdfs_isDefinedBy) (uri_rdfs_Resource))) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_Restriction)) != (iext (uri_owl_onProperty) (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z) (uri_ex_p))) % 4.26/4.42 ((tuple (iext (uri_rdf_type) (uri_rdf_Property) (uri_ex_c)) (iext (uri_ex_p) (uri_ex_s) (uri_rdf_Property))) != (tuple (true) (true))) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z)) != (iext (uri_rdfs_range) (uri_rdf__1) (uri_rdfs_Resource))) % 4.26/4.42 ((uri_rdf_Property) != (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z)) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Literal)) != (iext (uri_rdfs_range) (uri_rdfs_subPropertyOf) (uri_rdf_Property))) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Datatype)) != (true)) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_seeAlso)) != (iext (uri_rdf_type) (uri_rdf_rest) (uri_rdf_Property))) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_ContainerMembershipProperty)) != (iext (uri_rdfs_subClassOf) (uri_rdfs_Seq) (uri_rdfs_Container))) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) zenon_X0) != (iext (uri_rdfs_domain) (uri_rdf__3) (uri_rdfs_Resource))) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (uri_rdf_List)) != (iext (uri_rdf_type) (sK1_testcase_premise_fullish_009_Existential_Restriction_Entailments_BNODE_z) (uri_owl_Restriction))) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (uri_owl_Restriction)) != (iext (uri_rdfs_range) (uri_rdfs_comment) (uri_rdfs_Literal))) % 4.26/4.42 ((iext (uri_rdfs_range) (uri_rdfs_range) (uri_rdfs_Class)) = (true)) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Literal)) != (iext (uri_rdf_type) (uri_rdf_value) (uri_rdf_Property))) % 4.26/4.42 ((iext (uri_ex_p) (uri_ex_s) (uri_rdfs_Literal)) != (iext (uri_rdfs_domain) (uri_rdf__2) (uri_rdfs_Resource))) % 4.26/4.42 *) % 4.26/4.42 (* NO-PROOF *) % 4.26/4.42 % SZS status GaveUp % 4.26/4.42 Number of rewrites on terms: 0 % 4.26/4.42 Number of rewrites on props: 0 % 4.26/4.42 nodes searched: 148151 % 4.26/4.42 max branch formulas: 1334 % 4.26/4.42 proof nodes created: 1135 % 4.26/4.42 formulas created: 108420 % 4.26/4.42 %------------------------------------------------------------------------------