%------------------------------------------------------------------------------ % File : Metis---2.4 % Problem : SWB024-10 : TPTP v8.1.0. Released v7.3.0. % Transfm : none % Format : tptp:raw % Command : metis --show proof --show saturation %s % Computer : n027.cluster.edu % Model : x86_64 x86_64 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz % Memory : 8042.1875MB % OS : Linux 3.10.0-693.el7.x86_64 % CPULimit : 300s % WCLimit : 600s % DateTime : Tue Jul 19 19:15:27 EDT 2022 % Result : Satisfiable 0.84s 1.03s % Output : Saturation 0.92s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.00/0.12 % Problem : SWB024-10 : TPTP v8.1.0. Released v7.3.0. % 0.00/0.12 % Command : metis --show proof --show saturation %s % 0.12/0.33 % Computer : n027.cluster.edu % 0.12/0.33 % Model : x86_64 x86_64 % 0.12/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.12/0.33 % Memory : 8042.1875MB % 0.12/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.12/0.33 % CPULimit : 300 % 0.12/0.33 % WCLimit : 600 % 0.12/0.33 % DateTime : Wed Jun 1 05:46:18 EDT 2022 % 0.12/0.33 % CPUTime : % 0.12/0.34 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 0.84/1.03 % SZS status Satisfiable for /export/starexec/sandbox/benchmark/theBenchmark.p % 0.84/1.03 % 0.84/1.03 SZS output start Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 0.84/1.03 |- ifeq $A $A $B $C = $B % 0.84/1.03 |- ifeq (iext $P $S $O) true (ip $P) true = true % 0.84/1.03 |- ir $X = true % 0.84/1.03 |- ifeq (lv $X) true true true = true % 0.84/1.03 |- iext uri_rdf_type uri_rdf_first uri_rdf_Property = true % 0.84/1.03 |- iext uri_rdf_type uri_rdf_nil uri_rdf_List = true % 0.84/1.03 |- iext uri_rdf_type uri_rdf_rest uri_rdf_Property = true % 0.84/1.03 |- iext uri_rdf_type uri_rdf__1 uri_rdf_Property = true % 0.84/1.03 |- iext uri_rdf_type uri_rdf__2 uri_rdf_Property = true % 0.84/1.03 |- iext uri_rdf_type uri_rdf__3 uri_rdf_Property = true % 0.84/1.03 |- iext uri_rdf_type uri_rdf_object uri_rdf_Property = true % 0.84/1.03 |- iext uri_rdf_type uri_rdf_value uri_rdf_Property = true % 0.84/1.04 |- iext uri_rdf_type uri_rdf_subject uri_rdf_Property = true % 0.84/1.04 |- ifeq (ip $P) true (iext uri_rdf_type $P uri_rdf_Property) true = true % 0.84/1.04 |- ifeq (iext uri_rdf_type $P uri_rdf_Property) true (ip $P) true = true % 0.84/1.04 |- iext uri_rdf_type uri_rdf_type uri_rdf_Property = true % 0.84/1.04 |- iext uri_rdfs_domain uri_rdfs_comment uri_rdfs_Resource = true % 0.84/1.04 |- iext uri_rdfs_range uri_rdfs_comment uri_rdfs_Literal = true % 0.84/1.04 |- iext uri_rdfs_domain uri_rdfs_isDefinedBy uri_rdfs_Resource = true % 0.84/1.04 |- iext uri_rdfs_range uri_rdfs_isDefinedBy uri_rdfs_Resource = true % 0.84/1.04 |- iext uri_rdfs_subPropertyOf uri_rdfs_isDefinedBy uri_rdfs_seeAlso = true % 0.84/1.04 |- iext uri_rdfs_domain uri_rdfs_label uri_rdfs_Resource = true % 0.84/1.04 |- iext uri_rdfs_range uri_rdfs_label uri_rdfs_Literal = true % 0.84/1.04 |- iext uri_rdfs_domain uri_rdfs_seeAlso uri_rdfs_Resource = true % 0.84/1.04 |- iext uri_rdfs_range uri_rdfs_seeAlso uri_rdfs_Resource = true % 0.84/1.04 |- ifeq (icext $C $X) true (iext uri_rdf_type $X $C) true = true % 0.84/1.04 |- ifeq (iext uri_rdf_type $X $C) true (icext $C $X) true = true % 0.84/1.04 |- ifeq (ic $C) true (iext uri_rdfs_subClassOf $C uri_rdfs_Resource) true = % 0.84/1.04 true % 0.84/1.04 |- iext uri_rdfs_domain uri_rdf_first uri_rdf_List = true % 0.84/1.04 |- iext uri_rdfs_range uri_rdf_first uri_rdfs_Resource = true % 0.84/1.04 |- iext uri_rdfs_domain uri_rdf_rest uri_rdf_List = true % 0.84/1.04 |- iext uri_rdfs_range uri_rdf_rest uri_rdf_List = true % 0.84/1.04 |- iext uri_rdfs_subClassOf uri_rdf_Alt uri_rdfs_Container = true % 0.84/1.04 |- iext uri_rdfs_subClassOf uri_rdf_Bag uri_rdfs_Container = true % 0.84/1.04 |- ifeq (icext uri_rdfs_ContainerMembershipProperty $P) true % 0.84/1.04 (iext uri_rdfs_subPropertyOf $P uri_rdfs_member) true = true % 0.84/1.04 |- iext uri_rdfs_subClassOf uri_rdfs_ContainerMembershipProperty % 0.84/1.04 uri_rdf_Property = true % 0.84/1.04 |- iext uri_rdfs_domain uri_rdfs_member uri_rdfs_Resource = true % 0.84/1.04 |- iext uri_rdfs_range uri_rdfs_member uri_rdfs_Resource = true % 0.84/1.04 |- iext uri_rdfs_domain uri_rdf__1 uri_rdfs_Resource = true % 0.84/1.04 |- iext uri_rdfs_domain uri_rdf__2 uri_rdfs_Resource = true % 0.84/1.04 |- iext uri_rdfs_domain uri_rdf__3 uri_rdfs_Resource = true % 0.84/1.04 |- iext uri_rdfs_range uri_rdf__1 uri_rdfs_Resource = true % 0.84/1.04 |- iext uri_rdfs_range uri_rdf__2 uri_rdfs_Resource = true % 0.84/1.04 |- iext uri_rdfs_range uri_rdf__3 uri_rdfs_Resource = true % 0.84/1.04 |- iext uri_rdf_type uri_rdf__1 uri_rdfs_ContainerMembershipProperty = true % 0.84/1.04 |- iext uri_rdf_type uri_rdf__2 uri_rdfs_ContainerMembershipProperty = true % 0.84/1.04 |- iext uri_rdf_type uri_rdf__3 uri_rdfs_ContainerMembershipProperty = true % 0.84/1.04 |- iext uri_rdfs_subClassOf uri_rdfs_Seq uri_rdfs_Container = true % 0.84/1.04 |- iext uri_rdfs_subClassOf uri_rdf_XMLLiteral uri_rdfs_Literal = true % 0.84/1.04 |- iext uri_rdf_type uri_rdf_XMLLiteral uri_rdfs_Datatype = true % 0.84/1.04 |- ifeq (icext uri_rdfs_Datatype $D) true % 0.84/1.04 (iext uri_rdfs_subClassOf $D uri_rdfs_Literal) true = true % 0.84/1.04 |- iext uri_rdfs_subClassOf uri_rdfs_Datatype uri_rdfs_Class = true % 0.84/1.04 |- iext uri_rdfs_domain uri_rdfs_domain uri_rdf_Property = true % 0.84/1.04 |- ifeq (iext uri_rdfs_domain $P $C) true % 0.84/1.04 (ifeq (iext $P $X $Y) true (icext $C $X) true) true = true % 0.84/1.04 |- iext uri_rdfs_range uri_rdfs_domain uri_rdfs_Class = true % 0.84/1.04 |- ifeq (ic $X) true (icext uri_rdfs_Class $X) true = true % 0.84/1.04 |- ifeq (icext uri_rdfs_Class $X) true (ic $X) true = true % 0.84/1.04 |- icext uri_rdfs_Resource $X = true % 0.84/1.04 |- ifeq (icext uri_rdfs_Literal $X) true (lv $X) true = true % 0.84/1.04 |- ifeq (lv $X) true (icext uri_rdfs_Literal $X) true = true % 0.84/1.04 |- iext uri_rdf_type uri_rdf_Property uri_rdfs_Class = true % 0.84/1.04 |- iext uri_rdfs_domain uri_rdfs_range uri_rdf_Property = true % 0.84/1.04 |- ifeq (iext uri_rdfs_range $P $C) true % 0.84/1.04 (ifeq (iext $P $X $Y) true (icext $C $Y) true) true = true % 0.84/1.04 |- iext uri_rdfs_range uri_rdfs_range uri_rdfs_Class = true % 0.84/1.04 |- iext uri_rdfs_domain uri_rdf_object uri_rdfs_Statement = true % 0.84/1.04 |- iext uri_rdfs_range uri_rdf_predicate uri_rdfs_Resource = true % 0.84/1.04 |- iext uri_rdfs_domain uri_rdf_predicate uri_rdfs_Statement = true % 0.84/1.04 |- iext uri_rdfs_domain uri_rdf_subject uri_rdfs_Statement = true % 0.84/1.04 |- iext uri_rdfs_range uri_rdf_subject uri_rdfs_Resource = true % 0.84/1.04 |- iext uri_rdfs_domain uri_rdfs_subClassOf uri_rdfs_Class = true % 0.84/1.04 |- ifeq (icext $C $X) true % 0.84/1.04 (ifeq (iext uri_rdfs_subClassOf $C $D) true (icext $D $X) true) true = % 0.84/1.04 true % 0.84/1.04 |- ifeq (iext uri_rdfs_subClassOf $C $D) true (ic $D) true = true % 0.84/1.04 |- ifeq (iext uri_rdfs_subClassOf $C $D) true (ic $C) true = true % 0.84/1.04 |- iext uri_rdfs_range uri_rdfs_subClassOf uri_rdfs_Class = true % 0.84/1.04 |- ifeq (ic $C) true (iext uri_rdfs_subClassOf $C $C) true = true % 0.84/1.04 |- ifeq (iext uri_rdfs_subClassOf $D $E) true % 0.84/1.04 (ifeq (iext uri_rdfs_subClassOf $C $D) true % 0.84/1.04 (iext uri_rdfs_subClassOf $C $E) true) true = true % 0.84/1.04 |- iext uri_rdfs_domain uri_rdfs_subPropertyOf uri_rdf_Property = true % 0.84/1.04 |- ifeq (iext uri_rdfs_subPropertyOf $P $Q) true (ip $Q) true = true % 0.84/1.04 |- ifeq (iext uri_rdfs_subPropertyOf $P $Q) true (ip $P) true = true % 0.84/1.04 |- ifeq (iext uri_rdfs_subPropertyOf $P $Q) true % 0.84/1.04 (ifeq (iext $P $X $Y) true (iext $Q $X $Y) true) true = true % 0.84/1.04 |- iext uri_rdfs_range uri_rdfs_subPropertyOf uri_rdf_Property = true % 0.84/1.04 |- ifeq (ip $P) true (iext uri_rdfs_subPropertyOf $P $P) true = true % 0.84/1.04 |- ifeq (iext uri_rdfs_subPropertyOf $Q $R) true % 0.84/1.04 (ifeq (iext uri_rdfs_subPropertyOf $P $Q) true % 0.84/1.04 (iext uri_rdfs_subPropertyOf $P $R) true) true = true % 0.84/1.04 |- iext uri_rdfs_domain uri_rdf_type uri_rdfs_Resource = true % 0.84/1.04 |- iext uri_rdfs_range uri_rdf_type uri_rdfs_Class = true % 0.84/1.04 |- iext uri_rdfs_domain uri_rdf_value uri_rdfs_Resource = true % 0.84/1.04 |- iext uri_rdfs_range uri_rdf_value uri_rdfs_Resource = true % 0.84/1.04 |- iext uri_owl_minCardinality % 0.84/1.04 sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z % 0.84/1.04 (literal_typed dat_str_1 uri_xsd_nonNegativeInteger) = true % 0.84/1.04 |- iext uri_owl_onProperty % 0.84/1.04 sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z % 0.84/1.04 uri_ex_hasAncestor = true % 0.84/1.04 |- iext uri_rdf_type % 0.84/1.04 sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z % 0.84/1.04 uri_owl_Restriction = true % 0.84/1.04 |- iext uri_rdf_type uri_ex_bob uri_ex_Person = true % 0.84/1.04 |- iext uri_rdf_type uri_ex_alice uri_ex_Person = true % 0.84/1.04 |- iext uri_rdf_type uri_ex_hasAncestor uri_owl_TransitiveProperty = true % 0.84/1.04 |- iext uri_ex_hasAncestor uri_ex_alice uri_ex_bob = true % 0.84/1.04 |- iext uri_rdfs_subClassOf uri_ex_Person % 0.84/1.04 sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z = % 0.84/1.04 true % 0.84/1.04 |- ~(tuple (iext uri_ex_hasAncestor uri_ex_alice $BNODE_x) % 0.84/1.04 (iext uri_ex_hasAncestor uri_ex_bob $BNODE_x) = tuple true true) % 0.84/1.04 |- ip uri_rdf__1 = true % 0.84/1.04 |- ip uri_rdf__2 = true % 0.84/1.04 |- ip uri_rdf__3 = true % 0.84/1.04 |- ip uri_rdf_first = true % 0.84/1.04 |- ip uri_rdf_object = true % 0.84/1.04 |- ip uri_rdf_rest = true % 0.84/1.04 |- ip uri_rdf_subject = true % 0.84/1.04 |- ip uri_rdf_type = true % 0.84/1.04 |- ip uri_rdf_value = true % 0.84/1.04 |- iext uri_rdfs_subPropertyOf uri_rdf__1 uri_rdf__1 = true % 0.84/1.04 |- iext uri_rdfs_subPropertyOf uri_rdf__2 uri_rdf__2 = true % 0.84/1.04 |- iext uri_rdfs_subPropertyOf uri_rdf__3 uri_rdf__3 = true % 0.84/1.04 |- iext uri_rdfs_subPropertyOf uri_rdf_first uri_rdf_first = true % 0.84/1.04 |- iext uri_rdfs_subPropertyOf uri_rdf_object uri_rdf_object = true % 0.84/1.04 |- iext uri_rdfs_subPropertyOf uri_rdf_rest uri_rdf_rest = true % 0.84/1.04 |- iext uri_rdfs_subPropertyOf uri_rdf_subject uri_rdf_subject = true % 0.84/1.04 |- iext uri_rdfs_subPropertyOf uri_rdf_type uri_rdf_type = true % 0.84/1.04 |- iext uri_rdfs_subPropertyOf uri_rdf_value uri_rdf_value = true % 0.84/1.04 |- ip uri_rdfs_isDefinedBy = true % 0.84/1.04 |- iext uri_rdfs_subPropertyOf uri_rdfs_isDefinedBy uri_rdfs_isDefinedBy = % 0.84/1.04 true % 0.84/1.04 |- iext uri_rdf_type uri_rdfs_isDefinedBy uri_rdf_Property = true % 0.84/1.04 |- ic % 0.84/1.04 sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z = % 0.84/1.04 true % 0.84/1.04 |- ic uri_rdfs_Container = true % 0.84/1.04 |- ic uri_rdfs_Literal = true % 0.84/1.04 |- ic uri_rdf_Property = true % 0.84/1.04 |- ic uri_rdfs_Class = true % 0.84/1.04 |- iext uri_rdfs_subClassOf uri_rdfs_Container uri_rdfs_Container = true % 0.84/1.04 |- iext uri_rdfs_subClassOf uri_rdfs_Container uri_rdfs_Resource = true % 0.84/1.04 |- icext uri_rdfs_Class uri_rdfs_Container = true % 0.84/1.04 |- iext uri_rdfs_subClassOf uri_rdfs_Literal uri_rdfs_Literal = true % 0.84/1.04 |- iext uri_rdfs_subClassOf uri_rdfs_Literal uri_rdfs_Resource = true % 0.84/1.04 |- icext uri_rdfs_Class uri_rdfs_Literal = true % 0.84/1.04 |- iext uri_rdfs_subClassOf uri_rdf_Property uri_rdf_Property = true % 0.84/1.04 |- iext uri_rdfs_subClassOf uri_rdf_Property uri_rdfs_Resource = true % 0.84/1.04 |- icext uri_rdfs_Class uri_rdf_Property = true % 0.84/1.04 |- ic uri_rdfs_Resource = true % 0.84/1.04 |- iext uri_rdfs_subClassOf % 0.84/1.04 sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z % 0.84/1.04 sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z = % 0.84/1.04 true % 0.84/1.04 |- iext uri_rdfs_subClassOf % 0.84/1.04 sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z % 0.84/1.04 uri_rdfs_Resource = true % 0.84/1.04 |- icext uri_rdfs_Class % 0.84/1.04 sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z = % 0.84/1.04 true % 0.84/1.04 |- iext uri_rdfs_subClassOf uri_rdfs_Class uri_rdfs_Class = true % 0.84/1.04 |- iext uri_rdfs_subClassOf uri_rdfs_Class uri_rdfs_Resource = true % 0.84/1.04 |- icext uri_rdfs_Class uri_rdfs_Class = true % 0.84/1.04 |- iext uri_rdfs_subClassOf uri_rdfs_Resource uri_rdfs_Resource = true % 0.84/1.04 |- icext uri_rdfs_Class uri_rdfs_Resource = true % 0.84/1.04 |- ic uri_ex_Person = true % 0.84/1.04 |- ic uri_rdf_Alt = true % 0.84/1.04 |- ic uri_rdf_Bag = true % 0.84/1.04 |- ic uri_rdf_XMLLiteral = true % 0.84/1.04 |- ic uri_rdfs_ContainerMembershipProperty = true % 0.84/1.04 |- ic uri_rdfs_Datatype = true % 0.84/1.04 |- ic uri_rdfs_Seq = true % 0.84/1.04 |- iext uri_rdfs_subClassOf uri_rdf_Bag uri_rdf_Bag = true % 0.84/1.04 |- iext uri_rdfs_subClassOf uri_rdf_Bag uri_rdfs_Resource = true % 0.84/1.04 |- icext uri_rdfs_Class uri_rdf_Bag = true % 0.84/1.04 |- iext uri_rdfs_subClassOf uri_rdf_XMLLiteral uri_rdf_XMLLiteral = true % 0.84/1.04 |- iext uri_rdfs_subClassOf uri_rdf_XMLLiteral uri_rdfs_Resource = true % 0.84/1.04 |- icext uri_rdfs_Class uri_rdf_XMLLiteral = true % 0.84/1.04 |- iext uri_rdfs_subClassOf uri_rdfs_ContainerMembershipProperty % 0.84/1.04 uri_rdfs_ContainerMembershipProperty = true % 0.84/1.04 |- iext uri_rdfs_subClassOf uri_rdfs_ContainerMembershipProperty % 0.84/1.04 uri_rdfs_Resource = true % 0.84/1.04 |- icext uri_rdfs_Class uri_rdfs_ContainerMembershipProperty = true % 0.84/1.04 |- iext uri_rdfs_subClassOf uri_rdfs_Datatype uri_rdfs_Datatype = true % 0.84/1.04 |- iext uri_rdfs_subClassOf uri_rdfs_Datatype uri_rdfs_Resource = true % 0.84/1.04 |- icext uri_rdfs_Class uri_rdfs_Datatype = true % 0.84/1.04 |- iext uri_rdfs_subClassOf uri_rdfs_Seq uri_rdfs_Seq = true % 0.84/1.04 |- iext uri_rdfs_subClassOf uri_rdfs_Seq uri_rdfs_Resource = true % 0.84/1.04 |- icext uri_rdfs_Class uri_rdfs_Seq = true % 0.84/1.04 |- iext uri_rdfs_subClassOf uri_ex_Person uri_ex_Person = true % 0.84/1.04 |- iext uri_rdfs_subClassOf uri_ex_Person uri_rdfs_Resource = true % 0.84/1.04 |- icext uri_rdfs_Class uri_ex_Person = true % 0.84/1.04 |- iext uri_rdfs_subClassOf uri_rdf_Alt uri_rdf_Alt = true % 0.84/1.04 |- iext uri_rdfs_subClassOf uri_rdf_Alt uri_rdfs_Resource = true % 0.84/1.04 |- icext uri_rdfs_Class uri_rdf_Alt = true % 0.84/1.04 |- ip uri_rdfs_seeAlso = true % 0.84/1.04 |- iext uri_rdfs_subPropertyOf uri_rdfs_seeAlso uri_rdfs_seeAlso = true % 0.84/1.04 |- iext uri_rdf_type uri_rdfs_seeAlso uri_rdf_Property = true % 0.84/1.04 |- iext uri_rdf_type % 0.84/1.04 sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z % 0.84/1.04 uri_rdfs_Class = true % 0.84/1.04 |- iext uri_rdf_type uri_ex_Person uri_rdfs_Class = true % 0.84/1.04 |- iext uri_rdf_type uri_rdf_Alt uri_rdfs_Class = true % 0.84/1.04 |- iext uri_rdf_type uri_rdf_Bag uri_rdfs_Class = true % 0.84/1.04 |- iext uri_rdf_type uri_rdf_XMLLiteral uri_rdfs_Class = true % 0.84/1.04 |- iext uri_rdf_type uri_rdfs_Class uri_rdfs_Class = true % 0.84/1.04 |- iext uri_rdf_type uri_rdfs_Container uri_rdfs_Class = true % 0.84/1.04 |- iext uri_rdf_type uri_rdfs_ContainerMembershipProperty uri_rdfs_Class = % 0.84/1.04 true % 0.84/1.04 |- iext uri_rdf_type uri_rdfs_Datatype uri_rdfs_Class = true % 0.84/1.04 |- iext uri_rdf_type uri_rdfs_Literal uri_rdfs_Class = true % 0.84/1.04 |- iext uri_rdf_type uri_rdfs_Resource uri_rdfs_Class = true % 0.84/1.04 |- iext uri_rdf_type uri_rdfs_Seq uri_rdfs_Class = true % 0.84/1.04 |- iext uri_rdf_type $_56 uri_rdfs_Resource = true % 0.84/1.04 |- icext uri_owl_Restriction % 0.84/1.04 sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z = % 0.84/1.04 true % 0.84/1.04 |- icext uri_ex_Person uri_ex_alice = true % 0.84/1.04 |- icext uri_ex_Person uri_ex_bob = true % 0.84/1.04 |- icext uri_owl_TransitiveProperty uri_ex_hasAncestor = true % 0.84/1.04 |- icext uri_rdfs_Datatype uri_rdf_XMLLiteral = true % 0.84/1.04 |- icext uri_rdf_Property uri_rdf__1 = true % 0.84/1.04 |- icext uri_rdfs_ContainerMembershipProperty uri_rdf__1 = true % 0.84/1.04 |- icext uri_rdf_Property uri_rdf__2 = true % 0.84/1.04 |- icext uri_rdfs_ContainerMembershipProperty uri_rdf__2 = true % 0.84/1.04 |- icext uri_rdf_Property uri_rdf__3 = true % 0.84/1.04 |- icext uri_rdfs_ContainerMembershipProperty uri_rdf__3 = true % 0.84/1.04 |- icext uri_rdf_Property uri_rdf_first = true % 0.84/1.04 |- icext uri_rdf_List uri_rdf_nil = true % 0.84/1.04 |- icext uri_rdf_Property uri_rdf_object = true % 0.84/1.04 |- icext uri_rdf_Property uri_rdf_rest = true % 0.84/1.04 |- icext uri_rdf_Property uri_rdf_subject = true % 0.84/1.04 |- icext uri_rdf_Property uri_rdf_type = true % 0.84/1.04 |- icext uri_rdf_Property uri_rdf_value = true % 0.84/1.04 |- icext uri_rdf_Property uri_rdfs_isDefinedBy = true % 0.84/1.04 |- icext uri_rdf_Property uri_rdfs_seeAlso = true % 0.84/1.04 |- iext uri_rdfs_subPropertyOf uri_rdf__2 uri_rdfs_member = true % 0.84/1.04 |- ip uri_rdfs_member = true % 0.84/1.04 |- iext uri_rdfs_subPropertyOf uri_rdfs_member uri_rdfs_member = true % 0.84/1.04 |- iext uri_rdf_type uri_rdfs_member uri_rdf_Property = true % 0.84/1.04 |- icext uri_rdf_Property uri_rdfs_member = true % 0.84/1.04 |- iext uri_rdfs_subPropertyOf uri_rdf__1 uri_rdfs_member = true % 0.84/1.04 |- iext uri_rdfs_subPropertyOf uri_rdf__3 uri_rdfs_member = true % 0.84/1.04 |- ~(tuple true (iext uri_ex_hasAncestor uri_ex_bob uri_ex_bob) = % 0.84/1.04 tuple true true) % 0.84/1.04 |- ifeq (iext uri_rdf__1 $_83 $_81) true true true = true % 0.84/1.04 |- ifeq (iext uri_rdf__2 $_83 $_81) true true true = true % 0.84/1.04 |- ifeq (iext uri_rdf__3 $_83 $_81) true true true = true % 0.84/1.04 |- ifeq (iext uri_rdf_first $_83 $_81) true true true = true % 0.84/1.04 |- ifeq (iext uri_rdf_object $_83 $_81) true true true = true % 0.84/1.04 |- ifeq (iext uri_rdf_rest $_83 $_81) true true true = true % 0.84/1.04 |- ifeq (iext uri_rdf_subject $_83 $_81) true true true = true % 0.84/1.04 |- ifeq (iext uri_rdf_type $_83 $_81) true true true = true % 0.84/1.04 |- ifeq (iext uri_rdf_value $_83 $_81) true true true = true % 0.84/1.04 |- ifeq (iext uri_rdfs_isDefinedBy $_83 $_81) true true true = true % 0.84/1.04 |- ifeq (iext uri_rdfs_member $_83 $_81) true true true = true % 0.84/1.04 |- ifeq (iext uri_rdfs_seeAlso $_83 $_81) true true true = true % 0.84/1.04 |- ip uri_ex_hasAncestor = true % 0.84/1.04 |- ip uri_owl_minCardinality = true % 0.84/1.04 |- ip uri_owl_onProperty = true % 0.84/1.04 |- ip uri_rdfs_domain = true % 0.84/1.04 |- ip uri_rdfs_range = true % 0.84/1.04 |- ip uri_rdfs_subClassOf = true % 0.84/1.04 |- ip uri_rdfs_subPropertyOf = true % 0.84/1.04 |- ifeq (iext uri_ex_hasAncestor $S $O) true true true = true % 0.84/1.04 |- iext uri_rdfs_subPropertyOf uri_ex_hasAncestor uri_ex_hasAncestor = true % 0.84/1.04 |- iext uri_rdf_type uri_ex_hasAncestor uri_rdf_Property = true % 0.84/1.04 |- ifeq (iext uri_owl_minCardinality $S $O) true true true = true % 0.84/1.04 |- iext uri_rdfs_subPropertyOf uri_owl_minCardinality % 0.84/1.04 uri_owl_minCardinality = true % 0.84/1.04 |- iext uri_rdf_type uri_owl_minCardinality uri_rdf_Property = true % 0.84/1.04 |- ifeq (iext uri_owl_onProperty $S $O) true true true = true % 0.84/1.04 |- iext uri_rdfs_subPropertyOf uri_owl_onProperty uri_owl_onProperty = true % 0.84/1.04 |- iext uri_rdf_type uri_owl_onProperty uri_rdf_Property = true % 0.84/1.04 |- ifeq (iext uri_rdfs_subClassOf $S $O) true true true = true % 0.84/1.04 |- iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf uri_rdfs_subClassOf = % 0.84/1.04 true % 0.84/1.04 |- iext uri_rdf_type uri_rdfs_subClassOf uri_rdf_Property = true % 0.84/1.04 |- ifeq (iext uri_rdfs_subPropertyOf $S $O) true true true = true % 0.84/1.04 |- iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf % 0.84/1.04 uri_rdfs_subPropertyOf = true % 0.84/1.04 |- iext uri_rdf_type uri_rdfs_subPropertyOf uri_rdf_Property = true % 0.84/1.04 |- icext uri_rdf_Property uri_rdfs_subPropertyOf = true % 0.84/1.04 |- icext uri_rdf_Property uri_owl_onProperty = true % 0.84/1.04 |- ifeq (iext uri_rdfs_domain $S $O) true true true = true % 0.84/1.04 |- iext uri_rdfs_subPropertyOf uri_rdfs_domain uri_rdfs_domain = true % 0.84/1.04 |- iext uri_rdf_type uri_rdfs_domain uri_rdf_Property = true % 0.84/1.04 |- icext uri_rdf_Property uri_rdfs_domain = true % 0.84/1.04 |- ifeq (iext uri_rdfs_range $S $O) true true true = true % 0.84/1.04 |- iext uri_rdfs_subPropertyOf uri_rdfs_range uri_rdfs_range = true % 0.84/1.04 |- iext uri_rdf_type uri_rdfs_range uri_rdf_Property = true % 0.84/1.04 |- icext uri_rdf_Property uri_rdfs_range = true % 0.84/1.04 |- icext uri_rdf_Property uri_ex_hasAncestor = true % 0.84/1.04 |- icext uri_rdf_Property uri_owl_minCardinality = true % 0.84/1.04 |- icext uri_rdf_Property uri_rdfs_subClassOf = true % 0.84/1.04 |- ifeq (icext $_122 $_124) true true true = true % 0.84/1.04 |- ifeq % 0.84/1.04 (icext % 0.84/1.04 sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z % 0.84/1.04 $_124) true % 0.84/1.04 (icext % 0.84/1.04 sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z % 0.84/1.04 $_124) true = true % 0.84/1.04 |- ifeq (icext uri_ex_Person $_124) true % 0.84/1.04 (icext % 0.84/1.04 sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z % 0.84/1.04 $_124) true = true % 0.84/1.04 |- ifeq (icext uri_ex_Person $_124) true (icext uri_ex_Person $_124) true = % 0.84/1.04 true % 0.84/1.04 |- ifeq (icext uri_rdf_Alt $_124) true (icext uri_rdf_Alt $_124) true = % 0.84/1.04 true % 0.84/1.04 |- ifeq (icext uri_rdf_Alt $_124) true (icext uri_rdfs_Container $_124) % 0.84/1.04 true = true % 0.84/1.04 |- ifeq (icext uri_rdf_Bag $_124) true (icext uri_rdf_Bag $_124) true = % 0.84/1.04 true % 0.84/1.04 |- ifeq (icext uri_rdf_Bag $_124) true (icext uri_rdfs_Container $_124) % 0.84/1.04 true = true % 0.84/1.04 |- ifeq (icext uri_rdf_Property $_124) true (icext uri_rdf_Property $_124) % 0.84/1.04 true = true % 0.84/1.05 |- ifeq (icext uri_rdf_XMLLiteral $_124) true % 0.84/1.05 (icext uri_rdf_XMLLiteral $_124) true = true % 0.84/1.05 |- ifeq (icext uri_rdf_XMLLiteral $_124) true % 0.84/1.05 (icext uri_rdfs_Literal $_124) true = true % 0.84/1.05 |- ifeq (icext uri_rdfs_Class $_124) true (icext uri_rdfs_Class $_124) % 0.84/1.05 true = true % 0.84/1.05 |- ifeq (icext uri_rdfs_Container $_124) true % 0.84/1.05 (icext uri_rdfs_Container $_124) true = true % 0.84/1.05 |- ifeq (icext uri_rdfs_ContainerMembershipProperty $_124) true % 0.84/1.05 (icext uri_rdf_Property $_124) true = true % 0.84/1.05 |- ifeq (icext uri_rdfs_ContainerMembershipProperty $_124) true % 0.84/1.05 (icext uri_rdfs_ContainerMembershipProperty $_124) true = true % 0.84/1.05 |- ifeq (icext uri_rdfs_Datatype $_124) true (icext uri_rdfs_Class $_124) % 0.84/1.05 true = true % 0.84/1.05 |- ifeq (icext uri_rdfs_Datatype $_124) true % 0.84/1.05 (icext uri_rdfs_Datatype $_124) true = true % 0.84/1.05 |- ifeq (icext uri_rdfs_Literal $_124) true (icext uri_rdfs_Literal $_124) % 0.84/1.05 true = true % 0.84/1.05 |- ifeq (icext uri_rdfs_Seq $_124) true (icext uri_rdfs_Container $_124) % 0.84/1.05 true = true % 0.84/1.05 |- ifeq (icext uri_rdfs_Seq $_124) true (icext uri_rdfs_Seq $_124) true = % 0.84/1.05 true % 0.84/1.05 |- ifeq (iext uri_rdfs_subClassOf uri_ex_Person $_123) true % 0.84/1.05 (icext $_123 uri_ex_alice) true = true % 0.84/1.05 |- ifeq (iext uri_rdfs_subClassOf uri_ex_Person $_123) true % 0.84/1.05 (icext $_123 uri_ex_bob) true = true % 0.84/1.05 |- ifeq (iext uri_rdfs_subClassOf uri_owl_Restriction $_123) true % 0.84/1.05 (icext $_123 % 0.84/1.05 sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z) % 0.84/1.05 true = true % 0.84/1.05 |- ifeq (iext uri_rdfs_subClassOf uri_owl_TransitiveProperty $_123) true % 0.84/1.05 (icext $_123 uri_ex_hasAncestor) true = true % 0.84/1.05 |- ifeq (iext uri_rdfs_subClassOf uri_rdf_List $_123) true % 0.84/1.05 (icext $_123 uri_rdf_nil) true = true % 0.84/1.05 |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $_123) true % 0.84/1.05 (icext $_123 uri_ex_hasAncestor) true = true % 0.84/1.05 |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $_123) true % 0.84/1.05 (icext $_123 uri_owl_minCardinality) true = true % 0.84/1.05 |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $_123) true % 0.84/1.05 (icext $_123 uri_owl_onProperty) true = true % 0.84/1.05 |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $_123) true % 0.84/1.05 (icext $_123 uri_rdf__1) true = true % 0.84/1.05 |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $_123) true % 0.84/1.05 (icext $_123 uri_rdf__2) true = true % 0.84/1.05 |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $_123) true % 0.84/1.05 (icext $_123 uri_rdf__3) true = true % 0.84/1.05 |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $_123) true % 0.84/1.05 (icext $_123 uri_rdf_first) true = true % 0.84/1.05 |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $_123) true % 0.84/1.05 (icext $_123 uri_rdf_object) true = true % 0.84/1.05 |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $_123) true % 0.84/1.05 (icext $_123 uri_rdf_rest) true = true % 0.84/1.05 |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $_123) true % 0.84/1.05 (icext $_123 uri_rdf_subject) true = true % 0.84/1.05 |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $_123) true % 0.84/1.05 (icext $_123 uri_rdf_type) true = true % 0.84/1.05 |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $_123) true % 0.84/1.05 (icext $_123 uri_rdf_value) true = true % 0.84/1.05 |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $_123) true % 0.84/1.05 (icext $_123 uri_rdfs_domain) true = true % 0.84/1.05 |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $_123) true % 0.84/1.05 (icext $_123 uri_rdfs_isDefinedBy) true = true % 0.84/1.05 |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $_123) true % 0.84/1.05 (icext $_123 uri_rdfs_member) true = true % 0.84/1.05 |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $_123) true % 0.84/1.05 (icext $_123 uri_rdfs_range) true = true % 0.84/1.05 |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $_123) true % 0.84/1.05 (icext $_123 uri_rdfs_seeAlso) true = true % 0.84/1.05 |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $_123) true % 0.84/1.05 (icext $_123 uri_rdfs_subClassOf) true = true % 0.84/1.05 |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $_123) true % 0.84/1.05 (icext $_123 uri_rdfs_subPropertyOf) true = true % 0.84/1.05 |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Class $_123) true % 0.84/1.05 (icext $_123 % 0.84/1.05 sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z) % 0.84/1.05 true = true % 0.84/1.05 |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Class $_123) true % 0.84/1.05 (icext $_123 uri_ex_Person) true = true % 0.84/1.05 |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Class $_123) true % 0.84/1.05 (icext $_123 uri_rdf_Alt) true = true % 0.84/1.05 |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Class $_123) true % 0.84/1.05 (icext $_123 uri_rdf_Bag) true = true % 0.84/1.05 |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Class $_123) true % 0.84/1.05 (icext $_123 uri_rdf_Property) true = true % 0.84/1.05 |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Class $_123) true % 0.84/1.05 (icext $_123 uri_rdf_XMLLiteral) true = true % 0.84/1.05 |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Class $_123) true % 0.84/1.05 (icext $_123 uri_rdfs_Class) true = true % 0.84/1.05 |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Class $_123) true % 0.84/1.05 (icext $_123 uri_rdfs_Container) true = true % 0.84/1.05 |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Class $_123) true % 0.84/1.05 (icext $_123 uri_rdfs_ContainerMembershipProperty) true = true % 0.84/1.05 |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Class $_123) true % 0.84/1.05 (icext $_123 uri_rdfs_Datatype) true = true % 0.84/1.05 |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Class $_123) true % 0.84/1.05 (icext $_123 uri_rdfs_Literal) true = true % 0.84/1.05 |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Class $_123) true % 0.84/1.05 (icext $_123 uri_rdfs_Resource) true = true % 0.84/1.05 |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Class $_123) true % 0.84/1.05 (icext $_123 uri_rdfs_Seq) true = true % 0.84/1.05 |- ifeq % 0.84/1.05 (iext uri_rdfs_subClassOf uri_rdfs_ContainerMembershipProperty $_123) % 0.84/1.05 true (icext $_123 uri_rdf__1) true = true % 0.84/1.05 |- ifeq % 0.84/1.05 (iext uri_rdfs_subClassOf uri_rdfs_ContainerMembershipProperty $_123) % 0.84/1.05 true (icext $_123 uri_rdf__2) true = true % 0.84/1.05 |- ifeq % 0.84/1.05 (iext uri_rdfs_subClassOf uri_rdfs_ContainerMembershipProperty $_123) % 0.84/1.05 true (icext $_123 uri_rdf__3) true = true % 0.84/1.05 |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Datatype $_123) true % 0.84/1.05 (icext $_123 uri_rdf_XMLLiteral) true = true % 0.84/1.05 |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Resource $_123) true % 0.84/1.05 (icext $_123 $_124) true = true % 0.84/1.05 |- icext % 0.84/1.05 sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z % 0.84/1.05 uri_ex_alice = true % 0.84/1.05 |- icext % 0.84/1.05 sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z % 0.84/1.05 uri_ex_bob = true % 0.84/1.05 |- ifeq % 0.84/1.05 (iext uri_rdfs_subClassOf % 0.84/1.05 sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z % 0.84/1.05 $D) true (icext $D uri_ex_alice) true = true % 0.84/1.05 |- iext uri_rdf_type uri_ex_alice % 0.84/1.05 sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z = % 0.84/1.05 true % 0.84/1.05 |- ifeq % 0.84/1.05 (iext uri_rdfs_subClassOf % 0.84/1.05 sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z % 0.84/1.05 $D) true (icext $D uri_ex_bob) true = true % 0.84/1.05 |- iext uri_rdf_type uri_ex_bob % 0.84/1.05 sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z = % 0.84/1.05 true % 0.84/1.05 |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Resource $_193) true % 0.84/1.05 (iext uri_rdfs_subClassOf % 0.84/1.05 sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z % 0.84/1.05 $_193) true = true % 0.84/1.05 |- ifeq % 0.84/1.05 (iext uri_rdfs_subClassOf % 0.84/1.05 sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z % 0.84/1.05 $_193) true (iext uri_rdfs_subClassOf uri_ex_Person $_193) true = % 0.84/1.05 true % 0.84/1.05 |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Resource $_193) true % 0.84/1.05 (iext uri_rdfs_subClassOf uri_ex_Person $_193) true = true % 0.84/1.05 |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Container $_193) true % 0.84/1.05 (iext uri_rdfs_subClassOf uri_rdf_Alt $_193) true = true % 0.84/1.05 |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Resource $_193) true % 0.84/1.05 (iext uri_rdfs_subClassOf uri_rdf_Alt $_193) true = true % 0.84/1.05 |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Container $_193) true % 0.84/1.05 (iext uri_rdfs_subClassOf uri_rdf_Bag $_193) true = true % 0.84/1.05 |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Resource $_193) true % 0.84/1.05 (iext uri_rdfs_subClassOf uri_rdf_Bag $_193) true = true % 0.84/1.05 |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Resource $_193) true % 0.84/1.05 (iext uri_rdfs_subClassOf uri_rdf_Property $_193) true = true % 0.84/1.05 |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Literal $_193) true % 0.84/1.05 (iext uri_rdfs_subClassOf uri_rdf_XMLLiteral $_193) true = true % 0.84/1.05 |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Resource $_193) true % 0.84/1.05 (iext uri_rdfs_subClassOf uri_rdf_XMLLiteral $_193) true = true % 0.84/1.05 |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Resource $_193) true % 0.84/1.05 (iext uri_rdfs_subClassOf uri_rdfs_Class $_193) true = true % 0.84/1.05 |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Resource $_193) true % 0.84/1.05 (iext uri_rdfs_subClassOf uri_rdfs_Container $_193) true = true % 0.84/1.05 |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $_193) true % 0.84/1.05 (iext uri_rdfs_subClassOf uri_rdfs_ContainerMembershipProperty $_193) % 0.84/1.05 true = true % 0.84/1.05 |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Resource $_193) true % 0.84/1.05 (iext uri_rdfs_subClassOf uri_rdfs_ContainerMembershipProperty $_193) % 0.84/1.05 true = true % 0.84/1.05 |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Class $_193) true % 0.84/1.05 (iext uri_rdfs_subClassOf uri_rdfs_Datatype $_193) true = true % 0.84/1.05 |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Resource $_193) true % 0.84/1.05 (iext uri_rdfs_subClassOf uri_rdfs_Datatype $_193) true = true % 0.84/1.05 |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Resource $_193) true % 0.84/1.05 (iext uri_rdfs_subClassOf uri_rdfs_Literal $_193) true = true % 0.84/1.05 |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Container $_193) true % 0.84/1.05 (iext uri_rdfs_subClassOf uri_rdfs_Seq $_193) true = true % 0.84/1.05 |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Resource $_193) true % 0.84/1.05 (iext uri_rdfs_subClassOf uri_rdfs_Seq $_193) true = true % 0.84/1.05 |- ifeq % 0.84/1.05 (iext uri_rdfs_subClassOf $_191 % 0.84/1.05 sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z) % 0.84/1.05 true (iext uri_rdfs_subClassOf $_191 uri_rdfs_Resource) true = true % 0.84/1.05 |- ifeq (iext uri_rdfs_subClassOf $_191 uri_ex_Person) true % 0.84/1.05 (iext uri_rdfs_subClassOf $_191 % 0.84/1.05 sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z) % 0.84/1.05 true = true % 0.84/1.05 |- ifeq (iext uri_rdfs_subClassOf $_191 uri_ex_Person) true % 0.84/1.05 (iext uri_rdfs_subClassOf $_191 uri_rdfs_Resource) true = true % 0.84/1.05 |- ifeq (iext uri_rdfs_subClassOf $_191 uri_rdf_Alt) true % 0.84/1.05 (iext uri_rdfs_subClassOf $_191 uri_rdfs_Container) true = true % 0.84/1.05 |- ifeq (iext uri_rdfs_subClassOf $_191 uri_rdf_Alt) true % 0.84/1.05 (iext uri_rdfs_subClassOf $_191 uri_rdfs_Resource) true = true % 0.84/1.05 |- ifeq (iext uri_rdfs_subClassOf $_191 uri_rdf_Bag) true % 0.84/1.05 (iext uri_rdfs_subClassOf $_191 uri_rdfs_Container) true = true % 0.84/1.05 |- ifeq (iext uri_rdfs_subClassOf $_191 uri_rdf_Bag) true % 0.84/1.05 (iext uri_rdfs_subClassOf $_191 uri_rdfs_Resource) true = true % 0.84/1.05 |- ifeq (iext uri_rdfs_subClassOf $_191 uri_rdf_Property) true % 0.84/1.05 (iext uri_rdfs_subClassOf $_191 uri_rdfs_Resource) true = true % 0.84/1.05 |- ifeq (iext uri_rdfs_subClassOf $_191 uri_rdf_XMLLiteral) true % 0.84/1.05 (iext uri_rdfs_subClassOf $_191 uri_rdfs_Literal) true = true % 0.84/1.05 |- ifeq (iext uri_rdfs_subClassOf $_191 uri_rdf_XMLLiteral) true % 0.84/1.05 (iext uri_rdfs_subClassOf $_191 uri_rdfs_Resource) true = true % 0.84/1.05 |- ifeq (iext uri_rdfs_subClassOf $_191 uri_rdfs_Class) true % 0.84/1.05 (iext uri_rdfs_subClassOf $_191 uri_rdfs_Resource) true = true % 0.84/1.05 |- ifeq (iext uri_rdfs_subClassOf $_191 uri_rdfs_Container) true % 0.84/1.05 (iext uri_rdfs_subClassOf $_191 uri_rdfs_Resource) true = true % 0.84/1.05 |- ifeq % 0.84/1.05 (iext uri_rdfs_subClassOf $_191 uri_rdfs_ContainerMembershipProperty) % 0.84/1.05 true (iext uri_rdfs_subClassOf $_191 uri_rdf_Property) true = true % 0.84/1.05 |- ifeq % 0.84/1.05 (iext uri_rdfs_subClassOf $_191 uri_rdfs_ContainerMembershipProperty) % 0.84/1.05 true (iext uri_rdfs_subClassOf $_191 uri_rdfs_Resource) true = true % 0.84/1.05 |- ifeq (iext uri_rdfs_subClassOf $_191 uri_rdfs_Datatype) true % 0.84/1.05 (iext uri_rdfs_subClassOf $_191 uri_rdfs_Class) true = true % 0.84/1.05 |- ifeq (iext uri_rdfs_subClassOf $_191 uri_rdfs_Datatype) true % 0.84/1.05 (iext uri_rdfs_subClassOf $_191 uri_rdfs_Resource) true = true % 0.84/1.05 |- ifeq (iext uri_rdfs_subClassOf $_191 uri_rdfs_Literal) true % 0.84/1.05 (iext uri_rdfs_subClassOf $_191 uri_rdfs_Resource) true = true % 0.84/1.05 |- ifeq (iext uri_rdfs_subClassOf $_191 uri_rdfs_Seq) true % 0.84/1.05 (iext uri_rdfs_subClassOf $_191 uri_rdfs_Container) true = true % 0.84/1.05 |- ifeq (iext uri_rdfs_subClassOf $_191 uri_rdfs_Seq) true % 0.84/1.05 (iext uri_rdfs_subClassOf $_191 uri_rdfs_Resource) true = true % 0.84/1.05 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_member $_260) true % 0.84/1.05 (iext uri_rdfs_subPropertyOf uri_rdf__1 $_260) true = true % 0.84/1.05 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_member $_260) true % 0.84/1.05 (iext uri_rdfs_subPropertyOf uri_rdf__2 $_260) true = true % 0.84/1.05 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_member $_260) true % 0.84/1.05 (iext uri_rdfs_subPropertyOf uri_rdf__3 $_260) true = true % 0.84/1.05 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_seeAlso $_260) true % 0.84/1.05 (iext uri_rdfs_subPropertyOf uri_rdfs_isDefinedBy $_260) true = true % 0.84/1.05 |- ifeq (iext uri_rdfs_subPropertyOf $_258 uri_rdf__1) true % 0.84/1.05 (iext uri_rdfs_subPropertyOf $_258 uri_rdfs_member) true = true % 0.84/1.05 |- ifeq (iext uri_rdfs_subPropertyOf $_258 uri_rdf__2) true % 0.84/1.05 (iext uri_rdfs_subPropertyOf $_258 uri_rdfs_member) true = true % 0.84/1.05 |- ifeq (iext uri_rdfs_subPropertyOf $_258 uri_rdf__3) true % 0.84/1.05 (iext uri_rdfs_subPropertyOf $_258 uri_rdfs_member) true = true % 0.84/1.05 |- ifeq (iext uri_rdfs_subPropertyOf $_258 uri_rdfs_isDefinedBy) true % 0.84/1.05 (iext uri_rdfs_subPropertyOf $_258 uri_rdfs_seeAlso) true = true % 0.84/1.05 |- ifeq % 0.84/1.05 (iext uri_rdfs_domain $_308 % 0.84/1.05 sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z) % 0.84/1.05 true (ifeq (iext $_308 uri_ex_alice $_310) true true true) true = true % 0.84/1.05 |- ifeq % 0.84/1.05 (iext uri_rdfs_domain $_308 % 0.84/1.05 sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z) % 0.84/1.05 true (ifeq (iext $_308 uri_ex_bob $_310) true true true) true = true % 0.84/1.05 |- ifeq (iext uri_rdfs_domain $_308 uri_ex_Person) true % 0.84/1.05 (ifeq (iext $_308 uri_ex_alice $_310) true true true) true = true % 0.84/1.05 |- ifeq (iext uri_rdfs_domain $_308 uri_ex_Person) true % 0.84/1.05 (ifeq (iext $_308 uri_ex_bob $_310) true true true) true = true % 0.84/1.05 |- ifeq (iext uri_rdfs_domain $_308 uri_owl_Restriction) true % 0.84/1.05 (ifeq % 0.84/1.05 (iext $_308 % 0.84/1.05 sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z % 0.84/1.05 $_310) true true true) true = true % 0.84/1.05 |- ifeq (iext uri_rdfs_domain $_308 uri_owl_TransitiveProperty) true % 0.84/1.05 (ifeq (iext $_308 uri_ex_hasAncestor $_310) true true true) true = % 0.84/1.05 true % 0.84/1.05 |- ifeq (iext uri_rdfs_domain $_308 uri_rdf_List) true % 0.84/1.05 (ifeq (iext $_308 uri_rdf_nil $_310) true true true) true = true % 0.84/1.05 |- ifeq (iext uri_rdfs_domain $_308 uri_rdf_Property) true % 0.84/1.05 (ifeq (iext $_308 uri_ex_hasAncestor $_310) true true true) true = % 0.84/1.05 true % 0.84/1.05 |- ifeq (iext uri_rdfs_domain $_308 uri_rdf_Property) true % 0.84/1.05 (ifeq (iext $_308 uri_owl_minCardinality $_310) true true true) true = % 0.84/1.05 true % 0.84/1.05 |- ifeq (iext uri_rdfs_domain $_308 uri_rdf_Property) true % 0.84/1.05 (ifeq (iext $_308 uri_owl_onProperty $_310) true true true) true = % 0.84/1.05 true % 0.84/1.05 |- ifeq (iext uri_rdfs_domain $_308 uri_rdf_Property) true % 0.84/1.05 (ifeq (iext $_308 uri_rdf__1 $_310) true true true) true = true % 0.84/1.05 |- ifeq (iext uri_rdfs_domain $_308 uri_rdf_Property) true % 0.84/1.05 (ifeq (iext $_308 uri_rdf__2 $_310) true true true) true = true % 0.84/1.05 |- ifeq (iext uri_rdfs_domain $_308 uri_rdf_Property) true % 0.84/1.05 (ifeq (iext $_308 uri_rdf__3 $_310) true true true) true = true % 0.84/1.05 |- ifeq (iext uri_rdfs_domain $_308 uri_rdf_Property) true % 0.84/1.05 (ifeq (iext $_308 uri_rdf_first $_310) true true true) true = true % 0.84/1.05 |- ifeq (iext uri_rdfs_domain $_308 uri_rdf_Property) true % 0.84/1.05 (ifeq (iext $_308 uri_rdf_object $_310) true true true) true = true % 0.84/1.05 |- ifeq (iext uri_rdfs_domain $_308 uri_rdf_Property) true % 0.84/1.05 (ifeq (iext $_308 uri_rdf_rest $_310) true true true) true = true % 0.84/1.05 |- ifeq (iext uri_rdfs_domain $_308 uri_rdf_Property) true % 0.84/1.05 (ifeq (iext $_308 uri_rdf_subject $_310) true true true) true = true % 0.84/1.05 |- ifeq (iext uri_rdfs_domain $_308 uri_rdf_Property) true % 0.84/1.05 (ifeq (iext $_308 uri_rdf_type $_310) true true true) true = true % 0.84/1.05 |- ifeq (iext uri_rdfs_domain $_308 uri_rdf_Property) true % 0.84/1.05 (ifeq (iext $_308 uri_rdf_value $_310) true true true) true = true % 0.84/1.05 |- ifeq (iext uri_rdfs_domain $_308 uri_rdf_Property) true % 0.84/1.05 (ifeq (iext $_308 uri_rdfs_domain $_310) true true true) true = true % 0.84/1.05 |- ifeq (iext uri_rdfs_domain $_308 uri_rdf_Property) true % 0.84/1.05 (ifeq (iext $_308 uri_rdfs_isDefinedBy $_310) true true true) true = % 0.84/1.05 true % 0.84/1.05 |- ifeq (iext uri_rdfs_domain $_308 uri_rdf_Property) true % 0.84/1.05 (ifeq (iext $_308 uri_rdfs_member $_310) true true true) true = true % 0.84/1.05 |- ifeq (iext uri_rdfs_domain $_308 uri_rdf_Property) true % 0.84/1.05 (ifeq (iext $_308 uri_rdfs_range $_310) true true true) true = true % 0.84/1.05 |- ifeq (iext uri_rdfs_domain $_308 uri_rdf_Property) true % 0.84/1.05 (ifeq (iext $_308 uri_rdfs_seeAlso $_310) true true true) true = true % 0.84/1.05 |- ifeq (iext uri_rdfs_domain $_308 uri_rdf_Property) true % 0.84/1.05 (ifeq (iext $_308 uri_rdfs_subClassOf $_310) true true true) true = % 0.84/1.05 true % 0.84/1.05 |- ifeq (iext uri_rdfs_domain $_308 uri_rdf_Property) true % 0.84/1.05 (ifeq (iext $_308 uri_rdfs_subPropertyOf $_310) true true true) true = % 0.84/1.05 true % 0.84/1.05 |- ifeq (iext uri_rdfs_domain $_308 uri_rdfs_Class) true % 0.84/1.05 (ifeq % 0.84/1.05 (iext $_308 % 0.84/1.05 sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z % 0.84/1.05 $_310) true true true) true = true % 0.84/1.05 |- ifeq (iext uri_rdfs_domain $_308 uri_rdfs_Class) true % 0.84/1.05 (ifeq (iext $_308 uri_ex_Person $_310) true true true) true = true % 0.84/1.05 |- ifeq (iext uri_rdfs_domain $_308 uri_rdfs_Class) true % 0.84/1.05 (ifeq (iext $_308 uri_rdf_Alt $_310) true true true) true = true % 0.84/1.05 |- ifeq (iext uri_rdfs_domain $_308 uri_rdfs_Class) true % 0.84/1.05 (ifeq (iext $_308 uri_rdf_Bag $_310) true true true) true = true % 0.84/1.05 |- ifeq (iext uri_rdfs_domain $_308 uri_rdfs_Class) true % 0.84/1.05 (ifeq (iext $_308 uri_rdf_Property $_310) true true true) true = true % 0.84/1.05 |- ifeq (iext uri_rdfs_domain $_308 uri_rdfs_Class) true % 0.84/1.05 (ifeq (iext $_308 uri_rdf_XMLLiteral $_310) true true true) true = % 0.84/1.05 true % 0.84/1.05 |- ifeq (iext uri_rdfs_domain $_308 uri_rdfs_Class) true % 0.84/1.05 (ifeq (iext $_308 uri_rdfs_Class $_310) true true true) true = true % 0.84/1.05 |- ifeq (iext uri_rdfs_domain $_308 uri_rdfs_Class) true % 0.84/1.05 (ifeq (iext $_308 uri_rdfs_Container $_310) true true true) true = % 0.84/1.05 true % 0.84/1.05 |- ifeq (iext uri_rdfs_domain $_308 uri_rdfs_Class) true % 0.84/1.05 (ifeq (iext $_308 uri_rdfs_ContainerMembershipProperty $_310) true % 0.84/1.05 true true) true = true % 0.84/1.05 |- ifeq (iext uri_rdfs_domain $_308 uri_rdfs_Class) true % 0.84/1.05 (ifeq (iext $_308 uri_rdfs_Datatype $_310) true true true) true = true % 0.84/1.05 |- ifeq (iext uri_rdfs_domain $_308 uri_rdfs_Class) true % 0.84/1.05 (ifeq (iext $_308 uri_rdfs_Literal $_310) true true true) true = true % 0.84/1.05 |- ifeq (iext uri_rdfs_domain $_308 uri_rdfs_Class) true % 0.84/1.05 (ifeq (iext $_308 uri_rdfs_Resource $_310) true true true) true = true % 0.84/1.05 |- ifeq (iext uri_rdfs_domain $_308 uri_rdfs_Class) true % 0.84/1.05 (ifeq (iext $_308 uri_rdfs_Seq $_310) true true true) true = true % 0.84/1.05 |- ifeq (iext uri_rdfs_domain $_308 uri_rdfs_ContainerMembershipProperty) % 0.84/1.05 true (ifeq (iext $_308 uri_rdf__1 $_310) true true true) true = true % 0.84/1.05 |- ifeq (iext uri_rdfs_domain $_308 uri_rdfs_ContainerMembershipProperty) % 0.84/1.05 true (ifeq (iext $_308 uri_rdf__2 $_310) true true true) true = true % 0.84/1.05 |- ifeq (iext uri_rdfs_domain $_308 uri_rdfs_ContainerMembershipProperty) % 0.84/1.05 true (ifeq (iext $_308 uri_rdf__3 $_310) true true true) true = true % 0.84/1.05 |- ifeq (iext uri_rdfs_domain $_308 uri_rdfs_Datatype) true % 0.84/1.05 (ifeq (iext $_308 uri_rdf_XMLLiteral $_310) true true true) true = % 0.84/1.05 true % 0.84/1.05 |- ifeq (iext uri_rdfs_domain $_308 uri_rdfs_Resource) true % 0.84/1.05 (ifeq (iext $_308 $_309 $_310) true true true) true = true % 0.84/1.05 |- ifeq (iext uri_rdfs_domain uri_ex_hasAncestor $_307) true % 0.84/1.05 (icext $_307 uri_ex_alice) true = true % 0.84/1.05 |- ifeq (iext uri_rdfs_domain uri_owl_minCardinality $_307) true % 0.84/1.05 (icext $_307 % 0.84/1.05 sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z) % 0.84/1.05 true = true % 0.84/1.05 |- ifeq (iext uri_rdfs_domain uri_owl_onProperty $_307) true % 0.84/1.05 (icext $_307 % 0.84/1.05 sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z) % 0.84/1.05 true = true % 0.84/1.05 |- ifeq (iext uri_rdfs_domain uri_rdf_type $_307) true (icext $_307 $_309) % 0.84/1.05 true = true % 0.84/1.05 |- ifeq (iext uri_rdfs_domain uri_rdfs_domain $_307) true % 0.84/1.05 (icext $_307 uri_rdf__1) true = true % 0.84/1.05 |- ifeq (iext uri_rdfs_domain uri_rdfs_domain $_307) true % 0.84/1.05 (icext $_307 uri_rdf__2) true = true % 0.84/1.05 |- ifeq (iext uri_rdfs_domain uri_rdfs_domain $_307) true % 0.84/1.05 (icext $_307 uri_rdf__3) true = true % 0.84/1.05 |- ifeq (iext uri_rdfs_domain uri_rdfs_domain $_307) true % 0.84/1.05 (icext $_307 uri_rdf_first) true = true % 0.84/1.05 |- ifeq (iext uri_rdfs_domain uri_rdfs_domain $_307) true % 0.84/1.05 (icext $_307 uri_rdf_object) true = true % 0.84/1.05 |- ifeq (iext uri_rdfs_domain uri_rdfs_domain $_307) true % 0.84/1.05 (icext $_307 uri_rdf_predicate) true = true % 0.84/1.05 |- ifeq (iext uri_rdfs_domain uri_rdfs_domain $_307) true % 0.84/1.05 (icext $_307 uri_rdf_rest) true = true % 0.84/1.05 |- ifeq (iext uri_rdfs_domain uri_rdfs_domain $_307) true % 0.84/1.05 (icext $_307 uri_rdf_subject) true = true % 0.84/1.05 |- ifeq (iext uri_rdfs_domain uri_rdfs_domain $_307) true % 0.84/1.05 (icext $_307 uri_rdf_type) true = true % 0.84/1.05 |- ifeq (iext uri_rdfs_domain uri_rdfs_domain $_307) true % 0.84/1.05 (icext $_307 uri_rdf_value) true = true % 0.84/1.05 |- ifeq (iext uri_rdfs_domain uri_rdfs_domain $_307) true % 0.84/1.05 (icext $_307 uri_rdfs_comment) true = true % 0.84/1.05 |- ifeq (iext uri_rdfs_domain uri_rdfs_domain $_307) true % 0.84/1.05 (icext $_307 uri_rdfs_domain) true = true % 0.84/1.05 |- ifeq (iext uri_rdfs_domain uri_rdfs_domain $_307) true % 0.84/1.05 (icext $_307 uri_rdfs_isDefinedBy) true = true % 0.84/1.05 |- ifeq (iext uri_rdfs_domain uri_rdfs_domain $_307) true % 0.84/1.05 (icext $_307 uri_rdfs_label) true = true % 0.84/1.05 |- ifeq (iext uri_rdfs_domain uri_rdfs_domain $_307) true % 0.84/1.05 (icext $_307 uri_rdfs_member) true = true % 0.84/1.05 |- ifeq (iext uri_rdfs_domain uri_rdfs_domain $_307) true % 0.84/1.05 (icext $_307 uri_rdfs_range) true = true % 0.84/1.05 |- ifeq (iext uri_rdfs_domain uri_rdfs_domain $_307) true % 0.84/1.05 (icext $_307 uri_rdfs_seeAlso) true = true % 0.84/1.05 |- ifeq (iext uri_rdfs_domain uri_rdfs_domain $_307) true % 0.84/1.05 (icext $_307 uri_rdfs_subClassOf) true = true % 0.84/1.05 |- ifeq (iext uri_rdfs_domain uri_rdfs_domain $_307) true % 0.84/1.05 (icext $_307 uri_rdfs_subPropertyOf) true = true % 0.84/1.05 |- ifeq (iext uri_rdfs_domain uri_rdfs_range $_307) true % 0.84/1.05 (icext $_307 uri_rdf__1) true = true % 0.84/1.05 |- ifeq (iext uri_rdfs_domain uri_rdfs_range $_307) true % 0.84/1.05 (icext $_307 uri_rdf__2) true = true % 0.84/1.05 |- ifeq (iext uri_rdfs_domain uri_rdfs_range $_307) true % 0.84/1.05 (icext $_307 uri_rdf__3) true = true % 0.84/1.05 |- ifeq (iext uri_rdfs_domain uri_rdfs_range $_307) true % 0.84/1.05 (icext $_307 uri_rdf_first) true = true % 0.84/1.05 |- ifeq (iext uri_rdfs_domain uri_rdfs_range $_307) true % 0.84/1.05 (icext $_307 uri_rdf_predicate) true = true % 0.84/1.06 |- ifeq (iext uri_rdfs_domain uri_rdfs_range $_307) true % 0.84/1.06 (icext $_307 uri_rdf_rest) true = true % 0.84/1.06 |- ifeq (iext uri_rdfs_domain uri_rdfs_range $_307) true % 0.84/1.06 (icext $_307 uri_rdf_subject) true = true % 0.84/1.06 |- ifeq (iext uri_rdfs_domain uri_rdfs_range $_307) true % 0.84/1.06 (icext $_307 uri_rdf_type) true = true % 0.84/1.06 |- ifeq (iext uri_rdfs_domain uri_rdfs_range $_307) true % 0.84/1.06 (icext $_307 uri_rdf_value) true = true % 0.84/1.06 |- ifeq (iext uri_rdfs_domain uri_rdfs_range $_307) true % 0.84/1.06 (icext $_307 uri_rdfs_comment) true = true % 0.84/1.06 |- ifeq (iext uri_rdfs_domain uri_rdfs_range $_307) true % 0.84/1.06 (icext $_307 uri_rdfs_domain) true = true % 0.84/1.06 |- ifeq (iext uri_rdfs_domain uri_rdfs_range $_307) true % 0.84/1.06 (icext $_307 uri_rdfs_isDefinedBy) true = true % 0.84/1.06 |- ifeq (iext uri_rdfs_domain uri_rdfs_range $_307) true % 0.84/1.06 (icext $_307 uri_rdfs_label) true = true % 0.84/1.06 |- ifeq (iext uri_rdfs_domain uri_rdfs_range $_307) true % 0.84/1.06 (icext $_307 uri_rdfs_member) true = true % 0.84/1.06 |- ifeq (iext uri_rdfs_domain uri_rdfs_range $_307) true % 0.84/1.06 (icext $_307 uri_rdfs_range) true = true % 0.84/1.06 |- ifeq (iext uri_rdfs_domain uri_rdfs_range $_307) true % 0.84/1.06 (icext $_307 uri_rdfs_seeAlso) true = true % 0.84/1.06 |- ifeq (iext uri_rdfs_domain uri_rdfs_range $_307) true % 0.84/1.06 (icext $_307 uri_rdfs_subClassOf) true = true % 0.84/1.06 |- ifeq (iext uri_rdfs_domain uri_rdfs_range $_307) true % 0.84/1.06 (icext $_307 uri_rdfs_subPropertyOf) true = true % 0.84/1.06 |- ifeq (iext uri_rdfs_domain uri_rdfs_subClassOf $_307) true % 0.84/1.06 (icext $_307 % 0.84/1.06 sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z) % 0.84/1.06 true = true % 0.84/1.06 |- ifeq (iext uri_rdfs_domain uri_rdfs_subClassOf $_307) true % 0.84/1.06 (icext $_307 uri_ex_Person) true = true % 0.84/1.06 |- ifeq (iext uri_rdfs_domain uri_rdfs_subClassOf $_307) true % 0.84/1.06 (icext $_307 uri_rdf_Alt) true = true % 0.84/1.06 |- ifeq (iext uri_rdfs_domain uri_rdfs_subClassOf $_307) true % 0.84/1.06 (icext $_307 uri_rdf_Bag) true = true % 0.84/1.06 |- ifeq (iext uri_rdfs_domain uri_rdfs_subClassOf $_307) true % 0.84/1.06 (icext $_307 uri_rdf_Property) true = true % 0.84/1.06 |- ifeq (iext uri_rdfs_domain uri_rdfs_subClassOf $_307) true % 0.84/1.06 (icext $_307 uri_rdf_XMLLiteral) true = true % 0.84/1.06 |- ifeq (iext uri_rdfs_domain uri_rdfs_subClassOf $_307) true % 0.84/1.06 (icext $_307 uri_rdfs_Class) true = true % 0.84/1.06 |- ifeq (iext uri_rdfs_domain uri_rdfs_subClassOf $_307) true % 0.84/1.06 (icext $_307 uri_rdfs_Container) true = true % 0.84/1.06 |- ifeq (iext uri_rdfs_domain uri_rdfs_subClassOf $_307) true % 0.84/1.06 (icext $_307 uri_rdfs_ContainerMembershipProperty) true = true % 0.84/1.06 |- ifeq (iext uri_rdfs_domain uri_rdfs_subClassOf $_307) true % 0.84/1.06 (icext $_307 uri_rdfs_Datatype) true = true % 0.84/1.06 |- ifeq (iext uri_rdfs_domain uri_rdfs_subClassOf $_307) true % 0.84/1.06 (icext $_307 uri_rdfs_Literal) true = true % 0.84/1.06 |- ifeq (iext uri_rdfs_domain uri_rdfs_subClassOf $_307) true % 0.84/1.06 (icext $_307 uri_rdfs_Resource) true = true % 0.84/1.06 |- ifeq (iext uri_rdfs_domain uri_rdfs_subClassOf $_307) true % 0.84/1.06 (icext $_307 uri_rdfs_Seq) true = true % 0.84/1.06 |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $_307) true % 0.84/1.06 (icext $_307 uri_ex_hasAncestor) true = true % 0.84/1.06 |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $_307) true % 0.84/1.06 (icext $_307 uri_owl_minCardinality) true = true % 0.84/1.06 |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $_307) true % 0.84/1.06 (icext $_307 uri_owl_onProperty) true = true % 0.84/1.06 |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $_307) true % 0.84/1.06 (icext $_307 uri_rdf__1) true = true % 0.84/1.06 |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $_307) true % 0.84/1.06 (icext $_307 uri_rdf__2) true = true % 0.84/1.06 |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $_307) true % 0.84/1.06 (icext $_307 uri_rdf__3) true = true % 0.84/1.06 |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $_307) true % 0.84/1.06 (icext $_307 uri_rdf_first) true = true % 0.84/1.06 |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $_307) true % 0.84/1.06 (icext $_307 uri_rdf_object) true = true % 0.84/1.06 |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $_307) true % 0.84/1.06 (icext $_307 uri_rdf_rest) true = true % 0.84/1.06 |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $_307) true % 0.84/1.06 (icext $_307 uri_rdf_subject) true = true % 0.84/1.06 |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $_307) true % 0.84/1.06 (icext $_307 uri_rdf_type) true = true % 0.84/1.06 |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $_307) true % 0.84/1.06 (icext $_307 uri_rdf_value) true = true % 0.84/1.06 |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $_307) true % 0.84/1.06 (icext $_307 uri_rdfs_domain) true = true % 0.84/1.06 |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $_307) true % 0.84/1.06 (icext $_307 uri_rdfs_isDefinedBy) true = true % 0.84/1.06 |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $_307) true % 0.84/1.06 (icext $_307 uri_rdfs_member) true = true % 0.84/1.06 |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $_307) true % 0.84/1.06 (icext $_307 uri_rdfs_range) true = true % 0.84/1.06 |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $_307) true % 0.84/1.06 (icext $_307 uri_rdfs_seeAlso) true = true % 0.84/1.06 |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $_307) true % 0.84/1.06 (icext $_307 uri_rdfs_subClassOf) true = true % 0.84/1.06 |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $_307) true % 0.84/1.06 (icext $_307 uri_rdfs_subPropertyOf) true = true % 0.84/1.06 |- ifeq (iext uri_rdf_first $_309 $_310) true (icext uri_rdf_List $_309) % 0.84/1.06 true = true % 0.84/1.06 |- ifeq (iext uri_rdf_object $_309 $_310) true % 0.84/1.06 (icext uri_rdfs_Statement $_309) true = true % 0.84/1.06 |- ifeq (iext uri_rdf_predicate $_309 $_310) true % 0.84/1.06 (icext uri_rdfs_Statement $_309) true = true % 0.84/1.06 |- ifeq (iext uri_rdf_rest $_309 $_310) true (icext uri_rdf_List $_309) % 0.84/1.06 true = true % 0.84/1.06 |- ifeq (iext uri_rdf_subject $_309 $_310) true % 0.84/1.06 (icext uri_rdfs_Statement $_309) true = true % 0.84/1.06 |- ifeq (iext uri_rdfs_comment $_309 $_310) true true true = true % 0.84/1.06 |- ifeq (iext uri_rdfs_domain $_309 $_310) true % 0.84/1.06 (icext uri_rdf_Property $_309) true = true % 0.84/1.06 |- ifeq (iext uri_rdfs_label $_309 $_310) true true true = true % 0.84/1.06 |- ifeq (iext uri_rdfs_range $_309 $_310) true % 0.84/1.06 (icext uri_rdf_Property $_309) true = true % 0.84/1.06 |- ifeq (iext uri_rdfs_subClassOf $_309 $_310) true % 0.84/1.06 (icext uri_rdfs_Class $_309) true = true % 0.84/1.06 |- ifeq (iext uri_rdfs_subPropertyOf $_309 $_310) true % 0.84/1.06 (icext uri_rdf_Property $_309) true = true % 0.84/1.06 |- icext uri_rdf_Property uri_rdf_predicate = true % 0.84/1.06 |- ifeq (iext uri_rdfs_domain $P uri_rdf_Property) true % 0.84/1.06 (ifeq (iext $P uri_rdf_predicate $Y) true true true) true = true % 0.84/1.06 |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $D) true % 0.84/1.06 (icext $D uri_rdf_predicate) true = true % 0.84/1.06 |- iext uri_rdf_type uri_rdf_predicate uri_rdf_Property = true % 0.84/1.06 |- ip uri_rdf_predicate = true % 0.84/1.06 |- ifeq (iext uri_rdf_predicate $S $O) true true true = true % 0.84/1.06 |- iext uri_rdfs_subPropertyOf uri_rdf_predicate uri_rdf_predicate = true % 0.84/1.06 |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $C) true % 0.84/1.06 (icext $C uri_rdf_predicate) true = true % 0.84/1.06 |- icext uri_rdf_Property uri_rdfs_comment = true % 0.84/1.06 |- ifeq (iext uri_rdfs_domain $P uri_rdf_Property) true % 0.84/1.06 (ifeq (iext $P uri_rdfs_comment $Y) true true true) true = true % 0.84/1.06 |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $D) true % 0.84/1.06 (icext $D uri_rdfs_comment) true = true % 0.84/1.06 |- iext uri_rdf_type uri_rdfs_comment uri_rdf_Property = true % 0.84/1.06 |- ip uri_rdfs_comment = true % 0.84/1.06 |- iext uri_rdfs_subPropertyOf uri_rdfs_comment uri_rdfs_comment = true % 0.84/1.06 |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $C) true % 0.84/1.06 (icext $C uri_rdfs_comment) true = true % 0.84/1.06 |- icext uri_rdf_Property uri_rdfs_label = true % 0.84/1.06 |- ifeq (iext uri_rdfs_domain $P uri_rdf_Property) true % 0.84/1.06 (ifeq (iext $P uri_rdfs_label $Y) true true true) true = true % 0.84/1.07 |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $D) true % 0.84/1.07 (icext $D uri_rdfs_label) true = true % 0.84/1.07 |- iext uri_rdf_type uri_rdfs_label uri_rdf_Property = true % 0.84/1.07 |- ip uri_rdfs_label = true % 0.84/1.07 |- iext uri_rdfs_subPropertyOf uri_rdfs_label uri_rdfs_label = true % 0.84/1.07 |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $C) true % 0.84/1.07 (icext $C uri_rdfs_label) true = true % 0.84/1.07 |- ifeq % 0.84/1.07 (iext uri_rdfs_range $_422 % 0.84/1.07 sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z) % 0.84/1.07 true (ifeq (iext $_422 $_423 uri_ex_alice) true true true) true = true % 0.84/1.07 |- ifeq % 0.84/1.07 (iext uri_rdfs_range $_422 % 0.84/1.07 sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z) % 0.84/1.07 true (ifeq (iext $_422 $_423 uri_ex_bob) true true true) true = true % 0.84/1.07 |- ifeq (iext uri_rdfs_range $_422 uri_ex_Person) true % 0.84/1.07 (ifeq (iext $_422 $_423 uri_ex_alice) true true true) true = true % 0.84/1.07 |- ifeq (iext uri_rdfs_range $_422 uri_ex_Person) true % 0.84/1.07 (ifeq (iext $_422 $_423 uri_ex_bob) true true true) true = true % 0.84/1.07 |- ifeq (iext uri_rdfs_range $_422 uri_owl_Restriction) true % 0.84/1.07 (ifeq % 0.84/1.07 (iext $_422 $_423 % 0.84/1.07 sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z) % 0.84/1.07 true true true) true = true % 0.84/1.07 |- ifeq (iext uri_rdfs_range $_422 uri_owl_TransitiveProperty) true % 0.84/1.07 (ifeq (iext $_422 $_423 uri_ex_hasAncestor) true true true) true = % 0.84/1.07 true % 0.84/1.07 |- ifeq (iext uri_rdfs_range $_422 uri_rdf_List) true % 0.84/1.07 (ifeq (iext $_422 $_423 uri_rdf_nil) true true true) true = true % 0.84/1.07 |- ifeq (iext uri_rdfs_range $_422 uri_rdf_Property) true % 0.84/1.07 (ifeq (iext $_422 $_423 uri_ex_hasAncestor) true true true) true = % 0.84/1.07 true % 0.84/1.07 |- ifeq (iext uri_rdfs_range $_422 uri_rdf_Property) true % 0.84/1.07 (ifeq (iext $_422 $_423 uri_owl_minCardinality) true true true) true = % 0.84/1.07 true % 0.84/1.07 |- ifeq (iext uri_rdfs_range $_422 uri_rdf_Property) true % 0.84/1.07 (ifeq (iext $_422 $_423 uri_owl_onProperty) true true true) true = % 0.84/1.07 true % 0.84/1.07 |- ifeq (iext uri_rdfs_range $_422 uri_rdf_Property) true % 0.84/1.07 (ifeq (iext $_422 $_423 uri_rdf__1) true true true) true = true % 0.84/1.07 |- ifeq (iext uri_rdfs_range $_422 uri_rdf_Property) true % 0.84/1.07 (ifeq (iext $_422 $_423 uri_rdf__2) true true true) true = true % 0.84/1.07 |- ifeq (iext uri_rdfs_range $_422 uri_rdf_Property) true % 0.84/1.07 (ifeq (iext $_422 $_423 uri_rdf__3) true true true) true = true % 0.84/1.07 |- ifeq (iext uri_rdfs_range $_422 uri_rdf_Property) true % 0.84/1.07 (ifeq (iext $_422 $_423 uri_rdf_first) true true true) true = true % 0.84/1.07 |- ifeq (iext uri_rdfs_range $_422 uri_rdf_Property) true % 0.84/1.07 (ifeq (iext $_422 $_423 uri_rdf_object) true true true) true = true % 0.84/1.07 |- ifeq (iext uri_rdfs_range $_422 uri_rdf_Property) true % 0.84/1.07 (ifeq (iext $_422 $_423 uri_rdf_predicate) true true true) true = true % 0.84/1.07 |- ifeq (iext uri_rdfs_range $_422 uri_rdf_Property) true % 0.84/1.07 (ifeq (iext $_422 $_423 uri_rdf_rest) true true true) true = true % 0.84/1.07 |- ifeq (iext uri_rdfs_range $_422 uri_rdf_Property) true % 0.84/1.07 (ifeq (iext $_422 $_423 uri_rdf_subject) true true true) true = true % 0.84/1.07 |- ifeq (iext uri_rdfs_range $_422 uri_rdf_Property) true % 0.84/1.07 (ifeq (iext $_422 $_423 uri_rdf_type) true true true) true = true % 0.84/1.07 |- ifeq (iext uri_rdfs_range $_422 uri_rdf_Property) true % 0.84/1.07 (ifeq (iext $_422 $_423 uri_rdf_value) true true true) true = true % 0.84/1.07 |- ifeq (iext uri_rdfs_range $_422 uri_rdf_Property) true % 0.84/1.07 (ifeq (iext $_422 $_423 uri_rdfs_comment) true true true) true = true % 0.84/1.07 |- ifeq (iext uri_rdfs_range $_422 uri_rdf_Property) true % 0.84/1.07 (ifeq (iext $_422 $_423 uri_rdfs_domain) true true true) true = true % 0.84/1.07 |- ifeq (iext uri_rdfs_range $_422 uri_rdf_Property) true % 0.84/1.07 (ifeq (iext $_422 $_423 uri_rdfs_isDefinedBy) true true true) true = % 0.84/1.07 true % 0.84/1.07 |- ifeq (iext uri_rdfs_range $_422 uri_rdf_Property) true % 0.84/1.07 (ifeq (iext $_422 $_423 uri_rdfs_label) true true true) true = true % 0.84/1.07 |- ifeq (iext uri_rdfs_range $_422 uri_rdf_Property) true % 0.84/1.07 (ifeq (iext $_422 $_423 uri_rdfs_member) true true true) true = true % 0.84/1.07 |- ifeq (iext uri_rdfs_range $_422 uri_rdf_Property) true % 0.84/1.07 (ifeq (iext $_422 $_423 uri_rdfs_range) true true true) true = true % 0.84/1.07 |- ifeq (iext uri_rdfs_range $_422 uri_rdf_Property) true % 0.84/1.07 (ifeq (iext $_422 $_423 uri_rdfs_seeAlso) true true true) true = true % 0.84/1.07 |- ifeq (iext uri_rdfs_range $_422 uri_rdf_Property) true % 0.84/1.07 (ifeq (iext $_422 $_423 uri_rdfs_subClassOf) true true true) true = % 0.84/1.07 true % 0.84/1.07 |- ifeq (iext uri_rdfs_range $_422 uri_rdf_Property) true % 0.84/1.07 (ifeq (iext $_422 $_423 uri_rdfs_subPropertyOf) true true true) true = % 0.84/1.07 true % 0.84/1.07 |- ifeq (iext uri_rdfs_range $_422 uri_rdfs_Class) true % 0.84/1.07 (ifeq % 0.84/1.07 (iext $_422 $_423 % 0.84/1.07 sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z) % 0.84/1.07 true true true) true = true % 0.84/1.07 |- ifeq (iext uri_rdfs_range $_422 uri_rdfs_Class) true % 0.84/1.07 (ifeq (iext $_422 $_423 uri_ex_Person) true true true) true = true % 0.84/1.07 |- ifeq (iext uri_rdfs_range $_422 uri_rdfs_Class) true % 0.84/1.07 (ifeq (iext $_422 $_423 uri_rdf_Alt) true true true) true = true % 0.84/1.07 |- ifeq (iext uri_rdfs_range $_422 uri_rdfs_Class) true % 0.84/1.07 (ifeq (iext $_422 $_423 uri_rdf_Bag) true true true) true = true % 0.84/1.07 |- ifeq (iext uri_rdfs_range $_422 uri_rdfs_Class) true % 0.84/1.07 (ifeq (iext $_422 $_423 uri_rdf_Property) true true true) true = true % 0.84/1.07 |- ifeq (iext uri_rdfs_range $_422 uri_rdfs_Class) true % 0.84/1.07 (ifeq (iext $_422 $_423 uri_rdf_XMLLiteral) true true true) true = % 0.84/1.07 true % 0.84/1.07 |- ifeq (iext uri_rdfs_range $_422 uri_rdfs_Class) true % 0.84/1.07 (ifeq (iext $_422 $_423 uri_rdfs_Class) true true true) true = true % 0.84/1.07 |- ifeq (iext uri_rdfs_range $_422 uri_rdfs_Class) true % 0.84/1.07 (ifeq (iext $_422 $_423 uri_rdfs_Container) true true true) true = % 0.84/1.07 true % 0.84/1.07 |- ifeq (iext uri_rdfs_range $_422 uri_rdfs_Class) true % 0.84/1.07 (ifeq (iext $_422 $_423 uri_rdfs_ContainerMembershipProperty) true % 0.84/1.07 true true) true = true % 0.84/1.07 |- ifeq (iext uri_rdfs_range $_422 uri_rdfs_Class) true % 0.84/1.07 (ifeq (iext $_422 $_423 uri_rdfs_Datatype) true true true) true = true % 0.84/1.07 |- ifeq (iext uri_rdfs_range $_422 uri_rdfs_Class) true % 0.84/1.07 (ifeq (iext $_422 $_423 uri_rdfs_Literal) true true true) true = true % 0.84/1.07 |- ifeq (iext uri_rdfs_range $_422 uri_rdfs_Class) true % 0.84/1.07 (ifeq (iext $_422 $_423 uri_rdfs_Resource) true true true) true = true % 0.84/1.07 |- ifeq (iext uri_rdfs_range $_422 uri_rdfs_Class) true % 0.84/1.07 (ifeq (iext $_422 $_423 uri_rdfs_Seq) true true true) true = true % 0.84/1.07 |- ifeq (iext uri_rdfs_range $_422 uri_rdfs_ContainerMembershipProperty) % 0.84/1.07 true (ifeq (iext $_422 $_423 uri_rdf__1) true true true) true = true % 0.84/1.07 |- ifeq (iext uri_rdfs_range $_422 uri_rdfs_ContainerMembershipProperty) % 0.84/1.07 true (ifeq (iext $_422 $_423 uri_rdf__2) true true true) true = true % 0.84/1.07 |- ifeq (iext uri_rdfs_range $_422 uri_rdfs_ContainerMembershipProperty) % 0.84/1.07 true (ifeq (iext $_422 $_423 uri_rdf__3) true true true) true = true % 0.84/1.07 |- ifeq (iext uri_rdfs_range $_422 uri_rdfs_Datatype) true % 0.84/1.07 (ifeq (iext $_422 $_423 uri_rdf_XMLLiteral) true true true) true = % 0.84/1.07 true % 0.84/1.07 |- ifeq (iext uri_rdfs_range $_422 uri_rdfs_Resource) true % 0.84/1.07 (ifeq (iext $_422 $_423 $_424) true true true) true = true % 0.84/1.07 |- ifeq (iext uri_rdfs_range uri_ex_hasAncestor $_421) true % 0.84/1.07 (icext $_421 uri_ex_bob) true = true % 0.84/1.07 |- ifeq (iext uri_rdfs_range uri_owl_minCardinality $_421) true % 0.84/1.07 (icext $_421 (literal_typed dat_str_1 uri_xsd_nonNegativeInteger)) % 0.84/1.07 true = true % 0.84/1.07 |- ifeq (iext uri_rdfs_range uri_owl_onProperty $_421) true % 0.84/1.07 (icext $_421 uri_ex_hasAncestor) true = true % 0.84/1.07 |- ifeq (iext uri_rdfs_range uri_rdf_type $_421) true % 0.84/1.07 (icext $_421 uri_owl_Restriction) true = true % 0.84/1.07 |- ifeq (iext uri_rdfs_range uri_rdf_type $_421) true % 0.84/1.07 (icext $_421 uri_rdfs_Class) true = true % 0.84/1.07 |- ifeq (iext uri_rdfs_range uri_rdf_type $_421) true % 0.84/1.07 (icext $_421 % 0.84/1.07 sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z) % 0.84/1.07 true = true % 0.84/1.07 |- ifeq (iext uri_rdfs_range uri_rdf_type $_421) true % 0.84/1.07 (icext $_421 uri_ex_Person) true = true % 0.84/1.07 |- ifeq (iext uri_rdfs_range uri_rdf_type $_421) true % 0.84/1.07 (icext $_421 uri_owl_TransitiveProperty) true = true % 0.84/1.07 |- ifeq (iext uri_rdfs_range uri_rdf_type $_421) true % 0.84/1.07 (icext $_421 uri_rdf_Property) true = true % 0.84/1.07 |- ifeq (iext uri_rdfs_range uri_rdf_type $_421) true % 0.84/1.07 (icext $_421 uri_rdfs_Datatype) true = true % 0.84/1.07 |- ifeq (iext uri_rdfs_range uri_rdf_type $_421) true % 0.84/1.07 (icext $_421 uri_rdfs_ContainerMembershipProperty) true = true % 0.84/1.07 |- ifeq (iext uri_rdfs_range uri_rdf_type $_421) true % 0.84/1.07 (icext $_421 uri_rdf_List) true = true % 0.84/1.07 |- ifeq (iext uri_rdfs_range uri_rdf_type $_421) true % 0.84/1.07 (icext $_421 uri_rdfs_Resource) true = true % 0.84/1.07 |- ifeq (iext uri_rdfs_range uri_rdfs_domain $_421) true % 0.84/1.07 (icext $_421 uri_rdfs_Resource) true = true % 0.84/1.07 |- ifeq (iext uri_rdfs_range uri_rdfs_domain $_421) true % 0.84/1.07 (icext $_421 uri_rdf_List) true = true % 0.84/1.07 |- ifeq (iext uri_rdfs_range uri_rdfs_domain $_421) true % 0.84/1.07 (icext $_421 uri_rdfs_Statement) true = true % 0.84/1.07 |- ifeq (iext uri_rdfs_range uri_rdfs_domain $_421) true % 0.84/1.07 (icext $_421 uri_rdf_Property) true = true % 0.84/1.07 |- ifeq (iext uri_rdfs_range uri_rdfs_domain $_421) true % 0.84/1.07 (icext $_421 uri_rdfs_Class) true = true % 0.84/1.07 |- ifeq (iext uri_rdfs_range uri_rdfs_range $_421) true % 0.84/1.07 (icext $_421 uri_rdfs_Resource) true = true % 0.84/1.07 |- ifeq (iext uri_rdfs_range uri_rdfs_range $_421) true % 0.84/1.07 (icext $_421 uri_rdf_List) true = true % 0.84/1.07 |- ifeq (iext uri_rdfs_range uri_rdfs_range $_421) true % 0.84/1.07 (icext $_421 uri_rdfs_Class) true = true % 0.84/1.07 |- ifeq (iext uri_rdfs_range uri_rdfs_range $_421) true % 0.84/1.07 (icext $_421 uri_rdfs_Literal) true = true % 0.84/1.07 |- ifeq (iext uri_rdfs_range uri_rdfs_range $_421) true % 0.84/1.07 (icext $_421 uri_rdf_Property) true = true % 0.84/1.07 |- ifeq (iext uri_rdfs_range uri_rdfs_subClassOf $_421) true % 0.84/1.07 (icext $_421 % 0.84/1.07 sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z) % 0.84/1.07 true = true % 0.84/1.07 |- ifeq (iext uri_rdfs_range uri_rdfs_subClassOf $_421) true % 0.84/1.07 (icext $_421 uri_rdfs_Resource) true = true % 0.84/1.07 |- ifeq (iext uri_rdfs_range uri_rdfs_subClassOf $_421) true % 0.84/1.07 (icext $_421 uri_ex_Person) true = true % 0.84/1.07 |- ifeq (iext uri_rdfs_range uri_rdfs_subClassOf $_421) true % 0.84/1.07 (icext $_421 uri_rdf_Alt) true = true % 0.84/1.07 |- ifeq (iext uri_rdfs_range uri_rdfs_subClassOf $_421) true % 0.84/1.07 (icext $_421 uri_rdfs_Container) true = true % 0.84/1.07 |- ifeq (iext uri_rdfs_range uri_rdfs_subClassOf $_421) true % 0.84/1.07 (icext $_421 uri_rdf_Bag) true = true % 0.84/1.07 |- ifeq (iext uri_rdfs_range uri_rdfs_subClassOf $_421) true % 0.84/1.07 (icext $_421 uri_rdf_Property) true = true % 0.84/1.07 |- ifeq (iext uri_rdfs_range uri_rdfs_subClassOf $_421) true % 0.84/1.07 (icext $_421 uri_rdf_XMLLiteral) true = true % 0.84/1.07 |- ifeq (iext uri_rdfs_range uri_rdfs_subClassOf $_421) true % 0.84/1.07 (icext $_421 uri_rdfs_Literal) true = true % 0.84/1.07 |- ifeq (iext uri_rdfs_range uri_rdfs_subClassOf $_421) true % 0.84/1.07 (icext $_421 uri_rdfs_Class) true = true % 0.84/1.07 |- ifeq (iext uri_rdfs_range uri_rdfs_subClassOf $_421) true % 0.84/1.07 (icext $_421 uri_rdfs_ContainerMembershipProperty) true = true % 0.84/1.07 |- ifeq (iext uri_rdfs_range uri_rdfs_subClassOf $_421) true % 0.84/1.07 (icext $_421 uri_rdfs_Datatype) true = true % 0.84/1.07 |- ifeq (iext uri_rdfs_range uri_rdfs_subClassOf $_421) true % 0.84/1.07 (icext $_421 uri_rdfs_Seq) true = true % 0.84/1.07 |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_421) true % 0.84/1.07 (icext $_421 uri_ex_hasAncestor) true = true % 0.84/1.07 |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_421) true % 0.84/1.07 (icext $_421 uri_owl_minCardinality) true = true % 0.84/1.07 |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_421) true % 0.84/1.07 (icext $_421 uri_owl_onProperty) true = true % 0.84/1.07 |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_421) true % 0.84/1.07 (icext $_421 uri_rdf__1) true = true % 0.84/1.07 |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_421) true % 0.84/1.07 (icext $_421 uri_rdfs_member) true = true % 0.84/1.07 |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_421) true % 0.84/1.07 (icext $_421 uri_rdf__2) true = true % 0.84/1.07 |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_421) true % 0.84/1.07 (icext $_421 uri_rdf__3) true = true % 0.84/1.07 |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_421) true % 0.84/1.07 (icext $_421 uri_rdf_first) true = true % 0.84/1.07 |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_421) true % 0.84/1.07 (icext $_421 uri_rdf_object) true = true % 0.84/1.07 |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_421) true % 0.84/1.07 (icext $_421 uri_rdf_predicate) true = true % 0.84/1.07 |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_421) true % 0.84/1.07 (icext $_421 uri_rdf_rest) true = true % 0.84/1.07 |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_421) true % 0.84/1.07 (icext $_421 uri_rdf_subject) true = true % 0.84/1.07 |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_421) true % 0.84/1.07 (icext $_421 uri_rdf_type) true = true % 0.84/1.07 |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_421) true % 0.84/1.07 (icext $_421 uri_rdf_value) true = true % 0.84/1.07 |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_421) true % 0.84/1.07 (icext $_421 uri_rdfs_comment) true = true % 0.84/1.07 |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_421) true % 0.84/1.07 (icext $_421 uri_rdfs_domain) true = true % 0.84/1.07 |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_421) true % 0.84/1.07 (icext $_421 uri_rdfs_isDefinedBy) true = true % 0.84/1.07 |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_421) true % 0.84/1.07 (icext $_421 uri_rdfs_seeAlso) true = true % 0.84/1.07 |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_421) true % 0.84/1.07 (icext $_421 uri_rdfs_label) true = true % 0.84/1.07 |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_421) true % 0.84/1.07 (icext $_421 uri_rdfs_range) true = true % 0.84/1.07 |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_421) true % 0.84/1.07 (icext $_421 uri_rdfs_subClassOf) true = true % 0.84/1.07 |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_421) true % 0.84/1.07 (icext $_421 uri_rdfs_subPropertyOf) true = true % 0.84/1.07 |- ifeq (iext uri_rdf_rest $_423 $_424) true (icext uri_rdf_List $_424) % 0.84/1.07 true = true % 0.84/1.07 |- ifeq (iext uri_rdf_type $_423 $_424) true (icext uri_rdfs_Class $_424) % 0.84/1.07 true = true % 0.84/1.07 |- ifeq (iext uri_rdfs_comment $_423 $_424) true % 0.84/1.07 (icext uri_rdfs_Literal $_424) true = true % 0.84/1.07 |- ifeq (iext uri_rdfs_domain $_423 $_424) true % 0.84/1.07 (icext uri_rdfs_Class $_424) true = true % 0.84/1.07 |- ifeq (iext uri_rdfs_label $_423 $_424) true % 0.84/1.07 (icext uri_rdfs_Literal $_424) true = true % 0.84/1.07 |- ifeq (iext uri_rdfs_range $_423 $_424) true (icext uri_rdfs_Class $_424) % 0.84/1.07 true = true % 0.84/1.07 |- ifeq (iext uri_rdfs_subClassOf $_423 $_424) true % 0.84/1.07 (icext uri_rdfs_Class $_424) true = true % 0.84/1.07 |- ifeq (iext uri_rdfs_subPropertyOf $_423 $_424) true % 0.84/1.07 (icext uri_rdf_Property $_424) true = true % 0.84/1.07 |- icext uri_rdfs_Class uri_owl_Restriction = true % 0.84/1.07 |- ifeq (iext uri_rdfs_range $P uri_rdfs_Class) true % 0.84/1.07 (ifeq (iext $P $X uri_owl_Restriction) true true true) true = true % 0.84/1.07 |- ifeq (iext uri_rdfs_domain $P uri_rdfs_Class) true % 0.84/1.07 (ifeq (iext $P uri_owl_Restriction $Y) true true true) true = true % 0.84/1.07 |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Class $D) true % 0.84/1.07 (icext $D uri_owl_Restriction) true = true % 0.84/1.07 |- iext uri_rdf_type uri_owl_Restriction uri_rdfs_Class = true % 0.84/1.07 |- ic uri_owl_Restriction = true % 0.84/1.07 |- iext uri_rdfs_subClassOf uri_owl_Restriction uri_owl_Restriction = true % 0.84/1.07 |- iext uri_rdfs_subClassOf uri_owl_Restriction uri_rdfs_Resource = true % 0.84/1.07 |- ifeq (iext uri_rdfs_range uri_rdfs_subClassOf $C) true % 0.84/1.07 (icext $C uri_owl_Restriction) true = true % 0.84/1.07 |- ifeq (iext uri_rdfs_domain uri_rdfs_subClassOf $C) true % 0.84/1.07 (icext $C uri_owl_Restriction) true = true % 0.84/1.07 |- ifeq (icext uri_owl_Restriction $X) true (icext uri_owl_Restriction $X) % 0.84/1.07 true = true % 0.84/1.07 |- ifeq (iext uri_rdfs_subClassOf $C uri_owl_Restriction) true % 0.84/1.07 (iext uri_rdfs_subClassOf $C uri_rdfs_Resource) true = true % 0.84/1.07 |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Resource $E) true % 0.84/1.07 (iext uri_rdfs_subClassOf uri_owl_Restriction $E) true = true % 0.84/1.07 |- icext uri_rdfs_Class uri_owl_TransitiveProperty = true % 0.84/1.07 |- ifeq (iext uri_rdfs_range $P uri_rdfs_Class) true % 0.84/1.07 (ifeq (iext $P $X uri_owl_TransitiveProperty) true true true) true = % 0.84/1.07 true % 0.84/1.07 |- ifeq (iext uri_rdfs_domain $P uri_rdfs_Class) true % 0.84/1.07 (ifeq (iext $P uri_owl_TransitiveProperty $Y) true true true) true = % 0.84/1.07 true % 0.84/1.07 |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Class $D) true % 0.84/1.07 (icext $D uri_owl_TransitiveProperty) true = true % 0.84/1.07 |- iext uri_rdf_type uri_owl_TransitiveProperty uri_rdfs_Class = true % 0.84/1.07 |- ic uri_owl_TransitiveProperty = true % 0.84/1.07 |- iext uri_rdfs_subClassOf uri_owl_TransitiveProperty % 0.84/1.07 uri_owl_TransitiveProperty = true % 0.84/1.07 |- iext uri_rdfs_subClassOf uri_owl_TransitiveProperty uri_rdfs_Resource = % 0.84/1.07 true % 0.84/1.07 |- ifeq (iext uri_rdfs_range uri_rdfs_subClassOf $C) true % 0.84/1.07 (icext $C uri_owl_TransitiveProperty) true = true % 0.84/1.07 |- ifeq (iext uri_rdfs_domain uri_rdfs_subClassOf $C) true % 0.84/1.07 (icext $C uri_owl_TransitiveProperty) true = true % 0.84/1.07 |- ifeq (icext uri_owl_TransitiveProperty $X) true % 0.84/1.07 (icext uri_owl_TransitiveProperty $X) true = true % 0.84/1.07 |- ifeq (iext uri_rdfs_subClassOf $C uri_owl_TransitiveProperty) true % 0.84/1.07 (iext uri_rdfs_subClassOf $C uri_rdfs_Resource) true = true % 0.84/1.07 |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Resource $E) true % 0.84/1.07 (iext uri_rdfs_subClassOf uri_owl_TransitiveProperty $E) true = true % 0.84/1.07 |- icext uri_rdfs_Class uri_rdf_List = true % 0.84/1.07 |- ifeq (iext uri_rdfs_range $P uri_rdfs_Class) true % 0.84/1.07 (ifeq (iext $P $X uri_rdf_List) true true true) true = true % 0.84/1.08 |- ifeq (iext uri_rdfs_domain $P uri_rdfs_Class) true % 0.84/1.08 (ifeq (iext $P uri_rdf_List $Y) true true true) true = true % 0.84/1.08 |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Class $D) true % 0.84/1.08 (icext $D uri_rdf_List) true = true % 0.84/1.08 |- iext uri_rdf_type uri_rdf_List uri_rdfs_Class = true % 0.84/1.08 |- ic uri_rdf_List = true % 0.84/1.08 |- iext uri_rdfs_subClassOf uri_rdf_List uri_rdf_List = true % 0.84/1.08 |- iext uri_rdfs_subClassOf uri_rdf_List uri_rdfs_Resource = true % 0.84/1.08 |- ifeq (iext uri_rdfs_range uri_rdfs_subClassOf $C) true % 0.84/1.08 (icext $C uri_rdf_List) true = true % 0.84/1.08 |- ifeq (iext uri_rdfs_domain uri_rdfs_subClassOf $C) true % 0.84/1.08 (icext $C uri_rdf_List) true = true % 0.84/1.08 |- ifeq (icext uri_rdf_List $X) true (icext uri_rdf_List $X) true = true % 0.84/1.08 |- ifeq (iext uri_rdfs_subClassOf $C uri_rdf_List) true % 0.84/1.08 (iext uri_rdfs_subClassOf $C uri_rdfs_Resource) true = true % 0.84/1.08 |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Resource $E) true % 0.84/1.08 (iext uri_rdfs_subClassOf uri_rdf_List $E) true = true % 0.84/1.08 |- icext uri_rdfs_Class uri_rdfs_Statement = true % 0.84/1.08 |- ifeq (iext uri_rdfs_range $P uri_rdfs_Class) true % 0.84/1.08 (ifeq (iext $P $X uri_rdfs_Statement) true true true) true = true % 0.84/1.08 |- ifeq (iext uri_rdfs_domain $P uri_rdfs_Class) true % 0.84/1.08 (ifeq (iext $P uri_rdfs_Statement $Y) true true true) true = true % 0.84/1.08 |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Class $D) true % 0.84/1.08 (icext $D uri_rdfs_Statement) true = true % 0.84/1.08 |- iext uri_rdf_type uri_rdfs_Statement uri_rdfs_Class = true % 0.84/1.08 |- ic uri_rdfs_Statement = true % 0.84/1.08 |- iext uri_rdfs_subClassOf uri_rdfs_Statement uri_rdfs_Statement = true % 0.84/1.08 |- iext uri_rdfs_subClassOf uri_rdfs_Statement uri_rdfs_Resource = true % 0.84/1.08 |- ifeq (iext uri_rdfs_domain uri_rdfs_subClassOf $C) true % 0.84/1.08 (icext $C uri_rdfs_Statement) true = true % 0.84/1.08 |- ifeq (iext uri_rdfs_subClassOf $C uri_rdfs_Statement) true % 0.84/1.08 (iext uri_rdfs_subClassOf $C uri_rdfs_Resource) true = true % 0.84/1.08 |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Resource $E) true % 0.84/1.08 (iext uri_rdfs_subClassOf uri_rdfs_Statement $E) true = true % 0.84/1.08 |- ifeq (iext uri_rdfs_range uri_rdfs_subClassOf $C) true % 0.84/1.08 (icext $C uri_rdfs_Statement) true = true % 0.84/1.08 |- ifeq (icext uri_rdfs_Statement $X) true (icext uri_rdfs_Statement $X) % 0.84/1.08 true = true % 0.84/1.08 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_ex_hasAncestor) true % 0.84/1.08 (ifeq (iext $_635 uri_ex_alice uri_ex_bob) true true true) true = true % 0.84/1.08 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_owl_minCardinality) true % 0.84/1.08 (ifeq % 0.84/1.08 (iext $_635 % 0.84/1.08 sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z % 0.84/1.08 (literal_typed dat_str_1 uri_xsd_nonNegativeInteger)) true true % 0.84/1.08 true) true = true % 0.84/1.08 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_owl_onProperty) true % 0.84/1.08 (ifeq % 0.84/1.08 (iext $_635 % 0.84/1.08 sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z % 0.84/1.08 uri_ex_hasAncestor) true true true) true = true % 0.84/1.08 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdf_type) true % 0.84/1.08 (ifeq % 0.84/1.08 (iext $_635 % 0.84/1.08 sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z % 0.84/1.08 uri_owl_Restriction) true true true) true = true % 0.84/1.08 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdf_type) true % 0.84/1.08 (ifeq % 0.84/1.08 (iext $_635 % 0.84/1.08 sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z % 0.84/1.08 uri_rdfs_Class) true true true) true = true % 0.84/1.08 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdf_type) true % 0.84/1.08 (ifeq (iext $_635 uri_ex_Person uri_rdfs_Class) true true true) true = % 0.84/1.08 true % 0.84/1.08 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdf_type) true % 0.84/1.08 (ifeq % 0.84/1.08 (iext $_635 uri_ex_alice % 0.84/1.08 sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z) % 0.84/1.08 true true true) true = true % 0.84/1.08 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdf_type) true % 0.84/1.08 (ifeq (iext $_635 uri_ex_alice uri_ex_Person) true true true) true = % 0.84/1.08 true % 0.84/1.08 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdf_type) true % 0.84/1.08 (ifeq % 0.84/1.08 (iext $_635 uri_ex_bob % 0.84/1.08 sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z) % 0.84/1.08 true true true) true = true % 0.84/1.08 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdf_type) true % 0.84/1.08 (ifeq (iext $_635 uri_ex_bob uri_ex_Person) true true true) true = % 0.84/1.08 true % 0.84/1.08 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdf_type) true % 0.84/1.08 (ifeq (iext $_635 uri_ex_hasAncestor uri_owl_TransitiveProperty) true % 0.84/1.08 true true) true = true % 0.84/1.08 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdf_type) true % 0.84/1.08 (ifeq (iext $_635 uri_ex_hasAncestor uri_rdf_Property) true true true) % 0.84/1.08 true = true % 0.84/1.08 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdf_type) true % 0.84/1.08 (ifeq (iext $_635 uri_owl_Restriction uri_rdfs_Class) true true true) % 0.84/1.08 true = true % 0.84/1.08 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdf_type) true % 0.84/1.08 (ifeq (iext $_635 uri_owl_TransitiveProperty uri_rdfs_Class) true true % 0.84/1.08 true) true = true % 0.84/1.08 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdf_type) true % 0.84/1.08 (ifeq (iext $_635 uri_owl_minCardinality uri_rdf_Property) true true % 0.84/1.08 true) true = true % 0.84/1.08 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdf_type) true % 0.84/1.08 (ifeq (iext $_635 uri_owl_onProperty uri_rdf_Property) true true true) % 0.84/1.08 true = true % 0.84/1.08 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdf_type) true % 0.84/1.08 (ifeq (iext $_635 uri_rdf_Alt uri_rdfs_Class) true true true) true = % 0.84/1.08 true % 0.84/1.08 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdf_type) true % 0.84/1.08 (ifeq (iext $_635 uri_rdf_Bag uri_rdfs_Class) true true true) true = % 0.84/1.08 true % 0.84/1.08 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdf_type) true % 0.84/1.08 (ifeq (iext $_635 uri_rdf_List uri_rdfs_Class) true true true) true = % 0.84/1.08 true % 0.84/1.08 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdf_type) true % 0.84/1.08 (ifeq (iext $_635 uri_rdf_Property uri_rdfs_Class) true true true) % 0.84/1.08 true = true % 0.84/1.08 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdf_type) true % 0.84/1.08 (ifeq (iext $_635 uri_rdf_XMLLiteral uri_rdfs_Class) true true true) % 0.84/1.08 true = true % 0.84/1.08 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdf_type) true % 0.84/1.08 (ifeq (iext $_635 uri_rdf_XMLLiteral uri_rdfs_Datatype) true true % 0.84/1.08 true) true = true % 0.84/1.08 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdf_type) true % 0.84/1.08 (ifeq (iext $_635 uri_rdf__1 uri_rdf_Property) true true true) true = % 0.84/1.08 true % 0.84/1.08 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdf_type) true % 0.84/1.08 (ifeq (iext $_635 uri_rdf__1 uri_rdfs_ContainerMembershipProperty) % 0.84/1.08 true true true) true = true % 0.84/1.08 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdf_type) true % 0.84/1.08 (ifeq (iext $_635 uri_rdf__2 uri_rdf_Property) true true true) true = % 0.84/1.08 true % 0.84/1.08 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdf_type) true % 0.84/1.08 (ifeq (iext $_635 uri_rdf__2 uri_rdfs_ContainerMembershipProperty) % 0.84/1.08 true true true) true = true % 0.84/1.08 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdf_type) true % 0.84/1.08 (ifeq (iext $_635 uri_rdf__3 uri_rdf_Property) true true true) true = % 0.84/1.08 true % 0.84/1.08 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdf_type) true % 0.84/1.08 (ifeq (iext $_635 uri_rdf__3 uri_rdfs_ContainerMembershipProperty) % 0.84/1.08 true true true) true = true % 0.84/1.08 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdf_type) true % 0.84/1.08 (ifeq (iext $_635 uri_rdf_first uri_rdf_Property) true true true) % 0.84/1.08 true = true % 0.84/1.08 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdf_type) true % 0.84/1.08 (ifeq (iext $_635 uri_rdf_nil uri_rdf_List) true true true) true = % 0.84/1.08 true % 0.84/1.08 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdf_type) true % 0.84/1.08 (ifeq (iext $_635 uri_rdf_object uri_rdf_Property) true true true) % 0.84/1.08 true = true % 0.84/1.08 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdf_type) true % 0.84/1.08 (ifeq (iext $_635 uri_rdf_predicate uri_rdf_Property) true true true) % 0.84/1.08 true = true % 0.84/1.08 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdf_type) true % 0.84/1.08 (ifeq (iext $_635 uri_rdf_rest uri_rdf_Property) true true true) % 0.84/1.08 true = true % 0.84/1.08 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdf_type) true % 0.84/1.08 (ifeq (iext $_635 uri_rdf_subject uri_rdf_Property) true true true) % 0.84/1.08 true = true % 0.84/1.08 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdf_type) true % 0.84/1.08 (ifeq (iext $_635 uri_rdf_type uri_rdf_Property) true true true) % 0.84/1.08 true = true % 0.84/1.08 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdf_type) true % 0.84/1.08 (ifeq (iext $_635 uri_rdf_value uri_rdf_Property) true true true) % 0.84/1.08 true = true % 0.84/1.08 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdf_type) true % 0.84/1.08 (ifeq (iext $_635 uri_rdfs_Class uri_rdfs_Class) true true true) % 0.84/1.08 true = true % 0.84/1.08 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdf_type) true % 0.84/1.08 (ifeq (iext $_635 uri_rdfs_Container uri_rdfs_Class) true true true) % 0.84/1.08 true = true % 0.84/1.08 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdf_type) true % 0.84/1.08 (ifeq (iext $_635 uri_rdfs_ContainerMembershipProperty uri_rdfs_Class) % 0.84/1.08 true true true) true = true % 0.84/1.08 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdf_type) true % 0.84/1.08 (ifeq (iext $_635 uri_rdfs_Datatype uri_rdfs_Class) true true true) % 0.84/1.08 true = true % 0.84/1.08 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdf_type) true % 0.84/1.08 (ifeq (iext $_635 uri_rdfs_Literal uri_rdfs_Class) true true true) % 0.84/1.08 true = true % 0.84/1.08 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdf_type) true % 0.84/1.08 (ifeq (iext $_635 uri_rdfs_Resource uri_rdfs_Class) true true true) % 0.84/1.08 true = true % 0.84/1.08 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdf_type) true % 0.84/1.08 (ifeq (iext $_635 uri_rdfs_Seq uri_rdfs_Class) true true true) true = % 0.84/1.08 true % 0.84/1.08 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdf_type) true % 0.84/1.08 (ifeq (iext $_635 uri_rdfs_Statement uri_rdfs_Class) true true true) % 0.84/1.08 true = true % 0.84/1.08 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdf_type) true % 0.84/1.08 (ifeq (iext $_635 uri_rdfs_comment uri_rdf_Property) true true true) % 0.84/1.08 true = true % 0.84/1.08 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdf_type) true % 0.84/1.08 (ifeq (iext $_635 uri_rdfs_domain uri_rdf_Property) true true true) % 0.84/1.08 true = true % 0.84/1.08 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdf_type) true % 0.84/1.08 (ifeq (iext $_635 uri_rdfs_isDefinedBy uri_rdf_Property) true true % 0.84/1.08 true) true = true % 0.84/1.08 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdf_type) true % 0.84/1.08 (ifeq (iext $_635 uri_rdfs_label uri_rdf_Property) true true true) % 0.84/1.08 true = true % 0.84/1.08 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdf_type) true % 0.84/1.08 (ifeq (iext $_635 uri_rdfs_member uri_rdf_Property) true true true) % 0.84/1.08 true = true % 0.84/1.08 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdf_type) true % 0.84/1.08 (ifeq (iext $_635 uri_rdfs_range uri_rdf_Property) true true true) % 0.84/1.08 true = true % 0.84/1.08 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdf_type) true % 0.84/1.08 (ifeq (iext $_635 uri_rdfs_seeAlso uri_rdf_Property) true true true) % 0.84/1.08 true = true % 0.84/1.08 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdf_type) true % 0.84/1.08 (ifeq (iext $_635 uri_rdfs_subClassOf uri_rdf_Property) true true % 0.84/1.08 true) true = true % 0.84/1.08 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdf_type) true % 0.84/1.08 (ifeq (iext $_635 uri_rdfs_subPropertyOf uri_rdf_Property) true true % 0.84/1.08 true) true = true % 0.84/1.08 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdf_type) true % 0.84/1.08 (ifeq (iext $_635 $_637 uri_rdfs_Resource) true true true) true = true % 0.84/1.08 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdfs_domain) true % 0.84/1.08 (ifeq (iext $_635 uri_rdf__1 uri_rdfs_Resource) true true true) true = % 0.84/1.08 true % 0.84/1.08 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdfs_domain) true % 0.84/1.08 (ifeq (iext $_635 uri_rdf__2 uri_rdfs_Resource) true true true) true = % 0.84/1.08 true % 0.84/1.08 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdfs_domain) true % 0.84/1.08 (ifeq (iext $_635 uri_rdf__3 uri_rdfs_Resource) true true true) true = % 0.84/1.08 true % 0.84/1.08 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdfs_domain) true % 0.84/1.08 (ifeq (iext $_635 uri_rdf_first uri_rdf_List) true true true) true = % 0.84/1.08 true % 0.84/1.08 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdfs_domain) true % 0.84/1.08 (ifeq (iext $_635 uri_rdf_object uri_rdfs_Statement) true true true) % 0.84/1.08 true = true % 0.84/1.08 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdfs_domain) true % 0.84/1.08 (ifeq (iext $_635 uri_rdf_predicate uri_rdfs_Statement) true true % 0.84/1.08 true) true = true % 0.84/1.08 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdfs_domain) true % 0.84/1.08 (ifeq (iext $_635 uri_rdf_rest uri_rdf_List) true true true) true = % 0.84/1.08 true % 0.84/1.08 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdfs_domain) true % 0.84/1.08 (ifeq (iext $_635 uri_rdf_subject uri_rdfs_Statement) true true true) % 0.84/1.08 true = true % 0.84/1.08 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdfs_domain) true % 0.84/1.08 (ifeq (iext $_635 uri_rdf_type uri_rdfs_Resource) true true true) % 0.84/1.08 true = true % 0.84/1.08 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdfs_domain) true % 0.84/1.08 (ifeq (iext $_635 uri_rdf_value uri_rdfs_Resource) true true true) % 0.84/1.08 true = true % 0.84/1.08 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdfs_domain) true % 0.84/1.08 (ifeq (iext $_635 uri_rdfs_comment uri_rdfs_Resource) true true true) % 0.84/1.08 true = true % 0.84/1.08 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdfs_domain) true % 0.84/1.08 (ifeq (iext $_635 uri_rdfs_domain uri_rdf_Property) true true true) % 0.84/1.08 true = true % 0.84/1.08 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdfs_domain) true % 0.84/1.08 (ifeq (iext $_635 uri_rdfs_isDefinedBy uri_rdfs_Resource) true true % 0.84/1.08 true) true = true % 0.84/1.08 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdfs_domain) true % 0.84/1.08 (ifeq (iext $_635 uri_rdfs_label uri_rdfs_Resource) true true true) % 0.84/1.08 true = true % 0.84/1.08 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdfs_domain) true % 0.84/1.08 (ifeq (iext $_635 uri_rdfs_member uri_rdfs_Resource) true true true) % 0.84/1.08 true = true % 0.84/1.08 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdfs_domain) true % 0.84/1.08 (ifeq (iext $_635 uri_rdfs_range uri_rdf_Property) true true true) % 0.84/1.08 true = true % 0.84/1.08 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdfs_domain) true % 0.84/1.08 (ifeq (iext $_635 uri_rdfs_seeAlso uri_rdfs_Resource) true true true) % 0.84/1.08 true = true % 0.84/1.08 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdfs_domain) true % 0.84/1.08 (ifeq (iext $_635 uri_rdfs_subClassOf uri_rdfs_Class) true true true) % 0.84/1.08 true = true % 0.84/1.08 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdfs_domain) true % 0.84/1.08 (ifeq (iext $_635 uri_rdfs_subPropertyOf uri_rdf_Property) true true % 0.84/1.08 true) true = true % 0.84/1.08 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdfs_range) true % 0.84/1.08 (ifeq (iext $_635 uri_rdf__1 uri_rdfs_Resource) true true true) true = % 0.84/1.08 true % 0.92/1.08 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdfs_range) true % 0.92/1.08 (ifeq (iext $_635 uri_rdf__2 uri_rdfs_Resource) true true true) true = % 0.92/1.08 true % 0.92/1.08 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdfs_range) true % 0.92/1.08 (ifeq (iext $_635 uri_rdf__3 uri_rdfs_Resource) true true true) true = % 0.92/1.08 true % 0.92/1.08 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdfs_range) true % 0.92/1.08 (ifeq (iext $_635 uri_rdf_first uri_rdfs_Resource) true true true) % 0.92/1.08 true = true % 0.92/1.08 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdfs_range) true % 0.92/1.08 (ifeq (iext $_635 uri_rdf_predicate uri_rdfs_Resource) true true true) % 0.92/1.08 true = true % 0.92/1.08 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdfs_range) true % 0.92/1.08 (ifeq (iext $_635 uri_rdf_rest uri_rdf_List) true true true) true = % 0.92/1.08 true % 0.92/1.08 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdfs_range) true % 0.92/1.08 (ifeq (iext $_635 uri_rdf_subject uri_rdfs_Resource) true true true) % 0.92/1.08 true = true % 0.92/1.08 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdfs_range) true % 0.92/1.08 (ifeq (iext $_635 uri_rdf_type uri_rdfs_Class) true true true) true = % 0.92/1.08 true % 0.92/1.08 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdfs_range) true % 0.92/1.08 (ifeq (iext $_635 uri_rdf_value uri_rdfs_Resource) true true true) % 0.92/1.08 true = true % 0.92/1.08 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdfs_range) true % 0.92/1.08 (ifeq (iext $_635 uri_rdfs_comment uri_rdfs_Literal) true true true) % 0.92/1.08 true = true % 0.92/1.08 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdfs_range) true % 0.92/1.08 (ifeq (iext $_635 uri_rdfs_domain uri_rdfs_Class) true true true) % 0.92/1.08 true = true % 0.92/1.08 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdfs_range) true % 0.92/1.08 (ifeq (iext $_635 uri_rdfs_isDefinedBy uri_rdfs_Resource) true true % 0.92/1.08 true) true = true % 0.92/1.08 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdfs_range) true % 0.92/1.08 (ifeq (iext $_635 uri_rdfs_label uri_rdfs_Literal) true true true) % 0.92/1.08 true = true % 0.92/1.08 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdfs_range) true % 0.92/1.08 (ifeq (iext $_635 uri_rdfs_member uri_rdfs_Resource) true true true) % 0.92/1.08 true = true % 0.92/1.08 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdfs_range) true % 0.92/1.08 (ifeq (iext $_635 uri_rdfs_range uri_rdfs_Class) true true true) % 0.92/1.08 true = true % 0.92/1.08 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdfs_range) true % 0.92/1.08 (ifeq (iext $_635 uri_rdfs_seeAlso uri_rdfs_Resource) true true true) % 0.92/1.08 true = true % 0.92/1.08 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdfs_range) true % 0.92/1.08 (ifeq (iext $_635 uri_rdfs_subClassOf uri_rdfs_Class) true true true) % 0.92/1.08 true = true % 0.92/1.08 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdfs_range) true % 0.92/1.08 (ifeq (iext $_635 uri_rdfs_subPropertyOf uri_rdf_Property) true true % 0.92/1.08 true) true = true % 0.92/1.08 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdfs_subClassOf) true % 0.92/1.08 (ifeq % 0.92/1.08 (iext $_635 % 0.92/1.08 sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z % 0.92/1.08 sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z) % 0.92/1.08 true true true) true = true % 0.92/1.08 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdfs_subClassOf) true % 0.92/1.08 (ifeq % 0.92/1.08 (iext $_635 % 0.92/1.08 sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z % 0.92/1.08 uri_rdfs_Resource) true true true) true = true % 0.92/1.08 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdfs_subClassOf) true % 0.92/1.08 (ifeq % 0.92/1.08 (iext $_635 uri_ex_Person % 0.92/1.08 sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z) % 0.92/1.08 true true true) true = true % 0.92/1.08 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdfs_subClassOf) true % 0.92/1.08 (ifeq (iext $_635 uri_ex_Person uri_ex_Person) true true true) true = % 0.92/1.08 true % 0.92/1.08 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdfs_subClassOf) true % 0.92/1.08 (ifeq (iext $_635 uri_ex_Person uri_rdfs_Resource) true true true) % 0.92/1.08 true = true % 0.92/1.08 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdfs_subClassOf) true % 0.92/1.08 (ifeq (iext $_635 uri_owl_Restriction uri_owl_Restriction) true true % 0.92/1.08 true) true = true % 0.92/1.08 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdfs_subClassOf) true % 0.92/1.08 (ifeq (iext $_635 uri_owl_Restriction uri_rdfs_Resource) true true % 0.92/1.08 true) true = true % 0.92/1.08 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdfs_subClassOf) true % 0.92/1.08 (ifeq % 0.92/1.08 (iext $_635 uri_owl_TransitiveProperty uri_owl_TransitiveProperty) % 0.92/1.08 true true true) true = true % 0.92/1.08 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdfs_subClassOf) true % 0.92/1.08 (ifeq (iext $_635 uri_owl_TransitiveProperty uri_rdfs_Resource) true % 0.92/1.08 true true) true = true % 0.92/1.08 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdfs_subClassOf) true % 0.92/1.08 (ifeq (iext $_635 uri_rdf_Alt uri_rdf_Alt) true true true) true = true % 0.92/1.08 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdfs_subClassOf) true % 0.92/1.08 (ifeq (iext $_635 uri_rdf_Alt uri_rdfs_Container) true true true) % 0.92/1.08 true = true % 0.92/1.08 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdfs_subClassOf) true % 0.92/1.08 (ifeq (iext $_635 uri_rdf_Alt uri_rdfs_Resource) true true true) % 0.92/1.08 true = true % 0.92/1.08 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdfs_subClassOf) true % 0.92/1.08 (ifeq (iext $_635 uri_rdf_Bag uri_rdf_Bag) true true true) true = true % 0.92/1.08 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdfs_subClassOf) true % 0.92/1.08 (ifeq (iext $_635 uri_rdf_Bag uri_rdfs_Container) true true true) % 0.92/1.08 true = true % 0.92/1.08 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdfs_subClassOf) true % 0.92/1.08 (ifeq (iext $_635 uri_rdf_Bag uri_rdfs_Resource) true true true) % 0.92/1.08 true = true % 0.92/1.08 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdfs_subClassOf) true % 0.92/1.08 (ifeq (iext $_635 uri_rdf_List uri_rdf_List) true true true) true = % 0.92/1.08 true % 0.92/1.08 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdfs_subClassOf) true % 0.92/1.08 (ifeq (iext $_635 uri_rdf_List uri_rdfs_Resource) true true true) % 0.92/1.08 true = true % 0.92/1.08 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdfs_subClassOf) true % 0.92/1.08 (ifeq (iext $_635 uri_rdf_Property uri_rdf_Property) true true true) % 0.92/1.08 true = true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdfs_subClassOf) true % 0.92/1.09 (ifeq (iext $_635 uri_rdf_Property uri_rdfs_Resource) true true true) % 0.92/1.09 true = true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdfs_subClassOf) true % 0.92/1.09 (ifeq (iext $_635 uri_rdf_XMLLiteral uri_rdf_XMLLiteral) true true % 0.92/1.09 true) true = true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdfs_subClassOf) true % 0.92/1.09 (ifeq (iext $_635 uri_rdf_XMLLiteral uri_rdfs_Literal) true true true) % 0.92/1.09 true = true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdfs_subClassOf) true % 0.92/1.09 (ifeq (iext $_635 uri_rdf_XMLLiteral uri_rdfs_Resource) true true % 0.92/1.09 true) true = true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdfs_subClassOf) true % 0.92/1.09 (ifeq (iext $_635 uri_rdfs_Class uri_rdfs_Class) true true true) % 0.92/1.09 true = true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdfs_subClassOf) true % 0.92/1.09 (ifeq (iext $_635 uri_rdfs_Class uri_rdfs_Resource) true true true) % 0.92/1.09 true = true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdfs_subClassOf) true % 0.92/1.09 (ifeq (iext $_635 uri_rdfs_Container uri_rdfs_Container) true true % 0.92/1.09 true) true = true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdfs_subClassOf) true % 0.92/1.09 (ifeq (iext $_635 uri_rdfs_Container uri_rdfs_Resource) true true % 0.92/1.09 true) true = true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdfs_subClassOf) true % 0.92/1.09 (ifeq % 0.92/1.09 (iext $_635 uri_rdfs_ContainerMembershipProperty uri_rdf_Property) % 0.92/1.09 true true true) true = true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdfs_subClassOf) true % 0.92/1.09 (ifeq % 0.92/1.09 (iext $_635 uri_rdfs_ContainerMembershipProperty % 0.92/1.09 uri_rdfs_ContainerMembershipProperty) true true true) true = % 0.92/1.09 true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdfs_subClassOf) true % 0.92/1.09 (ifeq % 0.92/1.09 (iext $_635 uri_rdfs_ContainerMembershipProperty uri_rdfs_Resource) % 0.92/1.09 true true true) true = true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdfs_subClassOf) true % 0.92/1.09 (ifeq (iext $_635 uri_rdfs_Datatype uri_rdfs_Class) true true true) % 0.92/1.09 true = true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdfs_subClassOf) true % 0.92/1.09 (ifeq (iext $_635 uri_rdfs_Datatype uri_rdfs_Datatype) true true true) % 0.92/1.09 true = true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdfs_subClassOf) true % 0.92/1.09 (ifeq (iext $_635 uri_rdfs_Datatype uri_rdfs_Resource) true true true) % 0.92/1.09 true = true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdfs_subClassOf) true % 0.92/1.09 (ifeq (iext $_635 uri_rdfs_Literal uri_rdfs_Literal) true true true) % 0.92/1.09 true = true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdfs_subClassOf) true % 0.92/1.09 (ifeq (iext $_635 uri_rdfs_Literal uri_rdfs_Resource) true true true) % 0.92/1.09 true = true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdfs_subClassOf) true % 0.92/1.09 (ifeq (iext $_635 uri_rdfs_Resource uri_rdfs_Resource) true true true) % 0.92/1.09 true = true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdfs_subClassOf) true % 0.92/1.09 (ifeq (iext $_635 uri_rdfs_Seq uri_rdfs_Container) true true true) % 0.92/1.09 true = true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdfs_subClassOf) true % 0.92/1.09 (ifeq (iext $_635 uri_rdfs_Seq uri_rdfs_Resource) true true true) % 0.92/1.09 true = true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdfs_subClassOf) true % 0.92/1.09 (ifeq (iext $_635 uri_rdfs_Seq uri_rdfs_Seq) true true true) true = % 0.92/1.09 true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdfs_subClassOf) true % 0.92/1.09 (ifeq (iext $_635 uri_rdfs_Statement uri_rdfs_Resource) true true % 0.92/1.09 true) true = true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdfs_subClassOf) true % 0.92/1.09 (ifeq (iext $_635 uri_rdfs_Statement uri_rdfs_Statement) true true % 0.92/1.09 true) true = true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdfs_subPropertyOf) true % 0.92/1.09 (ifeq (iext $_635 uri_ex_hasAncestor uri_ex_hasAncestor) true true % 0.92/1.09 true) true = true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdfs_subPropertyOf) true % 0.92/1.09 (ifeq (iext $_635 uri_owl_minCardinality uri_owl_minCardinality) true % 0.92/1.09 true true) true = true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdfs_subPropertyOf) true % 0.92/1.09 (ifeq (iext $_635 uri_owl_onProperty uri_owl_onProperty) true true % 0.92/1.09 true) true = true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdfs_subPropertyOf) true % 0.92/1.09 (ifeq (iext $_635 uri_rdf__1 uri_rdf__1) true true true) true = true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdfs_subPropertyOf) true % 0.92/1.09 (ifeq (iext $_635 uri_rdf__1 uri_rdfs_member) true true true) true = % 0.92/1.09 true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdfs_subPropertyOf) true % 0.92/1.09 (ifeq (iext $_635 uri_rdf__2 uri_rdf__2) true true true) true = true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdfs_subPropertyOf) true % 0.92/1.09 (ifeq (iext $_635 uri_rdf__2 uri_rdfs_member) true true true) true = % 0.92/1.09 true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdfs_subPropertyOf) true % 0.92/1.09 (ifeq (iext $_635 uri_rdf__3 uri_rdf__3) true true true) true = true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdfs_subPropertyOf) true % 0.92/1.09 (ifeq (iext $_635 uri_rdf__3 uri_rdfs_member) true true true) true = % 0.92/1.09 true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdfs_subPropertyOf) true % 0.92/1.09 (ifeq (iext $_635 uri_rdf_first uri_rdf_first) true true true) true = % 0.92/1.09 true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdfs_subPropertyOf) true % 0.92/1.09 (ifeq (iext $_635 uri_rdf_object uri_rdf_object) true true true) % 0.92/1.09 true = true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdfs_subPropertyOf) true % 0.92/1.09 (ifeq (iext $_635 uri_rdf_predicate uri_rdf_predicate) true true true) % 0.92/1.09 true = true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdfs_subPropertyOf) true % 0.92/1.09 (ifeq (iext $_635 uri_rdf_rest uri_rdf_rest) true true true) true = % 0.92/1.09 true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdfs_subPropertyOf) true % 0.92/1.09 (ifeq (iext $_635 uri_rdf_subject uri_rdf_subject) true true true) % 0.92/1.09 true = true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdfs_subPropertyOf) true % 0.92/1.09 (ifeq (iext $_635 uri_rdf_type uri_rdf_type) true true true) true = % 0.92/1.09 true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdfs_subPropertyOf) true % 0.92/1.09 (ifeq (iext $_635 uri_rdf_value uri_rdf_value) true true true) true = % 0.92/1.09 true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdfs_subPropertyOf) true % 0.92/1.09 (ifeq (iext $_635 uri_rdfs_comment uri_rdfs_comment) true true true) % 0.92/1.09 true = true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdfs_subPropertyOf) true % 0.92/1.09 (ifeq (iext $_635 uri_rdfs_domain uri_rdfs_domain) true true true) % 0.92/1.09 true = true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdfs_subPropertyOf) true % 0.92/1.09 (ifeq (iext $_635 uri_rdfs_isDefinedBy uri_rdfs_isDefinedBy) true true % 0.92/1.09 true) true = true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdfs_subPropertyOf) true % 0.92/1.09 (ifeq (iext $_635 uri_rdfs_isDefinedBy uri_rdfs_seeAlso) true true % 0.92/1.09 true) true = true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdfs_subPropertyOf) true % 0.92/1.09 (ifeq (iext $_635 uri_rdfs_label uri_rdfs_label) true true true) % 0.92/1.09 true = true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdfs_subPropertyOf) true % 0.92/1.09 (ifeq (iext $_635 uri_rdfs_member uri_rdfs_member) true true true) % 0.92/1.09 true = true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdfs_subPropertyOf) true % 0.92/1.09 (ifeq (iext $_635 uri_rdfs_range uri_rdfs_range) true true true) % 0.92/1.09 true = true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdfs_subPropertyOf) true % 0.92/1.09 (ifeq (iext $_635 uri_rdfs_seeAlso uri_rdfs_seeAlso) true true true) % 0.92/1.09 true = true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdfs_subPropertyOf) true % 0.92/1.09 (ifeq (iext $_635 uri_rdfs_subClassOf uri_rdfs_subClassOf) true true % 0.92/1.09 true) true = true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf $_635 uri_rdfs_subPropertyOf) true % 0.92/1.09 (ifeq (iext $_635 uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf) true % 0.92/1.09 true true) true = true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf uri_ex_hasAncestor $_636) true % 0.92/1.09 (iext $_636 uri_ex_alice uri_ex_bob) true = true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf uri_owl_minCardinality $_636) true % 0.92/1.09 (iext $_636 % 0.92/1.09 sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z % 0.92/1.09 (literal_typed dat_str_1 uri_xsd_nonNegativeInteger)) true = true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf uri_owl_onProperty $_636) true % 0.92/1.09 (iext $_636 % 0.92/1.09 sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z % 0.92/1.09 uri_ex_hasAncestor) true = true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_636) true % 0.92/1.09 (iext $_636 % 0.92/1.09 sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z % 0.92/1.09 uri_owl_Restriction) true = true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_636) true % 0.92/1.09 (iext $_636 % 0.92/1.09 sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z % 0.92/1.09 uri_rdfs_Class) true = true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_636) true % 0.92/1.09 (iext $_636 uri_ex_Person uri_rdfs_Class) true = true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_636) true % 0.92/1.09 (iext $_636 uri_ex_alice % 0.92/1.09 sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z) % 0.92/1.09 true = true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_636) true % 0.92/1.09 (iext $_636 uri_ex_alice uri_ex_Person) true = true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_636) true % 0.92/1.09 (iext $_636 uri_ex_bob % 0.92/1.09 sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z) % 0.92/1.09 true = true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_636) true % 0.92/1.09 (iext $_636 uri_ex_bob uri_ex_Person) true = true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_636) true % 0.92/1.09 (iext $_636 uri_ex_hasAncestor uri_owl_TransitiveProperty) true = true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_636) true % 0.92/1.09 (iext $_636 uri_ex_hasAncestor uri_rdf_Property) true = true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_636) true % 0.92/1.09 (iext $_636 uri_owl_Restriction uri_rdfs_Class) true = true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_636) true % 0.92/1.09 (iext $_636 uri_owl_TransitiveProperty uri_rdfs_Class) true = true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_636) true % 0.92/1.09 (iext $_636 uri_owl_minCardinality uri_rdf_Property) true = true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_636) true % 0.92/1.09 (iext $_636 uri_owl_onProperty uri_rdf_Property) true = true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_636) true % 0.92/1.09 (iext $_636 uri_rdf_Alt uri_rdfs_Class) true = true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_636) true % 0.92/1.09 (iext $_636 uri_rdf_Bag uri_rdfs_Class) true = true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_636) true % 0.92/1.09 (iext $_636 uri_rdf_List uri_rdfs_Class) true = true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_636) true % 0.92/1.09 (iext $_636 uri_rdf_Property uri_rdfs_Class) true = true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_636) true % 0.92/1.09 (iext $_636 uri_rdf_XMLLiteral uri_rdfs_Class) true = true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_636) true % 0.92/1.09 (iext $_636 uri_rdf_XMLLiteral uri_rdfs_Datatype) true = true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_636) true % 0.92/1.09 (iext $_636 uri_rdf__1 uri_rdf_Property) true = true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_636) true % 0.92/1.09 (iext $_636 uri_rdf__1 uri_rdfs_ContainerMembershipProperty) true = % 0.92/1.09 true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_636) true % 0.92/1.09 (iext $_636 uri_rdf__2 uri_rdf_Property) true = true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_636) true % 0.92/1.09 (iext $_636 uri_rdf__2 uri_rdfs_ContainerMembershipProperty) true = % 0.92/1.09 true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_636) true % 0.92/1.09 (iext $_636 uri_rdf__3 uri_rdf_Property) true = true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_636) true % 0.92/1.09 (iext $_636 uri_rdf__3 uri_rdfs_ContainerMembershipProperty) true = % 0.92/1.09 true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_636) true % 0.92/1.09 (iext $_636 uri_rdf_first uri_rdf_Property) true = true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_636) true % 0.92/1.09 (iext $_636 uri_rdf_nil uri_rdf_List) true = true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_636) true % 0.92/1.09 (iext $_636 uri_rdf_object uri_rdf_Property) true = true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_636) true % 0.92/1.09 (iext $_636 uri_rdf_predicate uri_rdf_Property) true = true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_636) true % 0.92/1.09 (iext $_636 uri_rdf_rest uri_rdf_Property) true = true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_636) true % 0.92/1.09 (iext $_636 uri_rdf_subject uri_rdf_Property) true = true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_636) true % 0.92/1.09 (iext $_636 uri_rdf_type uri_rdf_Property) true = true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_636) true % 0.92/1.09 (iext $_636 uri_rdf_value uri_rdf_Property) true = true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_636) true % 0.92/1.09 (iext $_636 uri_rdfs_Class uri_rdfs_Class) true = true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_636) true % 0.92/1.09 (iext $_636 uri_rdfs_Container uri_rdfs_Class) true = true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_636) true % 0.92/1.09 (iext $_636 uri_rdfs_ContainerMembershipProperty uri_rdfs_Class) % 0.92/1.09 true = true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_636) true % 0.92/1.09 (iext $_636 uri_rdfs_Datatype uri_rdfs_Class) true = true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_636) true % 0.92/1.09 (iext $_636 uri_rdfs_Literal uri_rdfs_Class) true = true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_636) true % 0.92/1.09 (iext $_636 uri_rdfs_Resource uri_rdfs_Class) true = true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_636) true % 0.92/1.09 (iext $_636 uri_rdfs_Seq uri_rdfs_Class) true = true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_636) true % 0.92/1.09 (iext $_636 uri_rdfs_Statement uri_rdfs_Class) true = true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_636) true % 0.92/1.09 (iext $_636 uri_rdfs_comment uri_rdf_Property) true = true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_636) true % 0.92/1.09 (iext $_636 uri_rdfs_domain uri_rdf_Property) true = true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_636) true % 0.92/1.09 (iext $_636 uri_rdfs_isDefinedBy uri_rdf_Property) true = true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_636) true % 0.92/1.09 (iext $_636 uri_rdfs_label uri_rdf_Property) true = true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_636) true % 0.92/1.09 (iext $_636 uri_rdfs_member uri_rdf_Property) true = true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_636) true % 0.92/1.09 (iext $_636 uri_rdfs_range uri_rdf_Property) true = true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_636) true % 0.92/1.09 (iext $_636 uri_rdfs_seeAlso uri_rdf_Property) true = true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_636) true % 0.92/1.09 (iext $_636 uri_rdfs_subClassOf uri_rdf_Property) true = true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_636) true % 0.92/1.09 (iext $_636 uri_rdfs_subPropertyOf uri_rdf_Property) true = true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_636) true % 0.92/1.09 (iext $_636 $_637 uri_rdfs_Resource) true = true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_domain $_636) true % 0.92/1.09 (iext $_636 uri_rdf__1 uri_rdfs_Resource) true = true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_domain $_636) true % 0.92/1.09 (iext $_636 uri_rdf__2 uri_rdfs_Resource) true = true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_domain $_636) true % 0.92/1.09 (iext $_636 uri_rdf__3 uri_rdfs_Resource) true = true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_domain $_636) true % 0.92/1.09 (iext $_636 uri_rdf_first uri_rdf_List) true = true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_domain $_636) true % 0.92/1.09 (iext $_636 uri_rdf_object uri_rdfs_Statement) true = true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_domain $_636) true % 0.92/1.09 (iext $_636 uri_rdf_predicate uri_rdfs_Statement) true = true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_domain $_636) true % 0.92/1.09 (iext $_636 uri_rdf_rest uri_rdf_List) true = true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_domain $_636) true % 0.92/1.09 (iext $_636 uri_rdf_subject uri_rdfs_Statement) true = true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_domain $_636) true % 0.92/1.09 (iext $_636 uri_rdf_type uri_rdfs_Resource) true = true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_domain $_636) true % 0.92/1.09 (iext $_636 uri_rdf_value uri_rdfs_Resource) true = true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_domain $_636) true % 0.92/1.09 (iext $_636 uri_rdfs_comment uri_rdfs_Resource) true = true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_domain $_636) true % 0.92/1.09 (iext $_636 uri_rdfs_domain uri_rdf_Property) true = true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_domain $_636) true % 0.92/1.09 (iext $_636 uri_rdfs_isDefinedBy uri_rdfs_Resource) true = true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_domain $_636) true % 0.92/1.09 (iext $_636 uri_rdfs_label uri_rdfs_Resource) true = true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_domain $_636) true % 0.92/1.09 (iext $_636 uri_rdfs_member uri_rdfs_Resource) true = true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_domain $_636) true % 0.92/1.09 (iext $_636 uri_rdfs_range uri_rdf_Property) true = true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_domain $_636) true % 0.92/1.09 (iext $_636 uri_rdfs_seeAlso uri_rdfs_Resource) true = true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_domain $_636) true % 0.92/1.09 (iext $_636 uri_rdfs_subClassOf uri_rdfs_Class) true = true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_domain $_636) true % 0.92/1.09 (iext $_636 uri_rdfs_subPropertyOf uri_rdf_Property) true = true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_range $_636) true % 0.92/1.09 (iext $_636 uri_rdf__1 uri_rdfs_Resource) true = true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_range $_636) true % 0.92/1.09 (iext $_636 uri_rdf__2 uri_rdfs_Resource) true = true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_range $_636) true % 0.92/1.09 (iext $_636 uri_rdf__3 uri_rdfs_Resource) true = true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_range $_636) true % 0.92/1.09 (iext $_636 uri_rdf_first uri_rdfs_Resource) true = true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_range $_636) true % 0.92/1.09 (iext $_636 uri_rdf_predicate uri_rdfs_Resource) true = true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_range $_636) true % 0.92/1.09 (iext $_636 uri_rdf_rest uri_rdf_List) true = true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_range $_636) true % 0.92/1.09 (iext $_636 uri_rdf_subject uri_rdfs_Resource) true = true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_range $_636) true % 0.92/1.09 (iext $_636 uri_rdf_type uri_rdfs_Class) true = true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_range $_636) true % 0.92/1.09 (iext $_636 uri_rdf_value uri_rdfs_Resource) true = true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_range $_636) true % 0.92/1.09 (iext $_636 uri_rdfs_comment uri_rdfs_Literal) true = true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_range $_636) true % 0.92/1.09 (iext $_636 uri_rdfs_domain uri_rdfs_Class) true = true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_range $_636) true % 0.92/1.09 (iext $_636 uri_rdfs_isDefinedBy uri_rdfs_Resource) true = true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_range $_636) true % 0.92/1.09 (iext $_636 uri_rdfs_label uri_rdfs_Literal) true = true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_range $_636) true % 0.92/1.09 (iext $_636 uri_rdfs_member uri_rdfs_Resource) true = true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_range $_636) true % 0.92/1.09 (iext $_636 uri_rdfs_range uri_rdfs_Class) true = true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_range $_636) true % 0.92/1.09 (iext $_636 uri_rdfs_seeAlso uri_rdfs_Resource) true = true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_range $_636) true % 0.92/1.09 (iext $_636 uri_rdfs_subClassOf uri_rdfs_Class) true = true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_range $_636) true % 0.92/1.09 (iext $_636 uri_rdfs_subPropertyOf uri_rdf_Property) true = true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_636) true % 0.92/1.09 (iext $_636 % 0.92/1.09 sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z % 0.92/1.09 sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z) % 0.92/1.09 true = true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_636) true % 0.92/1.09 (iext $_636 % 0.92/1.09 sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z % 0.92/1.09 uri_rdfs_Resource) true = true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_636) true % 0.92/1.09 (iext $_636 uri_ex_Person % 0.92/1.09 sK1_testcase_premise_fullish_024_Cardinality_Restrictions_on_Complex_Properties_BNODE_z) % 0.92/1.09 true = true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_636) true % 0.92/1.09 (iext $_636 uri_ex_Person uri_ex_Person) true = true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_636) true % 0.92/1.09 (iext $_636 uri_ex_Person uri_rdfs_Resource) true = true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_636) true % 0.92/1.09 (iext $_636 uri_owl_Restriction uri_owl_Restriction) true = true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_636) true % 0.92/1.09 (iext $_636 uri_owl_Restriction uri_rdfs_Resource) true = true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_636) true % 0.92/1.09 (iext $_636 uri_owl_TransitiveProperty uri_owl_TransitiveProperty) % 0.92/1.09 true = true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_636) true % 0.92/1.09 (iext $_636 uri_owl_TransitiveProperty uri_rdfs_Resource) true = true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_636) true % 0.92/1.09 (iext $_636 uri_rdf_Alt uri_rdf_Alt) true = true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_636) true % 0.92/1.09 (iext $_636 uri_rdf_Alt uri_rdfs_Container) true = true % 0.92/1.09 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_636) true % 0.92/1.09 (iext $_636 uri_rdf_Alt uri_rdfs_Resource) true = true % 0.92/1.10 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_636) true % 0.92/1.10 (iext $_636 uri_rdf_Bag uri_rdf_Bag) true = true % 0.92/1.10 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_636) true % 0.92/1.10 (iext $_636 uri_rdf_Bag uri_rdfs_Container) true = true % 0.92/1.10 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_636) true % 0.92/1.10 (iext $_636 uri_rdf_Bag uri_rdfs_Resource) true = true % 0.92/1.10 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_636) true % 0.92/1.10 (iext $_636 uri_rdf_List uri_rdf_List) true = true % 0.92/1.10 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_636) true % 0.92/1.10 (iext $_636 uri_rdf_List uri_rdfs_Resource) true = true % 0.92/1.10 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_636) true % 0.92/1.10 (iext $_636 uri_rdf_Property uri_rdf_Property) true = true % 0.92/1.10 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_636) true % 0.92/1.10 (iext $_636 uri_rdf_Property uri_rdfs_Resource) true = true % 0.92/1.10 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_636) true % 0.92/1.10 (iext $_636 uri_rdf_XMLLiteral uri_rdf_XMLLiteral) true = true % 0.92/1.10 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_636) true % 0.92/1.10 (iext $_636 uri_rdf_XMLLiteral uri_rdfs_Literal) true = true % 0.92/1.10 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_636) true % 0.92/1.10 (iext $_636 uri_rdf_XMLLiteral uri_rdfs_Resource) true = true % 0.92/1.10 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_636) true % 0.92/1.10 (iext $_636 uri_rdfs_Class uri_rdfs_Class) true = true % 0.92/1.10 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_636) true % 0.92/1.10 (iext $_636 uri_rdfs_Class uri_rdfs_Resource) true = true % 0.92/1.10 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_636) true % 0.92/1.10 (iext $_636 uri_rdfs_Container uri_rdfs_Container) true = true % 0.92/1.10 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_636) true % 0.92/1.10 (iext $_636 uri_rdfs_Container uri_rdfs_Resource) true = true % 0.92/1.10 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_636) true % 0.92/1.10 (iext $_636 uri_rdfs_ContainerMembershipProperty uri_rdf_Property) % 0.92/1.10 true = true % 0.92/1.10 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_636) true % 0.92/1.10 (iext $_636 uri_rdfs_ContainerMembershipProperty % 0.92/1.10 uri_rdfs_ContainerMembershipProperty) true = true % 0.92/1.10 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_636) true % 0.92/1.10 (iext $_636 uri_rdfs_ContainerMembershipProperty uri_rdfs_Resource) % 0.92/1.10 true = true % 0.92/1.10 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_636) true % 0.92/1.10 (iext $_636 uri_rdfs_Datatype uri_rdfs_Class) true = true % 0.92/1.10 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_636) true % 0.92/1.10 (iext $_636 uri_rdfs_Datatype uri_rdfs_Datatype) true = true % 0.92/1.10 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_636) true % 0.92/1.10 (iext $_636 uri_rdfs_Datatype uri_rdfs_Resource) true = true % 0.92/1.10 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_636) true % 0.92/1.10 (iext $_636 uri_rdfs_Literal uri_rdfs_Literal) true = true % 0.92/1.10 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_636) true % 0.92/1.10 (iext $_636 uri_rdfs_Literal uri_rdfs_Resource) true = true % 0.92/1.10 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_636) true % 0.92/1.10 (iext $_636 uri_rdfs_Resource uri_rdfs_Resource) true = true % 0.92/1.10 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_636) true % 0.92/1.10 (iext $_636 uri_rdfs_Seq uri_rdfs_Container) true = true % 0.92/1.10 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_636) true % 0.92/1.10 (iext $_636 uri_rdfs_Seq uri_rdfs_Resource) true = true % 0.92/1.10 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_636) true % 0.92/1.10 (iext $_636 uri_rdfs_Seq uri_rdfs_Seq) true = true % 0.92/1.10 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_636) true % 0.92/1.10 (iext $_636 uri_rdfs_Statement uri_rdfs_Resource) true = true % 0.92/1.10 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_636) true % 0.92/1.10 (iext $_636 uri_rdfs_Statement uri_rdfs_Statement) true = true % 0.92/1.10 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_636) true % 0.92/1.10 (iext $_636 uri_ex_hasAncestor uri_ex_hasAncestor) true = true % 0.92/1.10 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_636) true % 0.92/1.10 (iext $_636 uri_owl_minCardinality uri_owl_minCardinality) true = true % 0.92/1.10 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_636) true % 0.92/1.10 (iext $_636 uri_owl_onProperty uri_owl_onProperty) true = true % 0.92/1.10 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_636) true % 0.92/1.10 (iext $_636 uri_rdf__1 uri_rdf__1) true = true % 0.92/1.10 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_636) true % 0.92/1.10 (iext $_636 uri_rdf__1 uri_rdfs_member) true = true % 0.92/1.10 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_636) true % 0.92/1.10 (iext $_636 uri_rdf__2 uri_rdf__2) true = true % 0.92/1.10 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_636) true % 0.92/1.10 (iext $_636 uri_rdf__2 uri_rdfs_member) true = true % 0.92/1.10 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_636) true % 0.92/1.10 (iext $_636 uri_rdf__3 uri_rdf__3) true = true % 0.92/1.10 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_636) true % 0.92/1.10 (iext $_636 uri_rdf__3 uri_rdfs_member) true = true % 0.92/1.10 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_636) true % 0.92/1.10 (iext $_636 uri_rdf_first uri_rdf_first) true = true % 0.92/1.10 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_636) true % 0.92/1.10 (iext $_636 uri_rdf_object uri_rdf_object) true = true % 0.92/1.10 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_636) true % 0.92/1.10 (iext $_636 uri_rdf_predicate uri_rdf_predicate) true = true % 0.92/1.10 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_636) true % 0.92/1.10 (iext $_636 uri_rdf_rest uri_rdf_rest) true = true % 0.92/1.10 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_636) true % 0.92/1.10 (iext $_636 uri_rdf_subject uri_rdf_subject) true = true % 0.92/1.10 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_636) true % 0.92/1.10 (iext $_636 uri_rdf_type uri_rdf_type) true = true % 0.92/1.10 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_636) true % 0.92/1.10 (iext $_636 uri_rdf_value uri_rdf_value) true = true % 0.92/1.10 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_636) true % 0.92/1.10 (iext $_636 uri_rdfs_comment uri_rdfs_comment) true = true % 0.92/1.10 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_636) true % 0.92/1.10 (iext $_636 uri_rdfs_domain uri_rdfs_domain) true = true % 0.92/1.10 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_636) true % 0.92/1.10 (iext $_636 uri_rdfs_isDefinedBy uri_rdfs_isDefinedBy) true = true % 0.92/1.10 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_636) true % 0.92/1.10 (iext $_636 uri_rdfs_isDefinedBy uri_rdfs_seeAlso) true = true % 0.92/1.10 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_636) true % 0.92/1.10 (iext $_636 uri_rdfs_label uri_rdfs_label) true = true % 0.92/1.10 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_636) true % 0.92/1.10 (iext $_636 uri_rdfs_member uri_rdfs_member) true = true % 0.92/1.10 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_636) true % 0.92/1.10 (iext $_636 uri_rdfs_range uri_rdfs_range) true = true % 0.92/1.10 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_636) true % 0.92/1.10 (iext $_636 uri_rdfs_seeAlso uri_rdfs_seeAlso) true = true % 0.92/1.10 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_636) true % 0.92/1.10 (iext $_636 uri_rdfs_subClassOf uri_rdfs_subClassOf) true = true % 0.92/1.10 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_636) true % 0.92/1.10 (iext $_636 uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf) true = true % 0.92/1.10 |- ifeq (iext uri_ex_hasAncestor $_637 $_638) true % 0.92/1.10 (iext uri_ex_hasAncestor $_637 $_638) true = true % 0.92/1.10 |- ifeq (iext uri_owl_minCardinality $_637 $_638) true % 0.92/1.10 (iext uri_owl_minCardinality $_637 $_638) true = true % 0.92/1.10 |- ifeq (iext uri_owl_onProperty $_637 $_638) true % 0.92/1.10 (iext uri_owl_onProperty $_637 $_638) true = true % 0.92/1.10 |- ifeq (iext uri_rdf__1 $_637 $_638) true (iext uri_rdf__1 $_637 $_638) % 0.92/1.10 true = true % 0.92/1.10 |- ifeq (iext uri_rdf__1 $_637 $_638) true % 0.92/1.10 (iext uri_rdfs_member $_637 $_638) true = true % 0.92/1.10 |- ifeq (iext uri_rdf__2 $_637 $_638) true (iext uri_rdf__2 $_637 $_638) % 0.92/1.10 true = true % 0.92/1.10 |- ifeq (iext uri_rdf__2 $_637 $_638) true % 0.92/1.10 (iext uri_rdfs_member $_637 $_638) true = true % 0.92/1.10 |- ifeq (iext uri_rdf__3 $_637 $_638) true (iext uri_rdf__3 $_637 $_638) % 0.92/1.10 true = true % 0.92/1.10 |- ifeq (iext uri_rdf__3 $_637 $_638) true % 0.92/1.10 (iext uri_rdfs_member $_637 $_638) true = true % 0.92/1.10 |- ifeq (iext uri_rdf_first $_637 $_638) true % 0.92/1.10 (iext uri_rdf_first $_637 $_638) true = true % 0.92/1.10 |- ifeq (iext uri_rdf_object $_637 $_638) true % 0.92/1.10 (iext uri_rdf_object $_637 $_638) true = true % 0.92/1.10 |- ifeq (iext uri_rdf_predicate $_637 $_638) true % 0.92/1.10 (iext uri_rdf_predicate $_637 $_638) true = true % 0.92/1.10 |- ifeq (iext uri_rdf_rest $_637 $_638) true % 0.92/1.10 (iext uri_rdf_rest $_637 $_638) true = true % 0.92/1.10 |- ifeq (iext uri_rdf_subject $_637 $_638) true % 0.92/1.10 (iext uri_rdf_subject $_637 $_638) true = true % 0.92/1.10 |- ifeq (iext uri_rdf_type $_637 $_638) true % 0.92/1.10 (iext uri_rdf_type $_637 $_638) true = true % 0.92/1.10 |- ifeq (iext uri_rdf_value $_637 $_638) true % 0.92/1.10 (iext uri_rdf_value $_637 $_638) true = true % 0.92/1.10 |- ifeq (iext uri_rdfs_comment $_637 $_638) true % 0.92/1.10 (iext uri_rdfs_comment $_637 $_638) true = true % 0.92/1.10 |- ifeq (iext uri_rdfs_domain $_637 $_638) true % 0.92/1.10 (iext uri_rdfs_domain $_637 $_638) true = true % 0.92/1.10 |- ifeq (iext uri_rdfs_isDefinedBy $_637 $_638) true % 0.92/1.10 (iext uri_rdfs_isDefinedBy $_637 $_638) true = true % 0.92/1.10 |- ifeq (iext uri_rdfs_isDefinedBy $_637 $_638) true % 0.92/1.10 (iext uri_rdfs_seeAlso $_637 $_638) true = true % 0.92/1.10 |- ifeq (iext uri_rdfs_label $_637 $_638) true % 0.92/1.10 (iext uri_rdfs_label $_637 $_638) true = true % 0.92/1.10 |- ifeq (iext uri_rdfs_member $_637 $_638) true % 0.92/1.10 (iext uri_rdfs_member $_637 $_638) true = true % 0.92/1.10 |- ifeq (iext uri_rdfs_range $_637 $_638) true % 0.92/1.10 (iext uri_rdfs_range $_637 $_638) true = true % 0.92/1.10 |- ifeq (iext uri_rdfs_seeAlso $_637 $_638) true % 0.92/1.10 (iext uri_rdfs_seeAlso $_637 $_638) true = true % 0.92/1.10 |- ifeq (iext uri_rdfs_subClassOf $_637 $_638) true % 0.92/1.10 (iext uri_rdfs_subClassOf $_637 $_638) true = true % 0.92/1.10 |- ifeq (iext uri_rdfs_subPropertyOf $_637 $_638) true % 0.92/1.10 (iext uri_rdfs_subPropertyOf $_637 $_638) true = true % 0.92/1.10 SZS output end Saturation for /export/starexec/sandbox/benchmark/theBenchmark.p % 0.92/1.10 %------------------------------------------------------------------------------