%------------------------------------------------------------------------------ % File : Metis---2.4 % Problem : SWB029-10 : TPTP v8.1.0. Released v7.5.0. % Transfm : none % Format : tptp:raw % Command : metis --show proof --show saturation %s % Computer : n017.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:31 EDT 2022 % Result : Satisfiable 0.83s 0.97s % Output : Saturation 0.83s % Verified : % SZS Type : - % Comments : %------------------------------------------------------------------------------ %----WARNING: Could not form TPTP format derivation %------------------------------------------------------------------------------ %----ORIGINAL SYSTEM OUTPUT % 0.03/0.12 % Problem : SWB029-10 : TPTP v8.1.0. Released v7.5.0. % 0.03/0.12 % Command : metis --show proof --show saturation %s % 0.13/0.33 % Computer : n017.cluster.edu % 0.13/0.33 % Model : x86_64 x86_64 % 0.13/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz % 0.13/0.33 % Memory : 8042.1875MB % 0.13/0.33 % OS : Linux 3.10.0-693.el7.x86_64 % 0.13/0.33 % CPULimit : 300 % 0.13/0.33 % WCLimit : 600 % 0.13/0.33 % DateTime : Tue May 31 23:48:11 EDT 2022 % 0.13/0.33 % CPUTime : % 0.13/0.34 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % 0.83/0.97 % SZS status Satisfiable for /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.83/0.97 % 0.83/0.97 SZS output start Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.83/0.97 |- ifeq $A $A $B $C = $B % 0.83/0.97 |- ifeq (iext $P $S $O) true (ip $P) true = true % 0.83/0.97 |- ir $X = true % 0.83/0.97 |- ifeq (lv $X) true true true = true % 0.83/0.97 |- iext uri_rdf_type uri_rdf_first uri_rdf_Property = true % 0.83/0.97 |- iext uri_rdf_type uri_rdf_nil uri_rdf_List = true % 0.83/0.97 |- iext uri_rdf_type uri_rdf_rest uri_rdf_Property = true % 0.83/0.97 |- iext uri_rdf_type uri_rdf__1 uri_rdf_Property = true % 0.83/0.97 |- iext uri_rdf_type uri_rdf__2 uri_rdf_Property = true % 0.83/0.97 |- iext uri_rdf_type uri_rdf__3 uri_rdf_Property = true % 0.83/0.97 |- iext uri_rdf_type uri_rdf_object uri_rdf_Property = true % 0.83/0.97 |- iext uri_rdf_type uri_rdf_value uri_rdf_Property = true % 0.83/0.97 |- iext uri_rdf_type uri_rdf_subject uri_rdf_Property = true % 0.83/0.97 |- ifeq (ip $P) true (iext uri_rdf_type $P uri_rdf_Property) true = true % 0.83/0.97 |- ifeq (iext uri_rdf_type $P uri_rdf_Property) true (ip $P) true = true % 0.83/0.97 |- iext uri_rdf_type uri_rdf_type uri_rdf_Property = true % 0.83/0.97 |- iext uri_rdfs_domain uri_rdfs_comment uri_rdfs_Resource = true % 0.83/0.97 |- iext uri_rdfs_range uri_rdfs_comment uri_rdfs_Literal = true % 0.83/0.97 |- iext uri_rdfs_domain uri_rdfs_isDefinedBy uri_rdfs_Resource = true % 0.83/0.97 |- iext uri_rdfs_range uri_rdfs_isDefinedBy uri_rdfs_Resource = true % 0.83/0.97 |- iext uri_rdfs_subPropertyOf uri_rdfs_isDefinedBy uri_rdfs_seeAlso = true % 0.83/0.97 |- iext uri_rdfs_domain uri_rdfs_label uri_rdfs_Resource = true % 0.83/0.97 |- iext uri_rdfs_range uri_rdfs_label uri_rdfs_Literal = true % 0.83/0.97 |- iext uri_rdfs_domain uri_rdfs_seeAlso uri_rdfs_Resource = true % 0.83/0.97 |- iext uri_rdfs_range uri_rdfs_seeAlso uri_rdfs_Resource = true % 0.83/0.97 |- ifeq (icext $C $X) true (iext uri_rdf_type $X $C) true = true % 0.83/0.97 |- ifeq (iext uri_rdf_type $X $C) true (icext $C $X) true = true % 0.83/0.97 |- ifeq (ic $C) true (iext uri_rdfs_subClassOf $C uri_rdfs_Resource) true = % 0.83/0.97 true % 0.83/0.97 |- iext uri_rdfs_domain uri_rdf_first uri_rdf_List = true % 0.83/0.97 |- iext uri_rdfs_range uri_rdf_first uri_rdfs_Resource = true % 0.83/0.97 |- iext uri_rdfs_domain uri_rdf_rest uri_rdf_List = true % 0.83/0.97 |- iext uri_rdfs_range uri_rdf_rest uri_rdf_List = true % 0.83/0.97 |- iext uri_rdfs_subClassOf uri_rdf_Alt uri_rdfs_Container = true % 0.83/0.97 |- iext uri_rdfs_subClassOf uri_rdf_Bag uri_rdfs_Container = true % 0.83/0.97 |- ifeq (icext uri_rdfs_ContainerMembershipProperty $P) true % 0.83/0.97 (iext uri_rdfs_subPropertyOf $P uri_rdfs_member) true = true % 0.83/0.97 |- iext uri_rdfs_subClassOf uri_rdfs_ContainerMembershipProperty % 0.83/0.97 uri_rdf_Property = true % 0.83/0.97 |- iext uri_rdfs_domain uri_rdfs_member uri_rdfs_Resource = true % 0.83/0.97 |- iext uri_rdfs_range uri_rdfs_member uri_rdfs_Resource = true % 0.83/0.97 |- iext uri_rdfs_domain uri_rdf__1 uri_rdfs_Resource = true % 0.83/0.97 |- iext uri_rdfs_domain uri_rdf__2 uri_rdfs_Resource = true % 0.83/0.97 |- iext uri_rdfs_domain uri_rdf__3 uri_rdfs_Resource = true % 0.83/0.97 |- iext uri_rdfs_range uri_rdf__1 uri_rdfs_Resource = true % 0.83/0.97 |- iext uri_rdfs_range uri_rdf__2 uri_rdfs_Resource = true % 0.83/0.97 |- iext uri_rdfs_range uri_rdf__3 uri_rdfs_Resource = true % 0.83/0.97 |- iext uri_rdf_type uri_rdf__1 uri_rdfs_ContainerMembershipProperty = true % 0.83/0.97 |- iext uri_rdf_type uri_rdf__2 uri_rdfs_ContainerMembershipProperty = true % 0.83/0.97 |- iext uri_rdf_type uri_rdf__3 uri_rdfs_ContainerMembershipProperty = true % 0.83/0.97 |- iext uri_rdfs_subClassOf uri_rdfs_Seq uri_rdfs_Container = true % 0.83/0.97 |- iext uri_rdfs_subClassOf uri_rdf_XMLLiteral uri_rdfs_Literal = true % 0.83/0.97 |- iext uri_rdf_type uri_rdf_XMLLiteral uri_rdfs_Datatype = true % 0.83/0.97 |- ifeq (icext uri_rdfs_Datatype $D) true % 0.83/0.97 (iext uri_rdfs_subClassOf $D uri_rdfs_Literal) true = true % 0.83/0.97 |- iext uri_rdfs_subClassOf uri_rdfs_Datatype uri_rdfs_Class = true % 0.83/0.97 |- iext uri_rdfs_domain uri_rdfs_domain uri_rdf_Property = true % 0.83/0.97 |- ifeq (iext uri_rdfs_domain $P $C) true % 0.83/0.97 (ifeq (iext $P $X $Y) true (icext $C $X) true) true = true % 0.83/0.97 |- iext uri_rdfs_range uri_rdfs_domain uri_rdfs_Class = true % 0.83/0.97 |- ifeq (ic $X) true (icext uri_rdfs_Class $X) true = true % 0.83/0.97 |- ifeq (icext uri_rdfs_Class $X) true (ic $X) true = true % 0.83/0.98 |- icext uri_rdfs_Resource $X = true % 0.83/0.98 |- ifeq (icext uri_rdfs_Literal $X) true (lv $X) true = true % 0.83/0.98 |- ifeq (lv $X) true (icext uri_rdfs_Literal $X) true = true % 0.83/0.98 |- iext uri_rdf_type uri_rdf_Property uri_rdfs_Class = true % 0.83/0.98 |- iext uri_rdfs_domain uri_rdfs_range uri_rdf_Property = true % 0.83/0.98 |- ifeq (iext uri_rdfs_range $P $C) true % 0.83/0.98 (ifeq (iext $P $X $Y) true (icext $C $Y) true) true = true % 0.83/0.98 |- iext uri_rdfs_range uri_rdfs_range uri_rdfs_Class = true % 0.83/0.98 |- iext uri_rdfs_domain uri_rdf_object uri_rdfs_Statement = true % 0.83/0.98 |- iext uri_rdfs_range uri_rdf_predicate uri_rdfs_Resource = true % 0.83/0.98 |- iext uri_rdfs_domain uri_rdf_predicate uri_rdfs_Statement = true % 0.83/0.98 |- iext uri_rdfs_domain uri_rdf_subject uri_rdfs_Statement = true % 0.83/0.98 |- iext uri_rdfs_range uri_rdf_subject uri_rdfs_Resource = true % 0.83/0.98 |- iext uri_rdfs_domain uri_rdfs_subClassOf uri_rdfs_Class = true % 0.83/0.98 |- ifeq (icext $C $X) true % 0.83/0.98 (ifeq (iext uri_rdfs_subClassOf $C $D) true (icext $D $X) true) true = % 0.83/0.98 true % 0.83/0.98 |- ifeq (iext uri_rdfs_subClassOf $C $D) true (ic $D) true = true % 0.83/0.98 |- ifeq (iext uri_rdfs_subClassOf $C $D) true (ic $C) true = true % 0.83/0.98 |- iext uri_rdfs_range uri_rdfs_subClassOf uri_rdfs_Class = true % 0.83/0.98 |- ifeq (ic $C) true (iext uri_rdfs_subClassOf $C $C) true = true % 0.83/0.98 |- ifeq (iext uri_rdfs_subClassOf $D $E) true % 0.83/0.98 (ifeq (iext uri_rdfs_subClassOf $C $D) true % 0.83/0.98 (iext uri_rdfs_subClassOf $C $E) true) true = true % 0.83/0.98 |- iext uri_rdfs_domain uri_rdfs_subPropertyOf uri_rdf_Property = true % 0.83/0.98 |- ifeq (iext uri_rdfs_subPropertyOf $P $Q) true (ip $Q) true = true % 0.83/0.98 |- ifeq (iext uri_rdfs_subPropertyOf $P $Q) true (ip $P) true = true % 0.83/0.98 |- ifeq (iext uri_rdfs_subPropertyOf $P $Q) true % 0.83/0.98 (ifeq (iext $P $X $Y) true (iext $Q $X $Y) true) true = true % 0.83/0.98 |- iext uri_rdfs_range uri_rdfs_subPropertyOf uri_rdf_Property = true % 0.83/0.98 |- ifeq (ip $P) true (iext uri_rdfs_subPropertyOf $P $P) true = true % 0.83/0.98 |- ifeq (iext uri_rdfs_subPropertyOf $Q $R) true % 0.83/0.98 (ifeq (iext uri_rdfs_subPropertyOf $P $Q) true % 0.83/0.98 (iext uri_rdfs_subPropertyOf $P $R) true) true = true % 0.83/0.98 |- iext uri_rdfs_domain uri_rdf_type uri_rdfs_Resource = true % 0.83/0.98 |- iext uri_rdfs_range uri_rdf_type uri_rdfs_Class = true % 0.83/0.98 |- iext uri_rdfs_domain uri_rdf_value uri_rdfs_Resource = true % 0.83/0.98 |- iext uri_rdfs_range uri_rdf_value uri_rdfs_Resource = true % 0.83/0.98 |- iext uri_owl_complementOf % 0.83/0.98 sK1_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_y uri_ex_A = % 0.83/0.98 true % 0.83/0.98 |- iext uri_owl_intersectionOf % 0.83/0.98 sK3_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_x % 0.83/0.98 sK4_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l1 = true % 0.83/0.98 |- iext uri_rdf_rest % 0.83/0.98 sK2_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l2 % 0.83/0.98 uri_rdf_nil = true % 0.83/0.98 |- iext uri_rdf_rest % 0.83/0.98 sK4_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l1 % 0.83/0.98 sK2_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l2 = true % 0.83/0.98 |- iext uri_rdf_first % 0.83/0.98 sK2_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l2 % 0.83/0.98 sK1_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_y = true % 0.83/0.98 |- iext uri_rdf_first % 0.83/0.98 sK4_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l1 % 0.83/0.98 uri_ex_A = true % 0.83/0.98 |- iext uri_rdf_type uri_ex_A uri_owl_Class = true % 0.83/0.98 |- iext uri_rdf_type uri_ex_B uri_owl_Class = true % 0.83/0.98 |- iext uri_rdf_type uri_ex_w % 0.83/0.98 sK3_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_x = true % 0.83/0.98 |- ~(iext uri_rdf_type uri_ex_w uri_ex_B = true) % 0.83/0.98 |- ip uri_rdf__1 = true % 0.83/0.98 |- ip uri_rdf__2 = true % 0.83/0.98 |- ip uri_rdf__3 = true % 0.83/0.98 |- ip uri_rdf_first = true % 0.83/0.98 |- ip uri_rdf_object = true % 0.83/0.98 |- ip uri_rdf_rest = true % 0.83/0.98 |- ip uri_rdf_subject = true % 0.83/0.98 |- ip uri_rdf_type = true % 0.83/0.98 |- ip uri_rdf_value = true % 0.83/0.98 |- iext uri_rdfs_subPropertyOf uri_rdf__1 uri_rdf__1 = true % 0.83/0.98 |- iext uri_rdfs_subPropertyOf uri_rdf__2 uri_rdf__2 = true % 0.83/0.98 |- iext uri_rdfs_subPropertyOf uri_rdf__3 uri_rdf__3 = true % 0.83/0.98 |- iext uri_rdfs_subPropertyOf uri_rdf_first uri_rdf_first = true % 0.83/0.98 |- iext uri_rdfs_subPropertyOf uri_rdf_object uri_rdf_object = true % 0.83/0.98 |- iext uri_rdfs_subPropertyOf uri_rdf_rest uri_rdf_rest = true % 0.83/0.98 |- iext uri_rdfs_subPropertyOf uri_rdf_subject uri_rdf_subject = true % 0.83/0.98 |- iext uri_rdfs_subPropertyOf uri_rdf_type uri_rdf_type = true % 0.83/0.98 |- iext uri_rdfs_subPropertyOf uri_rdf_value uri_rdf_value = true % 0.83/0.98 |- ic uri_rdf_Alt = true % 0.83/0.98 |- ic uri_rdf_Bag = true % 0.83/0.98 |- ic uri_rdf_XMLLiteral = true % 0.83/0.98 |- ic uri_rdfs_ContainerMembershipProperty = true % 0.83/0.98 |- ic uri_rdfs_Datatype = true % 0.83/0.98 |- ic uri_rdfs_Seq = true % 0.83/0.98 |- iext uri_rdfs_subClassOf uri_rdf_Alt uri_rdf_Alt = true % 0.83/0.98 |- iext uri_rdfs_subClassOf uri_rdf_Alt uri_rdfs_Resource = true % 0.83/0.98 |- icext uri_rdfs_Class uri_rdf_Alt = true % 0.83/0.98 |- iext uri_rdfs_subClassOf uri_rdf_Bag uri_rdf_Bag = true % 0.83/0.98 |- iext uri_rdfs_subClassOf uri_rdf_Bag uri_rdfs_Resource = true % 0.83/0.98 |- icext uri_rdfs_Class uri_rdf_Bag = true % 0.83/0.98 |- iext uri_rdfs_subClassOf uri_rdf_XMLLiteral uri_rdf_XMLLiteral = true % 0.83/0.98 |- iext uri_rdfs_subClassOf uri_rdf_XMLLiteral uri_rdfs_Resource = true % 0.83/0.99 |- icext uri_rdfs_Class uri_rdf_XMLLiteral = true % 0.83/0.99 |- iext uri_rdfs_subClassOf uri_rdfs_ContainerMembershipProperty % 0.83/0.99 uri_rdfs_ContainerMembershipProperty = true % 0.83/0.99 |- iext uri_rdfs_subClassOf uri_rdfs_ContainerMembershipProperty % 0.83/0.99 uri_rdfs_Resource = true % 0.83/0.99 |- icext uri_rdfs_Class uri_rdfs_ContainerMembershipProperty = true % 0.83/0.99 |- iext uri_rdfs_subClassOf uri_rdfs_Datatype uri_rdfs_Datatype = true % 0.83/0.99 |- iext uri_rdfs_subClassOf uri_rdfs_Datatype uri_rdfs_Resource = true % 0.83/0.99 |- icext uri_rdfs_Class uri_rdfs_Datatype = true % 0.83/0.99 |- iext uri_rdfs_subClassOf uri_rdfs_Seq uri_rdfs_Seq = true % 0.83/0.99 |- iext uri_rdfs_subClassOf uri_rdfs_Seq uri_rdfs_Resource = true % 0.83/0.99 |- icext uri_rdfs_Class uri_rdfs_Seq = true % 0.83/0.99 |- ip uri_rdfs_seeAlso = true % 0.83/0.99 |- iext uri_rdfs_subPropertyOf uri_rdfs_seeAlso uri_rdfs_seeAlso = true % 0.83/0.99 |- iext uri_rdf_type uri_rdfs_seeAlso uri_rdf_Property = true % 0.83/0.99 |- ic uri_rdfs_Container = true % 0.83/0.99 |- ic uri_rdfs_Resource = true % 0.83/0.99 |- ic uri_rdfs_Literal = true % 0.83/0.99 |- ic uri_rdf_Property = true % 0.83/0.99 |- ic uri_rdfs_Class = true % 0.83/0.99 |- iext uri_rdfs_subClassOf uri_rdfs_Container uri_rdfs_Container = true % 0.83/0.99 |- iext uri_rdfs_subClassOf uri_rdfs_Container uri_rdfs_Resource = true % 0.83/0.99 |- icext uri_rdfs_Class uri_rdfs_Container = true % 0.83/0.99 |- iext uri_rdfs_subClassOf uri_rdfs_Resource uri_rdfs_Resource = true % 0.83/0.99 |- icext uri_rdfs_Class uri_rdfs_Resource = true % 0.83/0.99 |- iext uri_rdfs_subClassOf uri_rdfs_Literal uri_rdfs_Literal = true % 0.83/0.99 |- iext uri_rdfs_subClassOf uri_rdfs_Literal uri_rdfs_Resource = true % 0.83/0.99 |- icext uri_rdfs_Class uri_rdfs_Literal = true % 0.83/0.99 |- iext uri_rdfs_subClassOf uri_rdf_Property uri_rdf_Property = true % 0.83/0.99 |- iext uri_rdfs_subClassOf uri_rdf_Property uri_rdfs_Resource = true % 0.83/0.99 |- icext uri_rdfs_Class uri_rdf_Property = true % 0.83/0.99 |- iext uri_rdfs_subClassOf uri_rdfs_Class uri_rdfs_Class = true % 0.83/0.99 |- iext uri_rdfs_subClassOf uri_rdfs_Class uri_rdfs_Resource = true % 0.83/0.99 |- icext uri_rdfs_Class uri_rdfs_Class = true % 0.83/0.99 |- ip uri_rdfs_isDefinedBy = true % 0.83/0.99 |- iext uri_rdfs_subPropertyOf uri_rdfs_isDefinedBy uri_rdfs_isDefinedBy = % 0.83/0.99 true % 0.83/0.99 |- iext uri_rdf_type uri_rdfs_isDefinedBy uri_rdf_Property = true % 0.83/0.99 |- iext uri_rdf_type uri_rdf_Alt uri_rdfs_Class = true % 0.83/0.99 |- iext uri_rdf_type uri_rdf_Bag uri_rdfs_Class = true % 0.83/0.99 |- iext uri_rdf_type uri_rdf_XMLLiteral uri_rdfs_Class = true % 0.83/0.99 |- iext uri_rdf_type uri_rdfs_Class uri_rdfs_Class = true % 0.83/0.99 |- iext uri_rdf_type uri_rdfs_Container uri_rdfs_Class = true % 0.83/0.99 |- iext uri_rdf_type uri_rdfs_ContainerMembershipProperty uri_rdfs_Class = % 0.83/0.99 true % 0.83/0.99 |- iext uri_rdf_type uri_rdfs_Datatype uri_rdfs_Class = true % 0.83/0.99 |- iext uri_rdf_type uri_rdfs_Literal uri_rdfs_Class = true % 0.83/0.99 |- iext uri_rdf_type uri_rdfs_Resource uri_rdfs_Class = true % 0.83/0.99 |- iext uri_rdf_type uri_rdfs_Seq uri_rdfs_Class = true % 0.83/0.99 |- iext uri_rdf_type $_58 uri_rdfs_Resource = true % 0.83/0.99 |- icext uri_owl_Class uri_ex_A = true % 0.83/0.99 |- icext uri_owl_Class uri_ex_B = true % 0.83/0.99 |- icext sK3_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_x % 0.83/0.99 uri_ex_w = true % 0.83/0.99 |- icext uri_rdfs_Datatype uri_rdf_XMLLiteral = true % 0.83/0.99 |- icext uri_rdf_Property uri_rdf__1 = true % 0.83/0.99 |- icext uri_rdfs_ContainerMembershipProperty uri_rdf__1 = true % 0.83/0.99 |- icext uri_rdf_Property uri_rdf__2 = true % 0.83/0.99 |- icext uri_rdfs_ContainerMembershipProperty uri_rdf__2 = true % 0.83/0.99 |- icext uri_rdf_Property uri_rdf__3 = true % 0.83/0.99 |- icext uri_rdfs_ContainerMembershipProperty uri_rdf__3 = true % 0.83/0.99 |- icext uri_rdf_Property uri_rdf_first = true % 0.83/0.99 |- icext uri_rdf_List uri_rdf_nil = true % 0.83/0.99 |- icext uri_rdf_Property uri_rdf_object = true % 0.83/0.99 |- icext uri_rdf_Property uri_rdf_rest = true % 0.83/0.99 |- icext uri_rdf_Property uri_rdf_subject = true % 0.83/0.99 |- icext uri_rdf_Property uri_rdf_type = true % 0.83/0.99 |- icext uri_rdf_Property uri_rdf_value = true % 0.83/0.99 |- icext uri_rdf_Property uri_rdfs_isDefinedBy = true % 0.83/0.99 |- icext uri_rdf_Property uri_rdfs_seeAlso = true % 0.83/0.99 |- iext uri_rdfs_subPropertyOf uri_rdf__1 uri_rdfs_member = true % 0.83/0.99 |- iext uri_rdfs_subPropertyOf uri_rdf__2 uri_rdfs_member = true % 0.83/0.99 |- iext uri_rdfs_subPropertyOf uri_rdf__3 uri_rdfs_member = true % 0.83/0.99 |- ip uri_rdfs_member = true % 0.83/0.99 |- iext uri_rdfs_subPropertyOf uri_rdfs_member uri_rdfs_member = true % 0.83/0.99 |- iext uri_rdf_type uri_rdfs_member uri_rdf_Property = true % 0.83/0.99 |- icext uri_rdf_Property uri_rdfs_member = true % 0.83/0.99 |- ifeq (iext uri_rdf__1 $_78 $_76) true true true = true % 0.83/0.99 |- ifeq (iext uri_rdf__2 $_78 $_76) true true true = true % 0.83/0.99 |- ifeq (iext uri_rdf__3 $_78 $_76) true true true = true % 0.83/0.99 |- ifeq (iext uri_rdf_first $_78 $_76) true true true = true % 0.83/0.99 |- ifeq (iext uri_rdf_object $_78 $_76) true true true = true % 0.83/0.99 |- ifeq (iext uri_rdf_rest $_78 $_76) true true true = true % 0.83/0.99 |- ifeq (iext uri_rdf_subject $_78 $_76) true true true = true % 0.83/0.99 |- ifeq (iext uri_rdf_type $_78 $_76) true true true = true % 0.83/0.99 |- ifeq (iext uri_rdf_value $_78 $_76) true true true = true % 0.83/0.99 |- ifeq (iext uri_rdfs_isDefinedBy $_78 $_76) true true true = true % 0.83/0.99 |- ifeq (iext uri_rdfs_member $_78 $_76) true true true = true % 0.83/0.99 |- ifeq (iext uri_rdfs_seeAlso $_78 $_76) true true true = true % 0.83/0.99 |- ip uri_owl_complementOf = true % 0.83/0.99 |- ip uri_owl_intersectionOf = true % 0.83/0.99 |- ip uri_rdfs_domain = true % 0.83/0.99 |- ip uri_rdfs_range = true % 0.83/0.99 |- ip uri_rdfs_subClassOf = true % 0.83/0.99 |- ip uri_rdfs_subPropertyOf = true % 0.83/0.99 |- ifeq (iext uri_owl_complementOf $S $O) true true true = true % 0.83/0.99 |- iext uri_rdfs_subPropertyOf uri_owl_complementOf uri_owl_complementOf = % 0.83/0.99 true % 0.83/0.99 |- iext uri_rdf_type uri_owl_complementOf uri_rdf_Property = true % 0.83/0.99 |- ifeq (iext uri_owl_intersectionOf $S $O) true true true = true % 0.83/0.99 |- iext uri_rdfs_subPropertyOf uri_owl_intersectionOf % 0.83/0.99 uri_owl_intersectionOf = true % 0.83/0.99 |- iext uri_rdf_type uri_owl_intersectionOf uri_rdf_Property = true % 0.83/0.99 |- ifeq (iext uri_rdfs_domain $S $O) true true true = true % 0.83/0.99 |- iext uri_rdfs_subPropertyOf uri_rdfs_domain uri_rdfs_domain = true % 0.83/0.99 |- iext uri_rdf_type uri_rdfs_domain uri_rdf_Property = true % 0.83/0.99 |- ifeq (iext uri_rdfs_range $S $O) true true true = true % 0.83/0.99 |- iext uri_rdfs_subPropertyOf uri_rdfs_range uri_rdfs_range = true % 0.83/0.99 |- iext uri_rdf_type uri_rdfs_range uri_rdf_Property = true % 0.83/0.99 |- ifeq (iext uri_rdfs_subClassOf $S $O) true true true = true % 0.83/0.99 |- iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf uri_rdfs_subClassOf = % 0.83/0.99 true % 0.83/0.99 |- iext uri_rdf_type uri_rdfs_subClassOf uri_rdf_Property = true % 0.83/0.99 |- ifeq (iext uri_rdfs_subPropertyOf $S $O) true true true = true % 0.83/0.99 |- iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf % 0.83/0.99 uri_rdfs_subPropertyOf = true % 0.83/0.99 |- iext uri_rdf_type uri_rdfs_subPropertyOf uri_rdf_Property = true % 0.83/0.99 |- icext uri_rdf_Property uri_rdfs_subPropertyOf = true % 0.83/0.99 |- icext uri_rdf_Property uri_owl_complementOf = true % 0.83/0.99 |- icext uri_rdf_Property uri_owl_intersectionOf = true % 0.83/0.99 |- icext uri_rdf_Property uri_rdfs_domain = true % 0.83/0.99 |- icext uri_rdf_Property uri_rdfs_range = true % 0.83/0.99 |- icext uri_rdf_Property uri_rdfs_subClassOf = true % 0.83/0.99 |- ifeq (icext $_115 $_117) true true true = true % 0.83/0.99 |- ifeq (icext uri_rdf_Alt $_117) true (icext uri_rdf_Alt $_117) true = % 0.83/0.99 true % 0.83/0.99 |- ifeq (icext uri_rdf_Alt $_117) true (icext uri_rdfs_Container $_117) % 0.83/0.99 true = true % 0.83/0.99 |- ifeq (icext uri_rdf_Bag $_117) true (icext uri_rdf_Bag $_117) true = % 0.83/0.99 true % 0.83/0.99 |- ifeq (icext uri_rdf_Bag $_117) true (icext uri_rdfs_Container $_117) % 0.83/0.99 true = true % 0.83/0.99 |- ifeq (icext uri_rdf_Property $_117) true (icext uri_rdf_Property $_117) % 0.83/0.99 true = true % 0.83/0.99 |- ifeq (icext uri_rdf_XMLLiteral $_117) true % 0.83/0.99 (icext uri_rdf_XMLLiteral $_117) true = true % 0.83/0.99 |- ifeq (icext uri_rdf_XMLLiteral $_117) true % 0.83/0.99 (icext uri_rdfs_Literal $_117) true = true % 0.83/0.99 |- ifeq (icext uri_rdfs_Class $_117) true (icext uri_rdfs_Class $_117) % 0.83/0.99 true = true % 0.83/0.99 |- ifeq (icext uri_rdfs_Container $_117) true % 0.83/0.99 (icext uri_rdfs_Container $_117) true = true % 0.83/0.99 |- ifeq (icext uri_rdfs_ContainerMembershipProperty $_117) true % 0.83/0.99 (icext uri_rdf_Property $_117) true = true % 0.83/0.99 |- ifeq (icext uri_rdfs_ContainerMembershipProperty $_117) true % 0.83/0.99 (icext uri_rdfs_ContainerMembershipProperty $_117) true = true % 0.83/0.99 |- ifeq (icext uri_rdfs_Datatype $_117) true (icext uri_rdfs_Class $_117) % 0.83/0.99 true = true % 0.83/0.99 |- ifeq (icext uri_rdfs_Datatype $_117) true % 0.83/0.99 (icext uri_rdfs_Datatype $_117) true = true % 0.83/0.99 |- ifeq (icext uri_rdfs_Literal $_117) true (icext uri_rdfs_Literal $_117) % 0.83/0.99 true = true % 0.83/0.99 |- ifeq (icext uri_rdfs_Seq $_117) true (icext uri_rdfs_Container $_117) % 0.83/0.99 true = true % 0.83/0.99 |- ifeq (icext uri_rdfs_Seq $_117) true (icext uri_rdfs_Seq $_117) true = % 0.83/0.99 true % 0.83/0.99 |- ifeq % 0.83/0.99 (iext uri_rdfs_subClassOf % 0.83/0.99 sK3_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_x $_116) % 0.83/0.99 true (icext $_116 uri_ex_w) true = true % 0.83/0.99 |- ifeq (iext uri_rdfs_subClassOf uri_owl_Class $_116) true % 0.83/0.99 (icext $_116 uri_ex_A) true = true % 0.83/0.99 |- ifeq (iext uri_rdfs_subClassOf uri_owl_Class $_116) true % 0.83/0.99 (icext $_116 uri_ex_B) true = true % 0.83/0.99 |- ifeq (iext uri_rdfs_subClassOf uri_rdf_List $_116) true % 0.83/0.99 (icext $_116 uri_rdf_nil) true = true % 0.83/0.99 |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $_116) true % 0.83/0.99 (icext $_116 uri_owl_complementOf) true = true % 0.83/0.99 |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $_116) true % 0.83/0.99 (icext $_116 uri_owl_intersectionOf) true = true % 0.83/0.99 |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $_116) true % 0.83/0.99 (icext $_116 uri_rdf__1) true = true % 0.83/0.99 |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $_116) true % 0.83/0.99 (icext $_116 uri_rdf__2) true = true % 0.83/0.99 |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $_116) true % 0.83/0.99 (icext $_116 uri_rdf__3) true = true % 0.83/0.99 |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $_116) true % 0.83/0.99 (icext $_116 uri_rdf_first) true = true % 0.83/0.99 |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $_116) true % 0.83/0.99 (icext $_116 uri_rdf_object) true = true % 0.83/0.99 |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $_116) true % 0.83/0.99 (icext $_116 uri_rdf_rest) true = true % 0.83/0.99 |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $_116) true % 0.83/0.99 (icext $_116 uri_rdf_subject) true = true % 0.83/0.99 |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $_116) true % 0.83/0.99 (icext $_116 uri_rdf_type) true = true % 0.83/0.99 |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $_116) true % 0.83/0.99 (icext $_116 uri_rdf_value) true = true % 0.83/0.99 |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $_116) true % 0.83/0.99 (icext $_116 uri_rdfs_domain) true = true % 0.83/0.99 |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $_116) true % 0.83/0.99 (icext $_116 uri_rdfs_isDefinedBy) true = true % 0.83/0.99 |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $_116) true % 0.83/0.99 (icext $_116 uri_rdfs_member) true = true % 0.83/0.99 |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $_116) true % 0.83/0.99 (icext $_116 uri_rdfs_range) true = true % 0.83/0.99 |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $_116) true % 0.83/0.99 (icext $_116 uri_rdfs_seeAlso) true = true % 0.83/0.99 |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $_116) true % 0.83/0.99 (icext $_116 uri_rdfs_subClassOf) true = true % 0.83/0.99 |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $_116) true % 0.83/0.99 (icext $_116 uri_rdfs_subPropertyOf) true = true % 0.83/0.99 |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Class $_116) true % 0.83/0.99 (icext $_116 uri_rdf_Alt) true = true % 0.83/0.99 |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Class $_116) true % 0.83/0.99 (icext $_116 uri_rdf_Bag) true = true % 0.83/0.99 |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Class $_116) true % 0.83/0.99 (icext $_116 uri_rdf_Property) true = true % 0.83/0.99 |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Class $_116) true % 0.83/0.99 (icext $_116 uri_rdf_XMLLiteral) true = true % 0.83/0.99 |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Class $_116) true % 0.83/0.99 (icext $_116 uri_rdfs_Class) true = true % 0.83/0.99 |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Class $_116) true % 0.83/0.99 (icext $_116 uri_rdfs_Container) true = true % 0.83/0.99 |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Class $_116) true % 0.83/0.99 (icext $_116 uri_rdfs_ContainerMembershipProperty) true = true % 0.83/0.99 |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Class $_116) true % 0.83/0.99 (icext $_116 uri_rdfs_Datatype) true = true % 0.83/0.99 |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Class $_116) true % 0.83/0.99 (icext $_116 uri_rdfs_Literal) true = true % 0.83/0.99 |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Class $_116) true % 0.83/0.99 (icext $_116 uri_rdfs_Resource) true = true % 0.83/0.99 |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Class $_116) true % 0.83/0.99 (icext $_116 uri_rdfs_Seq) true = true % 0.83/0.99 |- ifeq % 0.83/0.99 (iext uri_rdfs_subClassOf uri_rdfs_ContainerMembershipProperty $_116) % 0.83/0.99 true (icext $_116 uri_rdf__1) true = true % 0.83/0.99 |- ifeq % 0.83/0.99 (iext uri_rdfs_subClassOf uri_rdfs_ContainerMembershipProperty $_116) % 0.83/0.99 true (icext $_116 uri_rdf__2) true = true % 0.83/0.99 |- ifeq % 0.83/0.99 (iext uri_rdfs_subClassOf uri_rdfs_ContainerMembershipProperty $_116) % 0.83/0.99 true (icext $_116 uri_rdf__3) true = true % 0.83/0.99 |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Datatype $_116) true % 0.83/0.99 (icext $_116 uri_rdf_XMLLiteral) true = true % 0.83/0.99 |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Resource $_116) true % 0.83/0.99 (icext $_116 $_117) true = true % 0.83/0.99 |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Container $_177) true % 0.83/0.99 (iext uri_rdfs_subClassOf uri_rdf_Alt $_177) true = true % 0.83/0.99 |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Resource $_177) true % 0.83/0.99 (iext uri_rdfs_subClassOf uri_rdf_Alt $_177) true = true % 0.83/0.99 |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Container $_177) true % 0.83/0.99 (iext uri_rdfs_subClassOf uri_rdf_Bag $_177) true = true % 0.83/0.99 |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Resource $_177) true % 0.83/0.99 (iext uri_rdfs_subClassOf uri_rdf_Bag $_177) true = true % 0.83/0.99 |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Resource $_177) true % 0.83/0.99 (iext uri_rdfs_subClassOf uri_rdf_Property $_177) true = true % 0.83/0.99 |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Literal $_177) true % 0.83/0.99 (iext uri_rdfs_subClassOf uri_rdf_XMLLiteral $_177) true = true % 0.83/0.99 |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Resource $_177) true % 0.83/0.99 (iext uri_rdfs_subClassOf uri_rdf_XMLLiteral $_177) true = true % 0.83/1.00 |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Resource $_177) true % 0.83/1.00 (iext uri_rdfs_subClassOf uri_rdfs_Class $_177) true = true % 0.83/1.00 |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Resource $_177) true % 0.83/1.00 (iext uri_rdfs_subClassOf uri_rdfs_Container $_177) true = true % 0.83/1.00 |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $_177) true % 0.83/1.00 (iext uri_rdfs_subClassOf uri_rdfs_ContainerMembershipProperty $_177) % 0.83/1.00 true = true % 0.83/1.00 |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Resource $_177) true % 0.83/1.00 (iext uri_rdfs_subClassOf uri_rdfs_ContainerMembershipProperty $_177) % 0.83/1.00 true = true % 0.83/1.00 |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Class $_177) true % 0.83/1.00 (iext uri_rdfs_subClassOf uri_rdfs_Datatype $_177) true = true % 0.83/1.00 |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Resource $_177) true % 0.83/1.00 (iext uri_rdfs_subClassOf uri_rdfs_Datatype $_177) true = true % 0.83/1.00 |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Resource $_177) true % 0.83/1.00 (iext uri_rdfs_subClassOf uri_rdfs_Literal $_177) true = true % 0.83/1.00 |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Container $_177) true % 0.83/1.00 (iext uri_rdfs_subClassOf uri_rdfs_Seq $_177) true = true % 0.83/1.00 |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Resource $_177) true % 0.83/1.00 (iext uri_rdfs_subClassOf uri_rdfs_Seq $_177) true = true % 0.83/1.00 |- ifeq (iext uri_rdfs_subClassOf $_175 uri_rdf_Alt) true % 0.83/1.00 (iext uri_rdfs_subClassOf $_175 uri_rdfs_Container) true = true % 0.83/1.00 |- ifeq (iext uri_rdfs_subClassOf $_175 uri_rdf_Alt) true % 0.83/1.00 (iext uri_rdfs_subClassOf $_175 uri_rdfs_Resource) true = true % 0.83/1.00 |- ifeq (iext uri_rdfs_subClassOf $_175 uri_rdf_Bag) true % 0.83/1.00 (iext uri_rdfs_subClassOf $_175 uri_rdfs_Container) true = true % 0.83/1.00 |- ifeq (iext uri_rdfs_subClassOf $_175 uri_rdf_Bag) true % 0.83/1.00 (iext uri_rdfs_subClassOf $_175 uri_rdfs_Resource) true = true % 0.83/1.00 |- ifeq (iext uri_rdfs_subClassOf $_175 uri_rdf_Property) true % 0.83/1.00 (iext uri_rdfs_subClassOf $_175 uri_rdfs_Resource) true = true % 0.83/1.00 |- ifeq (iext uri_rdfs_subClassOf $_175 uri_rdf_XMLLiteral) true % 0.83/1.00 (iext uri_rdfs_subClassOf $_175 uri_rdfs_Literal) true = true % 0.83/1.00 |- ifeq (iext uri_rdfs_subClassOf $_175 uri_rdf_XMLLiteral) true % 0.83/1.00 (iext uri_rdfs_subClassOf $_175 uri_rdfs_Resource) true = true % 0.83/1.00 |- ifeq (iext uri_rdfs_subClassOf $_175 uri_rdfs_Class) true % 0.83/1.00 (iext uri_rdfs_subClassOf $_175 uri_rdfs_Resource) true = true % 0.83/1.00 |- ifeq (iext uri_rdfs_subClassOf $_175 uri_rdfs_Container) true % 0.83/1.00 (iext uri_rdfs_subClassOf $_175 uri_rdfs_Resource) true = true % 0.83/1.00 |- ifeq % 0.83/1.00 (iext uri_rdfs_subClassOf $_175 uri_rdfs_ContainerMembershipProperty) % 0.83/1.00 true (iext uri_rdfs_subClassOf $_175 uri_rdf_Property) true = true % 0.83/1.00 |- ifeq % 0.83/1.00 (iext uri_rdfs_subClassOf $_175 uri_rdfs_ContainerMembershipProperty) % 0.83/1.00 true (iext uri_rdfs_subClassOf $_175 uri_rdfs_Resource) true = true % 0.83/1.00 |- ifeq (iext uri_rdfs_subClassOf $_175 uri_rdfs_Datatype) true % 0.83/1.00 (iext uri_rdfs_subClassOf $_175 uri_rdfs_Class) true = true % 0.83/1.00 |- ifeq (iext uri_rdfs_subClassOf $_175 uri_rdfs_Datatype) true % 0.83/1.00 (iext uri_rdfs_subClassOf $_175 uri_rdfs_Resource) true = true % 0.83/1.00 |- ifeq (iext uri_rdfs_subClassOf $_175 uri_rdfs_Literal) true % 0.83/1.00 (iext uri_rdfs_subClassOf $_175 uri_rdfs_Resource) true = true % 0.83/1.00 |- ifeq (iext uri_rdfs_subClassOf $_175 uri_rdfs_Seq) true % 0.83/1.00 (iext uri_rdfs_subClassOf $_175 uri_rdfs_Container) true = true % 0.83/1.00 |- ifeq (iext uri_rdfs_subClassOf $_175 uri_rdfs_Seq) true % 0.83/1.00 (iext uri_rdfs_subClassOf $_175 uri_rdfs_Resource) true = true % 0.83/1.00 |- ifeq % 0.83/1.00 (iext uri_rdfs_domain $_233 % 0.83/1.00 sK3_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_x) true % 0.83/1.00 (ifeq (iext $_233 uri_ex_w $_235) true true true) true = true % 0.83/1.00 |- ifeq (iext uri_rdfs_domain $_233 uri_owl_Class) true % 0.83/1.00 (ifeq (iext $_233 uri_ex_A $_235) true true true) true = true % 0.83/1.00 |- ifeq (iext uri_rdfs_domain $_233 uri_owl_Class) true % 0.83/1.00 (ifeq (iext $_233 uri_ex_B $_235) true true true) true = true % 0.83/1.00 |- ifeq (iext uri_rdfs_domain $_233 uri_rdf_List) true % 0.83/1.00 (ifeq (iext $_233 uri_rdf_nil $_235) true true true) true = true % 0.83/1.00 |- ifeq (iext uri_rdfs_domain $_233 uri_rdf_Property) true % 0.83/1.00 (ifeq (iext $_233 uri_owl_complementOf $_235) true true true) true = % 0.83/1.00 true % 0.83/1.00 |- ifeq (iext uri_rdfs_domain $_233 uri_rdf_Property) true % 0.83/1.00 (ifeq (iext $_233 uri_owl_intersectionOf $_235) true true true) true = % 0.83/1.00 true % 0.83/1.00 |- ifeq (iext uri_rdfs_domain $_233 uri_rdf_Property) true % 0.83/1.00 (ifeq (iext $_233 uri_rdf__1 $_235) true true true) true = true % 0.83/1.00 |- ifeq (iext uri_rdfs_domain $_233 uri_rdf_Property) true % 0.83/1.00 (ifeq (iext $_233 uri_rdf__2 $_235) true true true) true = true % 0.83/1.00 |- ifeq (iext uri_rdfs_domain $_233 uri_rdf_Property) true % 0.83/1.00 (ifeq (iext $_233 uri_rdf__3 $_235) true true true) true = true % 0.83/1.00 |- ifeq (iext uri_rdfs_domain $_233 uri_rdf_Property) true % 0.83/1.00 (ifeq (iext $_233 uri_rdf_first $_235) true true true) true = true % 0.83/1.00 |- ifeq (iext uri_rdfs_domain $_233 uri_rdf_Property) true % 0.83/1.00 (ifeq (iext $_233 uri_rdf_object $_235) true true true) true = true % 0.83/1.00 |- ifeq (iext uri_rdfs_domain $_233 uri_rdf_Property) true % 0.83/1.00 (ifeq (iext $_233 uri_rdf_rest $_235) true true true) true = true % 0.83/1.00 |- ifeq (iext uri_rdfs_domain $_233 uri_rdf_Property) true % 0.83/1.00 (ifeq (iext $_233 uri_rdf_subject $_235) true true true) true = true % 0.83/1.00 |- ifeq (iext uri_rdfs_domain $_233 uri_rdf_Property) true % 0.83/1.00 (ifeq (iext $_233 uri_rdf_type $_235) true true true) true = true % 0.83/1.00 |- ifeq (iext uri_rdfs_domain $_233 uri_rdf_Property) true % 0.83/1.00 (ifeq (iext $_233 uri_rdf_value $_235) true true true) true = true % 0.83/1.00 |- ifeq (iext uri_rdfs_domain $_233 uri_rdf_Property) true % 0.83/1.00 (ifeq (iext $_233 uri_rdfs_domain $_235) true true true) true = true % 0.83/1.00 |- ifeq (iext uri_rdfs_domain $_233 uri_rdf_Property) true % 0.83/1.00 (ifeq (iext $_233 uri_rdfs_isDefinedBy $_235) true true true) true = % 0.83/1.00 true % 0.83/1.00 |- ifeq (iext uri_rdfs_domain $_233 uri_rdf_Property) true % 0.83/1.00 (ifeq (iext $_233 uri_rdfs_member $_235) true true true) true = true % 0.83/1.00 |- ifeq (iext uri_rdfs_domain $_233 uri_rdf_Property) true % 0.83/1.00 (ifeq (iext $_233 uri_rdfs_range $_235) true true true) true = true % 0.83/1.00 |- ifeq (iext uri_rdfs_domain $_233 uri_rdf_Property) true % 0.83/1.00 (ifeq (iext $_233 uri_rdfs_seeAlso $_235) true true true) true = true % 0.83/1.00 |- ifeq (iext uri_rdfs_domain $_233 uri_rdf_Property) true % 0.83/1.00 (ifeq (iext $_233 uri_rdfs_subClassOf $_235) true true true) true = % 0.83/1.00 true % 0.83/1.00 |- ifeq (iext uri_rdfs_domain $_233 uri_rdf_Property) true % 0.83/1.00 (ifeq (iext $_233 uri_rdfs_subPropertyOf $_235) true true true) true = % 0.83/1.00 true % 0.83/1.00 |- ifeq (iext uri_rdfs_domain $_233 uri_rdfs_Class) true % 0.83/1.00 (ifeq (iext $_233 uri_rdf_Alt $_235) true true true) true = true % 0.83/1.00 |- ifeq (iext uri_rdfs_domain $_233 uri_rdfs_Class) true % 0.83/1.00 (ifeq (iext $_233 uri_rdf_Bag $_235) true true true) true = true % 0.83/1.00 |- ifeq (iext uri_rdfs_domain $_233 uri_rdfs_Class) true % 0.83/1.00 (ifeq (iext $_233 uri_rdf_Property $_235) true true true) true = true % 0.83/1.00 |- ifeq (iext uri_rdfs_domain $_233 uri_rdfs_Class) true % 0.83/1.00 (ifeq (iext $_233 uri_rdf_XMLLiteral $_235) true true true) true = % 0.83/1.00 true % 0.83/1.00 |- ifeq (iext uri_rdfs_domain $_233 uri_rdfs_Class) true % 0.83/1.00 (ifeq (iext $_233 uri_rdfs_Class $_235) true true true) true = true % 0.83/1.00 |- ifeq (iext uri_rdfs_domain $_233 uri_rdfs_Class) true % 0.83/1.00 (ifeq (iext $_233 uri_rdfs_Container $_235) true true true) true = % 0.83/1.00 true % 0.83/1.00 |- ifeq (iext uri_rdfs_domain $_233 uri_rdfs_Class) true % 0.83/1.00 (ifeq (iext $_233 uri_rdfs_ContainerMembershipProperty $_235) true % 0.83/1.00 true true) true = true % 0.83/1.00 |- ifeq (iext uri_rdfs_domain $_233 uri_rdfs_Class) true % 0.83/1.00 (ifeq (iext $_233 uri_rdfs_Datatype $_235) true true true) true = true % 0.83/1.00 |- ifeq (iext uri_rdfs_domain $_233 uri_rdfs_Class) true % 0.83/1.00 (ifeq (iext $_233 uri_rdfs_Literal $_235) true true true) true = true % 0.83/1.00 |- ifeq (iext uri_rdfs_domain $_233 uri_rdfs_Class) true % 0.83/1.00 (ifeq (iext $_233 uri_rdfs_Resource $_235) true true true) true = true % 0.83/1.00 |- ifeq (iext uri_rdfs_domain $_233 uri_rdfs_Class) true % 0.83/1.00 (ifeq (iext $_233 uri_rdfs_Seq $_235) true true true) true = true % 0.83/1.00 |- ifeq (iext uri_rdfs_domain $_233 uri_rdfs_ContainerMembershipProperty) % 0.83/1.00 true (ifeq (iext $_233 uri_rdf__1 $_235) true true true) true = true % 0.83/1.00 |- ifeq (iext uri_rdfs_domain $_233 uri_rdfs_ContainerMembershipProperty) % 0.83/1.00 true (ifeq (iext $_233 uri_rdf__2 $_235) true true true) true = true % 0.83/1.00 |- ifeq (iext uri_rdfs_domain $_233 uri_rdfs_ContainerMembershipProperty) % 0.83/1.00 true (ifeq (iext $_233 uri_rdf__3 $_235) true true true) true = true % 0.83/1.00 |- ifeq (iext uri_rdfs_domain $_233 uri_rdfs_Datatype) true % 0.83/1.00 (ifeq (iext $_233 uri_rdf_XMLLiteral $_235) true true true) true = % 0.83/1.00 true % 0.83/1.00 |- ifeq (iext uri_rdfs_domain $_233 uri_rdfs_Resource) true % 0.83/1.00 (ifeq (iext $_233 $_234 $_235) true true true) true = true % 0.83/1.00 |- ifeq (iext uri_rdfs_domain uri_owl_complementOf $_232) true % 0.83/1.00 (icext $_232 % 0.83/1.00 sK1_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_y) true = % 0.83/1.00 true % 0.83/1.00 |- ifeq (iext uri_rdfs_domain uri_owl_intersectionOf $_232) true % 0.83/1.00 (icext $_232 % 0.83/1.00 sK3_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_x) true = % 0.83/1.00 true % 0.83/1.00 |- ifeq (iext uri_rdfs_domain uri_rdf_first $_232) true % 0.83/1.00 (icext $_232 % 0.83/1.00 sK2_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l2) % 0.83/1.00 true = true % 0.83/1.00 |- ifeq (iext uri_rdfs_domain uri_rdf_first $_232) true % 0.83/1.00 (icext $_232 % 0.83/1.00 sK4_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l1) % 0.83/1.00 true = true % 0.83/1.00 |- ifeq (iext uri_rdfs_domain uri_rdf_rest $_232) true % 0.83/1.00 (icext $_232 % 0.83/1.00 sK2_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l2) % 0.83/1.00 true = true % 0.83/1.00 |- ifeq (iext uri_rdfs_domain uri_rdf_rest $_232) true % 0.83/1.00 (icext $_232 % 0.83/1.00 sK4_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l1) % 0.83/1.00 true = true % 0.83/1.00 |- ifeq (iext uri_rdfs_domain uri_rdf_type $_232) true (icext $_232 $_234) % 0.83/1.00 true = true % 0.83/1.00 |- ifeq (iext uri_rdfs_domain uri_rdfs_domain $_232) true % 0.83/1.00 (icext $_232 uri_rdf__1) true = true % 0.83/1.00 |- ifeq (iext uri_rdfs_domain uri_rdfs_domain $_232) true % 0.83/1.00 (icext $_232 uri_rdf__2) true = true % 0.83/1.00 |- ifeq (iext uri_rdfs_domain uri_rdfs_domain $_232) true % 0.83/1.00 (icext $_232 uri_rdf__3) true = true % 0.83/1.00 |- ifeq (iext uri_rdfs_domain uri_rdfs_domain $_232) true % 0.83/1.00 (icext $_232 uri_rdf_first) true = true % 0.83/1.00 |- ifeq (iext uri_rdfs_domain uri_rdfs_domain $_232) true % 0.83/1.00 (icext $_232 uri_rdf_object) true = true % 0.83/1.00 |- ifeq (iext uri_rdfs_domain uri_rdfs_domain $_232) true % 0.83/1.00 (icext $_232 uri_rdf_predicate) true = true % 0.83/1.00 |- ifeq (iext uri_rdfs_domain uri_rdfs_domain $_232) true % 0.83/1.00 (icext $_232 uri_rdf_rest) true = true % 0.83/1.00 |- ifeq (iext uri_rdfs_domain uri_rdfs_domain $_232) true % 0.83/1.00 (icext $_232 uri_rdf_subject) true = true % 0.83/1.00 |- ifeq (iext uri_rdfs_domain uri_rdfs_domain $_232) true % 0.83/1.00 (icext $_232 uri_rdf_type) true = true % 0.83/1.00 |- ifeq (iext uri_rdfs_domain uri_rdfs_domain $_232) true % 0.83/1.00 (icext $_232 uri_rdf_value) true = true % 0.83/1.00 |- ifeq (iext uri_rdfs_domain uri_rdfs_domain $_232) true % 0.83/1.00 (icext $_232 uri_rdfs_comment) true = true % 0.83/1.00 |- ifeq (iext uri_rdfs_domain uri_rdfs_domain $_232) true % 0.83/1.00 (icext $_232 uri_rdfs_domain) true = true % 0.83/1.00 |- ifeq (iext uri_rdfs_domain uri_rdfs_domain $_232) true % 0.83/1.00 (icext $_232 uri_rdfs_isDefinedBy) true = true % 0.83/1.00 |- ifeq (iext uri_rdfs_domain uri_rdfs_domain $_232) true % 0.83/1.00 (icext $_232 uri_rdfs_label) true = true % 0.83/1.00 |- ifeq (iext uri_rdfs_domain uri_rdfs_domain $_232) true % 0.83/1.00 (icext $_232 uri_rdfs_member) true = true % 0.83/1.00 |- ifeq (iext uri_rdfs_domain uri_rdfs_domain $_232) true % 0.83/1.00 (icext $_232 uri_rdfs_range) true = true % 0.83/1.00 |- ifeq (iext uri_rdfs_domain uri_rdfs_domain $_232) true % 0.83/1.00 (icext $_232 uri_rdfs_seeAlso) true = true % 0.83/1.00 |- ifeq (iext uri_rdfs_domain uri_rdfs_domain $_232) true % 0.83/1.00 (icext $_232 uri_rdfs_subClassOf) true = true % 0.83/1.00 |- ifeq (iext uri_rdfs_domain uri_rdfs_domain $_232) true % 0.83/1.00 (icext $_232 uri_rdfs_subPropertyOf) true = true % 0.83/1.00 |- ifeq (iext uri_rdfs_domain uri_rdfs_range $_232) true % 0.83/1.00 (icext $_232 uri_rdf__1) true = true % 0.83/1.00 |- ifeq (iext uri_rdfs_domain uri_rdfs_range $_232) true % 0.83/1.00 (icext $_232 uri_rdf__2) true = true % 0.83/1.00 |- ifeq (iext uri_rdfs_domain uri_rdfs_range $_232) true % 0.83/1.00 (icext $_232 uri_rdf__3) true = true % 0.83/1.00 |- ifeq (iext uri_rdfs_domain uri_rdfs_range $_232) true % 0.83/1.00 (icext $_232 uri_rdf_first) true = true % 0.83/1.00 |- ifeq (iext uri_rdfs_domain uri_rdfs_range $_232) true % 0.83/1.00 (icext $_232 uri_rdf_predicate) true = true % 0.83/1.00 |- ifeq (iext uri_rdfs_domain uri_rdfs_range $_232) true % 0.83/1.00 (icext $_232 uri_rdf_rest) true = true % 0.83/1.00 |- ifeq (iext uri_rdfs_domain uri_rdfs_range $_232) true % 0.83/1.00 (icext $_232 uri_rdf_subject) true = true % 0.83/1.00 |- ifeq (iext uri_rdfs_domain uri_rdfs_range $_232) true % 0.83/1.00 (icext $_232 uri_rdf_type) true = true % 0.83/1.00 |- ifeq (iext uri_rdfs_domain uri_rdfs_range $_232) true % 0.83/1.00 (icext $_232 uri_rdf_value) true = true % 0.83/1.00 |- ifeq (iext uri_rdfs_domain uri_rdfs_range $_232) true % 0.83/1.00 (icext $_232 uri_rdfs_comment) true = true % 0.83/1.00 |- ifeq (iext uri_rdfs_domain uri_rdfs_range $_232) true % 0.83/1.00 (icext $_232 uri_rdfs_domain) true = true % 0.83/1.00 |- ifeq (iext uri_rdfs_domain uri_rdfs_range $_232) true % 0.83/1.00 (icext $_232 uri_rdfs_isDefinedBy) true = true % 0.83/1.00 |- ifeq (iext uri_rdfs_domain uri_rdfs_range $_232) true % 0.83/1.00 (icext $_232 uri_rdfs_label) true = true % 0.83/1.00 |- ifeq (iext uri_rdfs_domain uri_rdfs_range $_232) true % 0.83/1.00 (icext $_232 uri_rdfs_member) true = true % 0.83/1.00 |- ifeq (iext uri_rdfs_domain uri_rdfs_range $_232) true % 0.83/1.00 (icext $_232 uri_rdfs_range) true = true % 0.83/1.00 |- ifeq (iext uri_rdfs_domain uri_rdfs_range $_232) true % 0.83/1.00 (icext $_232 uri_rdfs_seeAlso) true = true % 0.83/1.00 |- ifeq (iext uri_rdfs_domain uri_rdfs_range $_232) true % 0.83/1.00 (icext $_232 uri_rdfs_subClassOf) true = true % 0.83/1.00 |- ifeq (iext uri_rdfs_domain uri_rdfs_range $_232) true % 0.83/1.00 (icext $_232 uri_rdfs_subPropertyOf) true = true % 0.83/1.00 |- ifeq (iext uri_rdfs_domain uri_rdfs_subClassOf $_232) true % 0.83/1.00 (icext $_232 uri_rdf_Alt) true = true % 0.83/1.00 |- ifeq (iext uri_rdfs_domain uri_rdfs_subClassOf $_232) true % 0.83/1.00 (icext $_232 uri_rdf_Bag) true = true % 0.83/1.00 |- ifeq (iext uri_rdfs_domain uri_rdfs_subClassOf $_232) true % 0.83/1.00 (icext $_232 uri_rdf_Property) true = true % 0.83/1.00 |- ifeq (iext uri_rdfs_domain uri_rdfs_subClassOf $_232) true % 0.83/1.00 (icext $_232 uri_rdf_XMLLiteral) true = true % 0.83/1.00 |- ifeq (iext uri_rdfs_domain uri_rdfs_subClassOf $_232) true % 0.83/1.00 (icext $_232 uri_rdfs_Class) true = true % 0.83/1.00 |- ifeq (iext uri_rdfs_domain uri_rdfs_subClassOf $_232) true % 0.83/1.00 (icext $_232 uri_rdfs_Container) true = true % 0.83/1.00 |- ifeq (iext uri_rdfs_domain uri_rdfs_subClassOf $_232) true % 0.83/1.00 (icext $_232 uri_rdfs_ContainerMembershipProperty) true = true % 0.83/1.00 |- ifeq (iext uri_rdfs_domain uri_rdfs_subClassOf $_232) true % 0.83/1.00 (icext $_232 uri_rdfs_Datatype) true = true % 0.83/1.00 |- ifeq (iext uri_rdfs_domain uri_rdfs_subClassOf $_232) true % 0.83/1.00 (icext $_232 uri_rdfs_Literal) true = true % 0.83/1.00 |- ifeq (iext uri_rdfs_domain uri_rdfs_subClassOf $_232) true % 0.83/1.00 (icext $_232 uri_rdfs_Resource) true = true % 0.83/1.00 |- ifeq (iext uri_rdfs_domain uri_rdfs_subClassOf $_232) true % 0.83/1.00 (icext $_232 uri_rdfs_Seq) true = true % 0.83/1.00 |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $_232) true % 0.83/1.00 (icext $_232 uri_owl_complementOf) true = true % 0.83/1.00 |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $_232) true % 0.83/1.00 (icext $_232 uri_owl_intersectionOf) true = true % 0.83/1.00 |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $_232) true % 0.83/1.00 (icext $_232 uri_rdf__1) true = true % 0.83/1.00 |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $_232) true % 0.83/1.00 (icext $_232 uri_rdf__2) true = true % 0.83/1.00 |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $_232) true % 0.83/1.00 (icext $_232 uri_rdf__3) true = true % 0.83/1.00 |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $_232) true % 0.83/1.00 (icext $_232 uri_rdf_first) true = true % 0.83/1.00 |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $_232) true % 0.83/1.00 (icext $_232 uri_rdf_object) true = true % 0.83/1.00 |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $_232) true % 0.83/1.00 (icext $_232 uri_rdf_rest) true = true % 0.83/1.00 |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $_232) true % 0.83/1.00 (icext $_232 uri_rdf_subject) true = true % 0.83/1.00 |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $_232) true % 0.83/1.00 (icext $_232 uri_rdf_type) true = true % 0.83/1.00 |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $_232) true % 0.83/1.00 (icext $_232 uri_rdf_value) true = true % 0.83/1.00 |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $_232) true % 0.83/1.00 (icext $_232 uri_rdfs_domain) true = true % 0.83/1.00 |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $_232) true % 0.83/1.00 (icext $_232 uri_rdfs_isDefinedBy) true = true % 0.83/1.00 |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $_232) true % 0.83/1.00 (icext $_232 uri_rdfs_member) true = true % 0.83/1.00 |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $_232) true % 0.83/1.00 (icext $_232 uri_rdfs_range) true = true % 0.83/1.00 |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $_232) true % 0.83/1.00 (icext $_232 uri_rdfs_seeAlso) true = true % 0.83/1.00 |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $_232) true % 0.83/1.00 (icext $_232 uri_rdfs_subClassOf) true = true % 0.83/1.00 |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $_232) true % 0.83/1.00 (icext $_232 uri_rdfs_subPropertyOf) true = true % 0.83/1.00 |- ifeq (iext uri_rdf_first $_234 $_235) true (icext uri_rdf_List $_234) % 0.83/1.00 true = true % 0.83/1.00 |- ifeq (iext uri_rdf_object $_234 $_235) true % 0.83/1.00 (icext uri_rdfs_Statement $_234) true = true % 0.83/1.00 |- ifeq (iext uri_rdf_predicate $_234 $_235) true % 0.83/1.00 (icext uri_rdfs_Statement $_234) true = true % 0.83/1.00 |- ifeq (iext uri_rdf_rest $_234 $_235) true (icext uri_rdf_List $_234) % 0.83/1.00 true = true % 0.83/1.01 |- ifeq (iext uri_rdf_subject $_234 $_235) true % 0.83/1.01 (icext uri_rdfs_Statement $_234) true = true % 0.83/1.01 |- ifeq (iext uri_rdfs_comment $_234 $_235) true true true = true % 0.83/1.01 |- ifeq (iext uri_rdfs_domain $_234 $_235) true % 0.83/1.01 (icext uri_rdf_Property $_234) true = true % 0.83/1.01 |- ifeq (iext uri_rdfs_label $_234 $_235) true true true = true % 0.83/1.01 |- ifeq (iext uri_rdfs_range $_234 $_235) true % 0.83/1.01 (icext uri_rdf_Property $_234) true = true % 0.83/1.01 |- ifeq (iext uri_rdfs_subClassOf $_234 $_235) true % 0.83/1.01 (icext uri_rdfs_Class $_234) true = true % 0.83/1.01 |- ifeq (iext uri_rdfs_subPropertyOf $_234 $_235) true % 0.83/1.01 (icext uri_rdf_Property $_234) true = true % 0.83/1.01 |- icext uri_rdf_List % 0.83/1.01 sK2_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l2 = true % 0.83/1.01 |- ifeq (iext uri_rdfs_domain $P uri_rdf_List) true % 0.83/1.01 (ifeq % 0.83/1.01 (iext $P % 0.83/1.01 sK2_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l2 $Y) % 0.83/1.01 true true true) true = true % 0.83/1.01 |- ifeq (iext uri_rdfs_subClassOf uri_rdf_List $D) true % 0.83/1.01 (icext $D % 0.83/1.01 sK2_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l2) % 0.83/1.01 true = true % 0.83/1.01 |- iext uri_rdf_type % 0.83/1.01 sK2_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l2 % 0.83/1.01 uri_rdf_List = true % 0.83/1.01 |- icext uri_rdf_List % 0.83/1.01 sK4_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l1 = true % 0.83/1.01 |- ifeq (iext uri_rdfs_domain $P uri_rdf_List) true % 0.83/1.01 (ifeq % 0.83/1.01 (iext $P % 0.83/1.01 sK4_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l1 $Y) % 0.83/1.01 true true true) true = true % 0.83/1.01 |- ifeq (iext uri_rdfs_subClassOf uri_rdf_List $D) true % 0.83/1.01 (icext $D % 0.83/1.01 sK4_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l1) % 0.83/1.01 true = true % 0.83/1.01 |- iext uri_rdf_type % 0.83/1.01 sK4_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l1 % 0.83/1.01 uri_rdf_List = true % 0.83/1.01 |- icext uri_rdf_Property uri_rdf_predicate = true % 0.83/1.01 |- ifeq (iext uri_rdfs_domain $P uri_rdf_Property) true % 0.83/1.01 (ifeq (iext $P uri_rdf_predicate $Y) true true true) true = true % 0.83/1.01 |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $D) true % 0.83/1.01 (icext $D uri_rdf_predicate) true = true % 0.83/1.01 |- iext uri_rdf_type uri_rdf_predicate uri_rdf_Property = true % 0.83/1.01 |- ip uri_rdf_predicate = true % 0.83/1.01 |- ifeq (iext uri_rdf_predicate $S $O) true true true = true % 0.83/1.01 |- iext uri_rdfs_subPropertyOf uri_rdf_predicate uri_rdf_predicate = true % 0.83/1.01 |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $C) true % 0.83/1.01 (icext $C uri_rdf_predicate) true = true % 0.83/1.01 |- icext uri_rdf_Property uri_rdfs_comment = true % 0.83/1.01 |- ifeq (iext uri_rdfs_domain $P uri_rdf_Property) true % 0.83/1.01 (ifeq (iext $P uri_rdfs_comment $Y) true true true) true = true % 0.83/1.01 |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $D) true % 0.83/1.01 (icext $D uri_rdfs_comment) true = true % 0.83/1.01 |- iext uri_rdf_type uri_rdfs_comment uri_rdf_Property = true % 0.83/1.01 |- ip uri_rdfs_comment = true % 0.83/1.01 |- iext uri_rdfs_subPropertyOf uri_rdfs_comment uri_rdfs_comment = true % 0.83/1.01 |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $C) true % 0.83/1.01 (icext $C uri_rdfs_comment) true = true % 0.83/1.01 |- icext uri_rdf_Property uri_rdfs_label = true % 0.83/1.01 |- ifeq (iext uri_rdfs_domain $P uri_rdf_Property) true % 0.83/1.01 (ifeq (iext $P uri_rdfs_label $Y) true true true) true = true % 0.83/1.01 |- ifeq (iext uri_rdfs_subClassOf uri_rdf_Property $D) true % 0.83/1.01 (icext $D uri_rdfs_label) true = true % 0.83/1.01 |- iext uri_rdf_type uri_rdfs_label uri_rdf_Property = true % 0.83/1.01 |- ip uri_rdfs_label = true % 0.83/1.01 |- iext uri_rdfs_subPropertyOf uri_rdfs_label uri_rdfs_label = true % 0.83/1.01 |- ifeq (iext uri_rdfs_domain uri_rdfs_subPropertyOf $C) true % 0.83/1.01 (icext $C uri_rdfs_label) true = true % 0.83/1.01 |- ifeq % 0.83/1.01 (iext uri_rdfs_range $_343 % 0.83/1.01 sK3_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_x) true % 0.83/1.01 (ifeq (iext $_343 $_344 uri_ex_w) true true true) true = true % 0.83/1.01 |- ifeq (iext uri_rdfs_range $_343 uri_owl_Class) true % 0.83/1.01 (ifeq (iext $_343 $_344 uri_ex_A) true true true) true = true % 0.83/1.01 |- ifeq (iext uri_rdfs_range $_343 uri_owl_Class) true % 0.83/1.01 (ifeq (iext $_343 $_344 uri_ex_B) true true true) true = true % 0.83/1.01 |- ifeq (iext uri_rdfs_range $_343 uri_rdf_List) true % 0.83/1.01 (ifeq % 0.83/1.01 (iext $_343 $_344 % 0.83/1.01 sK2_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l2) % 0.83/1.01 true true true) true = true % 0.83/1.01 |- ifeq (iext uri_rdfs_range $_343 uri_rdf_List) true % 0.83/1.01 (ifeq % 0.83/1.01 (iext $_343 $_344 % 0.83/1.01 sK4_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l1) % 0.83/1.01 true true true) true = true % 0.83/1.01 |- ifeq (iext uri_rdfs_range $_343 uri_rdf_List) true % 0.83/1.01 (ifeq (iext $_343 $_344 uri_rdf_nil) true true true) true = true % 0.83/1.01 |- ifeq (iext uri_rdfs_range $_343 uri_rdf_Property) true % 0.83/1.01 (ifeq (iext $_343 $_344 uri_owl_complementOf) true true true) true = % 0.83/1.01 true % 0.83/1.01 |- ifeq (iext uri_rdfs_range $_343 uri_rdf_Property) true % 0.83/1.01 (ifeq (iext $_343 $_344 uri_owl_intersectionOf) true true true) true = % 0.83/1.01 true % 0.83/1.01 |- ifeq (iext uri_rdfs_range $_343 uri_rdf_Property) true % 0.83/1.01 (ifeq (iext $_343 $_344 uri_rdf__1) true true true) true = true % 0.83/1.01 |- ifeq (iext uri_rdfs_range $_343 uri_rdf_Property) true % 0.83/1.01 (ifeq (iext $_343 $_344 uri_rdf__2) true true true) true = true % 0.83/1.01 |- ifeq (iext uri_rdfs_range $_343 uri_rdf_Property) true % 0.83/1.01 (ifeq (iext $_343 $_344 uri_rdf__3) true true true) true = true % 0.83/1.01 |- ifeq (iext uri_rdfs_range $_343 uri_rdf_Property) true % 0.83/1.01 (ifeq (iext $_343 $_344 uri_rdf_first) true true true) true = true % 0.83/1.01 |- ifeq (iext uri_rdfs_range $_343 uri_rdf_Property) true % 0.83/1.01 (ifeq (iext $_343 $_344 uri_rdf_object) true true true) true = true % 0.83/1.01 |- ifeq (iext uri_rdfs_range $_343 uri_rdf_Property) true % 0.83/1.01 (ifeq (iext $_343 $_344 uri_rdf_predicate) true true true) true = true % 0.83/1.01 |- ifeq (iext uri_rdfs_range $_343 uri_rdf_Property) true % 0.83/1.01 (ifeq (iext $_343 $_344 uri_rdf_rest) true true true) true = true % 0.83/1.01 |- ifeq (iext uri_rdfs_range $_343 uri_rdf_Property) true % 0.83/1.01 (ifeq (iext $_343 $_344 uri_rdf_subject) true true true) true = true % 0.83/1.01 |- ifeq (iext uri_rdfs_range $_343 uri_rdf_Property) true % 0.83/1.01 (ifeq (iext $_343 $_344 uri_rdf_type) true true true) true = true % 0.83/1.01 |- ifeq (iext uri_rdfs_range $_343 uri_rdf_Property) true % 0.83/1.01 (ifeq (iext $_343 $_344 uri_rdf_value) true true true) true = true % 0.83/1.01 |- ifeq (iext uri_rdfs_range $_343 uri_rdf_Property) true % 0.83/1.01 (ifeq (iext $_343 $_344 uri_rdfs_comment) true true true) true = true % 0.83/1.01 |- ifeq (iext uri_rdfs_range $_343 uri_rdf_Property) true % 0.83/1.01 (ifeq (iext $_343 $_344 uri_rdfs_domain) true true true) true = true % 0.83/1.01 |- ifeq (iext uri_rdfs_range $_343 uri_rdf_Property) true % 0.83/1.01 (ifeq (iext $_343 $_344 uri_rdfs_isDefinedBy) true true true) true = % 0.83/1.01 true % 0.83/1.01 |- ifeq (iext uri_rdfs_range $_343 uri_rdf_Property) true % 0.83/1.01 (ifeq (iext $_343 $_344 uri_rdfs_label) true true true) true = true % 0.83/1.01 |- ifeq (iext uri_rdfs_range $_343 uri_rdf_Property) true % 0.83/1.01 (ifeq (iext $_343 $_344 uri_rdfs_member) true true true) true = true % 0.83/1.01 |- ifeq (iext uri_rdfs_range $_343 uri_rdf_Property) true % 0.83/1.01 (ifeq (iext $_343 $_344 uri_rdfs_range) true true true) true = true % 0.83/1.01 |- ifeq (iext uri_rdfs_range $_343 uri_rdf_Property) true % 0.83/1.01 (ifeq (iext $_343 $_344 uri_rdfs_seeAlso) true true true) true = true % 0.83/1.01 |- ifeq (iext uri_rdfs_range $_343 uri_rdf_Property) true % 0.83/1.01 (ifeq (iext $_343 $_344 uri_rdfs_subClassOf) true true true) true = % 0.83/1.01 true % 0.83/1.01 |- ifeq (iext uri_rdfs_range $_343 uri_rdf_Property) true % 0.83/1.01 (ifeq (iext $_343 $_344 uri_rdfs_subPropertyOf) true true true) true = % 0.83/1.01 true % 0.83/1.01 |- ifeq (iext uri_rdfs_range $_343 uri_rdfs_Class) true % 0.83/1.01 (ifeq (iext $_343 $_344 uri_rdf_Alt) true true true) true = true % 0.83/1.01 |- ifeq (iext uri_rdfs_range $_343 uri_rdfs_Class) true % 0.83/1.01 (ifeq (iext $_343 $_344 uri_rdf_Bag) true true true) true = true % 0.83/1.01 |- ifeq (iext uri_rdfs_range $_343 uri_rdfs_Class) true % 0.83/1.01 (ifeq (iext $_343 $_344 uri_rdf_Property) true true true) true = true % 0.83/1.01 |- ifeq (iext uri_rdfs_range $_343 uri_rdfs_Class) true % 0.83/1.01 (ifeq (iext $_343 $_344 uri_rdf_XMLLiteral) true true true) true = % 0.83/1.01 true % 0.83/1.01 |- ifeq (iext uri_rdfs_range $_343 uri_rdfs_Class) true % 0.83/1.01 (ifeq (iext $_343 $_344 uri_rdfs_Class) true true true) true = true % 0.83/1.01 |- ifeq (iext uri_rdfs_range $_343 uri_rdfs_Class) true % 0.83/1.01 (ifeq (iext $_343 $_344 uri_rdfs_Container) true true true) true = % 0.83/1.01 true % 0.83/1.01 |- ifeq (iext uri_rdfs_range $_343 uri_rdfs_Class) true % 0.83/1.01 (ifeq (iext $_343 $_344 uri_rdfs_ContainerMembershipProperty) true % 0.83/1.01 true true) true = true % 0.83/1.01 |- ifeq (iext uri_rdfs_range $_343 uri_rdfs_Class) true % 0.83/1.01 (ifeq (iext $_343 $_344 uri_rdfs_Datatype) true true true) true = true % 0.83/1.01 |- ifeq (iext uri_rdfs_range $_343 uri_rdfs_Class) true % 0.83/1.01 (ifeq (iext $_343 $_344 uri_rdfs_Literal) true true true) true = true % 0.83/1.01 |- ifeq (iext uri_rdfs_range $_343 uri_rdfs_Class) true % 0.83/1.01 (ifeq (iext $_343 $_344 uri_rdfs_Resource) true true true) true = true % 0.83/1.01 |- ifeq (iext uri_rdfs_range $_343 uri_rdfs_Class) true % 0.83/1.01 (ifeq (iext $_343 $_344 uri_rdfs_Seq) true true true) true = true % 0.83/1.01 |- ifeq (iext uri_rdfs_range $_343 uri_rdfs_ContainerMembershipProperty) % 0.83/1.01 true (ifeq (iext $_343 $_344 uri_rdf__1) true true true) true = true % 0.83/1.01 |- ifeq (iext uri_rdfs_range $_343 uri_rdfs_ContainerMembershipProperty) % 0.83/1.01 true (ifeq (iext $_343 $_344 uri_rdf__2) true true true) true = true % 0.83/1.01 |- ifeq (iext uri_rdfs_range $_343 uri_rdfs_ContainerMembershipProperty) % 0.83/1.01 true (ifeq (iext $_343 $_344 uri_rdf__3) true true true) true = true % 0.83/1.01 |- ifeq (iext uri_rdfs_range $_343 uri_rdfs_Datatype) true % 0.83/1.01 (ifeq (iext $_343 $_344 uri_rdf_XMLLiteral) true true true) true = % 0.83/1.01 true % 0.83/1.01 |- ifeq (iext uri_rdfs_range $_343 uri_rdfs_Resource) true % 0.83/1.01 (ifeq (iext $_343 $_344 $_345) true true true) true = true % 0.83/1.01 |- ifeq (iext uri_rdfs_range uri_owl_complementOf $_342) true % 0.83/1.01 (icext $_342 uri_ex_A) true = true % 0.83/1.01 |- ifeq (iext uri_rdfs_range uri_owl_intersectionOf $_342) true % 0.83/1.01 (icext $_342 % 0.83/1.01 sK4_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l1) % 0.83/1.01 true = true % 0.83/1.01 |- ifeq (iext uri_rdfs_range uri_rdf_first $_342) true % 0.83/1.01 (icext $_342 % 0.83/1.01 sK1_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_y) true = % 0.83/1.01 true % 0.83/1.01 |- ifeq (iext uri_rdfs_range uri_rdf_first $_342) true % 0.83/1.01 (icext $_342 uri_ex_A) true = true % 0.83/1.01 |- ifeq (iext uri_rdfs_range uri_rdf_rest $_342) true % 0.83/1.01 (icext $_342 uri_rdf_nil) true = true % 0.83/1.01 |- ifeq (iext uri_rdfs_range uri_rdf_rest $_342) true % 0.83/1.01 (icext $_342 % 0.83/1.01 sK2_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l2) % 0.83/1.01 true = true % 0.83/1.01 |- ifeq (iext uri_rdfs_range uri_rdf_type $_342) true % 0.83/1.01 (icext $_342 uri_rdf_List) true = true % 0.83/1.01 |- ifeq (iext uri_rdfs_range uri_rdf_type $_342) true % 0.83/1.01 (icext $_342 uri_owl_Class) true = true % 0.83/1.01 |- ifeq (iext uri_rdfs_range uri_rdf_type $_342) true % 0.83/1.01 (icext $_342 % 0.83/1.01 sK3_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_x) true = % 0.83/1.01 true % 0.83/1.01 |- ifeq (iext uri_rdfs_range uri_rdf_type $_342) true % 0.83/1.01 (icext $_342 uri_rdf_Property) true = true % 0.83/1.01 |- ifeq (iext uri_rdfs_range uri_rdf_type $_342) true % 0.83/1.01 (icext $_342 uri_rdfs_Class) true = true % 0.83/1.01 |- ifeq (iext uri_rdfs_range uri_rdf_type $_342) true % 0.83/1.01 (icext $_342 uri_rdfs_Datatype) true = true % 0.83/1.01 |- ifeq (iext uri_rdfs_range uri_rdf_type $_342) true % 0.83/1.01 (icext $_342 uri_rdfs_ContainerMembershipProperty) true = true % 0.83/1.01 |- ifeq (iext uri_rdfs_range uri_rdf_type $_342) true % 0.83/1.01 (icext $_342 uri_rdfs_Resource) true = true % 0.83/1.01 |- ifeq (iext uri_rdfs_range uri_rdfs_domain $_342) true % 0.83/1.01 (icext $_342 uri_rdfs_Resource) true = true % 0.83/1.01 |- ifeq (iext uri_rdfs_range uri_rdfs_domain $_342) true % 0.83/1.01 (icext $_342 uri_rdf_List) true = true % 0.83/1.01 |- ifeq (iext uri_rdfs_range uri_rdfs_domain $_342) true % 0.83/1.01 (icext $_342 uri_rdfs_Statement) true = true % 0.83/1.01 |- ifeq (iext uri_rdfs_range uri_rdfs_domain $_342) true % 0.83/1.01 (icext $_342 uri_rdf_Property) true = true % 0.83/1.01 |- ifeq (iext uri_rdfs_range uri_rdfs_domain $_342) true % 0.83/1.01 (icext $_342 uri_rdfs_Class) true = true % 0.83/1.01 |- ifeq (iext uri_rdfs_range uri_rdfs_range $_342) true % 0.83/1.01 (icext $_342 uri_rdfs_Resource) true = true % 0.83/1.01 |- ifeq (iext uri_rdfs_range uri_rdfs_range $_342) true % 0.83/1.01 (icext $_342 uri_rdf_List) true = true % 0.83/1.01 |- ifeq (iext uri_rdfs_range uri_rdfs_range $_342) true % 0.83/1.01 (icext $_342 uri_rdfs_Class) true = true % 0.83/1.01 |- ifeq (iext uri_rdfs_range uri_rdfs_range $_342) true % 0.83/1.01 (icext $_342 uri_rdfs_Literal) true = true % 0.83/1.01 |- ifeq (iext uri_rdfs_range uri_rdfs_range $_342) true % 0.83/1.01 (icext $_342 uri_rdf_Property) true = true % 0.83/1.01 |- ifeq (iext uri_rdfs_range uri_rdfs_subClassOf $_342) true % 0.83/1.01 (icext $_342 uri_rdf_Alt) true = true % 0.83/1.01 |- ifeq (iext uri_rdfs_range uri_rdfs_subClassOf $_342) true % 0.83/1.01 (icext $_342 uri_rdfs_Container) true = true % 0.83/1.01 |- ifeq (iext uri_rdfs_range uri_rdfs_subClassOf $_342) true % 0.83/1.01 (icext $_342 uri_rdfs_Resource) true = true % 0.83/1.01 |- ifeq (iext uri_rdfs_range uri_rdfs_subClassOf $_342) true % 0.83/1.01 (icext $_342 uri_rdf_Bag) true = true % 0.83/1.01 |- ifeq (iext uri_rdfs_range uri_rdfs_subClassOf $_342) true % 0.83/1.01 (icext $_342 uri_rdf_Property) true = true % 0.83/1.01 |- ifeq (iext uri_rdfs_range uri_rdfs_subClassOf $_342) true % 0.83/1.01 (icext $_342 uri_rdf_XMLLiteral) true = true % 0.83/1.01 |- ifeq (iext uri_rdfs_range uri_rdfs_subClassOf $_342) true % 0.83/1.01 (icext $_342 uri_rdfs_Literal) true = true % 0.83/1.01 |- ifeq (iext uri_rdfs_range uri_rdfs_subClassOf $_342) true % 0.83/1.01 (icext $_342 uri_rdfs_Class) true = true % 0.83/1.01 |- ifeq (iext uri_rdfs_range uri_rdfs_subClassOf $_342) true % 0.83/1.01 (icext $_342 uri_rdfs_ContainerMembershipProperty) true = true % 0.83/1.01 |- ifeq (iext uri_rdfs_range uri_rdfs_subClassOf $_342) true % 0.83/1.01 (icext $_342 uri_rdfs_Datatype) true = true % 0.83/1.01 |- ifeq (iext uri_rdfs_range uri_rdfs_subClassOf $_342) true % 0.83/1.01 (icext $_342 uri_rdfs_Seq) true = true % 0.83/1.01 |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_342) true % 0.83/1.01 (icext $_342 uri_owl_complementOf) true = true % 0.83/1.01 |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_342) true % 0.83/1.01 (icext $_342 uri_owl_intersectionOf) true = true % 0.83/1.01 |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_342) true % 0.83/1.01 (icext $_342 uri_rdf__1) true = true % 0.83/1.01 |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_342) true % 0.83/1.01 (icext $_342 uri_rdfs_member) true = true % 0.83/1.01 |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_342) true % 0.83/1.01 (icext $_342 uri_rdf__2) true = true % 0.83/1.01 |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_342) true % 0.83/1.01 (icext $_342 uri_rdf__3) true = true % 0.83/1.01 |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_342) true % 0.83/1.01 (icext $_342 uri_rdf_first) true = true % 0.83/1.01 |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_342) true % 0.83/1.01 (icext $_342 uri_rdf_object) true = true % 0.83/1.01 |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_342) true % 0.83/1.01 (icext $_342 uri_rdf_predicate) true = true % 0.83/1.01 |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_342) true % 0.83/1.01 (icext $_342 uri_rdf_rest) true = true % 0.83/1.01 |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_342) true % 0.83/1.01 (icext $_342 uri_rdf_subject) true = true % 0.83/1.01 |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_342) true % 0.83/1.01 (icext $_342 uri_rdf_type) true = true % 0.83/1.01 |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_342) true % 0.83/1.01 (icext $_342 uri_rdf_value) true = true % 0.83/1.01 |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_342) true % 0.83/1.01 (icext $_342 uri_rdfs_comment) true = true % 0.83/1.01 |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_342) true % 0.83/1.01 (icext $_342 uri_rdfs_domain) true = true % 0.83/1.01 |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_342) true % 0.83/1.01 (icext $_342 uri_rdfs_isDefinedBy) true = true % 0.83/1.01 |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_342) true % 0.83/1.01 (icext $_342 uri_rdfs_seeAlso) true = true % 0.83/1.01 |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_342) true % 0.83/1.01 (icext $_342 uri_rdfs_label) true = true % 0.83/1.01 |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_342) true % 0.83/1.01 (icext $_342 uri_rdfs_range) true = true % 0.83/1.01 |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_342) true % 0.83/1.01 (icext $_342 uri_rdfs_subClassOf) true = true % 0.83/1.01 |- ifeq (iext uri_rdfs_range uri_rdfs_subPropertyOf $_342) true % 0.83/1.01 (icext $_342 uri_rdfs_subPropertyOf) true = true % 0.83/1.01 |- ifeq (iext uri_rdf_rest $_344 $_345) true (icext uri_rdf_List $_345) % 0.83/1.01 true = true % 0.83/1.01 |- ifeq (iext uri_rdf_type $_344 $_345) true (icext uri_rdfs_Class $_345) % 0.83/1.01 true = true % 0.83/1.01 |- ifeq (iext uri_rdfs_comment $_344 $_345) true % 0.83/1.01 (icext uri_rdfs_Literal $_345) true = true % 0.83/1.01 |- ifeq (iext uri_rdfs_domain $_344 $_345) true % 0.83/1.01 (icext uri_rdfs_Class $_345) true = true % 0.83/1.01 |- ifeq (iext uri_rdfs_label $_344 $_345) true % 0.83/1.01 (icext uri_rdfs_Literal $_345) true = true % 0.83/1.01 |- ifeq (iext uri_rdfs_range $_344 $_345) true (icext uri_rdfs_Class $_345) % 0.83/1.01 true = true % 0.83/1.01 |- ifeq (iext uri_rdfs_subClassOf $_344 $_345) true % 0.83/1.01 (icext uri_rdfs_Class $_345) true = true % 0.83/1.01 |- ifeq (iext uri_rdfs_subPropertyOf $_344 $_345) true % 0.83/1.01 (icext uri_rdf_Property $_345) true = true % 0.83/1.01 |- icext uri_rdfs_Class uri_rdf_List = true % 0.83/1.01 |- ifeq (iext uri_rdfs_range $P uri_rdfs_Class) true % 0.83/1.01 (ifeq (iext $P $X uri_rdf_List) true true true) true = true % 0.83/1.01 |- ifeq (iext uri_rdfs_domain $P uri_rdfs_Class) true % 0.83/1.01 (ifeq (iext $P uri_rdf_List $Y) true true true) true = true % 0.83/1.01 |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Class $D) true % 0.83/1.01 (icext $D uri_rdf_List) true = true % 0.83/1.01 |- iext uri_rdf_type uri_rdf_List uri_rdfs_Class = true % 0.83/1.01 |- ic uri_rdf_List = true % 0.83/1.01 |- iext uri_rdfs_subClassOf uri_rdf_List uri_rdf_List = true % 0.83/1.01 |- iext uri_rdfs_subClassOf uri_rdf_List uri_rdfs_Resource = true % 0.83/1.01 |- ifeq (iext uri_rdfs_range uri_rdfs_subClassOf $C) true % 0.83/1.01 (icext $C uri_rdf_List) true = true % 0.83/1.01 |- ifeq (iext uri_rdfs_domain uri_rdfs_subClassOf $C) true % 0.83/1.01 (icext $C uri_rdf_List) true = true % 0.83/1.01 |- ifeq (icext uri_rdf_List $X) true (icext uri_rdf_List $X) true = true % 0.83/1.01 |- ifeq (iext uri_rdfs_subClassOf $C uri_rdf_List) true % 0.83/1.01 (iext uri_rdfs_subClassOf $C uri_rdfs_Resource) true = true % 0.83/1.01 |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Resource $E) true % 0.83/1.01 (iext uri_rdfs_subClassOf uri_rdf_List $E) true = true % 0.83/1.01 |- icext uri_rdfs_Class uri_owl_Class = true % 0.83/1.01 |- ifeq (iext uri_rdfs_range $P uri_rdfs_Class) true % 0.83/1.01 (ifeq (iext $P $X uri_owl_Class) true true true) true = true % 0.83/1.01 |- ifeq (iext uri_rdfs_domain $P uri_rdfs_Class) true % 0.83/1.01 (ifeq (iext $P uri_owl_Class $Y) true true true) true = true % 0.83/1.01 |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Class $D) true % 0.83/1.01 (icext $D uri_owl_Class) true = true % 0.83/1.01 |- iext uri_rdf_type uri_owl_Class uri_rdfs_Class = true % 0.83/1.01 |- ic uri_owl_Class = true % 0.83/1.02 |- iext uri_rdfs_subClassOf uri_owl_Class uri_owl_Class = true % 0.83/1.02 |- iext uri_rdfs_subClassOf uri_owl_Class uri_rdfs_Resource = true % 0.83/1.02 |- ifeq (iext uri_rdfs_domain uri_rdfs_subClassOf $C) true % 0.83/1.02 (icext $C uri_owl_Class) true = true % 0.83/1.02 |- ifeq (iext uri_rdfs_subClassOf $C uri_owl_Class) true % 0.83/1.02 (iext uri_rdfs_subClassOf $C uri_rdfs_Resource) true = true % 0.83/1.02 |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Resource $E) true % 0.83/1.02 (iext uri_rdfs_subClassOf uri_owl_Class $E) true = true % 0.83/1.02 |- ifeq (iext uri_rdfs_range uri_rdfs_subClassOf $C) true % 0.83/1.02 (icext $C uri_owl_Class) true = true % 0.83/1.02 |- ifeq (icext uri_owl_Class $X) true (icext uri_owl_Class $X) true = true % 0.83/1.02 |- icext uri_rdfs_Class % 0.83/1.02 sK3_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_x = true % 0.83/1.02 |- ifeq (iext uri_rdfs_range $P uri_rdfs_Class) true % 0.83/1.02 (ifeq % 0.83/1.02 (iext $P $X % 0.83/1.02 sK3_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_x) % 0.83/1.02 true true true) true = true % 0.83/1.02 |- ifeq (iext uri_rdfs_domain $P uri_rdfs_Class) true % 0.83/1.02 (ifeq % 0.83/1.02 (iext $P % 0.83/1.02 sK3_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_x $Y) % 0.83/1.02 true true true) true = true % 0.83/1.02 |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Class $D) true % 0.83/1.02 (icext $D sK3_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_x) % 0.83/1.02 true = true % 0.83/1.02 |- iext uri_rdf_type % 0.83/1.02 sK3_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_x % 0.83/1.02 uri_rdfs_Class = true % 0.83/1.02 |- ic sK3_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_x = true % 0.83/1.02 |- iext uri_rdfs_subClassOf % 0.83/1.02 sK3_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_x % 0.83/1.02 sK3_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_x = true % 0.83/1.02 |- iext uri_rdfs_subClassOf % 0.83/1.02 sK3_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_x % 0.83/1.02 uri_rdfs_Resource = true % 0.83/1.02 |- ifeq (iext uri_rdfs_range uri_rdfs_subClassOf $C) true % 0.83/1.02 (icext $C sK3_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_x) % 0.83/1.02 true = true % 0.83/1.02 |- ifeq (iext uri_rdfs_domain uri_rdfs_subClassOf $C) true % 0.83/1.02 (icext $C sK3_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_x) % 0.83/1.02 true = true % 0.83/1.02 |- ifeq % 0.83/1.02 (icext sK3_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_x $X) % 0.83/1.02 true % 0.83/1.02 (icext sK3_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_x $X) % 0.83/1.02 true = true % 0.83/1.02 |- ifeq % 0.83/1.02 (iext uri_rdfs_subClassOf $C % 0.83/1.02 sK3_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_x) true % 0.83/1.02 (iext uri_rdfs_subClassOf $C uri_rdfs_Resource) true = true % 0.83/1.02 |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Resource $E) true % 0.83/1.02 (iext uri_rdfs_subClassOf % 0.83/1.02 sK3_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_x $E) % 0.83/1.02 true = true % 0.83/1.02 |- icext uri_rdfs_Class uri_rdfs_Statement = true % 0.83/1.02 |- ifeq (iext uri_rdfs_range $P uri_rdfs_Class) true % 0.83/1.02 (ifeq (iext $P $X uri_rdfs_Statement) true true true) true = true % 0.83/1.02 |- ifeq (iext uri_rdfs_domain $P uri_rdfs_Class) true % 0.83/1.02 (ifeq (iext $P uri_rdfs_Statement $Y) true true true) true = true % 0.83/1.02 |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Class $D) true % 0.83/1.02 (icext $D uri_rdfs_Statement) true = true % 0.83/1.02 |- iext uri_rdf_type uri_rdfs_Statement uri_rdfs_Class = true % 0.83/1.02 |- ic uri_rdfs_Statement = true % 0.83/1.02 |- iext uri_rdfs_subClassOf uri_rdfs_Statement uri_rdfs_Statement = true % 0.83/1.02 |- iext uri_rdfs_subClassOf uri_rdfs_Statement uri_rdfs_Resource = true % 0.83/1.02 |- ifeq (iext uri_rdfs_domain uri_rdfs_subClassOf $C) true % 0.83/1.02 (icext $C uri_rdfs_Statement) true = true % 0.83/1.02 |- ifeq (iext uri_rdfs_subClassOf $C uri_rdfs_Statement) true % 0.83/1.02 (iext uri_rdfs_subClassOf $C uri_rdfs_Resource) true = true % 0.83/1.02 |- ifeq (iext uri_rdfs_subClassOf uri_rdfs_Resource $E) true % 0.83/1.02 (iext uri_rdfs_subClassOf uri_rdfs_Statement $E) true = true % 0.83/1.02 |- ifeq (iext uri_rdfs_range uri_rdfs_subClassOf $C) true % 0.83/1.02 (icext $C uri_rdfs_Statement) true = true % 0.83/1.02 |- ifeq (icext uri_rdfs_Statement $X) true (icext uri_rdfs_Statement $X) % 0.83/1.02 true = true % 0.83/1.02 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_owl_complementOf) true % 0.83/1.02 (ifeq % 0.83/1.02 (iext $_450 % 0.83/1.02 sK1_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_y % 0.83/1.02 uri_ex_A) true true true) true = true % 0.83/1.02 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_owl_intersectionOf) true % 0.83/1.02 (ifeq % 0.83/1.02 (iext $_450 % 0.83/1.02 sK3_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_x % 0.83/1.02 sK4_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l1) % 0.83/1.02 true true true) true = true % 0.83/1.02 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdf_first) true % 0.83/1.02 (ifeq % 0.83/1.02 (iext $_450 % 0.83/1.02 sK2_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l2 % 0.83/1.02 sK1_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_y) % 0.83/1.02 true true true) true = true % 0.83/1.02 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdf_first) true % 0.83/1.02 (ifeq % 0.83/1.02 (iext $_450 % 0.83/1.02 sK4_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l1 % 0.83/1.02 uri_ex_A) true true true) true = true % 0.83/1.02 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdf_rest) true % 0.83/1.02 (ifeq % 0.83/1.02 (iext $_450 % 0.83/1.02 sK2_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l2 % 0.83/1.02 uri_rdf_nil) true true true) true = true % 0.83/1.02 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdf_rest) true % 0.83/1.02 (ifeq % 0.83/1.02 (iext $_450 % 0.83/1.02 sK4_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l1 % 0.83/1.02 sK2_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l2) % 0.83/1.02 true true true) true = true % 0.83/1.02 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdf_type) true % 0.83/1.02 (ifeq % 0.83/1.02 (iext $_450 % 0.83/1.02 sK2_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l2 % 0.83/1.02 uri_rdf_List) true true true) true = true % 0.83/1.02 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdf_type) true % 0.83/1.02 (ifeq % 0.83/1.02 (iext $_450 % 0.83/1.02 sK3_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_x % 0.83/1.02 uri_rdfs_Class) true true true) true = true % 0.83/1.02 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdf_type) true % 0.83/1.02 (ifeq % 0.83/1.02 (iext $_450 % 0.83/1.02 sK4_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l1 % 0.83/1.02 uri_rdf_List) true true true) true = true % 0.83/1.02 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdf_type) true % 0.83/1.02 (ifeq (iext $_450 uri_ex_A uri_owl_Class) true true true) true = true % 0.83/1.02 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdf_type) true % 0.83/1.02 (ifeq (iext $_450 uri_ex_B uri_owl_Class) true true true) true = true % 0.83/1.02 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdf_type) true % 0.83/1.02 (ifeq % 0.83/1.02 (iext $_450 uri_ex_w % 0.83/1.02 sK3_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_x) % 0.83/1.02 true true true) true = true % 0.83/1.02 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdf_type) true % 0.83/1.02 (ifeq (iext $_450 uri_owl_Class uri_rdfs_Class) true true true) true = % 0.83/1.02 true % 0.83/1.02 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdf_type) true % 0.83/1.02 (ifeq (iext $_450 uri_owl_complementOf uri_rdf_Property) true true % 0.83/1.02 true) true = true % 0.83/1.02 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdf_type) true % 0.83/1.02 (ifeq (iext $_450 uri_owl_intersectionOf uri_rdf_Property) true true % 0.83/1.02 true) true = true % 0.83/1.02 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdf_type) true % 0.83/1.02 (ifeq (iext $_450 uri_rdf_Alt uri_rdfs_Class) true true true) true = % 0.83/1.02 true % 0.83/1.02 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdf_type) true % 0.83/1.02 (ifeq (iext $_450 uri_rdf_Bag uri_rdfs_Class) true true true) true = % 0.83/1.02 true % 0.83/1.02 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdf_type) true % 0.83/1.02 (ifeq (iext $_450 uri_rdf_List uri_rdfs_Class) true true true) true = % 0.83/1.02 true % 0.83/1.02 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdf_type) true % 0.83/1.02 (ifeq (iext $_450 uri_rdf_Property uri_rdfs_Class) true true true) % 0.83/1.02 true = true % 0.83/1.02 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdf_type) true % 0.83/1.02 (ifeq (iext $_450 uri_rdf_XMLLiteral uri_rdfs_Class) true true true) % 0.83/1.02 true = true % 0.83/1.02 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdf_type) true % 0.83/1.02 (ifeq (iext $_450 uri_rdf_XMLLiteral uri_rdfs_Datatype) true true % 0.83/1.02 true) true = true % 0.83/1.02 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdf_type) true % 0.83/1.02 (ifeq (iext $_450 uri_rdf__1 uri_rdf_Property) true true true) true = % 0.83/1.02 true % 0.83/1.02 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdf_type) true % 0.83/1.02 (ifeq (iext $_450 uri_rdf__1 uri_rdfs_ContainerMembershipProperty) % 0.83/1.02 true true true) true = true % 0.83/1.02 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdf_type) true % 0.83/1.02 (ifeq (iext $_450 uri_rdf__2 uri_rdf_Property) true true true) true = % 0.83/1.02 true % 0.83/1.02 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdf_type) true % 0.83/1.02 (ifeq (iext $_450 uri_rdf__2 uri_rdfs_ContainerMembershipProperty) % 0.83/1.02 true true true) true = true % 0.83/1.02 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdf_type) true % 0.83/1.02 (ifeq (iext $_450 uri_rdf__3 uri_rdf_Property) true true true) true = % 0.83/1.02 true % 0.83/1.02 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdf_type) true % 0.83/1.02 (ifeq (iext $_450 uri_rdf__3 uri_rdfs_ContainerMembershipProperty) % 0.83/1.02 true true true) true = true % 0.83/1.02 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdf_type) true % 0.83/1.02 (ifeq (iext $_450 uri_rdf_first uri_rdf_Property) true true true) % 0.83/1.02 true = true % 0.83/1.02 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdf_type) true % 0.83/1.02 (ifeq (iext $_450 uri_rdf_nil uri_rdf_List) true true true) true = % 0.83/1.02 true % 0.83/1.02 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdf_type) true % 0.83/1.02 (ifeq (iext $_450 uri_rdf_object uri_rdf_Property) true true true) % 0.83/1.02 true = true % 0.83/1.02 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdf_type) true % 0.83/1.02 (ifeq (iext $_450 uri_rdf_predicate uri_rdf_Property) true true true) % 0.83/1.02 true = true % 0.83/1.02 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdf_type) true % 0.83/1.02 (ifeq (iext $_450 uri_rdf_rest uri_rdf_Property) true true true) % 0.83/1.02 true = true % 0.83/1.02 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdf_type) true % 0.83/1.02 (ifeq (iext $_450 uri_rdf_subject uri_rdf_Property) true true true) % 0.83/1.02 true = true % 0.83/1.02 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdf_type) true % 0.83/1.02 (ifeq (iext $_450 uri_rdf_type uri_rdf_Property) true true true) % 0.83/1.02 true = true % 0.83/1.02 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdf_type) true % 0.83/1.02 (ifeq (iext $_450 uri_rdf_value uri_rdf_Property) true true true) % 0.83/1.02 true = true % 0.83/1.02 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdf_type) true % 0.83/1.02 (ifeq (iext $_450 uri_rdfs_Class uri_rdfs_Class) true true true) % 0.83/1.02 true = true % 0.83/1.02 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdf_type) true % 0.83/1.02 (ifeq (iext $_450 uri_rdfs_Container uri_rdfs_Class) true true true) % 0.83/1.02 true = true % 0.83/1.02 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdf_type) true % 0.83/1.02 (ifeq (iext $_450 uri_rdfs_ContainerMembershipProperty uri_rdfs_Class) % 0.83/1.02 true true true) true = true % 0.83/1.02 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdf_type) true % 0.83/1.02 (ifeq (iext $_450 uri_rdfs_Datatype uri_rdfs_Class) true true true) % 0.83/1.02 true = true % 0.83/1.02 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdf_type) true % 0.83/1.02 (ifeq (iext $_450 uri_rdfs_Literal uri_rdfs_Class) true true true) % 0.83/1.02 true = true % 0.83/1.02 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdf_type) true % 0.83/1.02 (ifeq (iext $_450 uri_rdfs_Resource uri_rdfs_Class) true true true) % 0.83/1.02 true = true % 0.83/1.02 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdf_type) true % 0.83/1.02 (ifeq (iext $_450 uri_rdfs_Seq uri_rdfs_Class) true true true) true = % 0.83/1.02 true % 0.83/1.02 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdf_type) true % 0.83/1.02 (ifeq (iext $_450 uri_rdfs_Statement uri_rdfs_Class) true true true) % 0.83/1.02 true = true % 0.83/1.02 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdf_type) true % 0.83/1.02 (ifeq (iext $_450 uri_rdfs_comment uri_rdf_Property) true true true) % 0.83/1.02 true = true % 0.83/1.02 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdf_type) true % 0.83/1.02 (ifeq (iext $_450 uri_rdfs_domain uri_rdf_Property) true true true) % 0.83/1.02 true = true % 0.83/1.02 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdf_type) true % 0.83/1.02 (ifeq (iext $_450 uri_rdfs_isDefinedBy uri_rdf_Property) true true % 0.83/1.02 true) true = true % 0.83/1.02 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdf_type) true % 0.83/1.02 (ifeq (iext $_450 uri_rdfs_label uri_rdf_Property) true true true) % 0.83/1.02 true = true % 0.83/1.02 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdf_type) true % 0.83/1.02 (ifeq (iext $_450 uri_rdfs_member uri_rdf_Property) true true true) % 0.83/1.02 true = true % 0.83/1.02 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdf_type) true % 0.83/1.02 (ifeq (iext $_450 uri_rdfs_range uri_rdf_Property) true true true) % 0.83/1.02 true = true % 0.83/1.02 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdf_type) true % 0.83/1.02 (ifeq (iext $_450 uri_rdfs_seeAlso uri_rdf_Property) true true true) % 0.83/1.02 true = true % 0.83/1.02 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdf_type) true % 0.83/1.02 (ifeq (iext $_450 uri_rdfs_subClassOf uri_rdf_Property) true true % 0.83/1.02 true) true = true % 0.83/1.02 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdf_type) true % 0.83/1.02 (ifeq (iext $_450 uri_rdfs_subPropertyOf uri_rdf_Property) true true % 0.83/1.02 true) true = true % 0.83/1.02 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdf_type) true % 0.83/1.02 (ifeq (iext $_450 $_452 uri_rdfs_Resource) true true true) true = true % 0.83/1.02 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdfs_domain) true % 0.83/1.02 (ifeq (iext $_450 uri_rdf__1 uri_rdfs_Resource) true true true) true = % 0.83/1.02 true % 0.83/1.02 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdfs_domain) true % 0.83/1.02 (ifeq (iext $_450 uri_rdf__2 uri_rdfs_Resource) true true true) true = % 0.83/1.02 true % 0.83/1.02 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdfs_domain) true % 0.83/1.02 (ifeq (iext $_450 uri_rdf__3 uri_rdfs_Resource) true true true) true = % 0.83/1.02 true % 0.83/1.02 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdfs_domain) true % 0.83/1.02 (ifeq (iext $_450 uri_rdf_first uri_rdf_List) true true true) true = % 0.83/1.02 true % 0.83/1.02 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdfs_domain) true % 0.83/1.02 (ifeq (iext $_450 uri_rdf_object uri_rdfs_Statement) true true true) % 0.83/1.02 true = true % 0.83/1.02 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdfs_domain) true % 0.83/1.02 (ifeq (iext $_450 uri_rdf_predicate uri_rdfs_Statement) true true % 0.83/1.02 true) true = true % 0.83/1.02 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdfs_domain) true % 0.83/1.02 (ifeq (iext $_450 uri_rdf_rest uri_rdf_List) true true true) true = % 0.83/1.02 true % 0.83/1.02 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdfs_domain) true % 0.83/1.02 (ifeq (iext $_450 uri_rdf_subject uri_rdfs_Statement) true true true) % 0.83/1.02 true = true % 0.83/1.02 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdfs_domain) true % 0.83/1.02 (ifeq (iext $_450 uri_rdf_type uri_rdfs_Resource) true true true) % 0.83/1.02 true = true % 0.83/1.02 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdfs_domain) true % 0.83/1.02 (ifeq (iext $_450 uri_rdf_value uri_rdfs_Resource) true true true) % 0.83/1.02 true = true % 0.83/1.02 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdfs_domain) true % 0.83/1.02 (ifeq (iext $_450 uri_rdfs_comment uri_rdfs_Resource) true true true) % 0.83/1.02 true = true % 0.83/1.02 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdfs_domain) true % 0.83/1.02 (ifeq (iext $_450 uri_rdfs_domain uri_rdf_Property) true true true) % 0.83/1.02 true = true % 0.83/1.02 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdfs_domain) true % 0.83/1.02 (ifeq (iext $_450 uri_rdfs_isDefinedBy uri_rdfs_Resource) true true % 0.83/1.02 true) true = true % 0.83/1.02 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdfs_domain) true % 0.83/1.02 (ifeq (iext $_450 uri_rdfs_label uri_rdfs_Resource) true true true) % 0.83/1.02 true = true % 0.83/1.02 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdfs_domain) true % 0.83/1.02 (ifeq (iext $_450 uri_rdfs_member uri_rdfs_Resource) true true true) % 0.83/1.02 true = true % 0.83/1.02 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdfs_domain) true % 0.83/1.02 (ifeq (iext $_450 uri_rdfs_range uri_rdf_Property) true true true) % 0.83/1.02 true = true % 0.83/1.02 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdfs_domain) true % 0.83/1.02 (ifeq (iext $_450 uri_rdfs_seeAlso uri_rdfs_Resource) true true true) % 0.83/1.02 true = true % 0.83/1.02 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdfs_domain) true % 0.83/1.02 (ifeq (iext $_450 uri_rdfs_subClassOf uri_rdfs_Class) true true true) % 0.83/1.02 true = true % 0.83/1.02 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdfs_domain) true % 0.83/1.02 (ifeq (iext $_450 uri_rdfs_subPropertyOf uri_rdf_Property) true true % 0.83/1.02 true) true = true % 0.83/1.02 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdfs_range) true % 0.83/1.02 (ifeq (iext $_450 uri_rdf__1 uri_rdfs_Resource) true true true) true = % 0.83/1.02 true % 0.83/1.02 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdfs_range) true % 0.83/1.02 (ifeq (iext $_450 uri_rdf__2 uri_rdfs_Resource) true true true) true = % 0.83/1.02 true % 0.83/1.02 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdfs_range) true % 0.83/1.02 (ifeq (iext $_450 uri_rdf__3 uri_rdfs_Resource) true true true) true = % 0.83/1.02 true % 0.83/1.02 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdfs_range) true % 0.83/1.02 (ifeq (iext $_450 uri_rdf_first uri_rdfs_Resource) true true true) % 0.83/1.02 true = true % 0.83/1.02 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdfs_range) true % 0.83/1.02 (ifeq (iext $_450 uri_rdf_predicate uri_rdfs_Resource) true true true) % 0.83/1.02 true = true % 0.83/1.02 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdfs_range) true % 0.83/1.02 (ifeq (iext $_450 uri_rdf_rest uri_rdf_List) true true true) true = % 0.83/1.02 true % 0.83/1.02 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdfs_range) true % 0.83/1.02 (ifeq (iext $_450 uri_rdf_subject uri_rdfs_Resource) true true true) % 0.83/1.02 true = true % 0.83/1.02 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdfs_range) true % 0.83/1.02 (ifeq (iext $_450 uri_rdf_type uri_rdfs_Class) true true true) true = % 0.83/1.02 true % 0.83/1.02 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdfs_range) true % 0.83/1.02 (ifeq (iext $_450 uri_rdf_value uri_rdfs_Resource) true true true) % 0.83/1.02 true = true % 0.83/1.02 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdfs_range) true % 0.83/1.02 (ifeq (iext $_450 uri_rdfs_comment uri_rdfs_Literal) true true true) % 0.83/1.02 true = true % 0.83/1.02 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdfs_range) true % 0.83/1.02 (ifeq (iext $_450 uri_rdfs_domain uri_rdfs_Class) true true true) % 0.83/1.02 true = true % 0.83/1.02 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdfs_range) true % 0.83/1.02 (ifeq (iext $_450 uri_rdfs_isDefinedBy uri_rdfs_Resource) true true % 0.83/1.02 true) true = true % 0.83/1.02 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdfs_range) true % 0.83/1.02 (ifeq (iext $_450 uri_rdfs_label uri_rdfs_Literal) true true true) % 0.83/1.02 true = true % 0.83/1.02 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdfs_range) true % 0.83/1.02 (ifeq (iext $_450 uri_rdfs_member uri_rdfs_Resource) true true true) % 0.83/1.02 true = true % 0.83/1.02 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdfs_range) true % 0.83/1.02 (ifeq (iext $_450 uri_rdfs_range uri_rdfs_Class) true true true) % 0.83/1.02 true = true % 0.83/1.02 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdfs_range) true % 0.83/1.02 (ifeq (iext $_450 uri_rdfs_seeAlso uri_rdfs_Resource) true true true) % 0.83/1.02 true = true % 0.83/1.02 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdfs_range) true % 0.83/1.02 (ifeq (iext $_450 uri_rdfs_subClassOf uri_rdfs_Class) true true true) % 0.83/1.02 true = true % 0.83/1.02 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdfs_range) true % 0.83/1.02 (ifeq (iext $_450 uri_rdfs_subPropertyOf uri_rdf_Property) true true % 0.83/1.02 true) true = true % 0.83/1.02 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdfs_subClassOf) true % 0.83/1.02 (ifeq % 0.83/1.02 (iext $_450 % 0.83/1.02 sK3_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_x % 0.83/1.02 sK3_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_x) % 0.83/1.02 true true true) true = true % 0.83/1.02 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdfs_subClassOf) true % 0.83/1.02 (ifeq % 0.83/1.02 (iext $_450 % 0.83/1.02 sK3_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_x % 0.83/1.02 uri_rdfs_Resource) true true true) true = true % 0.83/1.02 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdfs_subClassOf) true % 0.83/1.02 (ifeq (iext $_450 uri_owl_Class uri_owl_Class) true true true) true = % 0.83/1.02 true % 0.83/1.02 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdfs_subClassOf) true % 0.83/1.02 (ifeq (iext $_450 uri_owl_Class uri_rdfs_Resource) true true true) % 0.83/1.02 true = true % 0.83/1.02 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdfs_subClassOf) true % 0.83/1.02 (ifeq (iext $_450 uri_rdf_Alt uri_rdf_Alt) true true true) true = true % 0.83/1.02 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdfs_subClassOf) true % 0.83/1.02 (ifeq (iext $_450 uri_rdf_Alt uri_rdfs_Container) true true true) % 0.83/1.02 true = true % 0.83/1.02 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdfs_subClassOf) true % 0.83/1.02 (ifeq (iext $_450 uri_rdf_Alt uri_rdfs_Resource) true true true) % 0.83/1.02 true = true % 0.83/1.02 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdfs_subClassOf) true % 0.83/1.02 (ifeq (iext $_450 uri_rdf_Bag uri_rdf_Bag) true true true) true = true % 0.83/1.02 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdfs_subClassOf) true % 0.83/1.02 (ifeq (iext $_450 uri_rdf_Bag uri_rdfs_Container) true true true) % 0.83/1.02 true = true % 0.83/1.02 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdfs_subClassOf) true % 0.83/1.02 (ifeq (iext $_450 uri_rdf_Bag uri_rdfs_Resource) true true true) % 0.83/1.02 true = true % 0.83/1.02 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdfs_subClassOf) true % 0.83/1.02 (ifeq (iext $_450 uri_rdf_List uri_rdf_List) true true true) true = % 0.83/1.02 true % 0.83/1.02 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdfs_subClassOf) true % 0.83/1.02 (ifeq (iext $_450 uri_rdf_List uri_rdfs_Resource) true true true) % 0.83/1.02 true = true % 0.83/1.02 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdfs_subClassOf) true % 0.83/1.02 (ifeq (iext $_450 uri_rdf_Property uri_rdf_Property) true true true) % 0.83/1.02 true = true % 0.83/1.02 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdfs_subClassOf) true % 0.83/1.02 (ifeq (iext $_450 uri_rdf_Property uri_rdfs_Resource) true true true) % 0.83/1.02 true = true % 0.83/1.02 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdfs_subClassOf) true % 0.83/1.02 (ifeq (iext $_450 uri_rdf_XMLLiteral uri_rdf_XMLLiteral) true true % 0.83/1.02 true) true = true % 0.83/1.02 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdfs_subClassOf) true % 0.83/1.02 (ifeq (iext $_450 uri_rdf_XMLLiteral uri_rdfs_Literal) true true true) % 0.83/1.02 true = true % 0.83/1.02 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdfs_subClassOf) true % 0.83/1.02 (ifeq (iext $_450 uri_rdf_XMLLiteral uri_rdfs_Resource) true true % 0.83/1.02 true) true = true % 0.83/1.02 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdfs_subClassOf) true % 0.83/1.02 (ifeq (iext $_450 uri_rdfs_Class uri_rdfs_Class) true true true) % 0.83/1.02 true = true % 0.83/1.02 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdfs_subClassOf) true % 0.83/1.02 (ifeq (iext $_450 uri_rdfs_Class uri_rdfs_Resource) true true true) % 0.83/1.02 true = true % 0.83/1.02 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdfs_subClassOf) true % 0.83/1.02 (ifeq (iext $_450 uri_rdfs_Container uri_rdfs_Container) true true % 0.83/1.02 true) true = true % 0.83/1.02 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdfs_subClassOf) true % 0.83/1.02 (ifeq (iext $_450 uri_rdfs_Container uri_rdfs_Resource) true true % 0.83/1.02 true) true = true % 0.83/1.02 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdfs_subClassOf) true % 0.83/1.02 (ifeq % 0.83/1.02 (iext $_450 uri_rdfs_ContainerMembershipProperty uri_rdf_Property) % 0.83/1.02 true true true) true = true % 0.83/1.02 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdfs_subClassOf) true % 0.83/1.02 (ifeq % 0.83/1.02 (iext $_450 uri_rdfs_ContainerMembershipProperty % 0.83/1.02 uri_rdfs_ContainerMembershipProperty) true true true) true = % 0.83/1.02 true % 0.83/1.02 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdfs_subClassOf) true % 0.83/1.02 (ifeq % 0.83/1.02 (iext $_450 uri_rdfs_ContainerMembershipProperty uri_rdfs_Resource) % 0.83/1.02 true true true) true = true % 0.83/1.02 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdfs_subClassOf) true % 0.83/1.02 (ifeq (iext $_450 uri_rdfs_Datatype uri_rdfs_Class) true true true) % 0.83/1.02 true = true % 0.83/1.02 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdfs_subClassOf) true % 0.83/1.02 (ifeq (iext $_450 uri_rdfs_Datatype uri_rdfs_Datatype) true true true) % 0.83/1.02 true = true % 0.83/1.02 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdfs_subClassOf) true % 0.83/1.02 (ifeq (iext $_450 uri_rdfs_Datatype uri_rdfs_Resource) true true true) % 0.83/1.02 true = true % 0.83/1.02 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdfs_subClassOf) true % 0.83/1.02 (ifeq (iext $_450 uri_rdfs_Literal uri_rdfs_Literal) true true true) % 0.83/1.02 true = true % 0.83/1.02 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdfs_subClassOf) true % 0.83/1.02 (ifeq (iext $_450 uri_rdfs_Literal uri_rdfs_Resource) true true true) % 0.83/1.02 true = true % 0.83/1.02 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdfs_subClassOf) true % 0.83/1.02 (ifeq (iext $_450 uri_rdfs_Resource uri_rdfs_Resource) true true true) % 0.83/1.02 true = true % 0.83/1.02 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdfs_subClassOf) true % 0.83/1.02 (ifeq (iext $_450 uri_rdfs_Seq uri_rdfs_Container) true true true) % 0.83/1.02 true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdfs_subClassOf) true % 0.83/1.03 (ifeq (iext $_450 uri_rdfs_Seq uri_rdfs_Resource) true true true) % 0.83/1.03 true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdfs_subClassOf) true % 0.83/1.03 (ifeq (iext $_450 uri_rdfs_Seq uri_rdfs_Seq) true true true) true = % 0.83/1.03 true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdfs_subClassOf) true % 0.83/1.03 (ifeq (iext $_450 uri_rdfs_Statement uri_rdfs_Resource) true true % 0.83/1.03 true) true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdfs_subClassOf) true % 0.83/1.03 (ifeq (iext $_450 uri_rdfs_Statement uri_rdfs_Statement) true true % 0.83/1.03 true) true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdfs_subPropertyOf) true % 0.83/1.03 (ifeq (iext $_450 uri_owl_complementOf uri_owl_complementOf) true true % 0.83/1.03 true) true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdfs_subPropertyOf) true % 0.83/1.03 (ifeq (iext $_450 uri_owl_intersectionOf uri_owl_intersectionOf) true % 0.83/1.03 true true) true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdfs_subPropertyOf) true % 0.83/1.03 (ifeq (iext $_450 uri_rdf__1 uri_rdf__1) true true true) true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdfs_subPropertyOf) true % 0.83/1.03 (ifeq (iext $_450 uri_rdf__1 uri_rdfs_member) true true true) true = % 0.83/1.03 true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdfs_subPropertyOf) true % 0.83/1.03 (ifeq (iext $_450 uri_rdf__2 uri_rdf__2) true true true) true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdfs_subPropertyOf) true % 0.83/1.03 (ifeq (iext $_450 uri_rdf__2 uri_rdfs_member) true true true) true = % 0.83/1.03 true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdfs_subPropertyOf) true % 0.83/1.03 (ifeq (iext $_450 uri_rdf__3 uri_rdf__3) true true true) true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdfs_subPropertyOf) true % 0.83/1.03 (ifeq (iext $_450 uri_rdf__3 uri_rdfs_member) true true true) true = % 0.83/1.03 true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdfs_subPropertyOf) true % 0.83/1.03 (ifeq (iext $_450 uri_rdf_first uri_rdf_first) true true true) true = % 0.83/1.03 true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdfs_subPropertyOf) true % 0.83/1.03 (ifeq (iext $_450 uri_rdf_object uri_rdf_object) true true true) % 0.83/1.03 true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdfs_subPropertyOf) true % 0.83/1.03 (ifeq (iext $_450 uri_rdf_predicate uri_rdf_predicate) true true true) % 0.83/1.03 true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdfs_subPropertyOf) true % 0.83/1.03 (ifeq (iext $_450 uri_rdf_rest uri_rdf_rest) true true true) true = % 0.83/1.03 true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdfs_subPropertyOf) true % 0.83/1.03 (ifeq (iext $_450 uri_rdf_subject uri_rdf_subject) true true true) % 0.83/1.03 true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdfs_subPropertyOf) true % 0.83/1.03 (ifeq (iext $_450 uri_rdf_type uri_rdf_type) true true true) true = % 0.83/1.03 true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdfs_subPropertyOf) true % 0.83/1.03 (ifeq (iext $_450 uri_rdf_value uri_rdf_value) true true true) true = % 0.83/1.03 true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdfs_subPropertyOf) true % 0.83/1.03 (ifeq (iext $_450 uri_rdfs_comment uri_rdfs_comment) true true true) % 0.83/1.03 true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdfs_subPropertyOf) true % 0.83/1.03 (ifeq (iext $_450 uri_rdfs_domain uri_rdfs_domain) true true true) % 0.83/1.03 true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdfs_subPropertyOf) true % 0.83/1.03 (ifeq (iext $_450 uri_rdfs_isDefinedBy uri_rdfs_isDefinedBy) true true % 0.83/1.03 true) true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdfs_subPropertyOf) true % 0.83/1.03 (ifeq (iext $_450 uri_rdfs_isDefinedBy uri_rdfs_seeAlso) true true % 0.83/1.03 true) true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdfs_subPropertyOf) true % 0.83/1.03 (ifeq (iext $_450 uri_rdfs_label uri_rdfs_label) true true true) % 0.83/1.03 true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdfs_subPropertyOf) true % 0.83/1.03 (ifeq (iext $_450 uri_rdfs_member uri_rdfs_member) true true true) % 0.83/1.03 true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdfs_subPropertyOf) true % 0.83/1.03 (ifeq (iext $_450 uri_rdfs_range uri_rdfs_range) true true true) % 0.83/1.03 true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdfs_subPropertyOf) true % 0.83/1.03 (ifeq (iext $_450 uri_rdfs_seeAlso uri_rdfs_seeAlso) true true true) % 0.83/1.03 true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdfs_subPropertyOf) true % 0.83/1.03 (ifeq (iext $_450 uri_rdfs_subClassOf uri_rdfs_subClassOf) true true % 0.83/1.03 true) true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf $_450 uri_rdfs_subPropertyOf) true % 0.83/1.03 (ifeq (iext $_450 uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf) true % 0.83/1.03 true true) true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf uri_owl_complementOf $_451) true % 0.83/1.03 (iext $_451 % 0.83/1.03 sK1_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_y % 0.83/1.03 uri_ex_A) true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf uri_owl_intersectionOf $_451) true % 0.83/1.03 (iext $_451 % 0.83/1.03 sK3_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_x % 0.83/1.03 sK4_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l1) % 0.83/1.03 true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_first $_451) true % 0.83/1.03 (iext $_451 % 0.83/1.03 sK2_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l2 % 0.83/1.03 sK1_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_y) true = % 0.83/1.03 true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_first $_451) true % 0.83/1.03 (iext $_451 % 0.83/1.03 sK4_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l1 % 0.83/1.03 uri_ex_A) true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_rest $_451) true % 0.83/1.03 (iext $_451 % 0.83/1.03 sK2_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l2 % 0.83/1.03 uri_rdf_nil) true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_rest $_451) true % 0.83/1.03 (iext $_451 % 0.83/1.03 sK4_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l1 % 0.83/1.03 sK2_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l2) % 0.83/1.03 true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_451) true % 0.83/1.03 (iext $_451 % 0.83/1.03 sK2_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l2 % 0.83/1.03 uri_rdf_List) true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_451) true % 0.83/1.03 (iext $_451 % 0.83/1.03 sK3_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_x % 0.83/1.03 uri_rdfs_Class) true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_451) true % 0.83/1.03 (iext $_451 % 0.83/1.03 sK4_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_l1 % 0.83/1.03 uri_rdf_List) true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_451) true % 0.83/1.03 (iext $_451 uri_ex_A uri_owl_Class) true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_451) true % 0.83/1.03 (iext $_451 uri_ex_B uri_owl_Class) true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_451) true % 0.83/1.03 (iext $_451 uri_ex_w % 0.83/1.03 sK3_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_x) true = % 0.83/1.03 true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_451) true % 0.83/1.03 (iext $_451 uri_owl_Class uri_rdfs_Class) true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_451) true % 0.83/1.03 (iext $_451 uri_owl_complementOf uri_rdf_Property) true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_451) true % 0.83/1.03 (iext $_451 uri_owl_intersectionOf uri_rdf_Property) true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_451) true % 0.83/1.03 (iext $_451 uri_rdf_Alt uri_rdfs_Class) true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_451) true % 0.83/1.03 (iext $_451 uri_rdf_Bag uri_rdfs_Class) true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_451) true % 0.83/1.03 (iext $_451 uri_rdf_List uri_rdfs_Class) true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_451) true % 0.83/1.03 (iext $_451 uri_rdf_Property uri_rdfs_Class) true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_451) true % 0.83/1.03 (iext $_451 uri_rdf_XMLLiteral uri_rdfs_Class) true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_451) true % 0.83/1.03 (iext $_451 uri_rdf_XMLLiteral uri_rdfs_Datatype) true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_451) true % 0.83/1.03 (iext $_451 uri_rdf__1 uri_rdf_Property) true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_451) true % 0.83/1.03 (iext $_451 uri_rdf__1 uri_rdfs_ContainerMembershipProperty) true = % 0.83/1.03 true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_451) true % 0.83/1.03 (iext $_451 uri_rdf__2 uri_rdf_Property) true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_451) true % 0.83/1.03 (iext $_451 uri_rdf__2 uri_rdfs_ContainerMembershipProperty) true = % 0.83/1.03 true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_451) true % 0.83/1.03 (iext $_451 uri_rdf__3 uri_rdf_Property) true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_451) true % 0.83/1.03 (iext $_451 uri_rdf__3 uri_rdfs_ContainerMembershipProperty) true = % 0.83/1.03 true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_451) true % 0.83/1.03 (iext $_451 uri_rdf_first uri_rdf_Property) true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_451) true % 0.83/1.03 (iext $_451 uri_rdf_nil uri_rdf_List) true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_451) true % 0.83/1.03 (iext $_451 uri_rdf_object uri_rdf_Property) true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_451) true % 0.83/1.03 (iext $_451 uri_rdf_predicate uri_rdf_Property) true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_451) true % 0.83/1.03 (iext $_451 uri_rdf_rest uri_rdf_Property) true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_451) true % 0.83/1.03 (iext $_451 uri_rdf_subject uri_rdf_Property) true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_451) true % 0.83/1.03 (iext $_451 uri_rdf_type uri_rdf_Property) true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_451) true % 0.83/1.03 (iext $_451 uri_rdf_value uri_rdf_Property) true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_451) true % 0.83/1.03 (iext $_451 uri_rdfs_Class uri_rdfs_Class) true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_451) true % 0.83/1.03 (iext $_451 uri_rdfs_Container uri_rdfs_Class) true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_451) true % 0.83/1.03 (iext $_451 uri_rdfs_ContainerMembershipProperty uri_rdfs_Class) % 0.83/1.03 true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_451) true % 0.83/1.03 (iext $_451 uri_rdfs_Datatype uri_rdfs_Class) true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_451) true % 0.83/1.03 (iext $_451 uri_rdfs_Literal uri_rdfs_Class) true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_451) true % 0.83/1.03 (iext $_451 uri_rdfs_Resource uri_rdfs_Class) true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_451) true % 0.83/1.03 (iext $_451 uri_rdfs_Seq uri_rdfs_Class) true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_451) true % 0.83/1.03 (iext $_451 uri_rdfs_Statement uri_rdfs_Class) true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_451) true % 0.83/1.03 (iext $_451 uri_rdfs_comment uri_rdf_Property) true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_451) true % 0.83/1.03 (iext $_451 uri_rdfs_domain uri_rdf_Property) true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_451) true % 0.83/1.03 (iext $_451 uri_rdfs_isDefinedBy uri_rdf_Property) true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_451) true % 0.83/1.03 (iext $_451 uri_rdfs_label uri_rdf_Property) true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_451) true % 0.83/1.03 (iext $_451 uri_rdfs_member uri_rdf_Property) true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_451) true % 0.83/1.03 (iext $_451 uri_rdfs_range uri_rdf_Property) true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_451) true % 0.83/1.03 (iext $_451 uri_rdfs_seeAlso uri_rdf_Property) true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_451) true % 0.83/1.03 (iext $_451 uri_rdfs_subClassOf uri_rdf_Property) true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_451) true % 0.83/1.03 (iext $_451 uri_rdfs_subPropertyOf uri_rdf_Property) true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdf_type $_451) true % 0.83/1.03 (iext $_451 $_452 uri_rdfs_Resource) true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_domain $_451) true % 0.83/1.03 (iext $_451 uri_rdf__1 uri_rdfs_Resource) true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_domain $_451) true % 0.83/1.03 (iext $_451 uri_rdf__2 uri_rdfs_Resource) true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_domain $_451) true % 0.83/1.03 (iext $_451 uri_rdf__3 uri_rdfs_Resource) true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_domain $_451) true % 0.83/1.03 (iext $_451 uri_rdf_first uri_rdf_List) true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_domain $_451) true % 0.83/1.03 (iext $_451 uri_rdf_object uri_rdfs_Statement) true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_domain $_451) true % 0.83/1.03 (iext $_451 uri_rdf_predicate uri_rdfs_Statement) true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_domain $_451) true % 0.83/1.03 (iext $_451 uri_rdf_rest uri_rdf_List) true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_domain $_451) true % 0.83/1.03 (iext $_451 uri_rdf_subject uri_rdfs_Statement) true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_domain $_451) true % 0.83/1.03 (iext $_451 uri_rdf_type uri_rdfs_Resource) true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_domain $_451) true % 0.83/1.03 (iext $_451 uri_rdf_value uri_rdfs_Resource) true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_domain $_451) true % 0.83/1.03 (iext $_451 uri_rdfs_comment uri_rdfs_Resource) true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_domain $_451) true % 0.83/1.03 (iext $_451 uri_rdfs_domain uri_rdf_Property) true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_domain $_451) true % 0.83/1.03 (iext $_451 uri_rdfs_isDefinedBy uri_rdfs_Resource) true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_domain $_451) true % 0.83/1.03 (iext $_451 uri_rdfs_label uri_rdfs_Resource) true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_domain $_451) true % 0.83/1.03 (iext $_451 uri_rdfs_member uri_rdfs_Resource) true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_domain $_451) true % 0.83/1.03 (iext $_451 uri_rdfs_range uri_rdf_Property) true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_domain $_451) true % 0.83/1.03 (iext $_451 uri_rdfs_seeAlso uri_rdfs_Resource) true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_domain $_451) true % 0.83/1.03 (iext $_451 uri_rdfs_subClassOf uri_rdfs_Class) true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_domain $_451) true % 0.83/1.03 (iext $_451 uri_rdfs_subPropertyOf uri_rdf_Property) true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_range $_451) true % 0.83/1.03 (iext $_451 uri_rdf__1 uri_rdfs_Resource) true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_range $_451) true % 0.83/1.03 (iext $_451 uri_rdf__2 uri_rdfs_Resource) true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_range $_451) true % 0.83/1.03 (iext $_451 uri_rdf__3 uri_rdfs_Resource) true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_range $_451) true % 0.83/1.03 (iext $_451 uri_rdf_first uri_rdfs_Resource) true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_range $_451) true % 0.83/1.03 (iext $_451 uri_rdf_predicate uri_rdfs_Resource) true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_range $_451) true % 0.83/1.03 (iext $_451 uri_rdf_rest uri_rdf_List) true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_range $_451) true % 0.83/1.03 (iext $_451 uri_rdf_subject uri_rdfs_Resource) true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_range $_451) true % 0.83/1.03 (iext $_451 uri_rdf_type uri_rdfs_Class) true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_range $_451) true % 0.83/1.03 (iext $_451 uri_rdf_value uri_rdfs_Resource) true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_range $_451) true % 0.83/1.03 (iext $_451 uri_rdfs_comment uri_rdfs_Literal) true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_range $_451) true % 0.83/1.03 (iext $_451 uri_rdfs_domain uri_rdfs_Class) true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_range $_451) true % 0.83/1.03 (iext $_451 uri_rdfs_isDefinedBy uri_rdfs_Resource) true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_range $_451) true % 0.83/1.03 (iext $_451 uri_rdfs_label uri_rdfs_Literal) true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_range $_451) true % 0.83/1.03 (iext $_451 uri_rdfs_member uri_rdfs_Resource) true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_range $_451) true % 0.83/1.03 (iext $_451 uri_rdfs_range uri_rdfs_Class) true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_range $_451) true % 0.83/1.03 (iext $_451 uri_rdfs_seeAlso uri_rdfs_Resource) true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_range $_451) true % 0.83/1.03 (iext $_451 uri_rdfs_subClassOf uri_rdfs_Class) true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_range $_451) true % 0.83/1.03 (iext $_451 uri_rdfs_subPropertyOf uri_rdf_Property) true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_451) true % 0.83/1.03 (iext $_451 % 0.83/1.03 sK3_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_x % 0.83/1.03 sK3_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_x) true = % 0.83/1.03 true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_451) true % 0.83/1.03 (iext $_451 % 0.83/1.03 sK3_testcase_premise_fullish_029_Ex_Falso_Quodlibet_BNODE_x % 0.83/1.03 uri_rdfs_Resource) true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_451) true % 0.83/1.03 (iext $_451 uri_owl_Class uri_owl_Class) true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_451) true % 0.83/1.03 (iext $_451 uri_owl_Class uri_rdfs_Resource) true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_451) true % 0.83/1.03 (iext $_451 uri_rdf_Alt uri_rdf_Alt) true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_451) true % 0.83/1.03 (iext $_451 uri_rdf_Alt uri_rdfs_Container) true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_451) true % 0.83/1.03 (iext $_451 uri_rdf_Alt uri_rdfs_Resource) true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_451) true % 0.83/1.03 (iext $_451 uri_rdf_Bag uri_rdf_Bag) true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_451) true % 0.83/1.03 (iext $_451 uri_rdf_Bag uri_rdfs_Container) true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_451) true % 0.83/1.03 (iext $_451 uri_rdf_Bag uri_rdfs_Resource) true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_451) true % 0.83/1.03 (iext $_451 uri_rdf_List uri_rdf_List) true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_451) true % 0.83/1.03 (iext $_451 uri_rdf_List uri_rdfs_Resource) true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_451) true % 0.83/1.03 (iext $_451 uri_rdf_Property uri_rdf_Property) true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_451) true % 0.83/1.03 (iext $_451 uri_rdf_Property uri_rdfs_Resource) true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_451) true % 0.83/1.03 (iext $_451 uri_rdf_XMLLiteral uri_rdf_XMLLiteral) true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_451) true % 0.83/1.03 (iext $_451 uri_rdf_XMLLiteral uri_rdfs_Literal) true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_451) true % 0.83/1.03 (iext $_451 uri_rdf_XMLLiteral uri_rdfs_Resource) true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_451) true % 0.83/1.03 (iext $_451 uri_rdfs_Class uri_rdfs_Class) true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_451) true % 0.83/1.03 (iext $_451 uri_rdfs_Class uri_rdfs_Resource) true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_451) true % 0.83/1.03 (iext $_451 uri_rdfs_Container uri_rdfs_Container) true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_451) true % 0.83/1.03 (iext $_451 uri_rdfs_Container uri_rdfs_Resource) true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_451) true % 0.83/1.03 (iext $_451 uri_rdfs_ContainerMembershipProperty uri_rdf_Property) % 0.83/1.03 true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_451) true % 0.83/1.03 (iext $_451 uri_rdfs_ContainerMembershipProperty % 0.83/1.03 uri_rdfs_ContainerMembershipProperty) true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_451) true % 0.83/1.03 (iext $_451 uri_rdfs_ContainerMembershipProperty uri_rdfs_Resource) % 0.83/1.03 true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_451) true % 0.83/1.03 (iext $_451 uri_rdfs_Datatype uri_rdfs_Class) true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_451) true % 0.83/1.03 (iext $_451 uri_rdfs_Datatype uri_rdfs_Datatype) true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_451) true % 0.83/1.03 (iext $_451 uri_rdfs_Datatype uri_rdfs_Resource) true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_451) true % 0.83/1.03 (iext $_451 uri_rdfs_Literal uri_rdfs_Literal) true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_451) true % 0.83/1.03 (iext $_451 uri_rdfs_Literal uri_rdfs_Resource) true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_451) true % 0.83/1.03 (iext $_451 uri_rdfs_Resource uri_rdfs_Resource) true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_451) true % 0.83/1.03 (iext $_451 uri_rdfs_Seq uri_rdfs_Container) true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_451) true % 0.83/1.03 (iext $_451 uri_rdfs_Seq uri_rdfs_Resource) true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_451) true % 0.83/1.03 (iext $_451 uri_rdfs_Seq uri_rdfs_Seq) true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_451) true % 0.83/1.03 (iext $_451 uri_rdfs_Statement uri_rdfs_Resource) true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subClassOf $_451) true % 0.83/1.03 (iext $_451 uri_rdfs_Statement uri_rdfs_Statement) true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_451) true % 0.83/1.03 (iext $_451 uri_owl_complementOf uri_owl_complementOf) true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_451) true % 0.83/1.03 (iext $_451 uri_owl_intersectionOf uri_owl_intersectionOf) true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_451) true % 0.83/1.03 (iext $_451 uri_rdf__1 uri_rdf__1) true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_451) true % 0.83/1.03 (iext $_451 uri_rdf__1 uri_rdfs_member) true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_451) true % 0.83/1.03 (iext $_451 uri_rdf__2 uri_rdf__2) true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_451) true % 0.83/1.03 (iext $_451 uri_rdf__2 uri_rdfs_member) true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_451) true % 0.83/1.03 (iext $_451 uri_rdf__3 uri_rdf__3) true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_451) true % 0.83/1.03 (iext $_451 uri_rdf__3 uri_rdfs_member) true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_451) true % 0.83/1.03 (iext $_451 uri_rdf_first uri_rdf_first) true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_451) true % 0.83/1.03 (iext $_451 uri_rdf_object uri_rdf_object) true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_451) true % 0.83/1.03 (iext $_451 uri_rdf_predicate uri_rdf_predicate) true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_451) true % 0.83/1.03 (iext $_451 uri_rdf_rest uri_rdf_rest) true = true % 0.83/1.03 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_451) true % 0.83/1.03 (iext $_451 uri_rdf_subject uri_rdf_subject) true = true % 0.83/1.04 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_451) true % 0.83/1.04 (iext $_451 uri_rdf_type uri_rdf_type) true = true % 0.83/1.04 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_451) true % 0.83/1.04 (iext $_451 uri_rdf_value uri_rdf_value) true = true % 0.83/1.04 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_451) true % 0.83/1.04 (iext $_451 uri_rdfs_comment uri_rdfs_comment) true = true % 0.83/1.04 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_451) true % 0.83/1.04 (iext $_451 uri_rdfs_domain uri_rdfs_domain) true = true % 0.83/1.04 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_451) true % 0.83/1.04 (iext $_451 uri_rdfs_isDefinedBy uri_rdfs_isDefinedBy) true = true % 0.83/1.04 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_451) true % 0.83/1.04 (iext $_451 uri_rdfs_isDefinedBy uri_rdfs_seeAlso) true = true % 0.83/1.04 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_451) true % 0.83/1.04 (iext $_451 uri_rdfs_label uri_rdfs_label) true = true % 0.83/1.04 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_451) true % 0.83/1.04 (iext $_451 uri_rdfs_member uri_rdfs_member) true = true % 0.83/1.04 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_451) true % 0.83/1.04 (iext $_451 uri_rdfs_range uri_rdfs_range) true = true % 0.83/1.04 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_451) true % 0.83/1.04 (iext $_451 uri_rdfs_seeAlso uri_rdfs_seeAlso) true = true % 0.83/1.04 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_451) true % 0.83/1.04 (iext $_451 uri_rdfs_subClassOf uri_rdfs_subClassOf) true = true % 0.83/1.04 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf $_451) true % 0.83/1.04 (iext $_451 uri_rdfs_subPropertyOf uri_rdfs_subPropertyOf) true = true % 0.83/1.04 |- ifeq (iext uri_owl_complementOf $_452 $_453) true % 0.83/1.04 (iext uri_owl_complementOf $_452 $_453) true = true % 0.83/1.04 |- ifeq (iext uri_owl_intersectionOf $_452 $_453) true % 0.83/1.04 (iext uri_owl_intersectionOf $_452 $_453) true = true % 0.83/1.04 |- ifeq (iext uri_rdf__1 $_452 $_453) true (iext uri_rdf__1 $_452 $_453) % 0.83/1.04 true = true % 0.83/1.04 |- ifeq (iext uri_rdf__1 $_452 $_453) true % 0.83/1.04 (iext uri_rdfs_member $_452 $_453) true = true % 0.83/1.04 |- ifeq (iext uri_rdf__2 $_452 $_453) true (iext uri_rdf__2 $_452 $_453) % 0.83/1.04 true = true % 0.83/1.04 |- ifeq (iext uri_rdf__2 $_452 $_453) true % 0.83/1.04 (iext uri_rdfs_member $_452 $_453) true = true % 0.83/1.04 |- ifeq (iext uri_rdf__3 $_452 $_453) true (iext uri_rdf__3 $_452 $_453) % 0.83/1.04 true = true % 0.83/1.04 |- ifeq (iext uri_rdf__3 $_452 $_453) true % 0.83/1.04 (iext uri_rdfs_member $_452 $_453) true = true % 0.83/1.04 |- ifeq (iext uri_rdf_first $_452 $_453) true % 0.83/1.04 (iext uri_rdf_first $_452 $_453) true = true % 0.83/1.04 |- ifeq (iext uri_rdf_object $_452 $_453) true % 0.83/1.04 (iext uri_rdf_object $_452 $_453) true = true % 0.83/1.04 |- ifeq (iext uri_rdf_predicate $_452 $_453) true % 0.83/1.04 (iext uri_rdf_predicate $_452 $_453) true = true % 0.83/1.04 |- ifeq (iext uri_rdf_rest $_452 $_453) true % 0.83/1.04 (iext uri_rdf_rest $_452 $_453) true = true % 0.83/1.04 |- ifeq (iext uri_rdf_subject $_452 $_453) true % 0.83/1.04 (iext uri_rdf_subject $_452 $_453) true = true % 0.83/1.04 |- ifeq (iext uri_rdf_type $_452 $_453) true % 0.83/1.04 (iext uri_rdf_type $_452 $_453) true = true % 0.83/1.04 |- ifeq (iext uri_rdf_value $_452 $_453) true % 0.83/1.04 (iext uri_rdf_value $_452 $_453) true = true % 0.83/1.04 |- ifeq (iext uri_rdfs_comment $_452 $_453) true % 0.83/1.04 (iext uri_rdfs_comment $_452 $_453) true = true % 0.83/1.04 |- ifeq (iext uri_rdfs_domain $_452 $_453) true % 0.83/1.04 (iext uri_rdfs_domain $_452 $_453) true = true % 0.83/1.04 |- ifeq (iext uri_rdfs_isDefinedBy $_452 $_453) true % 0.83/1.04 (iext uri_rdfs_isDefinedBy $_452 $_453) true = true % 0.83/1.04 |- ifeq (iext uri_rdfs_isDefinedBy $_452 $_453) true % 0.83/1.04 (iext uri_rdfs_seeAlso $_452 $_453) true = true % 0.83/1.04 |- ifeq (iext uri_rdfs_label $_452 $_453) true % 0.83/1.04 (iext uri_rdfs_label $_452 $_453) true = true % 0.83/1.04 |- ifeq (iext uri_rdfs_member $_452 $_453) true % 0.83/1.04 (iext uri_rdfs_member $_452 $_453) true = true % 0.83/1.04 |- ifeq (iext uri_rdfs_range $_452 $_453) true % 0.83/1.04 (iext uri_rdfs_range $_452 $_453) true = true % 0.83/1.04 |- ifeq (iext uri_rdfs_seeAlso $_452 $_453) true % 0.83/1.04 (iext uri_rdfs_seeAlso $_452 $_453) true = true % 0.83/1.04 |- ifeq (iext uri_rdfs_subClassOf $_452 $_453) true % 0.83/1.04 (iext uri_rdfs_subClassOf $_452 $_453) true = true % 0.83/1.04 |- ifeq (iext uri_rdfs_subPropertyOf $_452 $_453) true % 0.83/1.04 (iext uri_rdfs_subPropertyOf $_452 $_453) true = true % 0.83/1.04 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_member $_998) true % 0.83/1.04 (iext uri_rdfs_subPropertyOf uri_rdf__1 $_998) true = true % 0.83/1.04 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_member $_998) true % 0.83/1.04 (iext uri_rdfs_subPropertyOf uri_rdf__2 $_998) true = true % 0.83/1.04 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_member $_998) true % 0.83/1.04 (iext uri_rdfs_subPropertyOf uri_rdf__3 $_998) true = true % 0.83/1.04 |- ifeq (iext uri_rdfs_subPropertyOf uri_rdfs_seeAlso $_998) true % 0.83/1.04 (iext uri_rdfs_subPropertyOf uri_rdfs_isDefinedBy $_998) true = true % 0.83/1.04 |- ifeq (iext uri_rdfs_subPropertyOf $_996 uri_rdf__1) true % 0.83/1.04 (iext uri_rdfs_subPropertyOf $_996 uri_rdfs_member) true = true % 0.83/1.04 |- ifeq (iext uri_rdfs_subPropertyOf $_996 uri_rdf__2) true % 0.83/1.04 (iext uri_rdfs_subPropertyOf $_996 uri_rdfs_member) true = true % 0.83/1.04 |- ifeq (iext uri_rdfs_subPropertyOf $_996 uri_rdf__3) true % 0.83/1.04 (iext uri_rdfs_subPropertyOf $_996 uri_rdfs_member) true = true % 0.83/1.04 |- ifeq (iext uri_rdfs_subPropertyOf $_996 uri_rdfs_isDefinedBy) true % 0.83/1.04 (iext uri_rdfs_subPropertyOf $_996 uri_rdfs_seeAlso) true = true % 0.83/1.04 SZS output end Saturation for /export/starexec/sandbox2/benchmark/theBenchmark.p % 0.83/1.04 %------------------------------------------------------------------------------