%------------------------------------------------------------------------------ % File : ZenonModulo---0.5.0 % Problem : SWB024-10 : TPTP v8.2.0. Released v7.3.0. % Transfm : none % Format : tptp:raw % Command : run_zenon_modulo %d %s % Computer : n008.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:30 EDT 2024 % Result : Unknown 4.67s 4.89s % Output : None % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----No solution output by system %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.11/0.12 % Problem : SWB024-10 : TPTP v8.2.0. Released v7.3.0. % 0.11/0.12 % Command : run_zenon_modulo %d %s % 0.12/0.32 % Computer : n008.cluster.edu % 0.12/0.32 % Model : x86_64 x86_64 % 0.12/0.32 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.32 % Memory : 8042.1875MB % 0.12/0.32 % 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:28:09 EDT 2024 % 0.12/0.33 % CPUTime : % 4.67/4.87 Zenon error: exhausted search space without finding a proof % 4.67/4.87 (* Current branch: % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Resource)) != (iext (uri_rdfs_range) (uri_rdf__3) (uri_rdfs_Resource))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (literal_typed (dat_str_1) (uri_xsd_nonNegativeInteger))) != (iext (uri_rdfs_domain) (uri_rdf__3) (uri_rdfs_Resource))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Resource)) != (true)) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdf_Property)) != (iext (uri_rdfs_domain) (uri_rdfs_seeAlso) (uri_rdfs_Resource))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_owl_Restriction)) != (iext (uri_rdf_type) (uri_ex_alice) (uri_ex_Person))) % 4.67/4.87 ((uri_rdfs_Resource) != (uri_rdfs_Container)) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_hasAncestor)) != (iext (uri_rdf_type) (uri_rdf_Property) (uri_rdfs_Class))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdf_List)) != (iext (uri_rdfs_subClassOf) (uri_rdfs_Seq) (uri_rdfs_Container))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_ContainerMembershipProperty)) != (iext (uri_rdf_type) (uri_rdf_rest) (uri_rdf_Property))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_Person)) != (iext (uri_rdf_type) (uri_ex_bob) (uri_ex_Person))) % 4.67/4.87 ((iext (uri_rdfs_subClassOf) (uri_rdfs_Seq) (uri_rdfs_Container)) = (true)) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z)) != (iext (uri_rdfs_range) (uri_rdfs_subPropertyOf) (uri_rdf_Property))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z)) != (iext (uri_owl_onProperty) (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z) (uri_ex_hasAncestor))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_bob)) != (iext (uri_rdf_type) (uri_rdf_Property) (uri_rdfs_Class))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Datatype)) != (iext (uri_rdf_type) (uri_rdf_type) (uri_rdf_Property))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_ContainerMembershipProperty)) != (iext (uri_rdfs_subClassOf) (uri_rdf_Alt) (uri_rdfs_Container))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Datatype)) != (iext (uri_rdf_type) (uri_rdf__2) (uri_rdfs_ContainerMembershipProperty))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Resource)) != (iext (uri_rdfs_range) (uri_rdfs_subClassOf) (uri_rdfs_Class))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Statement)) != (iext (uri_rdf_type) (uri_rdf__1) (uri_rdfs_ContainerMembershipProperty))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdf_List)) != (iext (uri_rdfs_range) (uri_rdfs_comment) (uri_rdfs_Literal))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdf_List)) != (iext (uri_rdfs_range) (uri_rdf__3) (uri_rdfs_Resource))) % 4.67/4.87 ((uri_ex_bob) != (uri_ex_hasAncestor)) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdf_Property)) != (iext (uri_rdfs_range) (uri_rdfs_isDefinedBy) (uri_rdfs_Resource))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Statement)) != (iext (uri_rdfs_range) (uri_rdf_first) (uri_rdfs_Resource))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_hasAncestor)) != (iext (uri_rdfs_domain) (uri_rdfs_range) (uri_rdf_Property))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) zenon_X0) != (iext (uri_rdfs_range) (uri_rdfs_domain) (uri_rdfs_Class))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_seeAlso)) != (iext (uri_rdfs_range) (uri_rdfs_subPropertyOf) (uri_rdf_Property))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_bob)) != (iext (uri_rdf_type) (uri_rdf_XMLLiteral) (uri_rdfs_Datatype))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Resource)) != (iext (uri_rdfs_domain) (uri_rdf_predicate) (uri_rdfs_Statement))) % 4.67/4.87 ((uri_ex_bob) != (uri_ex_Person)) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_bob)) != (iext (uri_rdfs_domain) (uri_rdfs_range) (uri_rdf_Property))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Literal)) != (iext (uri_rdfs_subClassOf) (uri_rdfs_Seq) (uri_rdfs_Container))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) zenon_X0) != (iext (uri_rdfs_range) (uri_rdfs_isDefinedBy) (uri_rdfs_Resource))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_seeAlso)) != (iext (uri_rdf_type) (uri_rdf__3) (uri_rdfs_ContainerMembershipProperty))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdf_List)) != (iext (uri_rdfs_range) (uri_rdf_first) (uri_rdfs_Resource))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Datatype)) != (iext (uri_rdfs_range) (uri_rdfs_seeAlso) (uri_rdfs_Resource))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_owl_Restriction)) != (iext (uri_ex_hasAncestor) (uri_ex_alice) (uri_ex_bob))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_bob)) != (iext (uri_owl_onProperty) (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z) (uri_ex_hasAncestor))) % 4.67/4.87 (zenon_X0 != (uri_owl_Restriction)) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Literal)) != (iext (uri_rdfs_subClassOf) (uri_rdf_XMLLiteral) (uri_rdfs_Literal))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Container)) != (iext (uri_rdfs_subClassOf) (uri_rdfs_Seq) (uri_rdfs_Container))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Statement)) != (iext (uri_rdfs_domain) (uri_rdfs_subClassOf) (uri_rdfs_Class))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (literal_typed (dat_str_1) (uri_xsd_nonNegativeInteger))) != (iext (uri_ex_hasAncestor) (uri_ex_alice) (uri_ex_bob))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_hasAncestor)) != (iext (uri_rdfs_domain) (uri_rdf_subject) (uri_rdfs_Statement))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Statement)) != (iext (uri_rdfs_subPropertyOf) (uri_rdfs_isDefinedBy) (uri_rdfs_seeAlso))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdf_List)) != (iext (uri_rdfs_domain) (uri_rdf_type) (uri_rdfs_Resource))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_bob)) != (iext (uri_rdfs_range) (uri_rdfs_subPropertyOf) (uri_rdf_Property))) % 4.67/4.87 (zenon_X0 != (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z)) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Datatype)) != (iext (uri_rdfs_range) (uri_rdf__1) (uri_rdfs_Resource))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_Person)) != (iext (uri_rdfs_range) (uri_rdf_first) (uri_rdfs_Resource))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Resource)) != (iext (uri_rdfs_range) (uri_rdf_predicate) (uri_rdfs_Resource))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Statement)) != (iext (uri_rdfs_domain) (uri_rdf__1) (uri_rdfs_Resource))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z)) != (iext (uri_rdfs_range) (uri_rdf__3) (uri_rdfs_Resource))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z)) != (iext (uri_ex_hasAncestor) (uri_ex_alice) (uri_ex_bob))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_Person)) != (iext (uri_rdfs_range) (uri_rdf_rest) (uri_rdf_List))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_ContainerMembershipProperty)) != (iext (uri_rdfs_range) (uri_rdf_first) (uri_rdfs_Resource))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_Person)) != (iext (uri_rdfs_domain) (uri_rdf__3) (uri_rdfs_Resource))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (literal_typed (dat_str_1) (uri_xsd_nonNegativeInteger))) != (iext (uri_rdfs_range) (uri_rdf_value) (uri_rdfs_Resource))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Statement)) != (iext (uri_owl_onProperty) (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z) (uri_ex_hasAncestor))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdf_Property)) != (iext (uri_rdf_type) (uri_rdf__2) (uri_rdf_Property))) % 4.67/4.87 ((uri_rdfs_Literal) != (uri_rdfs_Class)) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Literal)) != (iext (uri_rdf_type) (uri_rdf_XMLLiteral) (uri_rdfs_Datatype))) % 4.67/4.87 ((iext (uri_rdfs_subClassOf) (uri_ex_Person) (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z)) = (true)) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_bob)) != (iext (uri_rdf_type) (uri_rdf_first) (uri_rdf_Property))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_seeAlso)) != (iext (uri_rdfs_domain) (uri_rdf_predicate) (uri_rdfs_Statement))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Statement)) != (iext (uri_rdf_type) (uri_rdf_value) (uri_rdf_Property))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Literal)) != (iext (uri_rdfs_range) (uri_rdfs_label) (uri_rdfs_Literal))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_ContainerMembershipProperty)) != (iext (uri_rdf_type) (uri_rdf__2) (uri_rdf_Property))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Resource)) != (iext (uri_rdfs_domain) (uri_rdfs_subClassOf) (uri_rdfs_Class))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Resource)) != (iext (uri_rdf_type) (uri_ex_bob) (uri_ex_Person))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_owl_Restriction)) != (iext (uri_rdfs_subClassOf) (uri_rdfs_ContainerMembershipProperty) (uri_rdf_Property))) % 4.67/4.87 ((tuple (iext (uri_ex_hasAncestor) (uri_ex_alice) (uri_ex_Person)) (iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_Person))) != (tuple (true) (true))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_bob)) != (iext (uri_rdf_type) (uri_rdf__2) (uri_rdf_Property))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_bob)) != (iext (uri_rdfs_domain) (uri_rdf_value) (uri_rdfs_Resource))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdf_List)) != (iext (uri_rdfs_range) (uri_rdfs_subClassOf) (uri_rdfs_Class))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_ContainerMembershipProperty)) != (iext (uri_rdfs_range) (uri_rdf_subject) (uri_rdfs_Resource))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Datatype)) != (iext (uri_rdf_type) (uri_rdf_Property) (uri_rdfs_Class))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Resource)) != (iext (uri_rdf_type) (uri_rdf__1) (uri_rdfs_ContainerMembershipProperty))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_owl_Restriction)) != (iext (uri_rdfs_domain) (uri_rdfs_subPropertyOf) (uri_rdf_Property))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_ContainerMembershipProperty)) != (iext (uri_rdfs_subClassOf) (uri_ex_Person) (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Container)) != (iext (uri_rdf_type) (uri_rdf_Property) (uri_rdfs_Class))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_Person)) != (iext (uri_rdfs_range) (uri_rdfs_domain) (uri_rdfs_Class))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Class)) != (iext (uri_rdfs_range) (uri_rdf_type) (uri_rdfs_Class))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_owl_Restriction)) != (iext (uri_rdfs_range) (uri_rdfs_member) (uri_rdfs_Resource))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Literal)) != (iext (uri_rdfs_range) (uri_rdfs_member) (uri_rdfs_Resource))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Container)) != (iext (uri_rdfs_range) (uri_rdfs_isDefinedBy) (uri_rdfs_Resource))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z)) != (iext (uri_rdfs_domain) (uri_rdfs_subClassOf) (uri_rdfs_Class))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_seeAlso)) != (iext (uri_rdfs_domain) (uri_rdf_object) (uri_rdfs_Statement))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Class)) != (iext (uri_rdf_type) (uri_rdf__3) (uri_rdfs_ContainerMembershipProperty))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_owl_Restriction)) != (iext (uri_rdfs_range) (uri_rdf_type) (uri_rdfs_Class))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Literal)) != (iext (uri_rdfs_range) (uri_rdfs_domain) (uri_rdfs_Class))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_seeAlso)) != (iext (uri_rdfs_range) (uri_rdf_rest) (uri_rdf_List))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Container)) != (iext (uri_rdf_type) (uri_rdf_rest) (uri_rdf_Property))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_ContainerMembershipProperty)) != (iext (uri_rdfs_range) (uri_rdfs_label) (uri_rdfs_Literal))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Resource)) != (iext (uri_rdfs_domain) (uri_rdf_value) (uri_rdfs_Resource))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Class)) != (iext (uri_rdfs_domain) (uri_rdf__3) (uri_rdfs_Resource))) % 4.67/4.87 ((iext (uri_rdfs_subClassOf) (uri_rdf_XMLLiteral) (uri_rdfs_Literal)) = (true)) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Statement)) != (iext (uri_rdf_type) (uri_rdf_XMLLiteral) (uri_rdfs_Datatype))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdf_List)) != (iext (uri_rdfs_domain) (uri_rdfs_domain) (uri_rdf_Property))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Literal)) != (iext (uri_rdfs_range) (uri_rdfs_range) (uri_rdfs_Class))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_ContainerMembershipProperty)) != (iext (uri_rdfs_domain) (uri_rdfs_subClassOf) (uri_rdfs_Class))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdf_Property)) != (iext (uri_rdf_type) (uri_rdf_nil) (uri_rdf_List))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdf_Property)) != (iext (uri_rdfs_range) (uri_rdfs_member) (uri_rdfs_Resource))) % 4.67/4.87 ((uri_rdfs_seeAlso) != (uri_ex_Person)) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_bob)) != (iext (uri_rdfs_subClassOf) (uri_rdfs_ContainerMembershipProperty) (uri_rdf_Property))) % 4.67/4.87 ((uri_rdf_Property) != (uri_rdfs_seeAlso)) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Container)) != (iext (uri_rdfs_domain) (uri_rdf_subject) (uri_rdfs_Statement))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Datatype)) != (iext (uri_rdf_type) (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z) (uri_owl_Restriction))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_owl_Restriction)) != (iext (uri_rdfs_range) (uri_rdfs_comment) (uri_rdfs_Literal))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (literal_typed (dat_str_1) (uri_xsd_nonNegativeInteger))) != (iext (uri_rdfs_domain) (uri_rdfs_seeAlso) (uri_rdfs_Resource))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Statement)) != (iext (uri_rdfs_subClassOf) (uri_rdfs_Seq) (uri_rdfs_Container))) % 4.67/4.87 ((uri_rdf_List) != (uri_rdfs_Resource)) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Container)) != (iext (uri_rdfs_range) (uri_rdf_rest) (uri_rdf_List))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_Person)) != (iext (uri_rdfs_range) (uri_rdf_subject) (uri_rdfs_Resource))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z)) != (iext (uri_rdf_type) (uri_rdf_type) (uri_rdf_Property))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_bob)) != (iext (uri_rdfs_subClassOf) (uri_rdfs_Seq) (uri_rdfs_Container))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_Person)) != (iext (uri_rdfs_domain) (uri_rdfs_comment) (uri_rdfs_Resource))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Literal)) != (iext (uri_rdf_type) (uri_rdf__3) (uri_rdf_Property))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Statement)) != (iext (uri_rdf_type) (uri_rdf_type) (uri_rdf_Property))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_owl_TransitiveProperty)) != (iext (uri_rdf_type) (uri_ex_alice) (uri_ex_Person))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (literal_typed (dat_str_1) (uri_xsd_nonNegativeInteger))) != (iext (uri_rdfs_subPropertyOf) (uri_rdfs_isDefinedBy) (uri_rdfs_seeAlso))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Class)) != (iext (uri_rdfs_domain) (uri_rdfs_domain) (uri_rdf_Property))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Statement)) != (iext (uri_rdfs_range) (uri_rdfs_member) (uri_rdfs_Resource))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_hasAncestor)) != (iext (uri_rdfs_domain) (uri_rdf_predicate) (uri_rdfs_Statement))) % 4.67/4.87 ((uri_ex_bob) != (uri_rdf_value)) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdf_Property)) != (iext (uri_rdfs_subClassOf) (uri_ex_Person) (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Statement)) != (iext (uri_rdf_type) (uri_rdf_object) (uri_rdf_Property))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) zenon_X0) != (iext (uri_rdfs_domain) (uri_rdfs_member) (uri_rdfs_Resource))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Resource)) != (iext (uri_rdfs_domain) (uri_rdf__3) (uri_rdfs_Resource))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Container)) != (iext (uri_rdfs_domain) (uri_rdf__3) (uri_rdfs_Resource))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_Person)) != (iext (uri_rdf_type) (uri_rdf_first) (uri_rdf_Property))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) zenon_X0) != (iext (uri_rdfs_domain) (uri_rdf_first) (uri_rdf_List))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_seeAlso)) != (iext (uri_rdfs_subClassOf) (uri_rdfs_Datatype) (uri_rdfs_Class))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Class)) != (iext (uri_rdf_type) (uri_rdf_XMLLiteral) (uri_rdfs_Datatype))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_owl_Restriction)) != (iext (uri_rdfs_range) (uri_rdf__1) (uri_rdfs_Resource))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_owl_TransitiveProperty)) != (iext (uri_rdf_type) (uri_rdf__2) (uri_rdfs_ContainerMembershipProperty))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_bob)) != (iext (uri_rdf_type) (uri_rdf__3) (uri_rdf_Property))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdf_List)) != (iext (uri_rdf_type) (uri_ex_alice) (uri_ex_Person))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_owl_Restriction)) != (iext (uri_rdf_type) (uri_rdf_subject) (uri_rdf_Property))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_owl_TransitiveProperty)) != (iext (uri_rdfs_domain) (uri_rdfs_seeAlso) (uri_rdfs_Resource))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z)) != (iext (uri_rdf_type) (uri_rdf_first) (uri_rdf_Property))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_Person)) != (iext (uri_rdfs_domain) (uri_rdf__2) (uri_rdfs_Resource))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (literal_typed (dat_str_1) (uri_xsd_nonNegativeInteger))) != (iext (uri_rdf_type) (uri_ex_alice) (uri_ex_Person))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_owl_TransitiveProperty)) != (iext (uri_rdfs_range) (uri_rdfs_subClassOf) (uri_rdfs_Class))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (literal_typed (dat_str_1) (uri_xsd_nonNegativeInteger))) != (iext (uri_rdfs_range) (uri_rdfs_domain) (uri_rdfs_Class))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_seeAlso)) != (iext (uri_ex_hasAncestor) (uri_ex_alice) (uri_ex_bob))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Container)) != (iext (uri_rdfs_subClassOf) (uri_rdf_Bag) (uri_rdfs_Container))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_Person)) != (iext (uri_rdf_type) (uri_rdf_object) (uri_rdf_Property))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Datatype)) != (iext (uri_rdfs_range) (uri_rdfs_domain) (uri_rdfs_Class))) % 4.67/4.87 ((uri_rdf_Property) != (uri_rdfs_Resource)) % 4.67/4.87 ((uri_rdf_Property) != (uri_rdfs_Class)) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_owl_TransitiveProperty)) != (iext (uri_rdfs_domain) (uri_rdf__3) (uri_rdfs_Resource))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_ContainerMembershipProperty)) != (iext (uri_rdf_type) (uri_rdf_XMLLiteral) (uri_rdfs_Datatype))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_owl_TransitiveProperty)) != (iext (uri_rdfs_range) (uri_rdf_type) (uri_rdfs_Class))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Container)) != (iext (uri_rdf_type) (uri_ex_bob) (uri_ex_Person))) % 4.67/4.87 ((uri_ex_bob) != (uri_rdf__2)) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) zenon_X0) != (iext (uri_rdf_type) (uri_rdf_nil) (uri_rdf_List))) % 4.67/4.87 ((uri_rdf_List) != (uri_ex_hasAncestor)) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_owl_Restriction)) != (iext (uri_rdfs_range) (uri_rdfs_subPropertyOf) (uri_rdf_Property))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdf_Property)) != (iext (uri_rdfs_range) (uri_rdf_rest) (uri_rdf_List))) % 4.67/4.87 (zenon_X0 != (uri_rdfs_Literal)) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Literal)) != (iext (uri_rdfs_range) (uri_rdfs_isDefinedBy) (uri_rdfs_Resource))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_alice) (uri_ex_bob)) = (true)) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z)) != (iext (uri_rdf_type) (uri_rdf_object) (uri_rdf_Property))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Datatype)) != (iext (uri_rdfs_range) (uri_rdfs_range) (uri_rdfs_Class))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_bob)) != (iext (uri_rdfs_range) (uri_rdfs_isDefinedBy) (uri_rdfs_Resource))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdf_List)) != (iext (uri_rdfs_domain) (uri_rdfs_subClassOf) (uri_rdfs_Class))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_seeAlso)) != (iext (uri_rdf_type) (uri_rdf__2) (uri_rdf_Property))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) zenon_X0) != (iext (uri_rdfs_domain) (uri_rdf_predicate) (uri_rdfs_Statement))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Resource)) != (iext (uri_rdfs_domain) (uri_rdf_subject) (uri_rdfs_Statement))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) zenon_X0) != (iext (uri_rdfs_range) (uri_rdf_value) (uri_rdfs_Resource))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Datatype)) != (iext (uri_rdfs_domain) (uri_rdf_predicate) (uri_rdfs_Statement))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_owl_TransitiveProperty)) != (iext (uri_rdf_type) (uri_rdf__1) (uri_rdf_Property))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_ContainerMembershipProperty)) != (iext (uri_rdfs_range) (uri_rdf__1) (uri_rdfs_Resource))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z)) != (iext (uri_rdfs_range) (uri_rdfs_seeAlso) (uri_rdfs_Resource))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdf_Property)) != (iext (uri_rdfs_subClassOf) (uri_rdf_Bag) (uri_rdfs_Container))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_seeAlso)) != (iext (uri_rdfs_range) (uri_rdf_subject) (uri_rdfs_Resource))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Class)) != (iext (uri_rdf_type) (uri_rdf__2) (uri_rdfs_ContainerMembershipProperty))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_Person)) != (iext (uri_rdfs_range) (uri_rdf_type) (uri_rdfs_Class))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_Person)) != (iext (uri_rdfs_domain) (uri_rdf_object) (uri_rdfs_Statement))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_owl_TransitiveProperty)) != (iext (uri_rdf_type) (uri_ex_hasAncestor) (uri_owl_TransitiveProperty))) % 4.67/4.87 ((uri_rdfs_Literal) != (uri_rdfs_Container)) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_owl_Restriction)) != (iext (uri_rdfs_domain) (uri_rdf_subject) (uri_rdfs_Statement))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Literal)) != (iext (uri_rdfs_range) (uri_rdf_first) (uri_rdfs_Resource))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_ContainerMembershipProperty)) != (iext (uri_rdfs_domain) (uri_rdf__1) (uri_rdfs_Resource))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdf_List)) != (iext (uri_rdf_type) (uri_rdf__3) (uri_rdf_Property))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_ContainerMembershipProperty)) != (iext (uri_rdfs_subClassOf) (uri_rdf_Bag) (uri_rdfs_Container))) % 4.67/4.87 ((iext (uri_rdf_type) (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z) (uri_owl_Restriction)) = (true)) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Statement)) != (iext (uri_rdfs_domain) (uri_rdfs_label) (uri_rdfs_Resource))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z)) != (iext (uri_rdfs_domain) (uri_rdf__1) (uri_rdfs_Resource))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_bob)) != (iext (uri_rdfs_domain) (uri_rdfs_isDefinedBy) (uri_rdfs_Resource))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_Person)) != (iext (uri_rdfs_domain) (uri_rdfs_range) (uri_rdf_Property))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_owl_TransitiveProperty)) != (iext (uri_rdfs_domain) (uri_rdf_type) (uri_rdfs_Resource))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Class)) != (iext (uri_rdfs_subClassOf) (uri_ex_Person) (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_ContainerMembershipProperty)) != (iext (uri_rdfs_domain) (uri_rdfs_member) (uri_rdfs_Resource))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Statement)) != (iext (uri_rdfs_domain) (uri_rdfs_seeAlso) (uri_rdfs_Resource))) % 4.67/4.87 ((iext (uri_rdf_type) (uri_rdf__2) (uri_rdfs_ContainerMembershipProperty)) = (true)) % 4.67/4.87 ((uri_rdfs_Datatype) != (uri_rdfs_Class)) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Class)) != (iext (uri_rdfs_range) (uri_rdf__1) (uri_rdfs_Resource))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Statement)) != (iext (uri_rdfs_domain) (uri_rdfs_range) (uri_rdf_Property))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Datatype)) != (iext (uri_rdf_type) (uri_rdf__1) (uri_rdf_Property))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_ContainerMembershipProperty)) != (iext (uri_rdfs_domain) (uri_rdf_predicate) (uri_rdfs_Statement))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdf_Property)) != (iext (uri_rdfs_range) (uri_rdfs_subClassOf) (uri_rdfs_Class))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_owl_Restriction)) != (iext (uri_rdf_type) (uri_rdf_rest) (uri_rdf_Property))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_owl_Restriction)) != (iext (uri_rdfs_domain) (uri_rdf_predicate) (uri_rdfs_Statement))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z)) != (iext (uri_rdf_type) (uri_rdf__3) (uri_rdfs_ContainerMembershipProperty))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Datatype)) != (iext (uri_rdf_type) (uri_rdf_rest) (uri_rdf_Property))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_Person)) != (iext (uri_rdfs_domain) (uri_rdfs_label) (uri_rdfs_Resource))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (literal_typed (dat_str_1) (uri_xsd_nonNegativeInteger))) != (iext (uri_rdf_type) (uri_rdf_XMLLiteral) (uri_rdfs_Datatype))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (literal_typed (dat_str_1) (uri_xsd_nonNegativeInteger))) != (iext (uri_rdf_type) (uri_ex_hasAncestor) (uri_owl_TransitiveProperty))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_seeAlso)) != (iext (uri_rdf_type) (uri_rdf_rest) (uri_rdf_Property))) % 4.67/4.87 ((iext (uri_rdfs_domain) (uri_rdfs_member) (uri_rdfs_Resource)) = (true)) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Literal)) != (iext (uri_rdf_type) (uri_rdf_subject) (uri_rdf_Property))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdf_List)) != (iext (uri_rdfs_range) (uri_rdfs_member) (uri_rdfs_Resource))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_seeAlso)) != (iext (uri_rdf_type) (uri_rdf__3) (uri_rdf_Property))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_hasAncestor)) != (iext (uri_rdfs_range) (uri_rdfs_label) (uri_rdfs_Literal))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdf_Property)) != (iext (uri_rdf_type) (uri_rdf_first) (uri_rdf_Property))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdf_List)) != (iext (uri_rdf_type) (uri_rdf_XMLLiteral) (uri_rdfs_Datatype))) % 4.67/4.87 ((iext (uri_rdf_type) (uri_rdf_value) (uri_rdf_Property)) = (true)) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_hasAncestor)) != (iext (uri_rdfs_subClassOf) (uri_ex_Person) (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Class)) != (iext (uri_rdf_type) (uri_rdf__3) (uri_rdf_Property))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Class)) != (iext (uri_rdfs_range) (uri_rdf_first) (uri_rdfs_Resource))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Container)) != (iext (uri_rdfs_subClassOf) (uri_rdf_XMLLiteral) (uri_rdfs_Literal))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z)) != (iext (uri_rdfs_range) (uri_rdfs_isDefinedBy) (uri_rdfs_Resource))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_Person)) != (iext (uri_rdf_type) (uri_ex_hasAncestor) (uri_owl_TransitiveProperty))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z)) != (iext (uri_rdfs_range) (uri_rdf__2) (uri_rdfs_Resource))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (literal_typed (dat_str_1) (uri_xsd_nonNegativeInteger))) != (iext (uri_rdfs_range) (uri_rdfs_comment) (uri_rdfs_Literal))) % 4.67/4.87 ((iext (uri_rdfs_range) (uri_rdf_subject) (uri_rdfs_Resource)) = (true)) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (literal_typed (dat_str_1) (uri_xsd_nonNegativeInteger))) != (iext (uri_rdf_type) (uri_rdf__3) (uri_rdf_Property))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Container)) != (iext (uri_rdfs_domain) (uri_rdf_type) (uri_rdfs_Resource))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Container)) != (iext (uri_rdfs_domain) (uri_rdf_value) (uri_rdfs_Resource))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_ContainerMembershipProperty)) != (iext (uri_rdfs_domain) (uri_rdf__3) (uri_rdfs_Resource))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_bob)) != (iext (uri_rdfs_range) (uri_rdfs_range) (uri_rdfs_Class))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_hasAncestor)) != (iext (uri_rdf_type) (uri_rdf_value) (uri_rdf_Property))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_owl_TransitiveProperty)) != (iext (uri_ex_hasAncestor) (uri_ex_alice) (uri_ex_bob))) % 4.67/4.87 ((uri_owl_TransitiveProperty) != (uri_ex_bob)) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdf_List)) != (iext (uri_rdf_type) (uri_rdf_rest) (uri_rdf_Property))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Datatype)) != (iext (uri_rdfs_domain) (uri_rdfs_label) (uri_rdfs_Resource))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Container)) != (iext (uri_owl_minCardinality) (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z) (literal_typed (dat_str_1) (uri_xsd_nonNegativeInteger)))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdf_List)) != (iext (uri_rdfs_subClassOf) (uri_rdf_Alt) (uri_rdfs_Container))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z)) != (iext (uri_rdfs_subClassOf) (uri_rdfs_Seq) (uri_rdfs_Container))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Class)) != (iext (uri_rdfs_subClassOf) (uri_rdfs_Seq) (uri_rdfs_Container))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) zenon_X0) != (iext (uri_rdfs_range) (uri_rdfs_member) (uri_rdfs_Resource))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdf_List)) != (iext (uri_rdf_type) (uri_ex_bob) (uri_ex_Person))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_Person)) != (iext (uri_rdfs_range) (uri_rdfs_range) (uri_rdfs_Class))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z)) != (iext (uri_rdfs_domain) (uri_rdf_predicate) (uri_rdfs_Statement))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_bob)) != (iext (uri_rdfs_range) (uri_rdf_value) (uri_rdfs_Resource))) % 4.67/4.87 (zenon_X0 != (uri_rdf_Property)) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdf_Property)) != (iext (uri_rdf_type) (uri_ex_bob) (uri_ex_Person))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_seeAlso)) != (iext (uri_rdf_type) (uri_rdf__2) (uri_rdfs_ContainerMembershipProperty))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_ContainerMembershipProperty)) != (iext (uri_rdfs_subClassOf) (uri_rdfs_ContainerMembershipProperty) (uri_rdf_Property))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_ContainerMembershipProperty)) != (iext (uri_rdfs_domain) (uri_rdf_object) (uri_rdfs_Statement))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Container)) != (iext (uri_rdfs_subClassOf) (uri_rdf_Alt) (uri_rdfs_Container))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) zenon_X0) != (iext (uri_rdfs_domain) (uri_rdfs_domain) (uri_rdf_Property))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Literal)) != (iext (uri_rdf_type) (uri_rdf_first) (uri_rdf_Property))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_bob)) != (iext (uri_rdfs_range) (uri_rdfs_comment) (uri_rdfs_Literal))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdf_Property)) != (iext (uri_rdfs_domain) (uri_rdf_predicate) (uri_rdfs_Statement))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_ContainerMembershipProperty)) != (iext (uri_rdfs_domain) (uri_rdf__2) (uri_rdfs_Resource))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_Person)) != (iext (uri_rdfs_subClassOf) (uri_rdf_Alt) (uri_rdfs_Container))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Container)) != (iext (uri_rdf_type) (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z) (uri_owl_Restriction))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_hasAncestor)) != (iext (uri_rdfs_domain) (uri_rdfs_comment) (uri_rdfs_Resource))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_owl_TransitiveProperty)) != (iext (uri_rdfs_subClassOf) (uri_rdfs_ContainerMembershipProperty) (uri_rdf_Property))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_seeAlso)) != (iext (uri_rdfs_domain) (uri_rdfs_subPropertyOf) (uri_rdf_Property))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) zenon_X0) != (iext (uri_rdfs_subClassOf) (uri_rdfs_ContainerMembershipProperty) (uri_rdf_Property))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Resource)) != (iext (uri_rdfs_range) (uri_rdfs_isDefinedBy) (uri_rdfs_Resource))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Statement)) != (iext (uri_rdfs_domain) (uri_rdf_first) (uri_rdf_List))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Statement)) != (iext (uri_rdfs_subClassOf) (uri_rdfs_ContainerMembershipProperty) (uri_rdf_Property))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_owl_TransitiveProperty)) != (iext (uri_rdfs_subClassOf) (uri_rdfs_Datatype) (uri_rdfs_Class))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_bob)) != (iext (uri_rdfs_domain) (uri_rdfs_domain) (uri_rdf_Property))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Class)) != (iext (uri_rdfs_subClassOf) (uri_rdf_XMLLiteral) (uri_rdfs_Literal))) % 4.67/4.87 ((uri_rdfs_Class) != (uri_ex_Person)) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Container)) != (iext (uri_rdf_type) (uri_rdf__2) (uri_rdf_Property))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdf_Property)) != (iext (uri_rdf_type) (uri_ex_hasAncestor) (uri_owl_TransitiveProperty))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_Person)) != (iext (uri_owl_onProperty) (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z) (uri_ex_hasAncestor))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdf_Property)) != (iext (uri_rdf_type) (uri_rdf__2) (uri_rdfs_ContainerMembershipProperty))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdf_List)) != (iext (uri_rdfs_range) (uri_rdfs_range) (uri_rdfs_Class))) % 4.67/4.87 ((uri_ex_bob) != (uri_rdfs_subPropertyOf)) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Container)) != (iext (uri_rdf_type) (uri_ex_hasAncestor) (uri_owl_TransitiveProperty))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_owl_Restriction)) != (iext (uri_rdfs_domain) (uri_rdfs_comment) (uri_rdfs_Resource))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Literal)) != (iext (uri_rdfs_domain) (uri_rdf_predicate) (uri_rdfs_Statement))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_hasAncestor)) != (iext (uri_rdfs_range) (uri_rdf__1) (uri_rdfs_Resource))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_bob)) != (iext (uri_rdfs_subClassOf) (uri_rdf_XMLLiteral) (uri_rdfs_Literal))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Class)) != (iext (uri_rdfs_domain) (uri_rdf_first) (uri_rdf_List))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_bob)) != (iext (uri_rdfs_range) (uri_rdfs_seeAlso) (uri_rdfs_Resource))) % 4.67/4.87 ((iext (uri_rdfs_domain) (uri_rdf_rest) (uri_rdf_List)) = (true)) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) zenon_X0) != (iext (uri_rdfs_domain) (uri_rdf_type) (uri_rdfs_Resource))) % 4.67/4.87 ((uri_rdfs_seeAlso) != (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z)) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Class)) != (iext (uri_rdfs_subClassOf) (uri_rdfs_Datatype) (uri_rdfs_Class))) % 4.67/4.87 ((uri_rdfs_Resource) != (uri_ex_bob)) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_owl_Restriction)) != (iext (uri_rdf_type) (uri_rdf_value) (uri_rdf_Property))) % 4.67/4.87 ((uri_owl_Restriction) != (uri_ex_hasAncestor)) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_owl_TransitiveProperty)) != (iext (uri_rdf_type) (uri_rdf_type) (uri_rdf_Property))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_ContainerMembershipProperty)) != (iext (uri_rdfs_range) (uri_rdf_rest) (uri_rdf_List))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (literal_typed (dat_str_1) (uri_xsd_nonNegativeInteger))) != (true)) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_ContainerMembershipProperty)) != (iext (uri_rdfs_domain) (uri_rdf_value) (uri_rdfs_Resource))) % 4.67/4.87 ((uri_rdfs_Literal) != (uri_ex_Person)) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z)) != (iext (uri_rdfs_domain) (uri_rdfs_member) (uri_rdfs_Resource))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_hasAncestor)) != (iext (uri_rdfs_range) (uri_rdf_subject) (uri_rdfs_Resource))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) zenon_X0) != (iext (uri_rdfs_subClassOf) (uri_rdfs_Seq) (uri_rdfs_Container))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_seeAlso)) != (iext (uri_rdf_type) (uri_rdf_first) (uri_rdf_Property))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Class)) != (iext (uri_rdf_type) (uri_ex_hasAncestor) (uri_owl_TransitiveProperty))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_hasAncestor)) != (iext (uri_rdfs_range) (uri_rdfs_isDefinedBy) (uri_rdfs_Resource))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdf_Property)) != (iext (uri_rdfs_domain) (uri_rdfs_isDefinedBy) (uri_rdfs_Resource))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Literal)) != (iext (uri_rdfs_domain) (uri_rdf_value) (uri_rdfs_Resource))) % 4.67/4.87 ((uri_rdfs_seeAlso) != (uri_owl_Restriction)) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_ContainerMembershipProperty)) != (iext (uri_rdfs_range) (uri_rdf__3) (uri_rdfs_Resource))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_owl_Restriction)) != (iext (uri_rdfs_domain) (uri_rdf_object) (uri_rdfs_Statement))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Container)) != (iext (uri_rdfs_domain) (uri_rdfs_isDefinedBy) (uri_rdfs_Resource))) % 4.67/4.87 (zenon_X0 != (uri_rdfs_Container)) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Container)) != (iext (uri_rdfs_subClassOf) (uri_ex_Person) (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z))) % 4.67/4.87 ((uri_rdf_List) != (uri_rdfs_Class)) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_hasAncestor)) != (iext (uri_rdfs_range) (uri_rdfs_domain) (uri_rdfs_Class))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (literal_typed (dat_str_1) (uri_xsd_nonNegativeInteger))) != (iext (uri_rdfs_subClassOf) (uri_ex_Person) (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_owl_TransitiveProperty)) != (iext (uri_rdfs_subClassOf) (uri_rdf_Alt) (uri_rdfs_Container))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_owl_TransitiveProperty)) != (iext (uri_rdf_type) (uri_rdf__1) (uri_rdfs_ContainerMembershipProperty))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Datatype)) != (true)) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_bob)) != (iext (uri_rdfs_domain) (uri_rdf_subject) (uri_rdfs_Statement))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_hasAncestor)) != (iext (uri_rdf_type) (uri_rdf_rest) (uri_rdf_Property))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_hasAncestor)) != (iext (uri_rdfs_range) (uri_rdf_rest) (uri_rdf_List))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_hasAncestor)) != (iext (uri_rdfs_domain) (uri_rdfs_subClassOf) (uri_rdfs_Class))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdf_List)) != (iext (uri_rdf_type) (uri_rdf_type) (uri_rdf_Property))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (literal_typed (dat_str_1) (uri_xsd_nonNegativeInteger))) != (iext (uri_rdfs_domain) (uri_rdf__2) (uri_rdfs_Resource))) % 4.67/4.87 ((iext (uri_rdfs_domain) (uri_rdf_predicate) (uri_rdfs_Statement)) = (true)) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Statement)) != (iext (uri_rdfs_range) (uri_rdfs_subPropertyOf) (uri_rdf_Property))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdf_List)) != (iext (uri_rdfs_domain) (uri_rdf__1) (uri_rdfs_Resource))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Class)) != (iext (uri_rdfs_subClassOf) (uri_rdf_Alt) (uri_rdfs_Container))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Resource)) != (iext (uri_rdfs_range) (uri_rdf_first) (uri_rdfs_Resource))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_hasAncestor)) != (iext (uri_rdf_type) (uri_rdf__1) (uri_rdfs_ContainerMembershipProperty))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdf_List)) != (iext (uri_rdfs_domain) (uri_rdf__3) (uri_rdfs_Resource))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z)) != (true)) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (literal_typed (dat_str_1) (uri_xsd_nonNegativeInteger))) != (iext (uri_rdf_type) (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z) (uri_owl_Restriction))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Container)) != (true)) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Class)) != (iext (uri_rdf_type) (uri_rdf_rest) (uri_rdf_Property))) % 4.67/4.87 ((uri_rdf_List) != (uri_rdfs_Literal)) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdf_List)) != (iext (uri_rdf_type) (uri_ex_hasAncestor) (uri_owl_TransitiveProperty))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Class)) != (iext (uri_rdf_type) (uri_ex_alice) (uri_ex_Person))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Statement)) != (iext (uri_rdfs_domain) (uri_rdf_rest) (uri_rdf_List))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Datatype)) != (iext (uri_rdfs_domain) (uri_rdf_object) (uri_rdfs_Statement))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_owl_TransitiveProperty)) != (iext (uri_rdfs_domain) (uri_rdf__2) (uri_rdfs_Resource))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_ContainerMembershipProperty)) != (iext (uri_rdfs_domain) (uri_rdf_type) (uri_rdfs_Resource))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Statement)) != (iext (uri_rdfs_domain) (uri_rdfs_subPropertyOf) (uri_rdf_Property))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) zenon_X0) != (iext (uri_rdfs_domain) (uri_rdfs_range) (uri_rdf_Property))) % 4.67/4.87 ((uri_rdf_Property) != (uri_rdfs_Container)) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_seeAlso)) != (iext (uri_rdfs_domain) (uri_rdf_first) (uri_rdf_List))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Resource)) != (iext (uri_rdfs_domain) (uri_rdfs_label) (uri_rdfs_Resource))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_seeAlso)) != (iext (uri_rdfs_domain) (uri_rdf_rest) (uri_rdf_List))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_owl_TransitiveProperty)) != (iext (uri_rdfs_domain) (uri_rdf_rest) (uri_rdf_List))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Datatype)) != (iext (uri_rdf_type) (uri_rdf__2) (uri_rdf_Property))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Class)) != (iext (uri_rdfs_range) (uri_rdf_predicate) (uri_rdfs_Resource))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_hasAncestor)) != (iext (uri_rdfs_range) (uri_rdfs_subClassOf) (uri_rdfs_Class))) % 4.67/4.87 (zenon_X0 != (uri_rdfs_ContainerMembershipProperty)) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_ContainerMembershipProperty)) != (iext (uri_rdf_type) (uri_rdf__3) (uri_rdf_Property))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Class)) != (iext (uri_rdf_type) (uri_rdf__2) (uri_rdf_Property))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) zenon_X0) != (iext (uri_rdfs_subClassOf) (uri_rdf_Alt) (uri_rdfs_Container))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z)) != (iext (uri_rdfs_subClassOf) (uri_rdfs_ContainerMembershipProperty) (uri_rdf_Property))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z)) != (iext (uri_rdfs_range) (uri_rdf_value) (uri_rdfs_Resource))) % 4.67/4.87 ((uri_rdf_List) != (uri_rdfs_seeAlso)) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Resource)) != (iext (uri_rdfs_domain) (uri_rdf_first) (uri_rdf_List))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_Person)) != (iext (uri_rdfs_range) (uri_rdfs_subClassOf) (uri_rdfs_Class))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_ContainerMembershipProperty)) != (iext (uri_rdf_type) (uri_rdf__3) (uri_rdfs_ContainerMembershipProperty))) % 4.67/4.87 ((iext (uri_rdf_type) (uri_ex_bob) (uri_ex_Person)) = (true)) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdf_Property)) != (iext (uri_rdfs_subClassOf) (uri_rdf_Alt) (uri_rdfs_Container))) % 4.67/4.87 ((uri_rdfs_Datatype) != (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z)) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Class)) != (iext (uri_rdfs_domain) (uri_rdfs_comment) (uri_rdfs_Resource))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Datatype)) != (iext (uri_rdfs_domain) (uri_rdfs_member) (uri_rdfs_Resource))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Datatype)) != (iext (uri_rdfs_domain) (uri_rdfs_domain) (uri_rdf_Property))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_owl_Restriction)) != (iext (uri_rdf_type) (uri_rdf_object) (uri_rdf_Property))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Datatype)) != (iext (uri_owl_minCardinality) (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z) (literal_typed (dat_str_1) (uri_xsd_nonNegativeInteger)))) % 4.67/4.87 ((uri_ex_bob) != (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z)) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_owl_TransitiveProperty)) != (iext (uri_rdf_type) (uri_ex_bob) (uri_ex_Person))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (literal_typed (dat_str_1) (uri_xsd_nonNegativeInteger))) != (iext (uri_rdf_type) (uri_rdf_rest) (uri_rdf_Property))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (literal_typed (dat_str_1) (uri_xsd_nonNegativeInteger))) != (iext (uri_rdf_type) (uri_ex_bob) (uri_ex_Person))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_hasAncestor)) != (iext (uri_rdfs_range) (uri_rdfs_member) (uri_rdfs_Resource))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) zenon_X0) != (iext (uri_rdf_type) (uri_ex_bob) (uri_ex_Person))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_hasAncestor)) != (iext (uri_rdf_type) (uri_rdf__2) (uri_rdf_Property))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Datatype)) != (iext (uri_rdfs_range) (uri_rdfs_member) (uri_rdfs_Resource))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Datatype)) != (iext (uri_rdf_type) (uri_rdf__1) (uri_rdfs_ContainerMembershipProperty))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_bob)) != (iext (uri_rdfs_domain) (uri_rdfs_comment) (uri_rdfs_Resource))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_Person)) != (iext (uri_rdfs_subClassOf) (uri_ex_Person) (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_ContainerMembershipProperty)) != (iext (uri_rdfs_domain) (uri_rdfs_comment) (uri_rdfs_Resource))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) zenon_X0) != (iext (uri_rdf_type) (uri_rdf_subject) (uri_rdf_Property))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_owl_Restriction)) != (iext (uri_rdfs_range) (uri_rdfs_range) (uri_rdfs_Class))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdf_Property)) != (iext (uri_rdf_type) (uri_rdf__3) (uri_rdfs_ContainerMembershipProperty))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Container)) != (iext (uri_rdf_type) (uri_rdf_type) (uri_rdf_Property))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_ContainerMembershipProperty)) != (iext (uri_ex_hasAncestor) (uri_ex_alice) (uri_ex_bob))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) zenon_X0) != (iext (uri_rdfs_subClassOf) (uri_ex_Person) (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Container)) != (iext (uri_rdfs_domain) (uri_rdf_rest) (uri_rdf_List))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdf_Property)) != (iext (uri_rdf_type) (uri_rdf_value) (uri_rdf_Property))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_owl_Restriction)) != (iext (uri_rdfs_domain) (uri_rdf_rest) (uri_rdf_List))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_Person)) != (iext (uri_rdfs_domain) (uri_rdfs_member) (uri_rdfs_Resource))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_bob)) != (iext (uri_rdfs_range) (uri_rdfs_domain) (uri_rdfs_Class))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) zenon_X0) != (iext (uri_rdfs_domain) (uri_rdfs_subClassOf) (uri_rdfs_Class))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Statement)) != (iext (uri_rdfs_domain) (uri_rdf_value) (uri_rdfs_Resource))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_owl_TransitiveProperty)) != (iext (uri_rdf_type) (uri_rdf_Property) (uri_rdfs_Class))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (literal_typed (dat_str_1) (uri_xsd_nonNegativeInteger))) != (iext (uri_rdfs_range) (uri_rdf__2) (uri_rdfs_Resource))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Class)) != (iext (uri_rdf_type) (uri_rdf__1) (uri_rdf_Property))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Container)) != (iext (uri_rdf_type) (uri_rdf__3) (uri_rdf_Property))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_seeAlso)) != (iext (uri_rdf_type) (uri_rdf_Property) (uri_rdfs_Class))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Container)) != (iext (uri_rdfs_domain) (uri_rdfs_subPropertyOf) (uri_rdf_Property))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_hasAncestor)) != (iext (uri_rdfs_subClassOf) (uri_rdf_XMLLiteral) (uri_rdfs_Literal))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (literal_typed (dat_str_1) (uri_xsd_nonNegativeInteger))) != (iext (uri_rdf_type) (uri_rdf_subject) (uri_rdf_Property))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_seeAlso)) != (iext (uri_rdfs_range) (uri_rdf_first) (uri_rdfs_Resource))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Container)) != (iext (uri_rdfs_subClassOf) (uri_rdfs_Datatype) (uri_rdfs_Class))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Statement)) != (iext (uri_rdfs_range) (uri_rdfs_comment) (uri_rdfs_Literal))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) zenon_X0) != (iext (uri_rdfs_range) (uri_rdf_predicate) (uri_rdfs_Resource))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (literal_typed (dat_str_1) (uri_xsd_nonNegativeInteger))) != (iext (uri_rdfs_range) (uri_rdfs_subPropertyOf) (uri_rdf_Property))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) zenon_X0) != (iext (uri_rdfs_domain) (uri_rdfs_subPropertyOf) (uri_rdf_Property))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Class)) != (iext (uri_rdfs_domain) (uri_rdf_subject) (uri_rdfs_Statement))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_owl_Restriction)) != (iext (uri_rdf_type) (uri_rdf_type) (uri_rdf_Property))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Statement)) != (iext (uri_rdfs_subClassOf) (uri_rdf_XMLLiteral) (uri_rdfs_Literal))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Statement)) != (iext (uri_rdfs_subClassOf) (uri_rdfs_Datatype) (uri_rdfs_Class))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_seeAlso)) != (true)) % 4.67/4.87 (zenon_X0 != (uri_owl_TransitiveProperty)) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Datatype)) != (iext (uri_rdf_type) (uri_rdf_XMLLiteral) (uri_rdfs_Datatype))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Class)) != (iext (uri_rdf_type) (uri_rdf_value) (uri_rdf_Property))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_hasAncestor)) != (iext (uri_rdfs_range) (uri_rdfs_comment) (uri_rdfs_Literal))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Resource)) != (iext (uri_rdfs_domain) (uri_rdfs_comment) (uri_rdfs_Resource))) % 4.67/4.87 ((iext (uri_rdfs_range) (uri_rdfs_subClassOf) (uri_rdfs_Class)) = (true)) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdf_List)) != (iext (uri_rdfs_subClassOf) (uri_rdf_XMLLiteral) (uri_rdfs_Literal))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_seeAlso)) != (iext (uri_rdfs_range) (uri_rdfs_label) (uri_rdfs_Literal))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Class)) != (iext (uri_rdfs_domain) (uri_rdf_rest) (uri_rdf_List))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_hasAncestor)) != (iext (uri_rdf_type) (uri_rdf__2) (uri_rdfs_ContainerMembershipProperty))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Literal)) != (iext (uri_rdfs_domain) (uri_rdf_first) (uri_rdf_List))) % 4.67/4.87 ((uri_rdf_Property) != (uri_rdfs_Statement)) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_bob)) != (iext (uri_rdfs_range) (uri_rdf_first) (uri_rdfs_Resource))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdf_Property)) != (iext (uri_rdfs_domain) (uri_rdfs_comment) (uri_rdfs_Resource))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) zenon_X0) != (iext (uri_rdf_type) (uri_rdf_type) (uri_rdf_Property))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z)) != (iext (uri_rdfs_domain) (uri_rdfs_isDefinedBy) (uri_rdfs_Resource))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (literal_typed (dat_str_1) (uri_xsd_nonNegativeInteger))) != (iext (uri_rdfs_range) (uri_rdf_predicate) (uri_rdfs_Resource))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Resource)) != (iext (uri_rdf_type) (uri_rdf_subject) (uri_rdf_Property))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Literal)) != (iext (uri_rdf_type) (uri_rdf__3) (uri_rdfs_ContainerMembershipProperty))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Container)) != (iext (uri_rdf_type) (uri_rdf_XMLLiteral) (uri_rdfs_Datatype))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_ContainerMembershipProperty)) != (iext (uri_rdfs_domain) (uri_rdfs_label) (uri_rdfs_Resource))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_ContainerMembershipProperty)) != (iext (uri_owl_minCardinality) (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z) (literal_typed (dat_str_1) (uri_xsd_nonNegativeInteger)))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_seeAlso)) != (iext (uri_rdf_type) (uri_rdf_XMLLiteral) (uri_rdfs_Datatype))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_bob)) != (iext (uri_rdfs_domain) (uri_rdf__1) (uri_rdfs_Resource))) % 4.67/4.87 ((iext (uri_rdfs_subPropertyOf) (uri_rdfs_isDefinedBy) (uri_rdfs_seeAlso)) = (true)) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdf_Property)) != (iext (uri_rdfs_range) (uri_rdf__3) (uri_rdfs_Resource))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Literal)) != (iext (uri_rdf_type) (uri_rdf_nil) (uri_rdf_List))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) zenon_X0) != (iext (uri_rdfs_subClassOf) (uri_rdf_XMLLiteral) (uri_rdfs_Literal))) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_hasAncestor)) != (true)) % 4.67/4.87 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z)) != (iext (uri_rdfs_subClassOf) (uri_ex_Person) (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_owl_TransitiveProperty)) != (iext (uri_rdfs_range) (uri_rdf__1) (uri_rdfs_Resource))) % 4.67/4.88 ((uri_rdfs_ContainerMembershipProperty) != (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z)) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (literal_typed (dat_str_1) (uri_xsd_nonNegativeInteger))) != (iext (uri_rdfs_domain) (uri_rdfs_comment) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Container)) != (iext (uri_ex_hasAncestor) (uri_ex_alice) (uri_ex_bob))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (literal_typed (dat_str_1) (uri_xsd_nonNegativeInteger))) != (iext (uri_rdfs_domain) (uri_rdf_object) (uri_rdfs_Statement))) % 4.67/4.88 ((uri_ex_bob) != (uri_rdf_type)) % 4.67/4.88 ((uri_rdfs_Resource) != (uri_ex_hasAncestor)) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Class)) != (iext (uri_rdfs_range) (uri_rdf_value) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Container)) != (iext (uri_rdfs_range) (uri_rdf__2) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_Person)) != (iext (uri_rdf_type) (uri_rdf_type) (uri_rdf_Property))) % 4.67/4.88 ((uri_rdf_List) != (uri_owl_TransitiveProperty)) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z)) != (iext (uri_rdfs_domain) (uri_rdfs_domain) (uri_rdf_Property))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdf_Property)) != (iext (uri_rdfs_subPropertyOf) (uri_rdfs_isDefinedBy) (uri_rdfs_seeAlso))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Literal)) != (iext (uri_rdfs_domain) (uri_rdf__1) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Container)) != (iext (uri_rdfs_range) (uri_rdf_first) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Class)) != (iext (uri_rdf_type) (uri_rdf__1) (uri_rdfs_ContainerMembershipProperty))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Literal)) != (iext (uri_rdf_type) (uri_rdf_object) (uri_rdf_Property))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) zenon_X0) != (iext (uri_rdfs_domain) (uri_rdfs_isDefinedBy) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdf_List)) != (iext (uri_rdf_type) (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z) (uri_owl_Restriction))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Datatype)) != (iext (uri_rdfs_domain) (uri_rdf_value) (uri_rdfs_Resource))) % 4.67/4.88 ((uri_rdf_List) != (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z)) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Literal)) != (iext (uri_owl_minCardinality) (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z) (literal_typed (dat_str_1) (uri_xsd_nonNegativeInteger)))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_owl_Restriction)) != (iext (uri_rdf_type) (uri_rdf__1) (uri_rdf_Property))) % 4.67/4.88 (zenon_X0 != (uri_ex_Person)) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_ContainerMembershipProperty)) != (iext (uri_rdf_type) (uri_rdf_value) (uri_rdf_Property))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_hasAncestor)) != (iext (uri_rdfs_range) (uri_rdf__2) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Resource)) != (iext (uri_rdf_type) (uri_ex_alice) (uri_ex_Person))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Class)) != (iext (uri_rdfs_range) (uri_rdf_rest) (uri_rdf_List))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Container)) != (iext (uri_rdfs_domain) (uri_rdf__2) (uri_rdfs_Resource))) % 4.67/4.88 ((uri_rdfs_Literal) != (uri_rdfs_Statement)) % 4.67/4.88 ((iext (uri_rdf_type) (uri_rdf__3) (uri_rdf_Property)) = (true)) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_hasAncestor)) != (iext (uri_rdfs_range) (uri_rdfs_subPropertyOf) (uri_rdf_Property))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdf_Property)) != (iext (uri_rdfs_range) (uri_rdf__2) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_seeAlso)) != (iext (uri_rdfs_domain) (uri_rdf__3) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_Person)) != (iext (uri_rdfs_domain) (uri_rdfs_domain) (uri_rdf_Property))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Statement)) != (iext (uri_rdfs_domain) (uri_rdf_type) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Statement)) != (iext (uri_rdf_type) (uri_rdf_Property) (uri_rdfs_Class))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_owl_TransitiveProperty)) != (iext (uri_rdfs_domain) (uri_rdfs_subPropertyOf) (uri_rdf_Property))) % 4.67/4.88 ((uri_ex_bob) != (uri_rdf_Bag)) % 4.67/4.88 ((uri_owl_Restriction) != (uri_ex_bob)) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdf_Property)) != (true)) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_bob)) != (iext (uri_rdf_type) (uri_rdf_value) (uri_rdf_Property))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_hasAncestor)) != (iext (uri_rdfs_domain) (uri_rdfs_label) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Datatype)) != (iext (uri_rdfs_range) (uri_rdfs_label) (uri_rdfs_Literal))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_Person)) != (iext (uri_rdfs_domain) (uri_rdf_rest) (uri_rdf_List))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_Person)) != (iext (uri_rdf_type) (uri_rdf_XMLLiteral) (uri_rdfs_Datatype))) % 4.67/4.88 ((uri_rdf_List) != (uri_rdfs_Statement)) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Statement)) != (iext (uri_rdfs_range) (uri_rdf_subject) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Literal)) != (iext (uri_rdfs_range) (uri_rdfs_subPropertyOf) (uri_rdf_Property))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_owl_Restriction)) != (iext (uri_rdf_type) (uri_rdf__3) (uri_rdf_Property))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_owl_TransitiveProperty)) != (iext (uri_rdfs_domain) (uri_rdfs_domain) (uri_rdf_Property))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_ContainerMembershipProperty)) != (iext (uri_owl_onProperty) (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z) (uri_ex_hasAncestor))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_owl_TransitiveProperty)) != (iext (uri_rdfs_subClassOf) (uri_rdf_Bag) (uri_rdfs_Container))) % 4.67/4.88 ((iext (uri_rdfs_domain) (uri_rdfs_label) (uri_rdfs_Resource)) = (true)) % 4.67/4.88 ((uri_ex_bob) != (uri_rdf__3)) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Resource)) != (iext (uri_rdf_type) (uri_rdf__1) (uri_rdf_Property))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z)) != (iext (uri_rdf_type) (uri_rdf__3) (uri_rdf_Property))) % 4.67/4.88 ((uri_ex_bob) != (uri_rdf_object)) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Resource)) != (iext (uri_rdf_type) (uri_rdf_nil) (uri_rdf_List))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Statement)) != (iext (uri_rdfs_range) (uri_rdf_type) (uri_rdfs_Class))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_owl_TransitiveProperty)) != (iext (uri_rdfs_domain) (uri_rdf_predicate) (uri_rdfs_Statement))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z)) != (iext (uri_rdfs_range) (uri_rdfs_subClassOf) (uri_rdfs_Class))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_Person)) != (iext (uri_rdf_type) (uri_rdf__1) (uri_rdfs_ContainerMembershipProperty))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) zenon_X0) != (iext (uri_rdfs_range) (uri_rdfs_subPropertyOf) (uri_rdf_Property))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_Person)) != (iext (uri_rdf_type) (uri_ex_alice) (uri_ex_Person))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Datatype)) != (iext (uri_rdfs_range) (uri_rdf_type) (uri_rdfs_Class))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Statement)) != (iext (uri_rdf_type) (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z) (uri_owl_Restriction))) % 4.67/4.88 ((uri_ex_bob) != (uri_ex_alice)) % 4.67/4.88 ((iext (uri_rdfs_domain) (uri_rdf_object) (uri_rdfs_Statement)) = (true)) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) zenon_X0) != (iext (uri_rdfs_range) (uri_rdf_type) (uri_rdfs_Class))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Resource)) != (iext (uri_rdf_type) (uri_rdf_first) (uri_rdf_Property))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Datatype)) != (iext (uri_rdfs_range) (uri_rdf__2) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_seeAlso)) != (iext (uri_rdfs_domain) (uri_rdfs_isDefinedBy) (uri_rdfs_Resource))) % 4.67/4.88 ((tuple (iext (uri_ex_hasAncestor) (uri_ex_alice) zenon_X0) (iext (uri_ex_hasAncestor) (uri_ex_bob) zenon_X0)) != (tuple (true) (true))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdf_List)) != (iext (uri_rdfs_range) (uri_rdfs_domain) (uri_rdfs_Class))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) zenon_X0) != (iext (uri_rdfs_range) (uri_rdfs_seeAlso) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) zenon_X0) != (iext (uri_rdf_type) (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z) (uri_owl_Restriction))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Resource)) != (iext (uri_rdfs_subClassOf) (uri_rdfs_Seq) (uri_rdfs_Container))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z)) != (iext (uri_rdf_type) (uri_rdf__1) (uri_rdf_Property))) % 4.67/4.88 ((uri_rdfs_Resource) != (uri_ex_Person)) % 4.67/4.88 ((uri_rdfs_Datatype) != (literal_typed (dat_str_1) (uri_xsd_nonNegativeInteger))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_bob)) != (iext (uri_rdfs_domain) (uri_rdfs_subClassOf) (uri_rdfs_Class))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Class)) != (iext (uri_rdfs_range) (uri_rdfs_subClassOf) (uri_rdfs_Class))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_bob)) != (iext (uri_rdfs_range) (uri_rdf_rest) (uri_rdf_List))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_hasAncestor)) != (iext (uri_rdfs_subClassOf) (uri_rdf_Alt) (uri_rdfs_Container))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdf_List)) != (iext (uri_rdfs_subClassOf) (uri_ex_Person) (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Statement)) != (iext (uri_rdfs_subClassOf) (uri_rdf_Bag) (uri_rdfs_Container))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_owl_Restriction)) != (iext (uri_rdf_type) (uri_ex_hasAncestor) (uri_owl_TransitiveProperty))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_seeAlso)) != (iext (uri_rdfs_domain) (uri_rdfs_seeAlso) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_seeAlso)) != (iext (uri_rdfs_subClassOf) (uri_rdf_Alt) (uri_rdfs_Container))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_seeAlso)) != (iext (uri_rdfs_subClassOf) (uri_rdfs_Seq) (uri_rdfs_Container))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_hasAncestor)) != (iext (uri_rdf_type) (uri_ex_bob) (uri_ex_Person))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Literal)) != (iext (uri_rdfs_domain) (uri_rdf__3) (uri_rdfs_Resource))) % 4.67/4.88 ((uri_rdfs_seeAlso) != (uri_rdfs_Container)) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Literal)) != (iext (uri_rdfs_subClassOf) (uri_rdfs_ContainerMembershipProperty) (uri_rdf_Property))) % 4.67/4.88 ((uri_rdfs_Class) != (literal_typed (dat_str_1) (uri_xsd_nonNegativeInteger))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_owl_TransitiveProperty)) != (iext (uri_rdfs_range) (uri_rdfs_label) (uri_rdfs_Literal))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdf_Property)) != (iext (uri_rdfs_range) (uri_rdf_predicate) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_rdfs_range) (uri_rdf__2) (uri_rdfs_Resource)) = (true)) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) zenon_X0) != (iext (uri_rdfs_range) (uri_rdfs_range) (uri_rdfs_Class))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Resource)) != (iext (uri_owl_minCardinality) (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z) (literal_typed (dat_str_1) (uri_xsd_nonNegativeInteger)))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Statement)) != (iext (uri_rdfs_range) (uri_rdfs_seeAlso) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_Person)) != (iext (uri_rdfs_domain) (uri_rdf__1) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (literal_typed (dat_str_1) (uri_xsd_nonNegativeInteger))) != (iext (uri_rdfs_range) (uri_rdf_rest) (uri_rdf_List))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_owl_Restriction)) != (iext (uri_rdf_type) (uri_rdf_XMLLiteral) (uri_rdfs_Datatype))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_hasAncestor)) != (iext (uri_rdfs_range) (uri_rdf_type) (uri_rdfs_Class))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Literal)) != (iext (uri_rdfs_range) (uri_rdf__1) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_rdfs_subClassOf) (uri_rdf_Alt) (uri_rdfs_Container)) = (true)) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z)) != (iext (uri_rdfs_domain) (uri_rdfs_subPropertyOf) (uri_rdf_Property))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_seeAlso)) != (iext (uri_rdfs_subClassOf) (uri_rdf_XMLLiteral) (uri_rdfs_Literal))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Container)) != (iext (uri_rdfs_domain) (uri_rdf_predicate) (uri_rdfs_Statement))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_ContainerMembershipProperty)) != (iext (uri_rdfs_range) (uri_rdfs_range) (uri_rdfs_Class))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z)) != (iext (uri_owl_minCardinality) (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z) (literal_typed (dat_str_1) (uri_xsd_nonNegativeInteger)))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Statement)) != (iext (uri_rdf_type) (uri_ex_alice) (uri_ex_Person))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_Person)) != (iext (uri_rdfs_subClassOf) (uri_rdfs_Seq) (uri_rdfs_Container))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z)) != (iext (uri_rdfs_range) (uri_rdfs_comment) (uri_rdfs_Literal))) % 4.67/4.88 ((tuple (iext (uri_ex_hasAncestor) (uri_ex_alice) (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z)) (iext (uri_ex_hasAncestor) (uri_ex_bob) (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z))) != (tuple (true) (true))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Container)) != (iext (uri_rdf_type) (uri_rdf__3) (uri_rdfs_ContainerMembershipProperty))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_bob)) != (iext (uri_rdf_type) (uri_rdf_type) (uri_rdf_Property))) % 4.67/4.88 ((iext (uri_rdf_type) (uri_rdf_nil) (uri_rdf_List)) = (true)) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_owl_TransitiveProperty)) != (iext (uri_rdfs_domain) (uri_rdf_first) (uri_rdf_List))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Resource)) != (iext (uri_rdfs_domain) (uri_rdf_type) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_rdf_type) (uri_rdf_type) (uri_rdf_Property)) = (true)) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) zenon_X0) != (iext (uri_rdfs_domain) (uri_rdfs_label) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Literal)) != (iext (uri_rdfs_range) (uri_rdfs_seeAlso) (uri_rdfs_Resource))) % 4.67/4.88 ((uri_ex_bob) != (uri_rdfs_subClassOf)) % 4.67/4.88 ((uri_rdf_Property) != (uri_owl_TransitiveProperty)) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Resource)) != (iext (uri_rdfs_domain) (uri_rdfs_domain) (uri_rdf_Property))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdf_Property)) != (iext (uri_rdfs_domain) (uri_rdfs_label) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_hasAncestor)) != (iext (uri_rdfs_domain) (uri_rdf_rest) (uri_rdf_List))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdf_Property)) != (iext (uri_rdfs_range) (uri_rdfs_subPropertyOf) (uri_rdf_Property))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Statement)) != (iext (uri_rdfs_range) (uri_rdfs_label) (uri_rdfs_Literal))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_Person)) != (iext (uri_rdfs_range) (uri_rdf__2) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_bob)) != (iext (uri_rdf_type) (uri_rdf__2) (uri_rdfs_ContainerMembershipProperty))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Container)) != (iext (uri_rdfs_range) (uri_rdfs_seeAlso) (uri_rdfs_Resource))) % 4.67/4.88 ((uri_ex_bob) != (uri_rdfs_domain)) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdf_List)) != (iext (uri_rdfs_domain) (uri_rdf_predicate) (uri_rdfs_Statement))) % 4.67/4.88 ((uri_rdfs_Literal) != (uri_rdfs_seeAlso)) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Datatype)) != (iext (uri_rdf_type) (uri_ex_hasAncestor) (uri_owl_TransitiveProperty))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Literal)) != (iext (uri_rdfs_range) (uri_rdf_type) (uri_rdfs_Class))) % 4.67/4.88 ((uri_ex_bob) != (uri_rdf_nil)) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Resource)) != (iext (uri_rdfs_range) (uri_rdf__1) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Container)) != (iext (uri_rdfs_range) (uri_rdf_predicate) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Literal)) != (iext (uri_rdfs_domain) (uri_rdfs_comment) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_owl_Restriction)) != (iext (uri_rdfs_range) (uri_rdf_first) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_owl_Restriction)) != (iext (uri_rdfs_domain) (uri_rdf__3) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) zenon_X0) != (iext (uri_rdfs_domain) (uri_rdfs_comment) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_bob)) != (iext (uri_rdfs_range) (uri_rdfs_member) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdf_List)) != (iext (uri_rdfs_subPropertyOf) (uri_rdfs_isDefinedBy) (uri_rdfs_seeAlso))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Statement)) != (iext (uri_rdf_type) (uri_rdf__2) (uri_rdfs_ContainerMembershipProperty))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdf_Property)) != (iext (uri_rdfs_subClassOf) (uri_rdfs_ContainerMembershipProperty) (uri_rdf_Property))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Resource)) != (iext (uri_rdfs_domain) (uri_rdf__2) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Class)) != (iext (uri_rdfs_domain) (uri_rdfs_subPropertyOf) (uri_rdf_Property))) % 4.67/4.88 ((iext (uri_rdf_type) (uri_rdf_subject) (uri_rdf_Property)) = (true)) % 4.67/4.88 ((uri_rdf_List) != (uri_rdfs_Container)) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (literal_typed (dat_str_1) (uri_xsd_nonNegativeInteger))) != (iext (uri_rdfs_subClassOf) (uri_rdfs_Seq) (uri_rdfs_Container))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) zenon_X0) != (iext (uri_rdf_type) (uri_rdf_XMLLiteral) (uri_rdfs_Datatype))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Resource)) != (iext (uri_rdfs_range) (uri_rdf_rest) (uri_rdf_List))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Statement)) != (iext (uri_rdfs_domain) (uri_rdfs_member) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_owl_TransitiveProperty)) != (iext (uri_rdf_type) (uri_rdf__3) (uri_rdf_Property))) % 4.67/4.88 ((iext (uri_rdfs_range) (uri_rdf_predicate) (uri_rdfs_Resource)) = (true)) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Resource)) != (iext (uri_rdfs_range) (uri_rdf_value) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_seeAlso)) != (iext (uri_rdf_type) (uri_rdf_object) (uri_rdf_Property))) % 4.67/4.88 ((iext (uri_rdfs_range) (uri_rdf__3) (uri_rdfs_Resource)) = (true)) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdf_Property)) != (iext (uri_rdfs_subClassOf) (uri_rdfs_Seq) (uri_rdfs_Container))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Literal)) != (iext (uri_rdf_type) (uri_ex_alice) (uri_ex_Person))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_bob)) != (iext (uri_rdfs_subClassOf) (uri_rdf_Bag) (uri_rdfs_Container))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Container)) != (iext (uri_rdfs_range) (uri_rdfs_subClassOf) (uri_rdfs_Class))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdf_List)) != (iext (uri_rdfs_domain) (uri_rdfs_member) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_ContainerMembershipProperty)) != (iext (uri_rdfs_range) (uri_rdfs_isDefinedBy) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_bob)) != (iext (uri_rdfs_subPropertyOf) (uri_rdfs_isDefinedBy) (uri_rdfs_seeAlso))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_owl_TransitiveProperty)) != (iext (uri_rdf_type) (uri_rdf_value) (uri_rdf_Property))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_ContainerMembershipProperty)) != (iext (uri_rdfs_range) (uri_rdfs_comment) (uri_rdfs_Literal))) % 4.67/4.88 ((uri_ex_bob) != (uri_rdfs_range)) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z)) != (iext (uri_rdf_type) (uri_ex_hasAncestor) (uri_owl_TransitiveProperty))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_seeAlso)) != (iext (uri_owl_minCardinality) (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z) (literal_typed (dat_str_1) (uri_xsd_nonNegativeInteger)))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Container)) != (iext (uri_rdfs_domain) (uri_rdf__1) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_rdfs_range) (uri_rdfs_label) (uri_rdfs_Literal)) = (true)) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) zenon_X0) != (iext (uri_rdfs_range) (uri_rdf__1) (uri_rdfs_Resource))) % 4.67/4.88 ((uri_rdf_List) != (literal_typed (dat_str_1) (uri_xsd_nonNegativeInteger))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (literal_typed (dat_str_1) (uri_xsd_nonNegativeInteger))) != (iext (uri_rdfs_domain) (uri_rdfs_member) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_Person)) != (true)) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdf_Property)) != (iext (uri_rdfs_domain) (uri_rdf_rest) (uri_rdf_List))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_owl_TransitiveProperty)) != (iext (uri_rdf_type) (uri_rdf__2) (uri_rdf_Property))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_ContainerMembershipProperty)) != (iext (uri_rdf_type) (uri_ex_bob) (uri_ex_Person))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (literal_typed (dat_str_1) (uri_xsd_nonNegativeInteger))) != (iext (uri_rdf_type) (uri_rdf_first) (uri_rdf_Property))) % 4.67/4.88 ((uri_ex_bob) != (uri_rdf_subject)) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Resource)) != (iext (uri_owl_onProperty) (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z) (uri_ex_hasAncestor))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) zenon_X0) != (iext (uri_rdf_type) (uri_rdf_object) (uri_rdf_Property))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_owl_Restriction)) != (iext (uri_rdfs_range) (uri_rdf_subject) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z)) != (iext (uri_rdfs_domain) (uri_rdf_rest) (uri_rdf_List))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_ContainerMembershipProperty)) != (iext (uri_rdfs_range) (uri_rdfs_subPropertyOf) (uri_rdf_Property))) % 4.67/4.88 ((iext (uri_rdfs_domain) (uri_rdf__1) (uri_rdfs_Resource)) = (true)) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Datatype)) != (iext (uri_rdf_type) (uri_rdf_subject) (uri_rdf_Property))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) zenon_X0) != (iext (uri_rdfs_domain) (uri_rdfs_seeAlso) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdf_Property)) != (iext (uri_rdfs_range) (uri_rdf_value) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_ContainerMembershipProperty)) != (iext (uri_rdfs_range) (uri_rdf_predicate) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_Person)) != (iext (uri_ex_hasAncestor) (uri_ex_alice) (uri_ex_bob))) % 4.67/4.88 ((uri_rdfs_Literal) != (uri_ex_bob)) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_owl_TransitiveProperty)) != (iext (uri_rdfs_subClassOf) (uri_rdf_XMLLiteral) (uri_rdfs_Literal))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Resource)) != (iext (uri_rdfs_subClassOf) (uri_rdf_Bag) (uri_rdfs_Container))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_hasAncestor)) != (iext (uri_rdf_type) (uri_ex_alice) (uri_ex_Person))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_bob)) != (iext (uri_rdfs_domain) (uri_rdf_first) (uri_rdf_List))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Class)) != (iext (uri_rdfs_domain) (uri_rdfs_subClassOf) (uri_rdfs_Class))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdf_List)) != (iext (uri_rdfs_range) (uri_rdf_value) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_seeAlso)) != (iext (uri_rdfs_range) (uri_rdf__3) (uri_rdfs_Resource))) % 4.67/4.88 ((uri_rdfs_Class) != (uri_ex_bob)) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z)) != (iext (uri_rdfs_domain) (uri_rdfs_comment) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z)) != (iext (uri_rdfs_range) (uri_rdf_predicate) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_bob)) != (iext (uri_rdfs_range) (uri_rdf__2) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) zenon_X0) != (iext (uri_rdfs_range) (uri_rdfs_comment) (uri_rdfs_Literal))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdf_List)) != (iext (uri_rdfs_domain) (uri_rdfs_isDefinedBy) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdf_List)) != (iext (uri_rdfs_range) (uri_rdf_rest) (uri_rdf_List))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdf_Property)) != (iext (uri_rdf_type) (uri_rdf_rest) (uri_rdf_Property))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_ContainerMembershipProperty)) != (iext (uri_rdf_type) (uri_ex_hasAncestor) (uri_owl_TransitiveProperty))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdf_Property)) != (iext (uri_rdf_type) (uri_rdf_XMLLiteral) (uri_rdfs_Datatype))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Statement)) != (iext (uri_ex_hasAncestor) (uri_ex_alice) (uri_ex_bob))) % 4.67/4.88 ((uri_rdf_List) != (uri_ex_Person)) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z)) != (iext (uri_rdfs_subClassOf) (uri_rdf_XMLLiteral) (uri_rdfs_Literal))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_seeAlso)) != (iext (uri_rdfs_domain) (uri_rdf__2) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Literal)) != (iext (uri_rdf_type) (uri_rdf__1) (uri_rdf_Property))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (literal_typed (dat_str_1) (uri_xsd_nonNegativeInteger))) != (iext (uri_rdfs_range) (uri_rdf__3) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (literal_typed (dat_str_1) (uri_xsd_nonNegativeInteger))) != (iext (uri_rdfs_range) (uri_rdf_type) (uri_rdfs_Class))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (literal_typed (dat_str_1) (uri_xsd_nonNegativeInteger))) != (iext (uri_rdfs_domain) (uri_rdfs_isDefinedBy) (uri_rdfs_Resource))) % 4.67/4.88 (zenon_X0 != (uri_rdfs_Datatype)) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_owl_Restriction)) != (iext (uri_rdfs_domain) (uri_rdfs_isDefinedBy) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Statement)) != (iext (uri_rdfs_subClassOf) (uri_ex_Person) (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z))) % 4.67/4.88 ((uri_ex_bob) != (uri_rdfs_comment)) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Statement)) != (iext (uri_rdf_type) (uri_ex_hasAncestor) (uri_owl_TransitiveProperty))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_seeAlso)) != (iext (uri_rdfs_subClassOf) (uri_rdfs_ContainerMembershipProperty) (uri_rdf_Property))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_seeAlso)) != (iext (uri_rdfs_range) (uri_rdfs_subClassOf) (uri_rdfs_Class))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Container)) != (iext (uri_rdfs_range) (uri_rdf__1) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_owl_Restriction)) != (iext (uri_rdf_type) (uri_ex_bob) (uri_ex_Person))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z)) != (iext (uri_rdfs_range) (uri_rdf_rest) (uri_rdf_List))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_Person)) != (iext (uri_rdfs_range) (uri_rdfs_seeAlso) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (literal_typed (dat_str_1) (uri_xsd_nonNegativeInteger))) != (iext (uri_rdf_type) (uri_rdf__1) (uri_rdf_Property))) % 4.67/4.88 ((iext (uri_rdfs_domain) (uri_rdfs_comment) (uri_rdfs_Resource)) = (true)) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_hasAncestor)) != (iext (uri_rdf_type) (uri_ex_hasAncestor) (uri_owl_TransitiveProperty))) % 4.67/4.88 ((iext (uri_rdfs_domain) (uri_rdfs_subPropertyOf) (uri_rdf_Property)) = (true)) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) zenon_X0) != (iext (uri_rdfs_subClassOf) (uri_rdfs_Datatype) (uri_rdfs_Class))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z)) != (iext (uri_rdf_type) (uri_ex_bob) (uri_ex_Person))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_seeAlso)) != (iext (uri_rdfs_domain) (uri_rdfs_member) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_hasAncestor)) != (iext (uri_rdfs_domain) (uri_rdf_object) (uri_rdfs_Statement))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Resource)) != (iext (uri_rdf_type) (uri_rdf_object) (uri_rdf_Property))) % 4.67/4.88 ((uri_rdfs_Resource) != (uri_owl_Restriction)) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) zenon_X0) != (iext (uri_rdf_type) (uri_rdf__3) (uri_rdfs_ContainerMembershipProperty))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Datatype)) != (iext (uri_rdf_type) (uri_rdf_nil) (uri_rdf_List))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_owl_Restriction)) != (iext (uri_rdfs_subClassOf) (uri_rdf_Alt) (uri_rdfs_Container))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Statement)) != (iext (uri_rdfs_domain) (uri_rdf_subject) (uri_rdfs_Statement))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Literal)) != (iext (uri_rdfs_range) (uri_rdf__3) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_Person)) != (iext (uri_rdfs_domain) (uri_rdfs_seeAlso) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_rdfs_subClassOf) (uri_rdfs_Datatype) (uri_rdfs_Class)) = (true)) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) zenon_X0) != (iext (uri_rdfs_domain) (uri_rdf_rest) (uri_rdf_List))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Literal)) != (iext (uri_rdfs_domain) (uri_rdf_subject) (uri_rdfs_Statement))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (literal_typed (dat_str_1) (uri_xsd_nonNegativeInteger))) != (iext (uri_rdf_type) (uri_rdf_nil) (uri_rdf_List))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_Person)) != (iext (uri_rdf_type) (uri_rdf_subject) (uri_rdf_Property))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Literal)) != (iext (uri_rdf_type) (uri_ex_bob) (uri_ex_Person))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Container)) != (iext (uri_rdfs_domain) (uri_rdfs_range) (uri_rdf_Property))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_ContainerMembershipProperty)) != (iext (uri_rdfs_range) (uri_rdf_type) (uri_rdfs_Class))) % 4.67/4.88 ((iext (uri_rdf_type) (uri_rdf_object) (uri_rdf_Property)) = (true)) % 4.67/4.88 (zenon_X0 != (uri_rdfs_Statement)) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdf_List)) != (iext (uri_rdfs_domain) (uri_rdf_value) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Statement)) != (iext (uri_rdfs_range) (uri_rdf__3) (uri_rdfs_Resource))) % 4.67/4.88 ((uri_rdfs_Statement) != (uri_ex_Person)) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_owl_TransitiveProperty)) != (iext (uri_rdfs_domain) (uri_rdf_object) (uri_rdfs_Statement))) % 4.67/4.88 ((iext (uri_rdf_type) (uri_rdf__2) (uri_rdf_Property)) = (true)) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Resource)) != (iext (uri_rdfs_domain) (uri_rdfs_subPropertyOf) (uri_rdf_Property))) % 4.67/4.88 ((uri_rdfs_Literal) != (uri_ex_hasAncestor)) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) zenon_X0) != (iext (uri_rdfs_domain) (uri_rdf__1) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_seeAlso)) != (iext (uri_rdfs_range) (uri_rdf__2) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_Person)) != (iext (uri_rdfs_range) (uri_rdf__1) (uri_rdfs_Resource))) % 4.67/4.88 ((tuple (iext (uri_ex_hasAncestor) (uri_ex_alice) (uri_rdfs_Literal)) (iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Literal))) != (tuple (true) (true))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_owl_Restriction)) != (iext (uri_rdfs_domain) (uri_rdf_first) (uri_rdf_List))) % 4.67/4.88 ((iext (uri_rdfs_domain) (uri_rdf__3) (uri_rdfs_Resource)) = (true)) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) zenon_X0) != (iext (uri_rdfs_subClassOf) (uri_rdf_Bag) (uri_rdfs_Container))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_hasAncestor)) != (iext (uri_rdf_type) (uri_rdf_nil) (uri_rdf_List))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) zenon_X0) != (iext (uri_rdfs_range) (uri_rdf__3) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Statement)) != (iext (uri_rdfs_domain) (uri_rdfs_isDefinedBy) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) zenon_X0) != (iext (uri_rdfs_range) (uri_rdf__2) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Resource)) != (iext (uri_rdfs_subClassOf) (uri_rdfs_ContainerMembershipProperty) (uri_rdf_Property))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Datatype)) != (iext (uri_rdfs_domain) (uri_rdfs_seeAlso) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (literal_typed (dat_str_1) (uri_xsd_nonNegativeInteger))) != (iext (uri_rdf_type) (uri_rdf__3) (uri_rdfs_ContainerMembershipProperty))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_bob)) != (iext (uri_rdf_type) (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z) (uri_owl_Restriction))) % 4.67/4.88 ((uri_ex_bob) != (uri_rdf_Alt)) % 4.67/4.88 ((iext (uri_rdfs_range) (uri_rdf_value) (uri_rdfs_Resource)) = (true)) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_ContainerMembershipProperty)) != (iext (uri_rdf_type) (uri_rdf_first) (uri_rdf_Property))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_Person)) != (iext (uri_rdfs_range) (uri_rdf_predicate) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_owl_Restriction)) != (iext (uri_owl_onProperty) (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z) (uri_ex_hasAncestor))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (literal_typed (dat_str_1) (uri_xsd_nonNegativeInteger))) != (iext (uri_rdfs_domain) (uri_rdfs_subPropertyOf) (uri_rdf_Property))) % 4.67/4.88 ((tuple (iext (uri_ex_hasAncestor) (uri_ex_alice) (uri_rdfs_Resource)) (iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Resource))) != (tuple (true) (true))) % 4.67/4.88 ((uri_rdfs_Resource) != (uri_rdfs_Class)) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdf_Property)) != (iext (uri_rdfs_subClassOf) (uri_rdf_XMLLiteral) (uri_rdfs_Literal))) % 4.67/4.88 ((uri_rdfs_seeAlso) != (uri_rdfs_Class)) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Class)) != (iext (uri_rdfs_domain) (uri_rdf_object) (uri_rdfs_Statement))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Statement)) != (iext (uri_owl_minCardinality) (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z) (literal_typed (dat_str_1) (uri_xsd_nonNegativeInteger)))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Class)) != (iext (uri_rdfs_subClassOf) (uri_rdfs_ContainerMembershipProperty) (uri_rdf_Property))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z)) != (iext (uri_rdfs_range) (uri_rdfs_member) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_Person)) != (iext (uri_rdfs_range) (uri_rdfs_member) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_owl_Restriction)) != (iext (uri_rdf_type) (uri_rdf_first) (uri_rdf_Property))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Class)) != (iext (uri_rdfs_domain) (uri_rdf__2) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_Person)) != (iext (uri_rdf_type) (uri_rdf__3) (uri_rdfs_ContainerMembershipProperty))) % 4.67/4.88 ((uri_rdf_Property) != (uri_owl_Restriction)) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdf_List)) != (iext (uri_rdfs_domain) (uri_rdfs_subPropertyOf) (uri_rdf_Property))) % 4.67/4.88 ((uri_rdfs_Literal) != (uri_rdfs_Resource)) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_owl_Restriction)) != (iext (uri_rdfs_domain) (uri_rdf__1) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Statement)) != (iext (uri_rdfs_range) (uri_rdf_rest) (uri_rdf_List))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_bob)) != (iext (uri_rdfs_domain) (uri_rdf_predicate) (uri_rdfs_Statement))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_hasAncestor)) != (iext (uri_rdf_type) (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z) (uri_owl_Restriction))) % 4.67/4.88 ((iext (uri_rdfs_range) (uri_rdf__1) (uri_rdfs_Resource)) = (true)) % 4.67/4.88 ((uri_rdf_Property) != (uri_rdf_List)) % 4.67/4.88 ((uri_rdfs_Literal) != (uri_owl_Restriction)) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Resource)) != (iext (uri_rdfs_range) (uri_rdfs_domain) (uri_rdfs_Class))) % 4.67/4.88 ((uri_rdfs_Container) != (uri_ex_hasAncestor)) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Literal)) != (iext (uri_rdfs_range) (uri_rdf_subject) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (literal_typed (dat_str_1) (uri_xsd_nonNegativeInteger))) != (iext (uri_rdfs_range) (uri_rdfs_label) (uri_rdfs_Literal))) % 4.67/4.88 (zenon_X0 != (uri_rdf_List)) % 4.67/4.88 ((tuple (iext (uri_ex_hasAncestor) (uri_ex_alice) (uri_ex_bob)) (iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_bob))) != (tuple (true) (true))) % 4.67/4.88 ((iext (uri_rdf_type) (uri_ex_hasAncestor) (uri_owl_TransitiveProperty)) = (true)) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Resource)) != (iext (uri_rdfs_domain) (uri_rdf_rest) (uri_rdf_List))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_seeAlso)) != (iext (uri_rdfs_subClassOf) (uri_rdf_Bag) (uri_rdfs_Container))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_owl_TransitiveProperty)) != (iext (uri_rdfs_range) (uri_rdf_predicate) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdf_Property)) != (iext (uri_rdfs_domain) (uri_rdf_first) (uri_rdf_List))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Class)) != (iext (uri_rdf_type) (uri_rdf_Property) (uri_rdfs_Class))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Container)) != (iext (uri_rdfs_range) (uri_rdfs_subPropertyOf) (uri_rdf_Property))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Resource)) != (iext (uri_rdfs_range) (uri_rdf_subject) (uri_rdfs_Resource))) % 4.67/4.88 ((uri_rdfs_Class) != (uri_owl_TransitiveProperty)) % 4.67/4.88 ((uri_rdfs_Container) != (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z)) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdf_Property)) != (iext (uri_rdf_type) (uri_rdf_object) (uri_rdf_Property))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_owl_TransitiveProperty)) != (iext (uri_rdfs_range) (uri_rdf_value) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_ContainerMembershipProperty)) != (iext (uri_rdfs_domain) (uri_rdf_first) (uri_rdf_List))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) zenon_X0) != (iext (uri_rdf_type) (uri_rdf__3) (uri_rdf_Property))) % 4.67/4.88 ((iext (uri_rdf_type) (uri_rdf_rest) (uri_rdf_Property)) = (true)) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Class)) != (iext (uri_rdfs_domain) (uri_rdfs_isDefinedBy) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Container)) != (iext (uri_rdf_type) (uri_rdf_object) (uri_rdf_Property))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (literal_typed (dat_str_1) (uri_xsd_nonNegativeInteger))) != (iext (uri_rdfs_domain) (uri_rdfs_range) (uri_rdf_Property))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Statement)) != (iext (uri_rdfs_domain) (uri_rdfs_domain) (uri_rdf_Property))) % 4.67/4.88 ((iext (uri_rdfs_range) (uri_rdf_first) (uri_rdfs_Resource)) = (true)) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdf_Property)) != (iext (uri_rdfs_domain) (uri_rdf__3) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Resource)) != (iext (uri_rdf_type) (uri_rdf_Property) (uri_rdfs_Class))) % 4.67/4.88 ((uri_rdfs_seeAlso) != (literal_typed (dat_str_1) (uri_xsd_nonNegativeInteger))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_Person)) != (iext (uri_rdfs_domain) (uri_rdf_value) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) zenon_X0) != (true)) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Datatype)) != (iext (uri_rdf_type) (uri_ex_bob) (uri_ex_Person))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdf_List)) != (iext (uri_rdf_type) (uri_rdf__2) (uri_rdfs_ContainerMembershipProperty))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdf_List)) != (iext (uri_rdfs_range) (uri_rdf__1) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_seeAlso)) != (iext (uri_rdf_type) (uri_rdf__1) (uri_rdfs_ContainerMembershipProperty))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_bob)) != (iext (uri_rdfs_domain) (uri_rdfs_subPropertyOf) (uri_rdf_Property))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Container)) != (iext (uri_rdfs_domain) (uri_rdfs_comment) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_owl_TransitiveProperty)) != (iext (uri_rdf_type) (uri_rdf__3) (uri_rdfs_ContainerMembershipProperty))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_ContainerMembershipProperty)) != (iext (uri_rdfs_subClassOf) (uri_rdf_XMLLiteral) (uri_rdfs_Literal))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdf_Property)) != (iext (uri_ex_hasAncestor) (uri_ex_alice) (uri_ex_bob))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_seeAlso)) != (iext (uri_rdfs_range) (uri_rdf_value) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_seeAlso)) != (iext (uri_rdfs_range) (uri_rdfs_domain) (uri_rdfs_Class))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_bob)) != (iext (uri_rdfs_range) (uri_rdf__1) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z)) != (iext (uri_rdfs_subClassOf) (uri_rdf_Alt) (uri_rdfs_Container))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdf_List)) != (iext (uri_rdfs_subClassOf) (uri_rdf_Bag) (uri_rdfs_Container))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Resource)) != (iext (uri_rdfs_subClassOf) (uri_rdf_Alt) (uri_rdfs_Container))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Statement)) != (iext (uri_rdf_type) (uri_rdf_subject) (uri_rdf_Property))) % 4.67/4.88 ((uri_rdfs_Container) != (literal_typed (dat_str_1) (uri_xsd_nonNegativeInteger))) % 4.67/4.88 ((uri_rdfs_Container) != (uri_ex_Person)) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (literal_typed (dat_str_1) (uri_xsd_nonNegativeInteger))) != (iext (uri_rdf_type) (uri_rdf_value) (uri_rdf_Property))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Literal)) != (true)) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdf_Property)) != (iext (uri_rdf_type) (uri_ex_alice) (uri_ex_Person))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_owl_Restriction)) != (iext (uri_rdfs_range) (uri_rdfs_subClassOf) (uri_rdfs_Class))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z)) != (iext (uri_rdf_type) (uri_rdf_subject) (uri_rdf_Property))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdf_Property)) != (iext (uri_rdf_type) (uri_rdf__3) (uri_rdf_Property))) % 4.67/4.88 ((tuple (iext (uri_ex_hasAncestor) (uri_ex_alice) (uri_owl_TransitiveProperty)) (iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_owl_TransitiveProperty))) != (tuple (true) (true))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Container)) != (iext (uri_rdfs_domain) (uri_rdf_object) (uri_rdfs_Statement))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_ContainerMembershipProperty)) != (iext (uri_rdfs_range) (uri_rdf__2) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_bob)) != (iext (uri_rdfs_range) (uri_rdfs_subClassOf) (uri_rdfs_Class))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (literal_typed (dat_str_1) (uri_xsd_nonNegativeInteger))) != (iext (uri_rdf_type) (uri_rdf__1) (uri_rdfs_ContainerMembershipProperty))) % 4.67/4.88 ((iext (uri_rdfs_range) (uri_rdf_type) (uri_rdfs_Class)) = (true)) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Statement)) != (iext (uri_rdfs_range) (uri_rdfs_range) (uri_rdfs_Class))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_Person)) != (iext (uri_rdfs_range) (uri_rdfs_subPropertyOf) (uri_rdf_Property))) % 4.67/4.88 ((uri_rdf_Property) != (uri_ex_bob)) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Literal)) != (iext (uri_rdfs_subPropertyOf) (uri_rdfs_isDefinedBy) (uri_rdfs_seeAlso))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Container)) != (iext (uri_rdfs_domain) (uri_rdfs_label) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_hasAncestor)) != (iext (uri_rdfs_domain) (uri_rdf__2) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_Person)) != (iext (uri_rdfs_subClassOf) (uri_rdf_XMLLiteral) (uri_rdfs_Literal))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_ContainerMembershipProperty)) != (iext (uri_rdf_type) (uri_rdf__1) (uri_rdfs_ContainerMembershipProperty))) % 4.67/4.88 ((uri_ex_bob) != (uri_rdfs_seeAlso)) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Class)) != (iext (uri_rdfs_domain) (uri_rdfs_label) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_owl_TransitiveProperty)) != (iext (uri_rdfs_range) (uri_rdfs_comment) (uri_rdfs_Literal))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_ContainerMembershipProperty)) != (iext (uri_rdfs_range) (uri_rdfs_domain) (uri_rdfs_Class))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Datatype)) != (iext (uri_rdf_type) (uri_rdf_object) (uri_rdf_Property))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_bob)) != (iext (uri_rdfs_domain) (uri_rdf_object) (uri_rdfs_Statement))) % 4.67/4.88 ((tuple (iext (uri_ex_hasAncestor) (uri_ex_alice) (uri_rdfs_ContainerMembershipProperty)) (iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_ContainerMembershipProperty))) != (tuple (true) (true))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Literal)) != (iext (uri_rdfs_range) (uri_rdf_predicate) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Literal)) != (iext (uri_rdfs_domain) (uri_rdfs_domain) (uri_rdf_Property))) % 4.67/4.88 ((tuple (iext (uri_ex_hasAncestor) (uri_ex_alice) (uri_rdfs_Datatype)) (iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Datatype))) != (tuple (true) (true))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_bob)) != (iext (uri_rdfs_domain) (uri_rdf__3) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_seeAlso)) != (iext (uri_rdfs_domain) (uri_rdfs_domain) (uri_rdf_Property))) % 4.67/4.88 ((uri_rdfs_Class) != (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z)) % 4.67/4.88 ((uri_owl_Restriction) != (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z)) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Statement)) != (iext (uri_rdfs_range) (uri_rdfs_domain) (uri_rdfs_Class))) % 4.67/4.88 ((iext (uri_owl_onProperty) (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z) (uri_ex_hasAncestor)) = (true)) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdf_Property)) != (iext (uri_rdfs_domain) (uri_rdf_subject) (uri_rdfs_Statement))) % 4.67/4.88 ((uri_rdfs_Datatype) != (uri_ex_Person)) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (literal_typed (dat_str_1) (uri_xsd_nonNegativeInteger))) != (iext (uri_rdfs_domain) (uri_rdfs_domain) (uri_rdf_Property))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z)) != (iext (uri_rdfs_range) (uri_rdf__1) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Datatype)) != (iext (uri_rdf_type) (uri_rdf_value) (uri_rdf_Property))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_owl_TransitiveProperty)) != (iext (uri_rdfs_domain) (uri_rdf_value) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (literal_typed (dat_str_1) (uri_xsd_nonNegativeInteger))) != (iext (uri_rdfs_subClassOf) (uri_rdf_Bag) (uri_rdfs_Container))) % 4.67/4.88 ((iext (uri_rdfs_range) (uri_rdf_rest) (uri_rdf_List)) = (true)) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_owl_Restriction)) != (iext (uri_rdf_type) (uri_rdf__3) (uri_rdfs_ContainerMembershipProperty))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Literal)) != (iext (uri_rdfs_subClassOf) (uri_rdfs_Datatype) (uri_rdfs_Class))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Datatype)) != (iext (uri_rdfs_domain) (uri_rdf__3) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_ContainerMembershipProperty)) != (iext (uri_rdf_type) (uri_ex_alice) (uri_ex_Person))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdf_List)) != (iext (uri_rdf_type) (uri_rdf__1) (uri_rdf_Property))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_owl_Restriction)) != (iext (uri_owl_minCardinality) (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z) (literal_typed (dat_str_1) (uri_xsd_nonNegativeInteger)))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) zenon_X0) != (iext (uri_rdf_type) (uri_rdf_Property) (uri_rdfs_Class))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdf_Property)) != (iext (uri_rdfs_range) (uri_rdfs_comment) (uri_rdfs_Literal))) % 4.67/4.88 ((uri_rdfs_Datatype) != (uri_rdfs_Container)) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Statement)) != (iext (uri_rdf_type) (uri_rdf__1) (uri_rdf_Property))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdf_Property)) != (iext (uri_rdfs_domain) (uri_rdfs_domain) (uri_rdf_Property))) % 4.67/4.88 ((uri_rdfs_seeAlso) != (uri_ex_hasAncestor)) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_ContainerMembershipProperty)) != (iext (uri_rdfs_range) (uri_rdfs_seeAlso) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z)) != (iext (uri_rdfs_domain) (uri_rdf_object) (uri_rdfs_Statement))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_bob)) != (iext (uri_rdfs_range) (uri_rdf_predicate) (uri_rdfs_Resource))) % 4.67/4.88 ((uri_rdfs_ContainerMembershipProperty) != (uri_ex_Person)) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_owl_TransitiveProperty)) != (iext (uri_rdfs_domain) (uri_rdf__1) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (literal_typed (dat_str_1) (uri_xsd_nonNegativeInteger))) != (iext (uri_rdf_type) (uri_rdf_object) (uri_rdf_Property))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_owl_Restriction)) != (iext (uri_rdf_type) (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z) (uri_owl_Restriction))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Statement)) != (iext (uri_rdfs_range) (uri_rdfs_isDefinedBy) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Datatype)) != (iext (uri_rdfs_domain) (uri_rdf_subject) (uri_rdfs_Statement))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Class)) != (iext (uri_rdfs_range) (uri_rdfs_domain) (uri_rdfs_Class))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_owl_Restriction)) != (iext (uri_rdfs_range) (uri_rdf__2) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdf_Property)) != (iext (uri_rdfs_domain) (uri_rdf__2) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdf_Property)) != (iext (uri_rdfs_domain) (uri_rdfs_subPropertyOf) (uri_rdf_Property))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (literal_typed (dat_str_1) (uri_xsd_nonNegativeInteger))) != (iext (uri_rdfs_range) (uri_rdf_first) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdf_Property)) != (iext (uri_rdfs_domain) (uri_rdf_type) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_owl_TransitiveProperty)) != (iext (uri_rdf_type) (uri_rdf_subject) (uri_rdf_Property))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z)) != (iext (uri_rdf_type) (uri_rdf_Property) (uri_rdfs_Class))) % 4.67/4.88 ((uri_ex_bob) != (uri_rdfs_label)) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Container)) != (iext (uri_rdfs_domain) (uri_rdfs_subClassOf) (uri_rdfs_Class))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Literal)) != (iext (uri_rdf_type) (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z) (uri_owl_Restriction))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_Person)) != (iext (uri_owl_minCardinality) (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z) (literal_typed (dat_str_1) (uri_xsd_nonNegativeInteger)))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_ContainerMembershipProperty)) != (true)) % 4.67/4.88 ((uri_rdf_Property) != (literal_typed (dat_str_1) (uri_xsd_nonNegativeInteger))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_owl_TransitiveProperty)) != (iext (uri_owl_minCardinality) (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z) (literal_typed (dat_str_1) (uri_xsd_nonNegativeInteger)))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (literal_typed (dat_str_1) (uri_xsd_nonNegativeInteger))) != (iext (uri_rdfs_range) (uri_rdfs_member) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (literal_typed (dat_str_1) (uri_xsd_nonNegativeInteger))) != (iext (uri_rdfs_domain) (uri_rdfs_subClassOf) (uri_rdfs_Class))) % 4.67/4.88 ((iext (uri_rdfs_domain) (uri_rdf_type) (uri_rdfs_Resource)) = (true)) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_owl_TransitiveProperty)) != (iext (uri_rdfs_domain) (uri_rdfs_comment) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_bob)) != (iext (uri_rdfs_domain) (uri_rdfs_seeAlso) (uri_rdfs_Resource))) % 4.67/4.88 ((uri_rdf_Property) != (uri_rdfs_Literal)) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Literal)) != (iext (uri_rdfs_domain) (uri_rdf_object) (uri_rdfs_Statement))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Datatype)) != (iext (uri_rdfs_range) (uri_rdfs_isDefinedBy) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_Person)) != (iext (uri_rdfs_range) (uri_rdf_value) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Literal)) != (iext (uri_rdfs_subClassOf) (uri_rdf_Bag) (uri_rdfs_Container))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_owl_Restriction)) != (iext (uri_rdf_type) (uri_rdf__1) (uri_rdfs_ContainerMembershipProperty))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_owl_TransitiveProperty)) != (iext (uri_rdfs_range) (uri_rdfs_domain) (uri_rdfs_Class))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_ContainerMembershipProperty)) != (iext (uri_rdfs_domain) (uri_rdfs_isDefinedBy) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Statement)) != (true)) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_Person)) != (iext (uri_rdfs_domain) (uri_rdf_first) (uri_rdf_List))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_owl_Restriction)) != (iext (uri_rdfs_range) (uri_rdf_predicate) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) zenon_X0) != (iext (uri_rdfs_range) (uri_rdf_rest) (uri_rdf_List))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) zenon_X0) != (iext (uri_rdf_type) (uri_ex_alice) (uri_ex_Person))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Datatype)) != (iext (uri_rdfs_domain) (uri_rdf_first) (uri_rdf_List))) % 4.67/4.88 ((tuple (iext (uri_ex_hasAncestor) (uri_ex_alice) (uri_rdf_List)) (iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdf_List))) != (tuple (true) (true))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdf_List)) != (iext (uri_rdf_type) (uri_rdf__1) (uri_rdfs_ContainerMembershipProperty))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Datatype)) != (iext (uri_rdf_type) (uri_ex_alice) (uri_ex_Person))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_seeAlso)) != (iext (uri_rdf_type) (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z) (uri_owl_Restriction))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z)) != (iext (uri_rdf_type) (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z) (uri_owl_Restriction))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_hasAncestor)) != (iext (uri_rdfs_subClassOf) (uri_rdfs_ContainerMembershipProperty) (uri_rdf_Property))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Resource)) != (iext (uri_rdfs_domain) (uri_rdfs_member) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Literal)) != (iext (uri_rdf_type) (uri_rdf__1) (uri_rdfs_ContainerMembershipProperty))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Class)) != (iext (uri_rdfs_range) (uri_rdfs_isDefinedBy) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Class)) != (iext (uri_rdfs_range) (uri_rdf__3) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Container)) != (iext (uri_rdfs_subClassOf) (uri_rdfs_ContainerMembershipProperty) (uri_rdf_Property))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Resource)) != (iext (uri_rdfs_range) (uri_rdfs_subPropertyOf) (uri_rdf_Property))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Resource)) != (iext (uri_rdf_type) (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z) (uri_owl_Restriction))) % 4.67/4.88 ((iext (uri_rdfs_range) (uri_rdfs_subPropertyOf) (uri_rdf_Property)) = (true)) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdf_List)) != (true)) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Statement)) != (iext (uri_rdf_type) (uri_rdf_first) (uri_rdf_Property))) % 4.67/4.88 ((uri_rdfs_Container) != (uri_ex_bob)) % 4.67/4.88 ((iext (uri_rdf_type) (uri_rdf_XMLLiteral) (uri_rdfs_Datatype)) = (true)) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_ContainerMembershipProperty)) != (iext (uri_rdf_type) (uri_rdf_Property) (uri_rdfs_Class))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (literal_typed (dat_str_1) (uri_xsd_nonNegativeInteger))) != (iext (uri_rdfs_range) (uri_rdfs_subClassOf) (uri_rdfs_Class))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Datatype)) != (iext (uri_owl_onProperty) (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z) (uri_ex_hasAncestor))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z)) != (iext (uri_rdfs_domain) (uri_rdfs_label) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdf_List)) != (iext (uri_rdfs_range) (uri_rdf_subject) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Statement)) != (iext (uri_rdf_type) (uri_rdf_rest) (uri_rdf_Property))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z)) != (iext (uri_rdfs_domain) (uri_rdf_type) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_Person)) != (iext (uri_rdf_type) (uri_rdf_Property) (uri_rdfs_Class))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_owl_Restriction)) != (iext (uri_rdf_type) (uri_rdf_nil) (uri_rdf_List))) % 4.67/4.88 ((uri_owl_TransitiveProperty) != (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z)) % 4.67/4.88 ((uri_rdf_List) != (uri_ex_bob)) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Datatype)) != (iext (uri_ex_hasAncestor) (uri_ex_alice) (uri_ex_bob))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_ContainerMembershipProperty)) != (iext (uri_rdfs_range) (uri_rdfs_subClassOf) (uri_rdfs_Class))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (literal_typed (dat_str_1) (uri_xsd_nonNegativeInteger))) != (iext (uri_rdfs_range) (uri_rdf_subject) (uri_rdfs_Resource))) % 4.67/4.88 ((uri_ex_bob) != (uri_rdf__1)) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Literal)) != (iext (uri_rdfs_domain) (uri_rdfs_subPropertyOf) (uri_rdf_Property))) % 4.67/4.88 ((uri_rdfs_Resource) != (uri_owl_TransitiveProperty)) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (literal_typed (dat_str_1) (uri_xsd_nonNegativeInteger))) != (iext (uri_rdfs_subClassOf) (uri_rdfs_Datatype) (uri_rdfs_Class))) % 4.67/4.88 ((uri_rdfs_Datatype) != (uri_owl_TransitiveProperty)) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_seeAlso)) != (iext (uri_rdfs_domain) (uri_rdf_value) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_hasAncestor)) != (iext (uri_rdfs_range) (uri_rdf__3) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Datatype)) != (iext (uri_rdfs_range) (uri_rdf__3) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Class)) != (iext (uri_rdfs_domain) (uri_rdf_value) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Class)) != (iext (uri_rdf_type) (uri_rdf_subject) (uri_rdf_Property))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_owl_TransitiveProperty)) != (iext (uri_rdfs_range) (uri_rdf__2) (uri_rdfs_Resource))) % 4.67/4.88 ((uri_rdfs_Literal) != (uri_owl_TransitiveProperty)) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Resource)) != (iext (uri_rdfs_subClassOf) (uri_ex_Person) (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Literal)) != (iext (uri_rdfs_range) (uri_rdf_value) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_rdfs_domain) (uri_rdf_first) (uri_rdf_List)) = (true)) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Literal)) != (iext (uri_rdfs_domain) (uri_rdf__2) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Datatype)) != (iext (uri_rdfs_subClassOf) (uri_rdf_XMLLiteral) (uri_rdfs_Literal))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Literal)) != (iext (uri_rdfs_range) (uri_rdfs_comment) (uri_rdfs_Literal))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Datatype)) != (iext (uri_rdfs_domain) (uri_rdf__2) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_hasAncestor)) != (iext (uri_rdf_type) (uri_rdf__1) (uri_rdf_Property))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (literal_typed (dat_str_1) (uri_xsd_nonNegativeInteger))) != (iext (uri_rdfs_domain) (uri_rdf_value) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Resource)) != (iext (uri_rdf_type) (uri_ex_hasAncestor) (uri_owl_TransitiveProperty))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_seeAlso)) != (iext (uri_rdfs_subPropertyOf) (uri_rdfs_isDefinedBy) (uri_rdfs_seeAlso))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_owl_Restriction)) != (iext (uri_rdfs_subClassOf) (uri_rdfs_Datatype) (uri_rdfs_Class))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdf_Property)) != (iext (uri_rdfs_range) (uri_rdf_first) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Container)) != (iext (uri_rdf_type) (uri_rdf_nil) (uri_rdf_List))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_bob)) != (iext (uri_rdfs_domain) (uri_rdfs_label) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_bob)) != (iext (uri_rdf_type) (uri_ex_bob) (uri_ex_Person))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Resource)) != (iext (uri_rdfs_domain) (uri_rdfs_isDefinedBy) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Datatype)) != (iext (uri_rdfs_range) (uri_rdf_subject) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_rdfs_subClassOf) (uri_rdfs_ContainerMembershipProperty) (uri_rdf_Property)) = (true)) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_seeAlso)) != (iext (uri_rdfs_domain) (uri_rdf_type) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Class)) != (iext (uri_rdf_type) (uri_rdf_type) (uri_rdf_Property))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_hasAncestor)) != (iext (uri_rdfs_domain) (uri_rdfs_domain) (uri_rdf_Property))) % 4.67/4.88 ((uri_ex_bob) != (uri_rdfs_member)) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z)) != (iext (uri_rdfs_domain) (uri_rdf__2) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Resource)) != (iext (uri_rdfs_domain) (uri_rdfs_range) (uri_rdf_Property))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_owl_Restriction)) != (iext (uri_rdf_type) (uri_rdf__2) (uri_rdfs_ContainerMembershipProperty))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdf_Property)) != (iext (uri_rdf_type) (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z) (uri_owl_Restriction))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Class)) != (iext (uri_rdfs_domain) (uri_rdfs_member) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_Person)) != (iext (uri_rdfs_subPropertyOf) (uri_rdfs_isDefinedBy) (uri_rdfs_seeAlso))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z)) != (iext (uri_rdfs_range) (uri_rdfs_range) (uri_rdfs_Class))) % 4.67/4.88 ((uri_rdfs_Datatype) != (uri_ex_hasAncestor)) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_owl_TransitiveProperty)) != (iext (uri_rdfs_domain) (uri_rdfs_isDefinedBy) (uri_rdfs_Resource))) % 4.67/4.88 ((uri_rdfs_Container) != (uri_owl_Restriction)) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (literal_typed (dat_str_1) (uri_xsd_nonNegativeInteger))) != (iext (uri_rdfs_domain) (uri_rdf_rest) (uri_rdf_List))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (literal_typed (dat_str_1) (uri_xsd_nonNegativeInteger))) != (iext (uri_rdfs_subClassOf) (uri_rdfs_ContainerMembershipProperty) (uri_rdf_Property))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_owl_Restriction)) != (iext (uri_rdfs_range) (uri_rdfs_domain) (uri_rdfs_Class))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Statement)) != (iext (uri_rdf_type) (uri_rdf__3) (uri_rdf_Property))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_ContainerMembershipProperty)) != (iext (uri_rdfs_domain) (uri_rdf_subject) (uri_rdfs_Statement))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_hasAncestor)) != (iext (uri_rdfs_subClassOf) (uri_rdfs_Seq) (uri_rdfs_Container))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Class)) != (iext (uri_rdfs_range) (uri_rdfs_range) (uri_rdfs_Class))) % 4.67/4.88 ((uri_ex_bob) != (uri_rdfs_Seq)) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_seeAlso)) != (iext (uri_rdf_type) (uri_ex_alice) (uri_ex_Person))) % 4.67/4.88 ((uri_owl_Restriction) != (literal_typed (dat_str_1) (uri_xsd_nonNegativeInteger))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z)) != (iext (uri_rdfs_range) (uri_rdfs_label) (uri_rdfs_Literal))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_Person)) != (iext (uri_rdfs_range) (uri_rdfs_label) (uri_rdfs_Literal))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Container)) != (iext (uri_rdfs_range) (uri_rdf_type) (uri_rdfs_Class))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_Person)) != (iext (uri_rdfs_range) (uri_rdf__3) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z)) != (iext (uri_rdfs_subClassOf) (uri_rdfs_Datatype) (uri_rdfs_Class))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_hasAncestor)) != (iext (uri_rdfs_domain) (uri_rdf__1) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_owl_Restriction)) != (iext (uri_rdfs_domain) (uri_rdfs_seeAlso) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_seeAlso)) != (iext (uri_rdf_type) (uri_rdf_nil) (uri_rdf_List))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) zenon_X0) != (iext (uri_rdfs_subPropertyOf) (uri_rdfs_isDefinedBy) (uri_rdfs_seeAlso))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Literal)) != (iext (uri_rdf_type) (uri_rdf_Property) (uri_rdfs_Class))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Datatype)) != (iext (uri_rdfs_domain) (uri_rdf_type) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Datatype)) != (iext (uri_rdfs_subClassOf) (uri_ex_Person) (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdf_Property)) != (iext (uri_rdf_type) (uri_rdf_Property) (uri_rdfs_Class))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Resource)) != (iext (uri_rdfs_domain) (uri_rdfs_seeAlso) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Container)) != (iext (uri_rdfs_domain) (uri_rdfs_member) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Literal)) != (iext (uri_rdf_type) (uri_ex_hasAncestor) (uri_owl_TransitiveProperty))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_seeAlso)) != (iext (uri_rdfs_range) (uri_rdfs_range) (uri_rdfs_Class))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_Person)) != (iext (uri_rdfs_domain) (uri_rdfs_subPropertyOf) (uri_rdf_Property))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdf_List)) != (iext (uri_rdfs_range) (uri_rdfs_isDefinedBy) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_seeAlso)) != (iext (uri_rdf_type) (uri_rdf_type) (uri_rdf_Property))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdf_Property)) != (iext (uri_rdfs_range) (uri_rdfs_domain) (uri_rdfs_Class))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Datatype)) != (iext (uri_rdfs_range) (uri_rdf_first) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_hasAncestor)) != (iext (uri_rdf_type) (uri_rdf_XMLLiteral) (uri_rdfs_Datatype))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) zenon_X0) != (iext (uri_rdfs_domain) (uri_rdf_object) (uri_rdfs_Statement))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Container)) != (iext (uri_rdfs_domain) (uri_rdfs_seeAlso) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_seeAlso)) != (iext (uri_rdf_type) (uri_ex_bob) (uri_ex_Person))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_hasAncestor)) != (iext (uri_rdfs_domain) (uri_rdf_first) (uri_rdf_List))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_bob)) != (iext (uri_rdf_type) (uri_rdf__1) (uri_rdfs_ContainerMembershipProperty))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_Person)) != (iext (uri_rdfs_subClassOf) (uri_rdfs_Datatype) (uri_rdfs_Class))) % 4.67/4.88 (zenon_X0 != (uri_ex_hasAncestor)) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_bob)) != (iext (uri_ex_hasAncestor) (uri_ex_alice) (uri_ex_bob))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Class)) != (iext (uri_rdf_type) (uri_rdf_object) (uri_rdf_Property))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Resource)) != (iext (uri_rdf_type) (uri_rdf__3) (uri_rdf_Property))) % 4.67/4.88 ((iext (uri_rdfs_domain) (uri_rdf__2) (uri_rdfs_Resource)) = (true)) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) zenon_X0) != (iext (uri_rdf_type) (uri_rdf_first) (uri_rdf_Property))) % 4.67/4.88 ((uri_rdfs_Statement) != (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z)) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z)) != (iext (uri_rdf_type) (uri_rdf_rest) (uri_rdf_Property))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z)) != (iext (uri_rdfs_domain) (uri_rdf__3) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdf_List)) != (iext (uri_rdf_type) (uri_rdf_Property) (uri_rdfs_Class))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_owl_Restriction)) != (iext (uri_rdf_type) (uri_rdf_Property) (uri_rdfs_Class))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z)) != (iext (uri_rdf_type) (uri_rdf_nil) (uri_rdf_List))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_Person)) != (iext (uri_rdfs_domain) (uri_rdfs_isDefinedBy) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_Person)) != (iext (uri_rdf_type) (uri_rdf__2) (uri_rdfs_ContainerMembershipProperty))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Class)) != (true)) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Datatype)) != (iext (uri_rdfs_subPropertyOf) (uri_rdfs_isDefinedBy) (uri_rdfs_seeAlso))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_Person)) != (iext (uri_rdfs_range) (uri_rdfs_isDefinedBy) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdf_List)) != (iext (uri_rdfs_domain) (uri_rdfs_range) (uri_rdf_Property))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Datatype)) != (iext (uri_rdfs_domain) (uri_rdfs_subClassOf) (uri_rdfs_Class))) % 4.67/4.88 ((iext (uri_rdf_type) (uri_rdf__3) (uri_rdfs_ContainerMembershipProperty)) = (true)) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdf_Property)) != (iext (uri_rdf_type) (uri_rdf_type) (uri_rdf_Property))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Resource)) != (iext (uri_rdf_type) (uri_rdf_XMLLiteral) (uri_rdfs_Datatype))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Class)) != (iext (uri_rdfs_range) (uri_rdf__2) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z)) != (iext (uri_rdfs_domain) (uri_rdfs_range) (uri_rdf_Property))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_bob)) != (iext (uri_rdfs_domain) (uri_rdf_type) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdf_Property)) != (iext (uri_rdf_type) (uri_rdf__1) (uri_rdfs_ContainerMembershipProperty))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Datatype)) != (iext (uri_rdfs_domain) (uri_rdfs_range) (uri_rdf_Property))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_seeAlso)) != (iext (uri_rdfs_range) (uri_rdf_type) (uri_rdfs_Class))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_owl_Restriction)) != (iext (uri_rdf_type) (uri_rdf__2) (uri_rdf_Property))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z)) != (iext (uri_rdf_type) (uri_rdf__1) (uri_rdfs_ContainerMembershipProperty))) % 4.67/4.88 ((uri_ex_bob) != (uri_rdf_XMLLiteral)) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Literal)) != (iext (uri_rdfs_domain) (uri_rdfs_subClassOf) (uri_rdfs_Class))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_ContainerMembershipProperty)) != (iext (uri_rdfs_range) (uri_rdfs_member) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_bob)) != (iext (uri_rdfs_subClassOf) (uri_rdf_Alt) (uri_rdfs_Container))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_Person)) != (iext (uri_rdf_type) (uri_rdf_nil) (uri_rdf_List))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_owl_Restriction)) != (iext (uri_rdfs_domain) (uri_rdfs_range) (uri_rdf_Property))) % 4.67/4.88 ((iext (uri_rdfs_domain) (uri_rdfs_seeAlso) (uri_rdfs_Resource)) = (true)) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdf_List)) != (iext (uri_rdfs_range) (uri_rdf_type) (uri_rdfs_Class))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_hasAncestor)) != (iext (uri_rdf_type) (uri_rdf_subject) (uri_rdf_Property))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) zenon_X0) != (iext (uri_rdfs_range) (uri_rdfs_label) (uri_rdfs_Literal))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Class)) != (iext (uri_rdfs_range) (uri_rdfs_comment) (uri_rdfs_Literal))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z)) != (iext (uri_rdfs_domain) (uri_rdf_subject) (uri_rdfs_Statement))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_Person)) != (iext (uri_rdfs_domain) (uri_rdf_type) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Statement)) != (iext (uri_rdfs_domain) (uri_rdf__3) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdf_List)) != (iext (uri_ex_hasAncestor) (uri_ex_alice) (uri_ex_bob))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Resource)) != (iext (uri_rdfs_range) (uri_rdf_type) (uri_rdfs_Class))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z)) != (iext (uri_rdfs_range) (uri_rdf_subject) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Literal)) != (iext (uri_rdf_type) (uri_rdf__2) (uri_rdf_Property))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Literal)) != (iext (uri_rdfs_domain) (uri_rdf_rest) (uri_rdf_List))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_seeAlso)) != (iext (uri_owl_onProperty) (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z) (uri_ex_hasAncestor))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdf_List)) != (iext (uri_rdfs_range) (uri_rdfs_subPropertyOf) (uri_rdf_Property))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_seeAlso)) != (iext (uri_rdfs_domain) (uri_rdf__1) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdf_List)) != (iext (uri_rdfs_domain) (uri_rdf__2) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_owl_Restriction)) != (iext (uri_rdfs_subClassOf) (uri_rdfs_Seq) (uri_rdfs_Container))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (literal_typed (dat_str_1) (uri_xsd_nonNegativeInteger))) != (iext (uri_rdfs_subClassOf) (uri_rdf_XMLLiteral) (uri_rdfs_Literal))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) zenon_X0) != (iext (uri_rdfs_domain) (uri_rdf_subject) (uri_rdfs_Statement))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) zenon_X0) != (iext (uri_rdfs_range) (uri_rdfs_subClassOf) (uri_rdfs_Class))) % 4.67/4.88 ((uri_rdf_Property) != (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z)) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Resource)) != (iext (uri_rdfs_range) (uri_rdfs_comment) (uri_rdfs_Literal))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_seeAlso)) != (iext (uri_rdfs_range) (uri_rdfs_comment) (uri_rdfs_Literal))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z)) != (iext (uri_rdf_type) (uri_rdf__2) (uri_rdfs_ContainerMembershipProperty))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Literal)) != (iext (uri_rdfs_domain) (uri_rdfs_member) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_seeAlso)) != (iext (uri_rdf_type) (uri_rdf__1) (uri_rdf_Property))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Statement)) != (iext (uri_rdfs_range) (uri_rdf_value) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Datatype)) != (iext (uri_rdfs_subClassOf) (uri_rdfs_Datatype) (uri_rdfs_Class))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_bob)) != (iext (uri_rdf_type) (uri_rdf_nil) (uri_rdf_List))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_Person)) != (iext (uri_rdfs_range) (uri_rdfs_comment) (uri_rdfs_Literal))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdf_Property)) != (iext (uri_rdfs_domain) (uri_rdf_object) (uri_rdfs_Statement))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_hasAncestor)) != (iext (uri_rdfs_domain) (uri_rdfs_member) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) zenon_X0) != (iext (uri_rdf_type) (uri_rdf__1) (uri_rdfs_ContainerMembershipProperty))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_owl_Restriction)) != (iext (uri_rdfs_domain) (uri_rdfs_subClassOf) (uri_rdfs_Class))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Datatype)) != (iext (uri_rdfs_range) (uri_rdf_rest) (uri_rdf_List))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_hasAncestor)) != (iext (uri_rdfs_domain) (uri_rdf_value) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Class)) != (iext (uri_rdf_type) (uri_rdf_nil) (uri_rdf_List))) % 4.67/4.88 ((iext (uri_rdfs_range) (uri_rdfs_isDefinedBy) (uri_rdfs_Resource)) = (true)) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdf_List)) != (iext (uri_owl_onProperty) (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z) (uri_ex_hasAncestor))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Resource)) != (iext (uri_ex_hasAncestor) (uri_ex_alice) (uri_ex_bob))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdf_List)) != (iext (uri_rdfs_domain) (uri_rdfs_comment) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Class)) != (iext (uri_rdf_type) (uri_ex_bob) (uri_ex_Person))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_owl_TransitiveProperty)) != (iext (uri_rdfs_subPropertyOf) (uri_rdfs_isDefinedBy) (uri_rdfs_seeAlso))) % 4.67/4.88 ((uri_rdf_Property) != (uri_rdfs_Datatype)) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_seeAlso)) != (iext (uri_rdfs_domain) (uri_rdfs_subClassOf) (uri_rdfs_Class))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_owl_TransitiveProperty)) != (iext (uri_rdfs_range) (uri_rdf_first) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdf_List)) != (iext (uri_rdf_type) (uri_rdf_nil) (uri_rdf_List))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdf_List)) != (iext (uri_rdfs_domain) (uri_rdf_rest) (uri_rdf_List))) % 4.67/4.88 ((uri_rdfs_Datatype) != (uri_ex_bob)) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_ContainerMembershipProperty)) != (iext (uri_rdfs_domain) (uri_rdfs_domain) (uri_rdf_Property))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_bob)) != (iext (uri_rdf_type) (uri_ex_alice) (uri_ex_Person))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (literal_typed (dat_str_1) (uri_xsd_nonNegativeInteger))) != (iext (uri_rdfs_domain) (uri_rdfs_label) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_owl_TransitiveProperty)) != (iext (uri_owl_onProperty) (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z) (uri_ex_hasAncestor))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_hasAncestor)) != (iext (uri_rdfs_domain) (uri_rdfs_seeAlso) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_rdf_type) (uri_rdf__1) (uri_rdf_Property)) = (true)) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) zenon_X0) != (iext (uri_rdf_type) (uri_rdf_rest) (uri_rdf_Property))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (literal_typed (dat_str_1) (uri_xsd_nonNegativeInteger))) != (iext (uri_rdf_type) (uri_rdf__2) (uri_rdf_Property))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdf_Property)) != (iext (uri_rdfs_domain) (uri_rdfs_member) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Literal)) != (iext (uri_rdfs_range) (uri_rdf_rest) (uri_rdf_List))) % 4.67/4.88 ((iext (uri_owl_minCardinality) (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z) (literal_typed (dat_str_1) (uri_xsd_nonNegativeInteger))) = (true)) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_owl_Restriction)) != (iext (uri_rdfs_domain) (uri_rdf_type) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Resource)) != (iext (uri_rdfs_range) (uri_rdfs_seeAlso) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdf_List)) != (iext (uri_rdf_type) (uri_rdf_object) (uri_rdf_Property))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_ContainerMembershipProperty)) != (iext (uri_rdfs_subPropertyOf) (uri_rdfs_isDefinedBy) (uri_rdfs_seeAlso))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_ContainerMembershipProperty)) != (iext (uri_rdf_type) (uri_rdf__2) (uri_rdfs_ContainerMembershipProperty))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_hasAncestor)) != (iext (uri_rdfs_subPropertyOf) (uri_rdfs_isDefinedBy) (uri_rdfs_seeAlso))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Literal)) != (iext (uri_rdf_type) (uri_rdf_type) (uri_rdf_Property))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_Person)) != (iext (uri_rdf_type) (uri_rdf_value) (uri_rdf_Property))) % 4.67/4.88 ((iext (uri_rdfs_domain) (uri_rdfs_range) (uri_rdf_Property)) = (true)) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_hasAncestor)) != (iext (uri_rdfs_range) (uri_rdfs_range) (uri_rdfs_Class))) % 4.67/4.88 ((uri_rdfs_Literal) != (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z)) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_owl_Restriction)) != (iext (uri_rdfs_subPropertyOf) (uri_rdfs_isDefinedBy) (uri_rdfs_seeAlso))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_Person)) != (iext (uri_rdfs_domain) (uri_rdf_predicate) (uri_rdfs_Statement))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_bob)) != (true)) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdf_List)) != (iext (uri_rdf_type) (uri_rdf__3) (uri_rdfs_ContainerMembershipProperty))) % 4.67/4.88 ((tuple (iext (uri_ex_hasAncestor) (uri_ex_alice) (uri_ex_hasAncestor)) (iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_hasAncestor))) != (tuple (true) (true))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Resource)) != (iext (uri_rdf_type) (uri_rdf_type) (uri_rdf_Property))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_hasAncestor)) != (iext (uri_rdfs_domain) (uri_rdf__3) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Class)) != (iext (uri_rdfs_range) (uri_rdfs_subPropertyOf) (uri_rdf_Property))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_owl_TransitiveProperty)) != (iext (uri_rdfs_domain) (uri_rdfs_subClassOf) (uri_rdfs_Class))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (literal_typed (dat_str_1) (uri_xsd_nonNegativeInteger))) != (iext (uri_rdfs_domain) (uri_rdf_subject) (uri_rdfs_Statement))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Datatype)) != (iext (uri_rdf_type) (uri_rdf_first) (uri_rdf_Property))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z)) != (iext (uri_rdf_type) (uri_rdf_XMLLiteral) (uri_rdfs_Datatype))) % 4.67/4.88 ((iext (uri_rdfs_domain) (uri_rdfs_domain) (uri_rdf_Property)) = (true)) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Datatype)) != (iext (uri_rdfs_range) (uri_rdfs_subPropertyOf) (uri_rdf_Property))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Container)) != (iext (uri_rdf_type) (uri_ex_alice) (uri_ex_Person))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_seeAlso)) != (iext (uri_rdfs_range) (uri_rdfs_isDefinedBy) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Literal)) != (iext (uri_rdfs_domain) (uri_rdfs_isDefinedBy) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Statement)) != (iext (uri_rdfs_domain) (uri_rdf_object) (uri_rdfs_Statement))) % 4.67/4.88 ((tuple (iext (uri_ex_hasAncestor) (uri_ex_alice) (uri_owl_Restriction)) (iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_owl_Restriction))) != (tuple (true) (true))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdf_List)) != (iext (uri_rdfs_domain) (uri_rdf_first) (uri_rdf_List))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Class)) != (iext (uri_rdfs_domain) (uri_rdfs_range) (uri_rdf_Property))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_owl_Restriction)) != (iext (uri_rdfs_range) (uri_rdf_rest) (uri_rdf_List))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_ContainerMembershipProperty)) != (iext (uri_rdf_type) (uri_rdf__1) (uri_rdf_Property))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_bob)) != (iext (uri_rdfs_subClassOf) (uri_rdfs_Datatype) (uri_rdfs_Class))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Container)) != (iext (uri_rdfs_range) (uri_rdfs_member) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Resource)) != (iext (uri_rdf_type) (uri_rdf_rest) (uri_rdf_Property))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_ContainerMembershipProperty)) != (iext (uri_rdf_type) (uri_rdf_object) (uri_rdf_Property))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdf_Property)) != (iext (uri_rdfs_range) (uri_rdf__1) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_owl_TransitiveProperty)) != (iext (uri_rdf_type) (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z) (uri_owl_Restriction))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdf_List)) != (iext (uri_rdfs_range) (uri_rdf__2) (uri_rdfs_Resource))) % 4.67/4.88 ((uri_rdf_Property) != (uri_ex_Person)) % 4.67/4.88 ((iext (uri_rdfs_range) (uri_rdfs_comment) (uri_rdfs_Literal)) = (true)) % 4.67/4.88 ((iext (uri_rdfs_domain) (uri_rdfs_isDefinedBy) (uri_rdfs_Resource)) = (true)) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) zenon_X0) != (iext (uri_rdfs_domain) (uri_rdf_value) (uri_rdfs_Resource))) % 4.67/4.88 ((uri_owl_TransitiveProperty) != (uri_ex_Person)) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdf_Property)) != (iext (uri_rdfs_domain) (uri_rdfs_subClassOf) (uri_rdfs_Class))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_owl_Restriction)) != (iext (uri_rdfs_range) (uri_rdfs_isDefinedBy) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Statement)) != (iext (uri_rdfs_range) (uri_rdfs_subClassOf) (uri_rdfs_Class))) % 4.67/4.88 ((uri_rdf_List) != (uri_owl_Restriction)) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Resource)) != (iext (uri_rdfs_subClassOf) (uri_rdf_XMLLiteral) (uri_rdfs_Literal))) % 4.67/4.88 ((uri_rdfs_Class) != (uri_rdfs_Container)) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_hasAncestor)) != (iext (uri_rdfs_range) (uri_rdf_value) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_owl_TransitiveProperty)) != (iext (uri_rdfs_subClassOf) (uri_ex_Person) (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_hasAncestor)) != (iext (uri_rdfs_subClassOf) (uri_rdfs_Datatype) (uri_rdfs_Class))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdf_Property)) != (iext (uri_rdfs_subClassOf) (uri_rdfs_Datatype) (uri_rdfs_Class))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Statement)) != (iext (uri_rdfs_range) (uri_rdf__1) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Statement)) != (iext (uri_rdfs_domain) (uri_rdf__2) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z)) != (iext (uri_rdfs_range) (uri_rdf_first) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_bob)) != (iext (uri_rdfs_domain) (uri_rdf__2) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) zenon_X0) != (iext (uri_owl_minCardinality) (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z) (literal_typed (dat_str_1) (uri_xsd_nonNegativeInteger)))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdf_List)) != (iext (uri_rdfs_domain) (uri_rdfs_seeAlso) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (literal_typed (dat_str_1) (uri_xsd_nonNegativeInteger))) != (iext (uri_rdfs_range) (uri_rdfs_seeAlso) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_rdf_type) (uri_rdf_first) (uri_rdf_Property)) = (true)) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (literal_typed (dat_str_1) (uri_xsd_nonNegativeInteger))) != (iext (uri_owl_minCardinality) (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z) (literal_typed (dat_str_1) (uri_xsd_nonNegativeInteger)))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z)) != (iext (uri_rdfs_domain) (uri_rdf_first) (uri_rdf_List))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_hasAncestor)) != (iext (uri_owl_minCardinality) (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z) (literal_typed (dat_str_1) (uri_xsd_nonNegativeInteger)))) % 4.67/4.88 ((tuple (iext (uri_ex_hasAncestor) (uri_ex_alice) (uri_rdfs_Container)) (iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Container))) != (tuple (true) (true))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Container)) != (iext (uri_rdfs_subPropertyOf) (uri_rdfs_isDefinedBy) (uri_rdfs_seeAlso))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_owl_TransitiveProperty)) != (iext (uri_rdfs_range) (uri_rdf_rest) (uri_rdf_List))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_hasAncestor)) != (iext (uri_owl_onProperty) (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z) (uri_ex_hasAncestor))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdf_List)) != (iext (uri_rdfs_subClassOf) (uri_rdfs_ContainerMembershipProperty) (uri_rdf_Property))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_owl_TransitiveProperty)) != (iext (uri_rdf_type) (uri_rdf_first) (uri_rdf_Property))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdf_List)) != (iext (uri_rdfs_range) (uri_rdfs_label) (uri_rdfs_Literal))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Datatype)) != (iext (uri_rdfs_domain) (uri_rdf_rest) (uri_rdf_List))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Datatype)) != (iext (uri_rdfs_range) (uri_rdf_value) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_bob)) != (iext (uri_rdf_type) (uri_rdf_subject) (uri_rdf_Property))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_owl_TransitiveProperty)) != (iext (uri_rdfs_range) (uri_rdfs_isDefinedBy) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (literal_typed (dat_str_1) (uri_xsd_nonNegativeInteger))) != (iext (uri_owl_onProperty) (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z) (uri_ex_hasAncestor))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Literal)) != (iext (uri_rdfs_subClassOf) (uri_rdf_Alt) (uri_rdfs_Container))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Container)) != (iext (uri_rdfs_range) (uri_rdfs_label) (uri_rdfs_Literal))) % 4.67/4.88 ((uri_rdfs_Class) != (uri_owl_Restriction)) % 4.67/4.88 ((iext (uri_rdfs_domain) (uri_rdfs_subClassOf) (uri_rdfs_Class)) = (true)) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_seeAlso)) != (iext (uri_rdfs_range) (uri_rdfs_member) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Datatype)) != (iext (uri_rdfs_subClassOf) (uri_rdfs_Seq) (uri_rdfs_Container))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdf_List)) != (iext (uri_rdf_type) (uri_rdf_value) (uri_rdf_Property))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_owl_TransitiveProperty)) != (true)) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z)) != (iext (uri_rdfs_subPropertyOf) (uri_rdfs_isDefinedBy) (uri_rdfs_seeAlso))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdf_List)) != (iext (uri_rdfs_range) (uri_rdf_predicate) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdf_List)) != (iext (uri_rdf_type) (uri_rdf__2) (uri_rdf_Property))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_bob)) != (iext (uri_owl_minCardinality) (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z) (literal_typed (dat_str_1) (uri_xsd_nonNegativeInteger)))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_seeAlso)) != (iext (uri_rdfs_domain) (uri_rdf_subject) (uri_rdfs_Statement))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Statement)) != (iext (uri_rdf_type) (uri_rdf__3) (uri_rdfs_ContainerMembershipProperty))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (literal_typed (dat_str_1) (uri_xsd_nonNegativeInteger))) != (iext (uri_rdfs_subClassOf) (uri_rdf_Alt) (uri_rdfs_Container))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_owl_Restriction)) != (iext (uri_rdfs_domain) (uri_rdf__2) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_bob)) != (iext (uri_rdf_type) (uri_rdf_object) (uri_rdf_Property))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Container)) != (iext (uri_rdfs_domain) (uri_rdfs_domain) (uri_rdf_Property))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_owl_TransitiveProperty)) != (iext (uri_rdfs_range) (uri_rdf__3) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_owl_TransitiveProperty)) != (iext (uri_rdfs_domain) (uri_rdf_subject) (uri_rdfs_Statement))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Resource)) != (iext (uri_rdfs_range) (uri_rdfs_range) (uri_rdfs_Class))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Class)) != (iext (uri_rdfs_domain) (uri_rdf_type) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Datatype)) != (iext (uri_rdfs_domain) (uri_rdfs_comment) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_owl_TransitiveProperty)) != (iext (uri_rdfs_range) (uri_rdfs_member) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_owl_TransitiveProperty)) != (iext (uri_rdfs_subClassOf) (uri_rdfs_Seq) (uri_rdfs_Container))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_owl_TransitiveProperty)) != (iext (uri_rdfs_range) (uri_rdf_subject) (uri_rdfs_Resource))) % 4.67/4.88 ((uri_ex_bob) != (uri_rdf_rest)) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Resource)) != (iext (uri_rdfs_domain) (uri_rdf_object) (uri_rdfs_Statement))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_hasAncestor)) != (iext (uri_rdfs_range) (uri_rdf_predicate) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdf_List)) != (iext (uri_rdfs_range) (uri_rdfs_seeAlso) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_bob)) != (iext (uri_rdfs_domain) (uri_rdf_rest) (uri_rdf_List))) % 4.67/4.88 ((uri_rdfs_Resource) != (literal_typed (dat_str_1) (uri_xsd_nonNegativeInteger))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Statement)) != (iext (uri_rdfs_domain) (uri_rdfs_comment) (uri_rdfs_Resource))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_ContainerMembershipProperty)) != (iext (uri_rdfs_subClassOf) (uri_rdfs_Datatype) (uri_rdfs_Class))) % 4.67/4.88 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z)) != (iext (uri_rdf_type) (uri_ex_alice) (uri_ex_Person))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_bob)) != (iext (uri_rdfs_range) (uri_rdfs_label) (uri_rdfs_Literal))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_bob)) != (iext (uri_rdf_type) (uri_rdf__3) (uri_rdfs_ContainerMembershipProperty))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Resource)) != (iext (uri_rdf_type) (uri_rdf__3) (uri_rdfs_ContainerMembershipProperty))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Container)) != (iext (uri_rdfs_domain) (uri_rdf_first) (uri_rdf_List))) % 4.67/4.89 ((uri_rdfs_Statement) != (uri_ex_bob)) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Literal)) != (iext (uri_rdf_type) (uri_rdf__2) (uri_rdfs_ContainerMembershipProperty))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (literal_typed (dat_str_1) (uri_xsd_nonNegativeInteger))) != (iext (uri_rdfs_range) (uri_rdf__1) (uri_rdfs_Resource))) % 4.67/4.89 ((uri_rdf_Property) != (uri_ex_hasAncestor)) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdf_List)) != (iext (uri_rdfs_domain) (uri_rdf_subject) (uri_rdfs_Statement))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Statement)) != (iext (uri_rdfs_domain) (uri_rdf_predicate) (uri_rdfs_Statement))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Resource)) != (iext (uri_rdfs_range) (uri_rdf__2) (uri_rdfs_Resource))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Class)) != (iext (uri_rdfs_domain) (uri_rdfs_seeAlso) (uri_rdfs_Resource))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Class)) != (iext (uri_rdfs_domain) (uri_rdf_predicate) (uri_rdfs_Statement))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_hasAncestor)) != (iext (uri_rdf_type) (uri_rdf_object) (uri_rdf_Property))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Class)) != (iext (uri_rdf_type) (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z) (uri_owl_Restriction))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Container)) != (iext (uri_rdf_type) (uri_rdf__1) (uri_rdf_Property))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_owl_TransitiveProperty)) != (iext (uri_rdfs_domain) (uri_rdfs_member) (uri_rdfs_Resource))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_ContainerMembershipProperty)) != (iext (uri_rdf_type) (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z) (uri_owl_Restriction))) % 4.67/4.89 (zenon_X0 != (uri_rdfs_Resource)) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Datatype)) != (iext (uri_rdfs_domain) (uri_rdfs_isDefinedBy) (uri_rdfs_Resource))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Container)) != (iext (uri_owl_onProperty) (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z) (uri_ex_hasAncestor))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_ContainerMembershipProperty)) != (iext (uri_rdf_type) (uri_rdf_type) (uri_rdf_Property))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_hasAncestor)) != (iext (uri_rdfs_subClassOf) (uri_rdf_Bag) (uri_rdfs_Container))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Class)) != (iext (uri_rdfs_subPropertyOf) (uri_rdfs_isDefinedBy) (uri_rdfs_seeAlso))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Class)) != (iext (uri_rdfs_subClassOf) (uri_rdf_Bag) (uri_rdfs_Container))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Datatype)) != (iext (uri_rdfs_subClassOf) (uri_rdfs_ContainerMembershipProperty) (uri_rdf_Property))) % 4.67/4.89 ((uri_ex_bob) != (uri_rdfs_ContainerMembershipProperty)) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Literal)) != (iext (uri_rdfs_domain) (uri_rdfs_range) (uri_rdf_Property))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (literal_typed (dat_str_1) (uri_xsd_nonNegativeInteger))) != (iext (uri_rdfs_domain) (uri_rdf_predicate) (uri_rdfs_Statement))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdf_Property)) != (iext (uri_rdfs_domain) (uri_rdf__1) (uri_rdfs_Resource))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdf_Property)) != (iext (uri_rdfs_range) (uri_rdf_subject) (uri_rdfs_Resource))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdf_List)) != (iext (uri_rdfs_subClassOf) (uri_rdfs_Datatype) (uri_rdfs_Class))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_owl_TransitiveProperty)) != (iext (uri_rdfs_range) (uri_rdfs_range) (uri_rdfs_Class))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z)) != (iext (uri_rdfs_domain) (uri_rdfs_seeAlso) (uri_rdfs_Resource))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdf_List)) != (iext (uri_rdfs_domain) (uri_rdf_object) (uri_rdfs_Statement))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_ContainerMembershipProperty)) != (iext (uri_rdf_type) (uri_rdf_subject) (uri_rdf_Property))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_bob)) != (iext (uri_rdf_type) (uri_ex_hasAncestor) (uri_owl_TransitiveProperty))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Literal)) != (iext (uri_rdfs_domain) (uri_rdfs_seeAlso) (uri_rdfs_Resource))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z)) != (iext (uri_rdfs_domain) (uri_rdf_value) (uri_rdfs_Resource))) % 4.67/4.89 ((tuple (iext (uri_ex_hasAncestor) (uri_ex_alice) (uri_rdf_Property)) (iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdf_Property))) != (tuple (true) (true))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Resource)) != (iext (uri_rdf_type) (uri_rdf_value) (uri_rdf_Property))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_seeAlso)) != (iext (uri_rdfs_range) (uri_rdf_predicate) (uri_rdfs_Resource))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Container)) != (iext (uri_rdfs_range) (uri_rdfs_domain) (uri_rdfs_Class))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z)) != (iext (uri_rdf_type) (uri_rdf__2) (uri_rdf_Property))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_hasAncestor)) != (iext (uri_rdf_type) (uri_rdf_first) (uri_rdf_Property))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Resource)) != (iext (uri_rdfs_range) (uri_rdfs_member) (uri_rdfs_Resource))) % 4.67/4.89 ((sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z) != (uri_ex_Person)) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_seeAlso)) != (iext (uri_rdfs_range) (uri_rdfs_seeAlso) (uri_rdfs_Resource))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Container)) != (iext (uri_rdf_type) (uri_rdf__1) (uri_rdfs_ContainerMembershipProperty))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_ContainerMembershipProperty)) != (iext (uri_rdfs_domain) (uri_rdfs_subPropertyOf) (uri_rdf_Property))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_bob)) != (iext (uri_rdf_type) (uri_rdf_rest) (uri_rdf_Property))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_Person)) != (iext (uri_rdfs_domain) (uri_rdf_subject) (uri_rdfs_Statement))) % 4.67/4.89 ((iext (uri_rdf_type) (uri_ex_alice) (uri_ex_Person)) = (true)) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_seeAlso)) != (iext (uri_rdf_type) (uri_ex_hasAncestor) (uri_owl_TransitiveProperty))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) zenon_X0) != (iext (uri_rdfs_domain) (uri_rdf__3) (uri_rdfs_Resource))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_owl_Restriction)) != (iext (uri_rdfs_domain) (uri_rdfs_domain) (uri_rdf_Property))) % 4.67/4.89 ((iext (uri_rdfs_range) (uri_rdfs_member) (uri_rdfs_Resource)) = (true)) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Container)) != (iext (uri_rdf_type) (uri_rdf_value) (uri_rdf_Property))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_hasAncestor)) != (iext (uri_rdf_type) (uri_rdf__3) (uri_rdf_Property))) % 4.67/4.89 ((iext (uri_rdfs_range) (uri_rdfs_seeAlso) (uri_rdfs_Resource)) = (true)) % 4.67/4.89 ((iext (uri_rdf_type) (uri_rdf_Property) (uri_rdfs_Class)) = (true)) % 4.67/4.89 (zenon_X0 != (uri_ex_bob)) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Literal)) != (iext (uri_ex_hasAncestor) (uri_ex_alice) (uri_ex_bob))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Statement)) != (iext (uri_rdf_type) (uri_rdf_nil) (uri_rdf_List))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_ContainerMembershipProperty)) != (iext (uri_rdfs_range) (uri_rdf_value) (uri_rdfs_Resource))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Statement)) != (iext (uri_rdfs_range) (uri_rdf_predicate) (uri_rdfs_Resource))) % 4.67/4.89 ((uri_ex_bob) != (uri_rdf_first)) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Literal)) != (iext (uri_rdfs_domain) (uri_rdfs_label) (uri_rdfs_Resource))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Class)) != (iext (uri_owl_minCardinality) (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z) (literal_typed (dat_str_1) (uri_xsd_nonNegativeInteger)))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (literal_typed (dat_str_1) (uri_xsd_nonNegativeInteger))) != (iext (uri_rdfs_range) (uri_rdfs_range) (uri_rdfs_Class))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_bob)) != (iext (uri_rdfs_range) (uri_rdf_type) (uri_rdfs_Class))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) zenon_X0) != (iext (uri_rdf_type) (uri_rdf__2) (uri_rdf_Property))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_seeAlso)) != (iext (uri_rdfs_domain) (uri_rdfs_range) (uri_rdf_Property))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Container)) != (iext (uri_rdfs_range) (uri_rdf_value) (uri_rdfs_Resource))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Datatype)) != (iext (uri_rdfs_range) (uri_rdfs_subClassOf) (uri_rdfs_Class))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (literal_typed (dat_str_1) (uri_xsd_nonNegativeInteger))) != (iext (uri_rdf_type) (uri_rdf__2) (uri_rdfs_ContainerMembershipProperty))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Statement)) != (iext (uri_rdf_type) (uri_rdf__2) (uri_rdf_Property))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Resource)) != (iext (uri_rdfs_subPropertyOf) (uri_rdfs_isDefinedBy) (uri_rdfs_seeAlso))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_owl_Restriction)) != (iext (uri_rdfs_subClassOf) (uri_rdf_XMLLiteral) (uri_rdfs_Literal))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_owl_TransitiveProperty)) != (iext (uri_rdf_type) (uri_rdf_XMLLiteral) (uri_rdfs_Datatype))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_hasAncestor)) != (iext (uri_ex_hasAncestor) (uri_ex_alice) (uri_ex_bob))) % 4.67/4.89 (zenon_X0 != (literal_typed (dat_str_1) (uri_xsd_nonNegativeInteger))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_seeAlso)) != (iext (uri_rdfs_range) (uri_rdf__1) (uri_rdfs_Resource))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Literal)) != (iext (uri_rdf_type) (uri_rdf_rest) (uri_rdf_Property))) % 4.67/4.89 ((iext (uri_rdfs_range) (uri_rdfs_domain) (uri_rdfs_Class)) = (true)) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Container)) != (iext (uri_rdf_type) (uri_rdf__2) (uri_rdfs_ContainerMembershipProperty))) % 4.67/4.89 ((uri_rdfs_Class) != (uri_ex_hasAncestor)) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_owl_TransitiveProperty)) != (iext (uri_rdfs_range) (uri_rdfs_subPropertyOf) (uri_rdf_Property))) % 4.67/4.89 (zenon_X0 != (uri_rdfs_Class)) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (literal_typed (dat_str_1) (uri_xsd_nonNegativeInteger))) != (iext (uri_rdfs_domain) (uri_rdf__1) (uri_rdfs_Resource))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Literal)) != (iext (uri_owl_onProperty) (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z) (uri_ex_hasAncestor))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Container)) != (iext (uri_rdfs_range) (uri_rdfs_comment) (uri_rdfs_Literal))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_hasAncestor)) != (iext (uri_rdfs_domain) (uri_rdf_type) (uri_rdfs_Resource))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Container)) != (iext (uri_rdfs_range) (uri_rdf_subject) (uri_rdfs_Resource))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_bob)) != (iext (uri_rdfs_subClassOf) (uri_ex_Person) (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_owl_TransitiveProperty)) != (iext (uri_rdf_type) (uri_rdf_object) (uri_rdf_Property))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdf_Property)) != (iext (uri_rdf_type) (uri_rdf_subject) (uri_rdf_Property))) % 4.67/4.89 ((uri_rdfs_Datatype) != (uri_owl_Restriction)) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_bob)) != (iext (uri_rdfs_range) (uri_rdf_subject) (uri_rdfs_Resource))) % 4.67/4.89 ((iext (uri_rdf_type) (uri_rdf__1) (uri_rdfs_ContainerMembershipProperty)) = (true)) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) zenon_X0) != (iext (uri_rdf_type) (uri_rdf_value) (uri_rdf_Property))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (literal_typed (dat_str_1) (uri_xsd_nonNegativeInteger))) != (iext (uri_rdfs_domain) (uri_rdf_first) (uri_rdf_List))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Class)) != (iext (uri_rdfs_range) (uri_rdfs_seeAlso) (uri_rdfs_Resource))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Statement)) != (iext (uri_rdfs_range) (uri_rdf__2) (uri_rdfs_Resource))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Class)) != (iext (uri_ex_hasAncestor) (uri_ex_alice) (uri_ex_bob))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_owl_Restriction)) != (iext (uri_rdfs_range) (uri_rdfs_label) (uri_rdfs_Literal))) % 4.67/4.89 ((uri_owl_Restriction) != (uri_owl_TransitiveProperty)) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_hasAncestor)) != (iext (uri_rdfs_range) (uri_rdfs_seeAlso) (uri_rdfs_Resource))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_ContainerMembershipProperty)) != (iext (uri_rdfs_domain) (uri_rdfs_range) (uri_rdf_Property))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (literal_typed (dat_str_1) (uri_xsd_nonNegativeInteger))) != (iext (uri_rdf_type) (uri_rdf_Property) (uri_rdfs_Class))) % 4.67/4.89 ((uri_rdfs_seeAlso) != (uri_owl_TransitiveProperty)) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_owl_Restriction)) != (iext (uri_rdfs_domain) (uri_rdfs_label) (uri_rdfs_Resource))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Container)) != (iext (uri_rdf_type) (uri_rdf_subject) (uri_rdf_Property))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_seeAlso)) != (iext (uri_rdf_type) (uri_rdf_subject) (uri_rdf_Property))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdf_Property)) != (iext (uri_rdfs_range) (uri_rdf_type) (uri_rdfs_Class))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z)) != (iext (uri_rdf_type) (uri_rdf_value) (uri_rdf_Property))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdf_Property)) != (iext (uri_rdfs_range) (uri_rdfs_label) (uri_rdfs_Literal))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Resource)) != (iext (uri_rdfs_subClassOf) (uri_rdfs_Datatype) (uri_rdfs_Class))) % 4.67/4.89 ((uri_rdfs_Resource) != (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z)) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Statement)) != (iext (uri_rdfs_subClassOf) (uri_rdf_Alt) (uri_rdfs_Container))) % 4.67/4.89 ((iext (uri_rdfs_domain) (uri_rdf_value) (uri_rdfs_Resource)) = (true)) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Resource)) != (iext (uri_rdf_type) (uri_rdf__2) (uri_rdf_Property))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdf_List)) != (iext (uri_rdf_type) (uri_rdf_subject) (uri_rdf_Property))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Container)) != (iext (uri_rdf_type) (uri_rdf_first) (uri_rdf_Property))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_owl_Restriction)) != (iext (uri_rdfs_range) (uri_rdfs_seeAlso) (uri_rdfs_Resource))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) zenon_X0) != (iext (uri_rdfs_range) (uri_rdf_subject) (uri_rdfs_Resource))) % 4.67/4.89 ((uri_rdf_List) != (uri_rdfs_Datatype)) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) zenon_X0) != (iext (uri_ex_hasAncestor) (uri_ex_alice) (uri_ex_bob))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_owl_Restriction)) != (iext (uri_rdfs_domain) (uri_rdf_value) (uri_rdfs_Resource))) % 4.67/4.89 (zenon_X0 != (uri_rdfs_seeAlso)) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Datatype)) != (iext (uri_rdfs_domain) (uri_rdf__1) (uri_rdfs_Resource))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Statement)) != (iext (uri_rdf_type) (uri_ex_bob) (uri_ex_Person))) % 4.67/4.89 ((tuple (iext (uri_ex_hasAncestor) (uri_ex_alice) (literal_typed (dat_str_1) (uri_xsd_nonNegativeInteger))) (iext (uri_ex_hasAncestor) (uri_ex_bob) (literal_typed (dat_str_1) (uri_xsd_nonNegativeInteger)))) != (tuple (true) (true))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Datatype)) != (iext (uri_rdf_type) (uri_rdf__3) (uri_rdf_Property))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_owl_Restriction)) != (true)) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Datatype)) != (iext (uri_rdf_type) (uri_rdf__3) (uri_rdfs_ContainerMembershipProperty))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Class)) != (iext (uri_rdf_type) (uri_rdf_first) (uri_rdf_Property))) % 4.67/4.89 ((uri_owl_Restriction) != (uri_ex_Person)) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Resource)) != (iext (uri_rdfs_range) (uri_rdfs_label) (uri_rdfs_Literal))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Class)) != (iext (uri_rdfs_domain) (uri_rdf__1) (uri_rdfs_Resource))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_hasAncestor)) != (iext (uri_rdfs_domain) (uri_rdfs_isDefinedBy) (uri_rdfs_Resource))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z)) != (iext (uri_rdfs_range) (uri_rdf_type) (uri_rdfs_Class))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (literal_typed (dat_str_1) (uri_xsd_nonNegativeInteger))) != (iext (uri_rdf_type) (uri_rdf_type) (uri_rdf_Property))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_owl_Restriction)) != (iext (uri_rdfs_subClassOf) (uri_ex_Person) (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_ContainerMembershipProperty)) != (iext (uri_rdf_type) (uri_rdf_nil) (uri_rdf_List))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_ContainerMembershipProperty)) != (iext (uri_rdfs_domain) (uri_rdfs_seeAlso) (uri_rdfs_Resource))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_hasAncestor)) != (iext (uri_rdfs_domain) (uri_rdfs_subPropertyOf) (uri_rdf_Property))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Container)) != (iext (uri_rdfs_range) (uri_rdf__3) (uri_rdfs_Resource))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_Person)) != (iext (uri_rdf_type) (uri_rdf__1) (uri_rdf_Property))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) zenon_X0) != (iext (uri_owl_onProperty) (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z) (uri_ex_hasAncestor))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdf_List)) != (iext (uri_owl_minCardinality) (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z) (literal_typed (dat_str_1) (uri_xsd_nonNegativeInteger)))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Datatype)) != (iext (uri_rdfs_subClassOf) (uri_rdf_Bag) (uri_rdfs_Container))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z)) != (iext (uri_rdfs_range) (uri_rdfs_domain) (uri_rdfs_Class))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Literal)) != (iext (uri_rdfs_subClassOf) (uri_ex_Person) (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_owl_Restriction)) != (iext (uri_rdfs_range) (uri_rdf__3) (uri_rdfs_Resource))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_hasAncestor)) != (iext (uri_rdfs_range) (uri_rdf_first) (uri_rdfs_Resource))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_owl_TransitiveProperty)) != (iext (uri_rdfs_domain) (uri_rdfs_label) (uri_rdfs_Resource))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (literal_typed (dat_str_1) (uri_xsd_nonNegativeInteger))) != (iext (uri_rdfs_domain) (uri_rdf_type) (uri_rdfs_Resource))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_Person)) != (iext (uri_rdfs_domain) (uri_rdfs_subClassOf) (uri_rdfs_Class))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_hasAncestor)) != (iext (uri_rdf_type) (uri_rdf__3) (uri_rdfs_ContainerMembershipProperty))) % 4.67/4.89 ((uri_ex_hasAncestor) != (uri_rdf_type)) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) zenon_X0) != (iext (uri_rdfs_range) (uri_rdf_first) (uri_rdfs_Resource))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_ContainerMembershipProperty)) != (iext (uri_rdfs_subClassOf) (uri_rdfs_Seq) (uri_rdfs_Container))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Literal)) != (iext (uri_rdfs_domain) (uri_rdf_type) (uri_rdfs_Resource))) % 4.67/4.89 ((uri_ex_bob) != (uri_rdf_predicate)) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Literal)) != (iext (uri_rdfs_range) (uri_rdf__2) (uri_rdfs_Resource))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Datatype)) != (iext (uri_rdfs_range) (uri_rdfs_comment) (uri_rdfs_Literal))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Class)) != (iext (uri_rdfs_range) (uri_rdfs_label) (uri_rdfs_Literal))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_Person)) != (iext (uri_rdf_type) (uri_rdf__3) (uri_rdf_Property))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_owl_TransitiveProperty)) != (iext (uri_rdf_type) (uri_rdf_nil) (uri_rdf_List))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Class)) != (iext (uri_owl_onProperty) (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z) (uri_ex_hasAncestor))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_owl_Restriction)) != (iext (uri_rdfs_domain) (uri_rdfs_member) (uri_rdfs_Resource))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) zenon_X0) != (iext (uri_rdf_type) (uri_ex_hasAncestor) (uri_owl_TransitiveProperty))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_owl_Restriction)) != (iext (uri_rdfs_subClassOf) (uri_rdf_Bag) (uri_rdfs_Container))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_Person)) != (iext (uri_rdf_type) (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z) (uri_owl_Restriction))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Literal)) != (iext (uri_rdfs_range) (uri_rdfs_subClassOf) (uri_rdfs_Class))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Resource)) != (iext (uri_rdf_type) (uri_rdf__2) (uri_rdfs_ContainerMembershipProperty))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_seeAlso)) != (iext (uri_rdfs_domain) (uri_rdfs_comment) (uri_rdfs_Resource))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_seeAlso)) != (iext (uri_rdfs_domain) (uri_rdfs_label) (uri_rdfs_Resource))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_Person)) != (iext (uri_rdf_type) (uri_rdf__2) (uri_rdf_Property))) % 4.67/4.89 ((iext (uri_rdfs_domain) (uri_rdf_subject) (uri_rdfs_Statement)) = (true)) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdf_Property)) != (iext (uri_rdfs_range) (uri_rdfs_range) (uri_rdfs_Class))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Resource)) != (iext (uri_rdfs_domain) (uri_rdf__1) (uri_rdfs_Resource))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdf_List)) != (iext (uri_rdfs_domain) (uri_rdfs_label) (uri_rdfs_Resource))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_seeAlso)) != (iext (uri_rdfs_subClassOf) (uri_ex_Person) (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Class)) != (iext (uri_rdfs_range) (uri_rdfs_member) (uri_rdfs_Resource))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdf_Property)) != (iext (uri_rdfs_domain) (uri_rdfs_range) (uri_rdf_Property))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z)) != (iext (uri_rdfs_subClassOf) (uri_rdf_Bag) (uri_rdfs_Container))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Datatype)) != (iext (uri_rdfs_domain) (uri_rdfs_subPropertyOf) (uri_rdf_Property))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Class)) != (iext (uri_rdfs_range) (uri_rdf_subject) (uri_rdfs_Resource))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_bob)) != (iext (uri_rdf_type) (uri_rdf__1) (uri_rdf_Property))) % 4.67/4.89 ((tuple (iext (uri_ex_hasAncestor) (uri_ex_alice) (uri_rdfs_Statement)) (iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Statement))) != (tuple (true) (true))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdf_Property)) != (iext (uri_owl_minCardinality) (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z) (literal_typed (dat_str_1) (uri_xsd_nonNegativeInteger)))) % 4.67/4.89 ((tuple (iext (uri_ex_hasAncestor) (uri_ex_alice) (uri_rdfs_seeAlso)) (iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_seeAlso))) != (tuple (true) (true))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_bob)) != (iext (uri_rdfs_range) (uri_rdf__3) (uri_rdfs_Resource))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_bob)) != (iext (uri_rdfs_domain) (uri_rdfs_member) (uri_rdfs_Resource))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_seeAlso)) != (iext (uri_rdf_type) (uri_rdf_value) (uri_rdf_Property))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) zenon_X0) != (iext (uri_rdf_type) (uri_rdf__1) (uri_rdf_Property))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdf_Property)) != (iext (uri_rdfs_range) (uri_rdfs_seeAlso) (uri_rdfs_Resource))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Datatype)) != (iext (uri_rdfs_range) (uri_rdf_predicate) (uri_rdfs_Resource))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_ContainerMembershipProperty)) != (iext (uri_rdfs_domain) (uri_rdf_rest) (uri_rdf_List))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_hasAncestor)) != (iext (uri_rdf_type) (uri_rdf_type) (uri_rdf_Property))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) zenon_X0) != (iext (uri_rdf_type) (uri_rdf__2) (uri_rdfs_ContainerMembershipProperty))) % 4.67/4.89 ((iext (uri_rdfs_subClassOf) (uri_rdf_Bag) (uri_rdfs_Container)) = (true)) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_Person)) != (iext (uri_rdf_type) (uri_rdf_rest) (uri_rdf_Property))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (literal_typed (dat_str_1) (uri_xsd_nonNegativeInteger))) != (iext (uri_rdfs_range) (uri_rdfs_isDefinedBy) (uri_rdfs_Resource))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdf_Property)) != (iext (uri_rdfs_domain) (uri_rdf_value) (uri_rdfs_Resource))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Container)) != (iext (uri_rdfs_range) (uri_rdfs_range) (uri_rdfs_Class))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdf_Property)) != (iext (uri_owl_onProperty) (sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z) (uri_ex_hasAncestor))) % 4.67/4.89 ((uri_ex_bob) != (uri_rdfs_isDefinedBy)) % 4.67/4.89 ((uri_rdfs_Statement) != (uri_owl_TransitiveProperty)) % 4.67/4.89 ((tuple (iext (uri_ex_hasAncestor) (uri_ex_alice) (uri_rdfs_Class)) (iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Class))) != (tuple (true) (true))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_owl_TransitiveProperty)) != (iext (uri_rdfs_domain) (uri_rdfs_range) (uri_rdf_Property))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_owl_TransitiveProperty)) != (iext (uri_rdf_type) (uri_rdf_rest) (uri_rdf_Property))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdf_Property)) != (iext (uri_rdf_type) (uri_rdf__1) (uri_rdf_Property))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_Person)) != (iext (uri_rdfs_subClassOf) (uri_rdfs_ContainerMembershipProperty) (uri_rdf_Property))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) zenon_X0) != (iext (uri_rdfs_domain) (uri_rdf__2) (uri_rdfs_Resource))) % 4.67/4.89 ((uri_rdfs_Container) != (uri_owl_TransitiveProperty)) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdf_List)) != (iext (uri_rdf_type) (uri_rdf_first) (uri_rdf_Property))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_owl_Restriction)) != (iext (uri_rdfs_range) (uri_rdf_value) (uri_rdfs_Resource))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_owl_TransitiveProperty)) != (iext (uri_rdfs_range) (uri_rdfs_seeAlso) (uri_rdfs_Resource))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_ex_Person)) != (iext (uri_rdfs_subClassOf) (uri_rdf_Bag) (uri_rdfs_Container))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Literal)) != (iext (uri_rdf_type) (uri_rdf_value) (uri_rdf_Property))) % 4.67/4.89 ((iext (uri_ex_hasAncestor) (uri_ex_bob) (uri_rdfs_Datatype)) != (iext (uri_rdfs_subClassOf) (uri_rdf_Alt) (uri_rdfs_Container))) % 4.67/4.89 ((iext (uri_rdfs_range) (uri_rdfs_range) (uri_rdfs_Class)) = (true)) % 4.67/4.89 ((uri_rdfs_Literal) != (literal_typed (dat_str_1) (uri_xsd_nonNegativeInteger))) % 4.67/4.89 *) % 4.67/4.89 (* NO-PROOF *) % 4.67/4.89 % SZS status GaveUp % 4.67/4.89 Number of rewrites on terms: 0 % 4.67/4.89 Number of rewrites on props: 0 % 4.67/4.89 nodes searched: 166513 % 4.67/4.89 max branch formulas: 1455 % 4.67/4.89 proof nodes created: 1237 % 4.67/4.89 formulas created: 124574 % 4.67/4.89 %------------------------------------------------------------------------------