%------------------------------------------------------------------------------
% File : ConnectPP---0.7.2
% Problem : SWB001+3 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n009.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Thu Sep 24 09:00:51 AM UTC 2026
% Result : Theorem 0.25s 0.53s
% Output : Proof 0.25s
% Verified :
% SZS Type : ERROR: Analysing output (MakeTreeStats fails)
% Comments :
%------------------------------------------------------------------------------
fof(owl_bool_complementof_class,axiom,
! [Z,C] :
( iext(uri_owl_complementOf,Z,C)
=> ( ! [X] :
( icext(Z,X)
<=> ~ icext(C,X) )
& ic(C)
& ic(Z) ) ),
file('SWB002+0.ax',owl_bool_complementof_class) ).
fof(owl_bool_intersectionof_class_000,axiom,
! [Z] :
( iext(uri_owl_intersectionOf,Z,uri_rdf_nil)
<=> ( ! [X] :
( icext(Z,X)
<=> ir(X) )
& ic(Z) ) ),
file('SWB002+0.ax',owl_bool_intersectionof_class_000) ).
fof(owl_bool_intersectionof_class_001,axiom,
! [Z,S1,C1] :
( ( iext(uri_rdf_rest,S1,uri_rdf_nil)
& iext(uri_rdf_first,S1,C1) )
=> ( iext(uri_owl_intersectionOf,Z,S1)
<=> ( ! [X] :
( icext(Z,X)
<=> icext(C1,X) )
& ic(C1)
& ic(Z) ) ) ),
file('SWB002+0.ax',owl_bool_intersectionof_class_001) ).
fof(owl_bool_intersectionof_class_002,axiom,
! [Z,S1,C1,S2,C2] :
( ( iext(uri_rdf_rest,S2,uri_rdf_nil)
& iext(uri_rdf_first,S2,C2)
& iext(uri_rdf_rest,S1,S2)
& iext(uri_rdf_first,S1,C1) )
=> ( iext(uri_owl_intersectionOf,Z,S1)
<=> ( ! [X] :
( icext(Z,X)
<=> ( icext(C2,X)
& icext(C1,X) ) )
& ic(C2)
& ic(C1)
& ic(Z) ) ) ),
file('SWB002+0.ax',owl_bool_intersectionof_class_002) ).
fof(owl_bool_intersectionof_class_003,axiom,
! [Z,S1,C1,S2,C2,S3,C3] :
( ( iext(uri_rdf_rest,S3,uri_rdf_nil)
& iext(uri_rdf_first,S3,C3)
& iext(uri_rdf_rest,S2,S3)
& iext(uri_rdf_first,S2,C2)
& iext(uri_rdf_rest,S1,S2)
& iext(uri_rdf_first,S1,C1) )
=> ( iext(uri_owl_intersectionOf,Z,S1)
<=> ( ! [X] :
( icext(Z,X)
<=> ( icext(C3,X)
& icext(C2,X)
& icext(C1,X) ) )
& ic(C3)
& ic(C2)
& ic(C1)
& ic(Z) ) ) ),
file('SWB002+0.ax',owl_bool_intersectionof_class_003) ).
fof(owl_bool_unionof_class_000,axiom,
! [Z] :
( iext(uri_owl_unionOf,Z,uri_rdf_nil)
<=> ( ! [X] : ~ icext(Z,X)
& ic(Z) ) ),
file('SWB002+0.ax',owl_bool_unionof_class_000) ).
fof(owl_bool_unionof_class_001,axiom,
! [Z,S1,C1] :
( ( iext(uri_rdf_rest,S1,uri_rdf_nil)
& iext(uri_rdf_first,S1,C1) )
=> ( iext(uri_owl_unionOf,Z,S1)
<=> ( ! [X] :
( icext(Z,X)
<=> icext(C1,X) )
& ic(C1)
& ic(Z) ) ) ),
file('SWB002+0.ax',owl_bool_unionof_class_001) ).
fof(owl_bool_unionof_class_002,axiom,
! [Z,S1,C1,S2,C2] :
( ( iext(uri_rdf_rest,S2,uri_rdf_nil)
& iext(uri_rdf_first,S2,C2)
& iext(uri_rdf_rest,S1,S2)
& iext(uri_rdf_first,S1,C1) )
=> ( iext(uri_owl_unionOf,Z,S1)
<=> ( ! [X] :
( icext(Z,X)
<=> ( icext(C2,X)
| icext(C1,X) ) )
& ic(C2)
& ic(C1)
& ic(Z) ) ) ),
file('SWB002+0.ax',owl_bool_unionof_class_002) ).
fof(owl_bool_unionof_class_003,axiom,
! [Z,S1,C1,S2,C2,S3,C3] :
( ( iext(uri_rdf_rest,S3,uri_rdf_nil)
& iext(uri_rdf_first,S3,C3)
& iext(uri_rdf_rest,S2,S3)
& iext(uri_rdf_first,S2,C2)
& iext(uri_rdf_rest,S1,S2)
& iext(uri_rdf_first,S1,C1) )
=> ( iext(uri_owl_unionOf,Z,S1)
<=> ( ! [X] :
( icext(Z,X)
<=> ( icext(C3,X)
| icext(C2,X)
| icext(C1,X) ) )
& ic(C3)
& ic(C2)
& ic(C1)
& ic(Z) ) ) ),
file('SWB002+0.ax',owl_bool_unionof_class_003) ).
fof(owl_class_nothing_ext,axiom,
! [X] : ~ icext(uri_owl_Nothing,X),
file('SWB002+0.ax',owl_class_nothing_ext) ).
fof(owl_class_nothing_type,axiom,
ic(uri_owl_Nothing),
file('SWB002+0.ax',owl_class_nothing_type) ).
fof(owl_class_thing_ext,axiom,
! [X] :
( icext(uri_owl_Thing,X)
<=> ir(X) ),
file('SWB002+0.ax',owl_class_thing_ext) ).
fof(owl_class_thing_type,axiom,
ic(uri_owl_Thing),
file('SWB002+0.ax',owl_class_thing_type) ).
fof(owl_parts_ic_cond_inst,axiom,
! [X] :
( ic(X)
=> ! [Y] :
( icext(X,Y)
=> ir(Y) ) ),
file('SWB002+0.ax',owl_parts_ic_cond_inst) ).
fof(owl_parts_ic_cond_set,axiom,
! [X] :
( ic(X)
=> ir(X) ),
file('SWB002+0.ax',owl_parts_ic_cond_set) ).
fof(owl_parts_ic_def,axiom,
! [X] :
( ic(X)
<=> iext(uri_rdf_type,X,uri_rdfs_Class) ),
file('SWB002+0.ax',owl_parts_ic_def) ).
fof(owl_parts_idc_cond_inst,axiom,
! [X] :
( idc(X)
=> ! [Y] :
( icext(X,Y)
=> lv(Y) ) ),
file('SWB002+0.ax',owl_parts_idc_cond_inst) ).
fof(owl_parts_idc_cond_set,axiom,
! [X] :
( idc(X)
=> ic(X) ),
file('SWB002+0.ax',owl_parts_idc_cond_set) ).
fof(owl_parts_idc_def,axiom,
! [X] :
( idc(X)
<=> iext(uri_rdf_type,X,uri_rdfs_Datatype) ),
file('SWB002+0.ax',owl_parts_idc_def) ).
fof(owl_parts_ioap_cond_inst,axiom,
! [X] :
( ioap(X)
=> ! [Y,Z] :
( iext(X,Y,Z)
=> ( ir(Z)
& ir(Y) ) ) ),
file('SWB002+0.ax',owl_parts_ioap_cond_inst) ).
fof(owl_parts_ioap_cond_set,axiom,
! [X] :
( ioap(X)
=> ip(X) ),
file('SWB002+0.ax',owl_parts_ioap_cond_set) ).
fof(owl_parts_ioap_def,axiom,
! [X] :
( ioap(X)
<=> iext(uri_rdf_type,X,uri_owl_AnnotationProperty) ),
file('SWB002+0.ax',owl_parts_ioap_def) ).
fof(owl_parts_iodp_cond_inst,axiom,
! [X] :
( iodp(X)
=> ! [Y,Z] :
( iext(X,Y,Z)
=> ( lv(Z)
& ir(Y) ) ) ),
file('SWB002+0.ax',owl_parts_iodp_cond_inst) ).
fof(owl_parts_iodp_cond_set,axiom,
! [X] :
( iodp(X)
=> ip(X) ),
file('SWB002+0.ax',owl_parts_iodp_cond_set) ).
fof(owl_parts_iodp_def,axiom,
! [X] :
( iodp(X)
<=> iext(uri_rdf_type,X,uri_owl_DatatypeProperty) ),
file('SWB002+0.ax',owl_parts_iodp_def) ).
fof(owl_parts_ioxp_cond_inst,axiom,
! [X] :
( ioxp(X)
=> ! [Y,Z] :
( iext(X,Y,Z)
=> ( ix(Z)
& ix(Y) ) ) ),
file('SWB002+0.ax',owl_parts_ioxp_cond_inst) ).
fof(owl_parts_ioxp_cond_set,axiom,
! [X] :
( ioxp(X)
=> ip(X) ),
file('SWB002+0.ax',owl_parts_ioxp_cond_set) ).
fof(owl_parts_ioxp_def,axiom,
! [X] :
( ioxp(X)
<=> iext(uri_rdf_type,X,uri_owl_OntologyProperty) ),
file('SWB002+0.ax',owl_parts_ioxp_def) ).
fof(owl_parts_ip_cond_inst,axiom,
! [X] :
( ip(X)
=> ! [Y,Z] :
( iext(X,Y,Z)
=> ( ir(Z)
& ir(Y) ) ) ),
file('SWB002+0.ax',owl_parts_ip_cond_inst) ).
fof(owl_parts_ip_cond_set,axiom,
! [X] :
( ip(X)
=> ir(X) ),
file('SWB002+0.ax',owl_parts_ip_cond_set) ).
fof(owl_parts_ip_def,axiom,
! [X] :
( ip(X)
<=> iext(uri_rdf_type,X,uri_rdf_Property) ),
file('SWB002+0.ax',owl_parts_ip_def) ).
fof(owl_parts_ir_cond_set,axiom,
? [X] : ir(X),
file('SWB002+0.ax',owl_parts_ir_cond_set) ).
fof(owl_parts_ir_def,axiom,
! [X] :
( ir(X)
<=> iext(uri_rdf_type,X,uri_rdfs_Resource) ),
file('SWB002+0.ax',owl_parts_ir_def) ).
fof(owl_parts_ix_cond_set,axiom,
! [X] :
( ix(X)
=> ir(X) ),
file('SWB002+0.ax',owl_parts_ix_cond_set) ).
fof(owl_parts_ix_def,axiom,
! [X] :
( ix(X)
<=> iext(uri_rdf_type,X,uri_owl_Ontology) ),
file('SWB002+0.ax',owl_parts_ix_def) ).
fof(owl_parts_lv_cond_set,axiom,
! [X] :
( lv(X)
=> ir(X) ),
file('SWB002+0.ax',owl_parts_lv_cond_set) ).
fof(owl_parts_lv_def,axiom,
! [X] :
( lv(X)
<=> iext(uri_rdf_type,X,uri_rdfs_Literal) ),
file('SWB002+0.ax',owl_parts_lv_def) ).
fof(owl_prop_allvaluesfrom_ext,axiom,
! [X,Y] :
( iext(uri_owl_allValuesFrom,X,Y)
=> ( ic(Y)
& icext(uri_owl_Restriction,X) ) ),
file('SWB002+0.ax',owl_prop_allvaluesfrom_ext) ).
fof(owl_prop_allvaluesfrom_type,axiom,
ip(uri_owl_allValuesFrom),
file('SWB002+0.ax',owl_prop_allvaluesfrom_type) ).
fof(owl_prop_complementof_ext,axiom,
! [X,Y] :
( iext(uri_owl_complementOf,X,Y)
=> ( ic(Y)
& ic(X) ) ),
file('SWB002+0.ax',owl_prop_complementof_ext) ).
fof(owl_prop_complementof_type,axiom,
ip(uri_owl_complementOf),
file('SWB002+0.ax',owl_prop_complementof_type) ).
fof(owl_prop_hasvalue_ext,axiom,
! [X,Y] :
( iext(uri_owl_hasValue,X,Y)
=> ( ir(Y)
& icext(uri_owl_Restriction,X) ) ),
file('SWB002+0.ax',owl_prop_hasvalue_ext) ).
fof(owl_prop_hasvalue_type,axiom,
ip(uri_owl_hasValue),
file('SWB002+0.ax',owl_prop_hasvalue_type) ).
fof(owl_prop_intersectionof_ext,axiom,
! [X,Y] :
( iext(uri_owl_intersectionOf,X,Y)
=> ( icext(uri_rdf_List,Y)
& ic(X) ) ),
file('SWB002+0.ax',owl_prop_intersectionof_ext) ).
fof(owl_prop_intersectionof_type,axiom,
ip(uri_owl_intersectionOf),
file('SWB002+0.ax',owl_prop_intersectionof_type) ).
fof(owl_prop_onproperty_ext,axiom,
! [X,Y] :
( iext(uri_owl_onProperty,X,Y)
=> ( ip(Y)
& icext(uri_owl_Restriction,X) ) ),
file('SWB002+0.ax',owl_prop_onproperty_ext) ).
fof(owl_prop_onproperty_type,axiom,
ip(uri_owl_onProperty),
file('SWB002+0.ax',owl_prop_onproperty_type) ).
fof(owl_prop_somevaluesfrom_ext,axiom,
! [X,Y] :
( iext(uri_owl_someValuesFrom,X,Y)
=> ( ic(Y)
& icext(uri_owl_Restriction,X) ) ),
file('SWB002+0.ax',owl_prop_somevaluesfrom_ext) ).
fof(owl_prop_somevaluesfrom_type,axiom,
ip(uri_owl_someValuesFrom),
file('SWB002+0.ax',owl_prop_somevaluesfrom_type) ).
fof(owl_prop_unionof_ext,axiom,
! [X,Y] :
( iext(uri_owl_unionOf,X,Y)
=> ( icext(uri_rdf_List,Y)
& ic(X) ) ),
file('SWB002+0.ax',owl_prop_unionof_ext) ).
fof(owl_prop_unionof_type,axiom,
ip(uri_owl_unionOf),
file('SWB002+0.ax',owl_prop_unionof_type) ).
fof(owl_rdfsext_domain,axiom,
! [P,C] :
( iext(uri_rdfs_domain,P,C)
<=> ( ! [X,Y] :
( iext(P,X,Y)
=> icext(C,X) )
& ic(C)
& ip(P) ) ),
file('SWB002+0.ax',owl_rdfsext_domain) ).
fof(owl_rdfsext_range,axiom,
! [P,C] :
( iext(uri_rdfs_range,P,C)
<=> ( ! [X,Y] :
( iext(P,X,Y)
=> icext(C,Y) )
& ip(C)
& ip(P) ) ),
file('SWB002+0.ax',owl_rdfsext_range) ).
fof(owl_rdfsext_subclassof,axiom,
! [C1,C2] :
( iext(uri_rdfs_subClassOf,C1,C2)
<=> ( ! [X] :
( icext(C1,X)
=> icext(C2,X) )
& ic(C2)
& ic(C1) ) ),
file('SWB002+0.ax',owl_rdfsext_subclassof) ).
fof(owl_rdfsext_subpropertyof,axiom,
! [P1,P2] :
( iext(uri_rdfs_subPropertyOf,P1,P2)
<=> ( ! [X,Y] :
( iext(P1,X,Y)
=> iext(P2,X,Y) )
& ip(P2)
& ip(P1) ) ),
file('SWB002+0.ax',owl_rdfsext_subpropertyof) ).
fof(owl_restrict_allvaluesfrom,axiom,
! [Z,P,C] :
( ( iext(uri_owl_onProperty,Z,P)
& iext(uri_owl_allValuesFrom,Z,C) )
=> ! [X] :
( icext(Z,X)
<=> ! [Y] :
( iext(P,X,Y)
=> icext(C,Y) ) ) ),
file('SWB002+0.ax',owl_restrict_allvaluesfrom) ).
fof(owl_restrict_hasvalue,axiom,
! [Z,P,A] :
( ( iext(uri_owl_onProperty,Z,P)
& iext(uri_owl_hasValue,Z,A) )
=> ! [X] :
( icext(Z,X)
<=> iext(P,X,A) ) ),
file('SWB002+0.ax',owl_restrict_hasvalue) ).
fof(owl_restrict_somevaluesfrom,axiom,
! [Z,P,C] :
( ( iext(uri_owl_onProperty,Z,P)
& iext(uri_owl_someValuesFrom,Z,C) )
=> ! [X] :
( icext(Z,X)
<=> ? [Y] :
( icext(C,Y)
& iext(P,X,Y) ) ) ),
file('SWB002+0.ax',owl_restrict_somevaluesfrom) ).
fof(rdf_collection_first_type,axiom,
iext(uri_rdf_type,uri_rdf_first,uri_rdf_Property),
file('SWB002+0.ax',rdf_collection_first_type) ).
fof(rdf_collection_nil_type,axiom,
iext(uri_rdf_type,uri_rdf_nil,uri_rdf_List),
file('SWB002+0.ax',rdf_collection_nil_type) ).
fof(rdf_collection_rest_type,axiom,
iext(uri_rdf_type,uri_rdf_rest,uri_rdf_Property),
file('SWB002+0.ax',rdf_collection_rest_type) ).
fof(rdf_container_n_type_001,axiom,
iext(uri_rdf_type,uri_rdf__1,uri_rdf_Property),
file('SWB002+0.ax',rdf_container_n_type_001) ).
fof(rdf_container_n_type_002,axiom,
iext(uri_rdf_type,uri_rdf__2,uri_rdf_Property),
file('SWB002+0.ax',rdf_container_n_type_002) ).
fof(rdf_container_n_type_003,axiom,
iext(uri_rdf_type,uri_rdf__3,uri_rdf_Property),
file('SWB002+0.ax',rdf_container_n_type_003) ).
fof(rdf_reification_object_type,axiom,
iext(uri_rdf_type,uri_rdf_object,uri_rdf_Property),
file('SWB002+0.ax',rdf_reification_object_type) ).
fof(rdf_reification_predicate_type,axiom,
iext(uri_rdf_type,uri_rdf_value,uri_rdf_Property),
file('SWB002+0.ax',rdf_reification_predicate_type) ).
fof(rdf_reification_subject_type,axiom,
iext(uri_rdf_type,uri_rdf_subject,uri_rdf_Property),
file('SWB002+0.ax',rdf_reification_subject_type) ).
fof(rdf_type_ip,axiom,
! [P] :
( iext(uri_rdf_type,P,uri_rdf_Property)
<=> ip(P) ),
file('SWB002+0.ax',rdf_type_ip) ).
fof(rdf_type_type,axiom,
iext(uri_rdf_type,uri_rdf_type,uri_rdf_Property),
file('SWB002+0.ax',rdf_type_type) ).
fof(rdf_value_type,axiom,
iext(uri_rdf_type,uri_rdf_type,uri_rdf_Property),
file('SWB002+0.ax',rdf_value_type) ).
fof(rdfs_annotation_comment_domain,axiom,
iext(uri_rdfs_domain,uri_rdfs_comment,uri_rdfs_Resource),
file('SWB002+0.ax',rdfs_annotation_comment_domain) ).
fof(rdfs_annotation_comment_range,axiom,
iext(uri_rdfs_range,uri_rdfs_comment,uri_rdfs_Literal),
file('SWB002+0.ax',rdfs_annotation_comment_range) ).
fof(rdfs_annotation_isdefinedby_domain,axiom,
iext(uri_rdfs_domain,uri_rdfs_isDefinedBy,uri_rdfs_Resource),
file('SWB002+0.ax',rdfs_annotation_isdefinedby_domain) ).
fof(rdfs_annotation_isdefinedby_range,axiom,
iext(uri_rdfs_range,uri_rdfs_isDefinedBy,uri_rdfs_Resource),
file('SWB002+0.ax',rdfs_annotation_isdefinedby_range) ).
fof(rdfs_annotation_isdefinedby_sub,axiom,
iext(uri_rdfs_subPropertyOf,uri_rdfs_isDefinedBy,uri_rdfs_seeAlso),
file('SWB002+0.ax',rdfs_annotation_isdefinedby_sub) ).
fof(rdfs_annotation_label_domain,axiom,
iext(uri_rdfs_domain,uri_rdfs_label,uri_rdfs_Resource),
file('SWB002+0.ax',rdfs_annotation_label_domain) ).
fof(rdfs_annotation_label_range,axiom,
iext(uri_rdfs_range,uri_rdfs_label,uri_rdfs_Literal),
file('SWB002+0.ax',rdfs_annotation_label_range) ).
fof(rdfs_annotation_seealso_domain,axiom,
iext(uri_rdfs_domain,uri_rdfs_seeAlso,uri_rdfs_Resource),
file('SWB002+0.ax',rdfs_annotation_seealso_domain) ).
fof(rdfs_annotation_seealso_range,axiom,
iext(uri_rdfs_range,uri_rdfs_seeAlso,uri_rdfs_Resource),
file('SWB002+0.ax',rdfs_annotation_seealso_range) ).
fof(rdfs_cext_def,axiom,
! [X,C] :
( iext(uri_rdf_type,X,C)
<=> icext(C,X) ),
file('SWB002+0.ax',rdfs_cext_def) ).
fof(rdfs_class_instsub_resource,axiom,
! [C] :
( ic(C)
=> iext(uri_rdfs_subClassOf,C,uri_rdfs_Resource) ),
file('SWB002+0.ax',rdfs_class_instsub_resource) ).
fof(rdfs_collection_first_domain,axiom,
iext(uri_rdfs_domain,uri_rdf_first,uri_rdf_List),
file('SWB002+0.ax',rdfs_collection_first_domain) ).
fof(rdfs_collection_first_range,axiom,
iext(uri_rdfs_range,uri_rdf_first,uri_rdfs_Resource),
file('SWB002+0.ax',rdfs_collection_first_range) ).
fof(rdfs_collection_rest_domain,axiom,
iext(uri_rdfs_domain,uri_rdf_rest,uri_rdf_List),
file('SWB002+0.ax',rdfs_collection_rest_domain) ).
fof(rdfs_collection_rest_range,axiom,
iext(uri_rdfs_range,uri_rdf_rest,uri_rdf_List),
file('SWB002+0.ax',rdfs_collection_rest_range) ).
fof(rdfs_container_alt_sub,axiom,
iext(uri_rdfs_subClassOf,uri_rdf_Alt,uri_rdfs_Container),
file('SWB002+0.ax',rdfs_container_alt_sub) ).
fof(rdfs_container_bag_sub,axiom,
iext(uri_rdfs_subClassOf,uri_rdf_Bag,uri_rdfs_Container),
file('SWB002+0.ax',rdfs_container_bag_sub) ).
fof(rdfs_container_containermembershipproperty_instsub_member,axiom,
! [P] :
( icext(uri_rdfs_ContainerMembershipProperty,P)
=> iext(uri_rdfs_subPropertyOf,P,uri_rdfs_member) ),
file('SWB002+0.ax',rdfs_container_containermembershipproperty_instsub_member) ).
fof(rdfs_container_containermembershipproperty_sub,axiom,
iext(uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty,uri_rdf_Property),
file('SWB002+0.ax',rdfs_container_containermembershipproperty_sub) ).
fof(rdfs_container_member_domain,axiom,
iext(uri_rdfs_domain,uri_rdfs_member,uri_rdfs_Resource),
file('SWB002+0.ax',rdfs_container_member_domain) ).
fof(rdfs_container_member_range,axiom,
iext(uri_rdfs_range,uri_rdfs_member,uri_rdfs_Resource),
file('SWB002+0.ax',rdfs_container_member_range) ).
fof(rdfs_container_n_domain_001,axiom,
iext(uri_rdfs_domain,uri_rdf__1,uri_rdfs_Resource),
file('SWB002+0.ax',rdfs_container_n_domain_001) ).
fof(rdfs_container_n_domain_002,axiom,
iext(uri_rdfs_domain,uri_rdf__2,uri_rdfs_Resource),
file('SWB002+0.ax',rdfs_container_n_domain_002) ).
fof(rdfs_container_n_domain_003,axiom,
iext(uri_rdfs_domain,uri_rdf__3,uri_rdfs_Resource),
file('SWB002+0.ax',rdfs_container_n_domain_003) ).
fof(rdfs_container_n_range_001,axiom,
iext(uri_rdfs_range,uri_rdf__1,uri_rdfs_Resource),
file('SWB002+0.ax',rdfs_container_n_range_001) ).
fof(rdfs_container_n_range_002,axiom,
iext(uri_rdfs_range,uri_rdf__2,uri_rdfs_Resource),
file('SWB002+0.ax',rdfs_container_n_range_002) ).
fof(rdfs_container_n_range_003,axiom,
iext(uri_rdfs_range,uri_rdf__3,uri_rdfs_Resource),
file('SWB002+0.ax',rdfs_container_n_range_003) ).
fof(rdfs_container_n_type_001,axiom,
iext(uri_rdf_type,uri_rdf__1,uri_rdfs_ContainerMembershipProperty),
file('SWB002+0.ax',rdfs_container_n_type_001) ).
fof(rdfs_container_n_type_002,axiom,
iext(uri_rdf_type,uri_rdf__2,uri_rdfs_ContainerMembershipProperty),
file('SWB002+0.ax',rdfs_container_n_type_002) ).
fof(rdfs_container_n_type_003,axiom,
iext(uri_rdf_type,uri_rdf__3,uri_rdfs_ContainerMembershipProperty),
file('SWB002+0.ax',rdfs_container_n_type_003) ).
fof(rdfs_container_seq_sub,axiom,
iext(uri_rdfs_subClassOf,uri_rdfs_Seq,uri_rdfs_Container),
file('SWB002+0.ax',rdfs_container_seq_sub) ).
fof(rdfs_dat_xmlliteral_sub,axiom,
iext(uri_rdfs_subClassOf,uri_rdf_XMLLiteral,uri_rdfs_Literal),
file('SWB002+0.ax',rdfs_dat_xmlliteral_sub) ).
fof(rdfs_dat_xmlliteral_type,axiom,
iext(uri_rdf_type,uri_rdf_XMLLiteral,uri_rdfs_Datatype),
file('SWB002+0.ax',rdfs_dat_xmlliteral_type) ).
fof(rdfs_datatype_instsub_literal,axiom,
! [D] :
( icext(uri_rdfs_Datatype,D)
=> iext(uri_rdfs_subClassOf,D,uri_rdfs_Literal) ),
file('SWB002+0.ax',rdfs_datatype_instsub_literal) ).
fof(rdfs_datatype_sub,axiom,
iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,uri_rdfs_Class),
file('SWB002+0.ax',rdfs_datatype_sub) ).
fof(rdfs_domain_domain,axiom,
iext(uri_rdfs_domain,uri_rdfs_domain,uri_rdf_Property),
file('SWB002+0.ax',rdfs_domain_domain) ).
fof(rdfs_domain_main,axiom,
! [P,C,X,Y] :
( ( iext(P,X,Y)
& iext(uri_rdfs_domain,P,C) )
=> icext(C,X) ),
file('SWB002+0.ax',rdfs_domain_main) ).
fof(rdfs_domain_range,axiom,
iext(uri_rdfs_range,uri_rdfs_domain,uri_rdfs_Class),
file('SWB002+0.ax',rdfs_domain_range) ).
fof(rdfs_ic_def,axiom,
! [X] :
( ic(X)
<=> icext(uri_rdfs_Class,X) ),
file('SWB002+0.ax',rdfs_ic_def) ).
fof(rdfs_ir_def,axiom,
! [X] :
( ir(X)
<=> icext(uri_rdfs_Resource,X) ),
file('SWB002+0.ax',rdfs_ir_def) ).
fof(rdfs_lv_def,axiom,
! [X] :
( lv(X)
<=> icext(uri_rdfs_Literal,X) ),
file('SWB002+0.ax',rdfs_lv_def) ).
fof(rdfs_property_type,axiom,
iext(uri_rdf_type,uri_rdf_Property,uri_rdfs_Class),
file('SWB002+0.ax',rdfs_property_type) ).
fof(rdfs_range_domain,axiom,
iext(uri_rdfs_domain,uri_rdfs_range,uri_rdf_Property),
file('SWB002+0.ax',rdfs_range_domain) ).
fof(rdfs_range_main,axiom,
! [P,C,X,Y] :
( ( iext(P,X,Y)
& iext(uri_rdfs_range,P,C) )
=> icext(C,Y) ),
file('SWB002+0.ax',rdfs_range_main) ).
fof(rdfs_range_range,axiom,
iext(uri_rdfs_range,uri_rdfs_range,uri_rdfs_Class),
file('SWB002+0.ax',rdfs_range_range) ).
fof(rdfs_reification_object_domain,axiom,
iext(uri_rdfs_domain,uri_rdf_object,uri_rdfs_Statement),
file('SWB002+0.ax',rdfs_reification_object_domain) ).
fof(rdfs_reification_object_range,axiom,
iext(uri_rdfs_range,uri_rdf_predicate,uri_rdfs_Resource),
file('SWB002+0.ax',rdfs_reification_object_range) ).
fof(rdfs_reification_predicate_domain,axiom,
iext(uri_rdfs_domain,uri_rdf_predicate,uri_rdfs_Statement),
file('SWB002+0.ax',rdfs_reification_predicate_domain) ).
fof(rdfs_reification_predicate_range,axiom,
iext(uri_rdfs_range,uri_rdf_predicate,uri_rdfs_Resource),
file('SWB002+0.ax',rdfs_reification_predicate_range) ).
fof(rdfs_reification_subject_domain,axiom,
iext(uri_rdfs_domain,uri_rdf_subject,uri_rdfs_Statement),
file('SWB002+0.ax',rdfs_reification_subject_domain) ).
fof(rdfs_reification_subject_range,axiom,
iext(uri_rdfs_range,uri_rdf_subject,uri_rdfs_Resource),
file('SWB002+0.ax',rdfs_reification_subject_range) ).
fof(rdfs_subclassof_domain,axiom,
iext(uri_rdfs_domain,uri_rdfs_subClassOf,uri_rdfs_Class),
file('SWB002+0.ax',rdfs_subclassof_domain) ).
fof(rdfs_subclassof_main,axiom,
! [C,D] :
( iext(uri_rdfs_subClassOf,C,D)
=> ( ! [X] :
( icext(C,X)
=> icext(D,X) )
& ic(D)
& ic(C) ) ),
file('SWB002+0.ax',rdfs_subclassof_main) ).
fof(rdfs_subclassof_range,axiom,
iext(uri_rdfs_range,uri_rdfs_subClassOf,uri_rdfs_Class),
file('SWB002+0.ax',rdfs_subclassof_range) ).
fof(rdfs_subclassof_reflex,axiom,
! [C] :
( ic(C)
=> iext(uri_rdfs_subClassOf,C,C) ),
file('SWB002+0.ax',rdfs_subclassof_reflex) ).
fof(rdfs_subclassof_trans,axiom,
! [C,D,E] :
( ( iext(uri_rdfs_subClassOf,D,E)
& iext(uri_rdfs_subClassOf,C,D) )
=> iext(uri_rdfs_subClassOf,C,E) ),
file('SWB002+0.ax',rdfs_subclassof_trans) ).
fof(rdfs_subpropertyof_domain,axiom,
iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,uri_rdf_Property),
file('SWB002+0.ax',rdfs_subpropertyof_domain) ).
fof(rdfs_subpropertyof_main,axiom,
! [P,Q] :
( iext(uri_rdfs_subPropertyOf,P,Q)
=> ( ! [X,Y] :
( iext(P,X,Y)
=> iext(Q,X,Y) )
& ip(Q)
& ip(P) ) ),
file('SWB002+0.ax',rdfs_subpropertyof_main) ).
fof(rdfs_subpropertyof_range,axiom,
iext(uri_rdfs_range,uri_rdfs_subPropertyOf,uri_rdf_Property),
file('SWB002+0.ax',rdfs_subpropertyof_range) ).
fof(rdfs_subpropertyof_reflex,axiom,
! [P] :
( ip(P)
=> iext(uri_rdfs_subPropertyOf,P,P) ),
file('SWB002+0.ax',rdfs_subpropertyof_reflex) ).
fof(rdfs_subpropertyof_trans,axiom,
! [P,Q,R] :
( ( iext(uri_rdfs_subPropertyOf,Q,R)
& iext(uri_rdfs_subPropertyOf,P,Q) )
=> iext(uri_rdfs_subPropertyOf,P,R) ),
file('SWB002+0.ax',rdfs_subpropertyof_trans) ).
fof(rdfs_type_domain,axiom,
iext(uri_rdfs_domain,uri_rdf_type,uri_rdfs_Resource),
file('SWB002+0.ax',rdfs_type_domain) ).
fof(rdfs_type_range,axiom,
iext(uri_rdfs_range,uri_rdf_type,uri_rdfs_Class),
file('SWB002+0.ax',rdfs_type_range) ).
fof(rdfs_value_domain,axiom,
iext(uri_rdfs_domain,uri_rdf_value,uri_rdfs_Resource),
file('SWB002+0.ax',rdfs_value_domain) ).
fof(rdfs_value_range,axiom,
iext(uri_rdfs_range,uri_rdf_value,uri_rdfs_Resource),
file('SWB002+0.ax',rdfs_value_range) ).
fof(simple_iext_property,axiom,
! [S,P,O] :
( iext(P,S,O)
=> ip(P) ),
file('SWB002+0.ax',simple_iext_property) ).
fof(simple_ir,axiom,
! [X] : ir(X),
file('SWB002+0.ax',simple_ir) ).
fof(simple_lv,axiom,
! [X] :
( lv(X)
=> ir(X) ),
file('SWB002+0.ax',simple_lv) ).
fof(testcase_conclusion_fullish_001_Subgraph_Entailment,conjecture,
( iext(uri_owl_onProperty,uri_ex_r,uri_ex_p)
& iext(uri_rdf_type,uri_ex_r,uri_owl_Restriction) ),
file('theBenchmark.p',testcase_conclusion_fullish_001_Subgraph_Entailment) ).
fof(testcase_premise_fullish_001_Subgraph_Entailment,axiom,
( iext(uri_owl_someValuesFrom,uri_ex_r,uri_ex_d)
& iext(uri_owl_onProperty,uri_ex_r,uri_ex_p)
& iext(uri_rdf_type,uri_ex_r,uri_owl_Restriction)
& iext(uri_rdfs_subClassOf,uri_ex_c,uri_ex_r) ),
file('theBenchmark.p',testcase_premise_fullish_001_Subgraph_Entailment) ).
fof(f_1_1,plain,
! [Z,C] :
( ( ! [X] :
( ( icext(Z,X)
| icext(C,X) )
& ( ~ icext(C,X)
| ~ icext(Z,X) ) )
& ic(C)
& ic(Z) )
| ~ iext(uri_owl_complementOf,Z,C) ),
inference(fof_nnf,[status(thm)],[owl_bool_complementof_class]) ).
fof(f_1_2,plain,
! [U_2,U_1] :
( ( ! [U_0] :
( ( icext(U_2,U_0)
| icext(U_1,U_0) )
& ( ~ icext(U_1,U_0)
| ~ icext(U_2,U_0) ) )
& ic(U_1)
& ic(U_2) )
| ~ iext(uri_owl_complementOf,U_2,U_1) ),
inference(variable_rename,[status(thm)],[f_1_1]) ).
fof(f_1_3,plain,
! [U_2,U_1] :
( ( ! [U_4] :
( icext(U_2,U_4)
| icext(U_1,U_4) )
& ! [U_3] :
( ~ icext(U_1,U_3)
| ~ icext(U_2,U_3) )
& ic(U_1)
& ic(U_2) )
| ~ iext(uri_owl_complementOf,U_2,U_1) ),
inference(miniscope,[status(thm)],[f_1_2]) ).
cnf(f_1_4,plain,
( ic(U_2)
| ~ iext(uri_owl_complementOf,U_2,U_1) ),
inference(clausify,[status(thm)],[f_1_3]) ).
cnf(f_1_5,plain,
( ic(U_1)
| ~ iext(uri_owl_complementOf,U_2,U_1) ),
inference(clausify,[status(thm)],[f_1_3]) ).
cnf(f_1_6,plain,
( ~ icext(U_1,U_3)
| ~ icext(U_2,U_3)
| ~ iext(uri_owl_complementOf,U_2,U_1) ),
inference(clausify,[status(thm)],[f_1_3]) ).
cnf(f_1_7,plain,
( icext(U_2,U_4)
| icext(U_1,U_4)
| ~ iext(uri_owl_complementOf,U_2,U_1) ),
inference(clausify,[status(thm)],[f_1_3]) ).
fof(f_2_1,plain,
! [Z] :
( ( iext(uri_owl_intersectionOf,Z,uri_rdf_nil)
| ? [X] :
( ( ~ icext(Z,X)
& ir(X) )
| ( ~ ir(X)
& icext(Z,X) ) )
| ~ ic(Z) )
& ( ( ! [X] :
( ( icext(Z,X)
| ~ ir(X) )
& ( ir(X)
| ~ icext(Z,X) ) )
& ic(Z) )
| ~ iext(uri_owl_intersectionOf,Z,uri_rdf_nil) ) ),
inference(fof_nnf,[status(thm)],[owl_bool_intersectionof_class_000]) ).
fof(f_2_2,plain,
! [U_7] :
( ( iext(uri_owl_intersectionOf,U_7,uri_rdf_nil)
| ? [U_6] :
( ( ~ icext(U_7,U_6)
& ir(U_6) )
| ( ~ ir(U_6)
& icext(U_7,U_6) ) )
| ~ ic(U_7) )
& ( ( ! [U_5] :
( ( icext(U_7,U_5)
| ~ ir(U_5) )
& ( ir(U_5)
| ~ icext(U_7,U_5) ) )
& ic(U_7) )
| ~ iext(uri_owl_intersectionOf,U_7,uri_rdf_nil) ) ),
inference(variable_rename,[status(thm)],[f_2_1]) ).
fof(f_2_3,plain,
( ! [U_13] :
( iext(uri_owl_intersectionOf,U_13,uri_rdf_nil)
| ? [U_11] :
( ~ icext(U_13,U_11)
& ir(U_11) )
| ? [U_10] :
( ~ ir(U_10)
& icext(U_13,U_10) )
| ~ ic(U_13) )
& ! [U_12] :
( ( ! [U_9] :
( icext(U_12,U_9)
| ~ ir(U_9) )
& ! [U_8] :
( ir(U_8)
| ~ icext(U_12,U_8) )
& ic(U_12) )
| ~ iext(uri_owl_intersectionOf,U_12,uri_rdf_nil) ) ),
inference(miniscope,[status(thm)],[f_2_2]) ).
fof(f_2_4,plain,
( ! [U_13] :
( iext(uri_owl_intersectionOf,U_13,uri_rdf_nil)
| ? [U_11] :
( ~ icext(U_13,U_11)
& ir(U_11) )
| ( ~ ir(sK1(U_13))
& icext(U_13,sK1(U_13)) )
| ~ ic(U_13) )
& ! [U_12] :
( ( ! [U_9] :
( icext(U_12,U_9)
| ~ ir(U_9) )
& ! [U_8] :
( ir(U_8)
| ~ icext(U_12,U_8) )
& ic(U_12) )
| ~ iext(uri_owl_intersectionOf,U_12,uri_rdf_nil) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK1]),skolemize(U_10,sK1(U_13))],[f_2_3]) ).
fof(f_2_5,plain,
( ! [U_13] :
( iext(uri_owl_intersectionOf,U_13,uri_rdf_nil)
| ( ~ icext(U_13,sK2(U_13))
& ir(sK2(U_13)) )
| ( ~ ir(sK1(U_13))
& icext(U_13,sK1(U_13)) )
| ~ ic(U_13) )
& ! [U_12] :
( ( ! [U_9] :
( icext(U_12,U_9)
| ~ ir(U_9) )
& ! [U_8] :
( ir(U_8)
| ~ icext(U_12,U_8) )
& ic(U_12) )
| ~ iext(uri_owl_intersectionOf,U_12,uri_rdf_nil) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK2]),skolemize(U_11,sK2(U_13))],[f_2_4]) ).
cnf(f_2_6,plain,
( ic(U_12)
| ~ iext(uri_owl_intersectionOf,U_12,uri_rdf_nil) ),
inference(clausify,[status(thm)],[f_2_5]) ).
cnf(f_2_7,plain,
( ir(U_8)
| ~ icext(U_12,U_8)
| ~ iext(uri_owl_intersectionOf,U_12,uri_rdf_nil) ),
inference(clausify,[status(thm)],[f_2_5]) ).
cnf(f_2_8,plain,
( icext(U_12,U_9)
| ~ ir(U_9)
| ~ iext(uri_owl_intersectionOf,U_12,uri_rdf_nil) ),
inference(clausify,[status(thm)],[f_2_5]) ).
cnf(f_2_9,plain,
( ir(sK2(U_13))
| icext(U_13,sK1(U_13))
| ~ ic(U_13)
| iext(uri_owl_intersectionOf,U_13,uri_rdf_nil) ),
inference(clausify,[status(thm)],[f_2_5]) ).
cnf(f_2_10,plain,
( ~ icext(U_13,sK2(U_13))
| icext(U_13,sK1(U_13))
| ~ ic(U_13)
| iext(uri_owl_intersectionOf,U_13,uri_rdf_nil) ),
inference(clausify,[status(thm)],[f_2_5]) ).
cnf(f_2_11,plain,
( ir(sK2(U_13))
| ~ ir(sK1(U_13))
| ~ ic(U_13)
| iext(uri_owl_intersectionOf,U_13,uri_rdf_nil) ),
inference(clausify,[status(thm)],[f_2_5]) ).
cnf(f_2_12,plain,
( ~ icext(U_13,sK2(U_13))
| ~ ir(sK1(U_13))
| ~ ic(U_13)
| iext(uri_owl_intersectionOf,U_13,uri_rdf_nil) ),
inference(clausify,[status(thm)],[f_2_5]) ).
fof(f_3_1,plain,
! [Z,S1,C1] :
( ( ( iext(uri_owl_intersectionOf,Z,S1)
| ? [X] :
( ( ~ icext(Z,X)
& icext(C1,X) )
| ( ~ icext(C1,X)
& icext(Z,X) ) )
| ~ ic(C1)
| ~ ic(Z) )
& ( ( ! [X] :
( ( icext(Z,X)
| ~ icext(C1,X) )
& ( icext(C1,X)
| ~ icext(Z,X) ) )
& ic(C1)
& ic(Z) )
| ~ iext(uri_owl_intersectionOf,Z,S1) ) )
| ~ iext(uri_rdf_rest,S1,uri_rdf_nil)
| ~ iext(uri_rdf_first,S1,C1) ),
inference(fof_nnf,[status(thm)],[owl_bool_intersectionof_class_001]) ).
fof(f_3_2,plain,
! [U_18,U_17,U_16] :
( ( ( iext(uri_owl_intersectionOf,U_18,U_17)
| ? [U_15] :
( ( ~ icext(U_18,U_15)
& icext(U_16,U_15) )
| ( ~ icext(U_16,U_15)
& icext(U_18,U_15) ) )
| ~ ic(U_16)
| ~ ic(U_18) )
& ( ( ! [U_14] :
( ( icext(U_18,U_14)
| ~ icext(U_16,U_14) )
& ( icext(U_16,U_14)
| ~ icext(U_18,U_14) ) )
& ic(U_16)
& ic(U_18) )
| ~ iext(uri_owl_intersectionOf,U_18,U_17) ) )
| ~ iext(uri_rdf_rest,U_17,uri_rdf_nil)
| ~ iext(uri_rdf_first,U_17,U_16) ),
inference(variable_rename,[status(thm)],[f_3_1]) ).
fof(f_3_3,plain,
! [U_18,U_17,U_16] :
( ( ( iext(uri_owl_intersectionOf,U_18,U_17)
| ? [U_22] :
( ~ icext(U_18,U_22)
& icext(U_16,U_22) )
| ? [U_21] :
( ~ icext(U_16,U_21)
& icext(U_18,U_21) )
| ~ ic(U_16)
| ~ ic(U_18) )
& ( ( ! [U_20] :
( icext(U_18,U_20)
| ~ icext(U_16,U_20) )
& ! [U_19] :
( icext(U_16,U_19)
| ~ icext(U_18,U_19) )
& ic(U_16)
& ic(U_18) )
| ~ iext(uri_owl_intersectionOf,U_18,U_17) ) )
| ~ iext(uri_rdf_rest,U_17,uri_rdf_nil)
| ~ iext(uri_rdf_first,U_17,U_16) ),
inference(miniscope,[status(thm)],[f_3_2]) ).
fof(f_3_4,plain,
! [U_18,U_17,U_16] :
( ( ( iext(uri_owl_intersectionOf,U_18,U_17)
| ? [U_22] :
( ~ icext(U_18,U_22)
& icext(U_16,U_22) )
| ( ~ icext(U_16,sK3(U_18,U_17,U_16))
& icext(U_18,sK3(U_18,U_17,U_16)) )
| ~ ic(U_16)
| ~ ic(U_18) )
& ( ( ! [U_20] :
( icext(U_18,U_20)
| ~ icext(U_16,U_20) )
& ! [U_19] :
( icext(U_16,U_19)
| ~ icext(U_18,U_19) )
& ic(U_16)
& ic(U_18) )
| ~ iext(uri_owl_intersectionOf,U_18,U_17) ) )
| ~ iext(uri_rdf_rest,U_17,uri_rdf_nil)
| ~ iext(uri_rdf_first,U_17,U_16) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK3]),skolemize(U_21,sK3(U_18,U_17,U_16))],[f_3_3]) ).
fof(f_3_5,plain,
! [U_18,U_17,U_16] :
( ( ( iext(uri_owl_intersectionOf,U_18,U_17)
| ( ~ icext(U_18,sK4(U_18,U_17,U_16))
& icext(U_16,sK4(U_18,U_17,U_16)) )
| ( ~ icext(U_16,sK3(U_18,U_17,U_16))
& icext(U_18,sK3(U_18,U_17,U_16)) )
| ~ ic(U_16)
| ~ ic(U_18) )
& ( ( ! [U_20] :
( icext(U_18,U_20)
| ~ icext(U_16,U_20) )
& ! [U_19] :
( icext(U_16,U_19)
| ~ icext(U_18,U_19) )
& ic(U_16)
& ic(U_18) )
| ~ iext(uri_owl_intersectionOf,U_18,U_17) ) )
| ~ iext(uri_rdf_rest,U_17,uri_rdf_nil)
| ~ iext(uri_rdf_first,U_17,U_16) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK4]),skolemize(U_22,sK4(U_18,U_17,U_16))],[f_3_4]) ).
cnf(f_3_6,plain,
( ic(U_18)
| ~ iext(uri_owl_intersectionOf,U_18,U_17)
| ~ iext(uri_rdf_rest,U_17,uri_rdf_nil)
| ~ iext(uri_rdf_first,U_17,U_16) ),
inference(clausify,[status(thm)],[f_3_5]) ).
cnf(f_3_7,plain,
( ic(U_16)
| ~ iext(uri_owl_intersectionOf,U_18,U_17)
| ~ iext(uri_rdf_rest,U_17,uri_rdf_nil)
| ~ iext(uri_rdf_first,U_17,U_16) ),
inference(clausify,[status(thm)],[f_3_5]) ).
cnf(f_3_8,plain,
( icext(U_16,U_19)
| ~ icext(U_18,U_19)
| ~ iext(uri_owl_intersectionOf,U_18,U_17)
| ~ iext(uri_rdf_rest,U_17,uri_rdf_nil)
| ~ iext(uri_rdf_first,U_17,U_16) ),
inference(clausify,[status(thm)],[f_3_5]) ).
cnf(f_3_9,plain,
( icext(U_18,U_20)
| ~ icext(U_16,U_20)
| ~ iext(uri_owl_intersectionOf,U_18,U_17)
| ~ iext(uri_rdf_rest,U_17,uri_rdf_nil)
| ~ iext(uri_rdf_first,U_17,U_16) ),
inference(clausify,[status(thm)],[f_3_5]) ).
cnf(f_3_10,plain,
( icext(U_16,sK4(U_18,U_17,U_16))
| icext(U_18,sK3(U_18,U_17,U_16))
| ~ ic(U_16)
| ~ ic(U_18)
| iext(uri_owl_intersectionOf,U_18,U_17)
| ~ iext(uri_rdf_rest,U_17,uri_rdf_nil)
| ~ iext(uri_rdf_first,U_17,U_16) ),
inference(clausify,[status(thm)],[f_3_5]) ).
cnf(f_3_11,plain,
( ~ icext(U_18,sK4(U_18,U_17,U_16))
| icext(U_18,sK3(U_18,U_17,U_16))
| ~ ic(U_16)
| ~ ic(U_18)
| iext(uri_owl_intersectionOf,U_18,U_17)
| ~ iext(uri_rdf_rest,U_17,uri_rdf_nil)
| ~ iext(uri_rdf_first,U_17,U_16) ),
inference(clausify,[status(thm)],[f_3_5]) ).
cnf(f_3_12,plain,
( icext(U_16,sK4(U_18,U_17,U_16))
| ~ icext(U_16,sK3(U_18,U_17,U_16))
| ~ ic(U_16)
| ~ ic(U_18)
| iext(uri_owl_intersectionOf,U_18,U_17)
| ~ iext(uri_rdf_rest,U_17,uri_rdf_nil)
| ~ iext(uri_rdf_first,U_17,U_16) ),
inference(clausify,[status(thm)],[f_3_5]) ).
cnf(f_3_13,plain,
( ~ icext(U_18,sK4(U_18,U_17,U_16))
| ~ icext(U_16,sK3(U_18,U_17,U_16))
| ~ ic(U_16)
| ~ ic(U_18)
| iext(uri_owl_intersectionOf,U_18,U_17)
| ~ iext(uri_rdf_rest,U_17,uri_rdf_nil)
| ~ iext(uri_rdf_first,U_17,U_16) ),
inference(clausify,[status(thm)],[f_3_5]) ).
fof(f_4_1,plain,
! [Z,S1,C1,S2,C2] :
( ( ( iext(uri_owl_intersectionOf,Z,S1)
| ? [X] :
( ( ~ icext(Z,X)
& icext(C2,X)
& icext(C1,X) )
| ( ( ~ icext(C2,X)
| ~ icext(C1,X) )
& icext(Z,X) ) )
| ~ ic(C2)
| ~ ic(C1)
| ~ ic(Z) )
& ( ( ! [X] :
( ( icext(Z,X)
| ~ icext(C2,X)
| ~ icext(C1,X) )
& ( ( icext(C2,X)
& icext(C1,X) )
| ~ icext(Z,X) ) )
& ic(C2)
& ic(C1)
& ic(Z) )
| ~ iext(uri_owl_intersectionOf,Z,S1) ) )
| ~ iext(uri_rdf_rest,S2,uri_rdf_nil)
| ~ iext(uri_rdf_first,S2,C2)
| ~ iext(uri_rdf_rest,S1,S2)
| ~ iext(uri_rdf_first,S1,C1) ),
inference(fof_nnf,[status(thm)],[owl_bool_intersectionof_class_002]) ).
fof(f_4_2,plain,
! [U_29,U_28,U_27,U_26,U_25] :
( ( ( iext(uri_owl_intersectionOf,U_29,U_28)
| ? [U_24] :
( ( ~ icext(U_29,U_24)
& icext(U_25,U_24)
& icext(U_27,U_24) )
| ( ( ~ icext(U_25,U_24)
| ~ icext(U_27,U_24) )
& icext(U_29,U_24) ) )
| ~ ic(U_25)
| ~ ic(U_27)
| ~ ic(U_29) )
& ( ( ! [U_23] :
( ( icext(U_29,U_23)
| ~ icext(U_25,U_23)
| ~ icext(U_27,U_23) )
& ( ( icext(U_25,U_23)
& icext(U_27,U_23) )
| ~ icext(U_29,U_23) ) )
& ic(U_25)
& ic(U_27)
& ic(U_29) )
| ~ iext(uri_owl_intersectionOf,U_29,U_28) ) )
| ~ iext(uri_rdf_rest,U_26,uri_rdf_nil)
| ~ iext(uri_rdf_first,U_26,U_25)
| ~ iext(uri_rdf_rest,U_28,U_26)
| ~ iext(uri_rdf_first,U_28,U_27) ),
inference(variable_rename,[status(thm)],[f_4_1]) ).
fof(f_4_3,plain,
! [U_29,U_28,U_27,U_26,U_25] :
( ( ( iext(uri_owl_intersectionOf,U_29,U_28)
| ? [U_33] :
( ~ icext(U_29,U_33)
& icext(U_25,U_33)
& icext(U_27,U_33) )
| ? [U_32] :
( ( ~ icext(U_25,U_32)
| ~ icext(U_27,U_32) )
& icext(U_29,U_32) )
| ~ ic(U_25)
| ~ ic(U_27)
| ~ ic(U_29) )
& ( ( ! [U_31] :
( icext(U_29,U_31)
| ~ icext(U_25,U_31)
| ~ icext(U_27,U_31) )
& ! [U_30] :
( ( icext(U_25,U_30)
& icext(U_27,U_30) )
| ~ icext(U_29,U_30) )
& ic(U_25)
& ic(U_27)
& ic(U_29) )
| ~ iext(uri_owl_intersectionOf,U_29,U_28) ) )
| ~ iext(uri_rdf_rest,U_26,uri_rdf_nil)
| ~ iext(uri_rdf_first,U_26,U_25)
| ~ iext(uri_rdf_rest,U_28,U_26)
| ~ iext(uri_rdf_first,U_28,U_27) ),
inference(miniscope,[status(thm)],[f_4_2]) ).
fof(f_4_4,plain,
! [U_29,U_28,U_27,U_26,U_25] :
( ( ( iext(uri_owl_intersectionOf,U_29,U_28)
| ? [U_33] :
( ~ icext(U_29,U_33)
& icext(U_25,U_33)
& icext(U_27,U_33) )
| ( ( ~ icext(U_25,sK5(U_29,U_28,U_27,U_26,U_25))
| ~ icext(U_27,sK5(U_29,U_28,U_27,U_26,U_25)) )
& icext(U_29,sK5(U_29,U_28,U_27,U_26,U_25)) )
| ~ ic(U_25)
| ~ ic(U_27)
| ~ ic(U_29) )
& ( ( ! [U_31] :
( icext(U_29,U_31)
| ~ icext(U_25,U_31)
| ~ icext(U_27,U_31) )
& ! [U_30] :
( ( icext(U_25,U_30)
& icext(U_27,U_30) )
| ~ icext(U_29,U_30) )
& ic(U_25)
& ic(U_27)
& ic(U_29) )
| ~ iext(uri_owl_intersectionOf,U_29,U_28) ) )
| ~ iext(uri_rdf_rest,U_26,uri_rdf_nil)
| ~ iext(uri_rdf_first,U_26,U_25)
| ~ iext(uri_rdf_rest,U_28,U_26)
| ~ iext(uri_rdf_first,U_28,U_27) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK5]),skolemize(U_32,sK5(U_29,U_28,U_27,U_26,U_25))],[f_4_3]) ).
fof(f_4_5,plain,
! [U_29,U_28,U_27,U_26,U_25] :
( ( ( iext(uri_owl_intersectionOf,U_29,U_28)
| ( ~ icext(U_29,sK6(U_29,U_28,U_27,U_26,U_25))
& icext(U_25,sK6(U_29,U_28,U_27,U_26,U_25))
& icext(U_27,sK6(U_29,U_28,U_27,U_26,U_25)) )
| ( ( ~ icext(U_25,sK5(U_29,U_28,U_27,U_26,U_25))
| ~ icext(U_27,sK5(U_29,U_28,U_27,U_26,U_25)) )
& icext(U_29,sK5(U_29,U_28,U_27,U_26,U_25)) )
| ~ ic(U_25)
| ~ ic(U_27)
| ~ ic(U_29) )
& ( ( ! [U_31] :
( icext(U_29,U_31)
| ~ icext(U_25,U_31)
| ~ icext(U_27,U_31) )
& ! [U_30] :
( ( icext(U_25,U_30)
& icext(U_27,U_30) )
| ~ icext(U_29,U_30) )
& ic(U_25)
& ic(U_27)
& ic(U_29) )
| ~ iext(uri_owl_intersectionOf,U_29,U_28) ) )
| ~ iext(uri_rdf_rest,U_26,uri_rdf_nil)
| ~ iext(uri_rdf_first,U_26,U_25)
| ~ iext(uri_rdf_rest,U_28,U_26)
| ~ iext(uri_rdf_first,U_28,U_27) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK6]),skolemize(U_33,sK6(U_29,U_28,U_27,U_26,U_25))],[f_4_4]) ).
cnf(f_4_6,plain,
( ic(U_29)
| ~ iext(uri_owl_intersectionOf,U_29,U_28)
| ~ iext(uri_rdf_rest,U_26,uri_rdf_nil)
| ~ iext(uri_rdf_first,U_26,U_25)
| ~ iext(uri_rdf_rest,U_28,U_26)
| ~ iext(uri_rdf_first,U_28,U_27) ),
inference(clausify,[status(thm)],[f_4_5]) ).
cnf(f_4_7,plain,
( ic(U_27)
| ~ iext(uri_owl_intersectionOf,U_29,U_28)
| ~ iext(uri_rdf_rest,U_26,uri_rdf_nil)
| ~ iext(uri_rdf_first,U_26,U_25)
| ~ iext(uri_rdf_rest,U_28,U_26)
| ~ iext(uri_rdf_first,U_28,U_27) ),
inference(clausify,[status(thm)],[f_4_5]) ).
cnf(f_4_8,plain,
( ic(U_25)
| ~ iext(uri_owl_intersectionOf,U_29,U_28)
| ~ iext(uri_rdf_rest,U_26,uri_rdf_nil)
| ~ iext(uri_rdf_first,U_26,U_25)
| ~ iext(uri_rdf_rest,U_28,U_26)
| ~ iext(uri_rdf_first,U_28,U_27) ),
inference(clausify,[status(thm)],[f_4_5]) ).
cnf(f_4_9,plain,
( icext(U_27,U_30)
| ~ icext(U_29,U_30)
| ~ iext(uri_owl_intersectionOf,U_29,U_28)
| ~ iext(uri_rdf_rest,U_26,uri_rdf_nil)
| ~ iext(uri_rdf_first,U_26,U_25)
| ~ iext(uri_rdf_rest,U_28,U_26)
| ~ iext(uri_rdf_first,U_28,U_27) ),
inference(clausify,[status(thm)],[f_4_5]) ).
cnf(f_4_10,plain,
( icext(U_25,U_30)
| ~ icext(U_29,U_30)
| ~ iext(uri_owl_intersectionOf,U_29,U_28)
| ~ iext(uri_rdf_rest,U_26,uri_rdf_nil)
| ~ iext(uri_rdf_first,U_26,U_25)
| ~ iext(uri_rdf_rest,U_28,U_26)
| ~ iext(uri_rdf_first,U_28,U_27) ),
inference(clausify,[status(thm)],[f_4_5]) ).
cnf(f_4_11,plain,
( icext(U_29,U_31)
| ~ icext(U_25,U_31)
| ~ icext(U_27,U_31)
| ~ iext(uri_owl_intersectionOf,U_29,U_28)
| ~ iext(uri_rdf_rest,U_26,uri_rdf_nil)
| ~ iext(uri_rdf_first,U_26,U_25)
| ~ iext(uri_rdf_rest,U_28,U_26)
| ~ iext(uri_rdf_first,U_28,U_27) ),
inference(clausify,[status(thm)],[f_4_5]) ).
cnf(f_4_12,plain,
( icext(U_27,sK6(U_29,U_28,U_27,U_26,U_25))
| icext(U_29,sK5(U_29,U_28,U_27,U_26,U_25))
| ~ ic(U_25)
| ~ ic(U_27)
| ~ ic(U_29)
| iext(uri_owl_intersectionOf,U_29,U_28)
| ~ iext(uri_rdf_rest,U_26,uri_rdf_nil)
| ~ iext(uri_rdf_first,U_26,U_25)
| ~ iext(uri_rdf_rest,U_28,U_26)
| ~ iext(uri_rdf_first,U_28,U_27) ),
inference(clausify,[status(thm)],[f_4_5]) ).
cnf(f_4_13,plain,
( icext(U_25,sK6(U_29,U_28,U_27,U_26,U_25))
| icext(U_29,sK5(U_29,U_28,U_27,U_26,U_25))
| ~ ic(U_25)
| ~ ic(U_27)
| ~ ic(U_29)
| iext(uri_owl_intersectionOf,U_29,U_28)
| ~ iext(uri_rdf_rest,U_26,uri_rdf_nil)
| ~ iext(uri_rdf_first,U_26,U_25)
| ~ iext(uri_rdf_rest,U_28,U_26)
| ~ iext(uri_rdf_first,U_28,U_27) ),
inference(clausify,[status(thm)],[f_4_5]) ).
cnf(f_4_14,plain,
( ~ icext(U_29,sK6(U_29,U_28,U_27,U_26,U_25))
| icext(U_29,sK5(U_29,U_28,U_27,U_26,U_25))
| ~ ic(U_25)
| ~ ic(U_27)
| ~ ic(U_29)
| iext(uri_owl_intersectionOf,U_29,U_28)
| ~ iext(uri_rdf_rest,U_26,uri_rdf_nil)
| ~ iext(uri_rdf_first,U_26,U_25)
| ~ iext(uri_rdf_rest,U_28,U_26)
| ~ iext(uri_rdf_first,U_28,U_27) ),
inference(clausify,[status(thm)],[f_4_5]) ).
cnf(f_4_15,plain,
( icext(U_27,sK6(U_29,U_28,U_27,U_26,U_25))
| ~ icext(U_25,sK5(U_29,U_28,U_27,U_26,U_25))
| ~ icext(U_27,sK5(U_29,U_28,U_27,U_26,U_25))
| ~ ic(U_25)
| ~ ic(U_27)
| ~ ic(U_29)
| iext(uri_owl_intersectionOf,U_29,U_28)
| ~ iext(uri_rdf_rest,U_26,uri_rdf_nil)
| ~ iext(uri_rdf_first,U_26,U_25)
| ~ iext(uri_rdf_rest,U_28,U_26)
| ~ iext(uri_rdf_first,U_28,U_27) ),
inference(clausify,[status(thm)],[f_4_5]) ).
cnf(f_4_16,plain,
( icext(U_25,sK6(U_29,U_28,U_27,U_26,U_25))
| ~ icext(U_25,sK5(U_29,U_28,U_27,U_26,U_25))
| ~ icext(U_27,sK5(U_29,U_28,U_27,U_26,U_25))
| ~ ic(U_25)
| ~ ic(U_27)
| ~ ic(U_29)
| iext(uri_owl_intersectionOf,U_29,U_28)
| ~ iext(uri_rdf_rest,U_26,uri_rdf_nil)
| ~ iext(uri_rdf_first,U_26,U_25)
| ~ iext(uri_rdf_rest,U_28,U_26)
| ~ iext(uri_rdf_first,U_28,U_27) ),
inference(clausify,[status(thm)],[f_4_5]) ).
cnf(f_4_17,plain,
( ~ icext(U_29,sK6(U_29,U_28,U_27,U_26,U_25))
| ~ icext(U_25,sK5(U_29,U_28,U_27,U_26,U_25))
| ~ icext(U_27,sK5(U_29,U_28,U_27,U_26,U_25))
| ~ ic(U_25)
| ~ ic(U_27)
| ~ ic(U_29)
| iext(uri_owl_intersectionOf,U_29,U_28)
| ~ iext(uri_rdf_rest,U_26,uri_rdf_nil)
| ~ iext(uri_rdf_first,U_26,U_25)
| ~ iext(uri_rdf_rest,U_28,U_26)
| ~ iext(uri_rdf_first,U_28,U_27) ),
inference(clausify,[status(thm)],[f_4_5]) ).
fof(f_5_1,plain,
! [Z,S1,C1,S2,C2,S3,C3] :
( ( ( iext(uri_owl_intersectionOf,Z,S1)
| ? [X] :
( ( ~ icext(Z,X)
& icext(C3,X)
& icext(C2,X)
& icext(C1,X) )
| ( ( ~ icext(C3,X)
| ~ icext(C2,X)
| ~ icext(C1,X) )
& icext(Z,X) ) )
| ~ ic(C3)
| ~ ic(C2)
| ~ ic(C1)
| ~ ic(Z) )
& ( ( ! [X] :
( ( icext(Z,X)
| ~ icext(C3,X)
| ~ icext(C2,X)
| ~ icext(C1,X) )
& ( ( icext(C3,X)
& icext(C2,X)
& icext(C1,X) )
| ~ icext(Z,X) ) )
& ic(C3)
& ic(C2)
& ic(C1)
& ic(Z) )
| ~ iext(uri_owl_intersectionOf,Z,S1) ) )
| ~ iext(uri_rdf_rest,S3,uri_rdf_nil)
| ~ iext(uri_rdf_first,S3,C3)
| ~ iext(uri_rdf_rest,S2,S3)
| ~ iext(uri_rdf_first,S2,C2)
| ~ iext(uri_rdf_rest,S1,S2)
| ~ iext(uri_rdf_first,S1,C1) ),
inference(fof_nnf,[status(thm)],[owl_bool_intersectionof_class_003]) ).
fof(f_5_2,plain,
! [U_42,U_41,U_40,U_39,U_38,U_37,U_36] :
( ( ( iext(uri_owl_intersectionOf,U_42,U_41)
| ? [U_35] :
( ( ~ icext(U_42,U_35)
& icext(U_36,U_35)
& icext(U_38,U_35)
& icext(U_40,U_35) )
| ( ( ~ icext(U_36,U_35)
| ~ icext(U_38,U_35)
| ~ icext(U_40,U_35) )
& icext(U_42,U_35) ) )
| ~ ic(U_36)
| ~ ic(U_38)
| ~ ic(U_40)
| ~ ic(U_42) )
& ( ( ! [U_34] :
( ( icext(U_42,U_34)
| ~ icext(U_36,U_34)
| ~ icext(U_38,U_34)
| ~ icext(U_40,U_34) )
& ( ( icext(U_36,U_34)
& icext(U_38,U_34)
& icext(U_40,U_34) )
| ~ icext(U_42,U_34) ) )
& ic(U_36)
& ic(U_38)
& ic(U_40)
& ic(U_42) )
| ~ iext(uri_owl_intersectionOf,U_42,U_41) ) )
| ~ iext(uri_rdf_rest,U_37,uri_rdf_nil)
| ~ iext(uri_rdf_first,U_37,U_36)
| ~ iext(uri_rdf_rest,U_39,U_37)
| ~ iext(uri_rdf_first,U_39,U_38)
| ~ iext(uri_rdf_rest,U_41,U_39)
| ~ iext(uri_rdf_first,U_41,U_40) ),
inference(variable_rename,[status(thm)],[f_5_1]) ).
fof(f_5_3,plain,
! [U_42,U_41,U_40,U_39,U_38,U_37,U_36] :
( ( ( iext(uri_owl_intersectionOf,U_42,U_41)
| ? [U_46] :
( ~ icext(U_42,U_46)
& icext(U_36,U_46)
& icext(U_38,U_46)
& icext(U_40,U_46) )
| ? [U_45] :
( ( ~ icext(U_36,U_45)
| ~ icext(U_38,U_45)
| ~ icext(U_40,U_45) )
& icext(U_42,U_45) )
| ~ ic(U_36)
| ~ ic(U_38)
| ~ ic(U_40)
| ~ ic(U_42) )
& ( ( ! [U_44] :
( icext(U_42,U_44)
| ~ icext(U_36,U_44)
| ~ icext(U_38,U_44)
| ~ icext(U_40,U_44) )
& ! [U_43] :
( ( icext(U_36,U_43)
& icext(U_38,U_43)
& icext(U_40,U_43) )
| ~ icext(U_42,U_43) )
& ic(U_36)
& ic(U_38)
& ic(U_40)
& ic(U_42) )
| ~ iext(uri_owl_intersectionOf,U_42,U_41) ) )
| ~ iext(uri_rdf_rest,U_37,uri_rdf_nil)
| ~ iext(uri_rdf_first,U_37,U_36)
| ~ iext(uri_rdf_rest,U_39,U_37)
| ~ iext(uri_rdf_first,U_39,U_38)
| ~ iext(uri_rdf_rest,U_41,U_39)
| ~ iext(uri_rdf_first,U_41,U_40) ),
inference(miniscope,[status(thm)],[f_5_2]) ).
fof(f_5_4,plain,
! [U_42,U_41,U_40,U_39,U_38,U_37,U_36] :
( ( ( iext(uri_owl_intersectionOf,U_42,U_41)
| ? [U_46] :
( ~ icext(U_42,U_46)
& icext(U_36,U_46)
& icext(U_38,U_46)
& icext(U_40,U_46) )
| ( ( ~ icext(U_36,sK7(U_42,U_41,U_40,U_39,U_38,U_37,U_36))
| ~ icext(U_38,sK7(U_42,U_41,U_40,U_39,U_38,U_37,U_36))
| ~ icext(U_40,sK7(U_42,U_41,U_40,U_39,U_38,U_37,U_36)) )
& icext(U_42,sK7(U_42,U_41,U_40,U_39,U_38,U_37,U_36)) )
| ~ ic(U_36)
| ~ ic(U_38)
| ~ ic(U_40)
| ~ ic(U_42) )
& ( ( ! [U_44] :
( icext(U_42,U_44)
| ~ icext(U_36,U_44)
| ~ icext(U_38,U_44)
| ~ icext(U_40,U_44) )
& ! [U_43] :
( ( icext(U_36,U_43)
& icext(U_38,U_43)
& icext(U_40,U_43) )
| ~ icext(U_42,U_43) )
& ic(U_36)
& ic(U_38)
& ic(U_40)
& ic(U_42) )
| ~ iext(uri_owl_intersectionOf,U_42,U_41) ) )
| ~ iext(uri_rdf_rest,U_37,uri_rdf_nil)
| ~ iext(uri_rdf_first,U_37,U_36)
| ~ iext(uri_rdf_rest,U_39,U_37)
| ~ iext(uri_rdf_first,U_39,U_38)
| ~ iext(uri_rdf_rest,U_41,U_39)
| ~ iext(uri_rdf_first,U_41,U_40) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK7]),skolemize(U_45,sK7(U_42,U_41,U_40,U_39,U_38,U_37,U_36))],[f_5_3]) ).
fof(f_5_5,plain,
! [U_42,U_41,U_40,U_39,U_38,U_37,U_36] :
( ( ( iext(uri_owl_intersectionOf,U_42,U_41)
| ( ~ icext(U_42,sK8(U_42,U_41,U_40,U_39,U_38,U_37,U_36))
& icext(U_36,sK8(U_42,U_41,U_40,U_39,U_38,U_37,U_36))
& icext(U_38,sK8(U_42,U_41,U_40,U_39,U_38,U_37,U_36))
& icext(U_40,sK8(U_42,U_41,U_40,U_39,U_38,U_37,U_36)) )
| ( ( ~ icext(U_36,sK7(U_42,U_41,U_40,U_39,U_38,U_37,U_36))
| ~ icext(U_38,sK7(U_42,U_41,U_40,U_39,U_38,U_37,U_36))
| ~ icext(U_40,sK7(U_42,U_41,U_40,U_39,U_38,U_37,U_36)) )
& icext(U_42,sK7(U_42,U_41,U_40,U_39,U_38,U_37,U_36)) )
| ~ ic(U_36)
| ~ ic(U_38)
| ~ ic(U_40)
| ~ ic(U_42) )
& ( ( ! [U_44] :
( icext(U_42,U_44)
| ~ icext(U_36,U_44)
| ~ icext(U_38,U_44)
| ~ icext(U_40,U_44) )
& ! [U_43] :
( ( icext(U_36,U_43)
& icext(U_38,U_43)
& icext(U_40,U_43) )
| ~ icext(U_42,U_43) )
& ic(U_36)
& ic(U_38)
& ic(U_40)
& ic(U_42) )
| ~ iext(uri_owl_intersectionOf,U_42,U_41) ) )
| ~ iext(uri_rdf_rest,U_37,uri_rdf_nil)
| ~ iext(uri_rdf_first,U_37,U_36)
| ~ iext(uri_rdf_rest,U_39,U_37)
| ~ iext(uri_rdf_first,U_39,U_38)
| ~ iext(uri_rdf_rest,U_41,U_39)
| ~ iext(uri_rdf_first,U_41,U_40) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK8]),skolemize(U_46,sK8(U_42,U_41,U_40,U_39,U_38,U_37,U_36))],[f_5_4]) ).
cnf(f_5_6,plain,
( ic(U_42)
| ~ iext(uri_owl_intersectionOf,U_42,U_41)
| ~ iext(uri_rdf_rest,U_37,uri_rdf_nil)
| ~ iext(uri_rdf_first,U_37,U_36)
| ~ iext(uri_rdf_rest,U_39,U_37)
| ~ iext(uri_rdf_first,U_39,U_38)
| ~ iext(uri_rdf_rest,U_41,U_39)
| ~ iext(uri_rdf_first,U_41,U_40) ),
inference(clausify,[status(thm)],[f_5_5]) ).
cnf(f_5_7,plain,
( ic(U_40)
| ~ iext(uri_owl_intersectionOf,U_42,U_41)
| ~ iext(uri_rdf_rest,U_37,uri_rdf_nil)
| ~ iext(uri_rdf_first,U_37,U_36)
| ~ iext(uri_rdf_rest,U_39,U_37)
| ~ iext(uri_rdf_first,U_39,U_38)
| ~ iext(uri_rdf_rest,U_41,U_39)
| ~ iext(uri_rdf_first,U_41,U_40) ),
inference(clausify,[status(thm)],[f_5_5]) ).
cnf(f_5_8,plain,
( ic(U_38)
| ~ iext(uri_owl_intersectionOf,U_42,U_41)
| ~ iext(uri_rdf_rest,U_37,uri_rdf_nil)
| ~ iext(uri_rdf_first,U_37,U_36)
| ~ iext(uri_rdf_rest,U_39,U_37)
| ~ iext(uri_rdf_first,U_39,U_38)
| ~ iext(uri_rdf_rest,U_41,U_39)
| ~ iext(uri_rdf_first,U_41,U_40) ),
inference(clausify,[status(thm)],[f_5_5]) ).
cnf(f_5_9,plain,
( ic(U_36)
| ~ iext(uri_owl_intersectionOf,U_42,U_41)
| ~ iext(uri_rdf_rest,U_37,uri_rdf_nil)
| ~ iext(uri_rdf_first,U_37,U_36)
| ~ iext(uri_rdf_rest,U_39,U_37)
| ~ iext(uri_rdf_first,U_39,U_38)
| ~ iext(uri_rdf_rest,U_41,U_39)
| ~ iext(uri_rdf_first,U_41,U_40) ),
inference(clausify,[status(thm)],[f_5_5]) ).
cnf(f_5_10,plain,
( icext(U_40,U_43)
| ~ icext(U_42,U_43)
| ~ iext(uri_owl_intersectionOf,U_42,U_41)
| ~ iext(uri_rdf_rest,U_37,uri_rdf_nil)
| ~ iext(uri_rdf_first,U_37,U_36)
| ~ iext(uri_rdf_rest,U_39,U_37)
| ~ iext(uri_rdf_first,U_39,U_38)
| ~ iext(uri_rdf_rest,U_41,U_39)
| ~ iext(uri_rdf_first,U_41,U_40) ),
inference(clausify,[status(thm)],[f_5_5]) ).
cnf(f_5_11,plain,
( icext(U_38,U_43)
| ~ icext(U_42,U_43)
| ~ iext(uri_owl_intersectionOf,U_42,U_41)
| ~ iext(uri_rdf_rest,U_37,uri_rdf_nil)
| ~ iext(uri_rdf_first,U_37,U_36)
| ~ iext(uri_rdf_rest,U_39,U_37)
| ~ iext(uri_rdf_first,U_39,U_38)
| ~ iext(uri_rdf_rest,U_41,U_39)
| ~ iext(uri_rdf_first,U_41,U_40) ),
inference(clausify,[status(thm)],[f_5_5]) ).
cnf(f_5_12,plain,
( icext(U_36,U_43)
| ~ icext(U_42,U_43)
| ~ iext(uri_owl_intersectionOf,U_42,U_41)
| ~ iext(uri_rdf_rest,U_37,uri_rdf_nil)
| ~ iext(uri_rdf_first,U_37,U_36)
| ~ iext(uri_rdf_rest,U_39,U_37)
| ~ iext(uri_rdf_first,U_39,U_38)
| ~ iext(uri_rdf_rest,U_41,U_39)
| ~ iext(uri_rdf_first,U_41,U_40) ),
inference(clausify,[status(thm)],[f_5_5]) ).
cnf(f_5_13,plain,
( icext(U_42,U_44)
| ~ icext(U_36,U_44)
| ~ icext(U_38,U_44)
| ~ icext(U_40,U_44)
| ~ iext(uri_owl_intersectionOf,U_42,U_41)
| ~ iext(uri_rdf_rest,U_37,uri_rdf_nil)
| ~ iext(uri_rdf_first,U_37,U_36)
| ~ iext(uri_rdf_rest,U_39,U_37)
| ~ iext(uri_rdf_first,U_39,U_38)
| ~ iext(uri_rdf_rest,U_41,U_39)
| ~ iext(uri_rdf_first,U_41,U_40) ),
inference(clausify,[status(thm)],[f_5_5]) ).
cnf(f_5_14,plain,
( icext(U_40,sK8(U_42,U_41,U_40,U_39,U_38,U_37,U_36))
| icext(U_42,sK7(U_42,U_41,U_40,U_39,U_38,U_37,U_36))
| ~ ic(U_36)
| ~ ic(U_38)
| ~ ic(U_40)
| ~ ic(U_42)
| iext(uri_owl_intersectionOf,U_42,U_41)
| ~ iext(uri_rdf_rest,U_37,uri_rdf_nil)
| ~ iext(uri_rdf_first,U_37,U_36)
| ~ iext(uri_rdf_rest,U_39,U_37)
| ~ iext(uri_rdf_first,U_39,U_38)
| ~ iext(uri_rdf_rest,U_41,U_39)
| ~ iext(uri_rdf_first,U_41,U_40) ),
inference(clausify,[status(thm)],[f_5_5]) ).
cnf(f_5_15,plain,
( icext(U_38,sK8(U_42,U_41,U_40,U_39,U_38,U_37,U_36))
| icext(U_42,sK7(U_42,U_41,U_40,U_39,U_38,U_37,U_36))
| ~ ic(U_36)
| ~ ic(U_38)
| ~ ic(U_40)
| ~ ic(U_42)
| iext(uri_owl_intersectionOf,U_42,U_41)
| ~ iext(uri_rdf_rest,U_37,uri_rdf_nil)
| ~ iext(uri_rdf_first,U_37,U_36)
| ~ iext(uri_rdf_rest,U_39,U_37)
| ~ iext(uri_rdf_first,U_39,U_38)
| ~ iext(uri_rdf_rest,U_41,U_39)
| ~ iext(uri_rdf_first,U_41,U_40) ),
inference(clausify,[status(thm)],[f_5_5]) ).
cnf(f_5_16,plain,
( icext(U_36,sK8(U_42,U_41,U_40,U_39,U_38,U_37,U_36))
| icext(U_42,sK7(U_42,U_41,U_40,U_39,U_38,U_37,U_36))
| ~ ic(U_36)
| ~ ic(U_38)
| ~ ic(U_40)
| ~ ic(U_42)
| iext(uri_owl_intersectionOf,U_42,U_41)
| ~ iext(uri_rdf_rest,U_37,uri_rdf_nil)
| ~ iext(uri_rdf_first,U_37,U_36)
| ~ iext(uri_rdf_rest,U_39,U_37)
| ~ iext(uri_rdf_first,U_39,U_38)
| ~ iext(uri_rdf_rest,U_41,U_39)
| ~ iext(uri_rdf_first,U_41,U_40) ),
inference(clausify,[status(thm)],[f_5_5]) ).
cnf(f_5_17,plain,
( ~ icext(U_42,sK8(U_42,U_41,U_40,U_39,U_38,U_37,U_36))
| icext(U_42,sK7(U_42,U_41,U_40,U_39,U_38,U_37,U_36))
| ~ ic(U_36)
| ~ ic(U_38)
| ~ ic(U_40)
| ~ ic(U_42)
| iext(uri_owl_intersectionOf,U_42,U_41)
| ~ iext(uri_rdf_rest,U_37,uri_rdf_nil)
| ~ iext(uri_rdf_first,U_37,U_36)
| ~ iext(uri_rdf_rest,U_39,U_37)
| ~ iext(uri_rdf_first,U_39,U_38)
| ~ iext(uri_rdf_rest,U_41,U_39)
| ~ iext(uri_rdf_first,U_41,U_40) ),
inference(clausify,[status(thm)],[f_5_5]) ).
cnf(f_5_18,plain,
( icext(U_40,sK8(U_42,U_41,U_40,U_39,U_38,U_37,U_36))
| ~ icext(U_36,sK7(U_42,U_41,U_40,U_39,U_38,U_37,U_36))
| ~ icext(U_38,sK7(U_42,U_41,U_40,U_39,U_38,U_37,U_36))
| ~ icext(U_40,sK7(U_42,U_41,U_40,U_39,U_38,U_37,U_36))
| ~ ic(U_36)
| ~ ic(U_38)
| ~ ic(U_40)
| ~ ic(U_42)
| iext(uri_owl_intersectionOf,U_42,U_41)
| ~ iext(uri_rdf_rest,U_37,uri_rdf_nil)
| ~ iext(uri_rdf_first,U_37,U_36)
| ~ iext(uri_rdf_rest,U_39,U_37)
| ~ iext(uri_rdf_first,U_39,U_38)
| ~ iext(uri_rdf_rest,U_41,U_39)
| ~ iext(uri_rdf_first,U_41,U_40) ),
inference(clausify,[status(thm)],[f_5_5]) ).
cnf(f_5_19,plain,
( icext(U_38,sK8(U_42,U_41,U_40,U_39,U_38,U_37,U_36))
| ~ icext(U_36,sK7(U_42,U_41,U_40,U_39,U_38,U_37,U_36))
| ~ icext(U_38,sK7(U_42,U_41,U_40,U_39,U_38,U_37,U_36))
| ~ icext(U_40,sK7(U_42,U_41,U_40,U_39,U_38,U_37,U_36))
| ~ ic(U_36)
| ~ ic(U_38)
| ~ ic(U_40)
| ~ ic(U_42)
| iext(uri_owl_intersectionOf,U_42,U_41)
| ~ iext(uri_rdf_rest,U_37,uri_rdf_nil)
| ~ iext(uri_rdf_first,U_37,U_36)
| ~ iext(uri_rdf_rest,U_39,U_37)
| ~ iext(uri_rdf_first,U_39,U_38)
| ~ iext(uri_rdf_rest,U_41,U_39)
| ~ iext(uri_rdf_first,U_41,U_40) ),
inference(clausify,[status(thm)],[f_5_5]) ).
cnf(f_5_20,plain,
( icext(U_36,sK8(U_42,U_41,U_40,U_39,U_38,U_37,U_36))
| ~ icext(U_36,sK7(U_42,U_41,U_40,U_39,U_38,U_37,U_36))
| ~ icext(U_38,sK7(U_42,U_41,U_40,U_39,U_38,U_37,U_36))
| ~ icext(U_40,sK7(U_42,U_41,U_40,U_39,U_38,U_37,U_36))
| ~ ic(U_36)
| ~ ic(U_38)
| ~ ic(U_40)
| ~ ic(U_42)
| iext(uri_owl_intersectionOf,U_42,U_41)
| ~ iext(uri_rdf_rest,U_37,uri_rdf_nil)
| ~ iext(uri_rdf_first,U_37,U_36)
| ~ iext(uri_rdf_rest,U_39,U_37)
| ~ iext(uri_rdf_first,U_39,U_38)
| ~ iext(uri_rdf_rest,U_41,U_39)
| ~ iext(uri_rdf_first,U_41,U_40) ),
inference(clausify,[status(thm)],[f_5_5]) ).
cnf(f_5_21,plain,
( ~ icext(U_42,sK8(U_42,U_41,U_40,U_39,U_38,U_37,U_36))
| ~ icext(U_36,sK7(U_42,U_41,U_40,U_39,U_38,U_37,U_36))
| ~ icext(U_38,sK7(U_42,U_41,U_40,U_39,U_38,U_37,U_36))
| ~ icext(U_40,sK7(U_42,U_41,U_40,U_39,U_38,U_37,U_36))
| ~ ic(U_36)
| ~ ic(U_38)
| ~ ic(U_40)
| ~ ic(U_42)
| iext(uri_owl_intersectionOf,U_42,U_41)
| ~ iext(uri_rdf_rest,U_37,uri_rdf_nil)
| ~ iext(uri_rdf_first,U_37,U_36)
| ~ iext(uri_rdf_rest,U_39,U_37)
| ~ iext(uri_rdf_first,U_39,U_38)
| ~ iext(uri_rdf_rest,U_41,U_39)
| ~ iext(uri_rdf_first,U_41,U_40) ),
inference(clausify,[status(thm)],[f_5_5]) ).
fof(f_6_1,plain,
! [Z] :
( ( iext(uri_owl_unionOf,Z,uri_rdf_nil)
| ? [X] : icext(Z,X)
| ~ ic(Z) )
& ( ( ! [X] : ~ icext(Z,X)
& ic(Z) )
| ~ iext(uri_owl_unionOf,Z,uri_rdf_nil) ) ),
inference(fof_nnf,[status(thm)],[owl_bool_unionof_class_000]) ).
fof(f_6_2,plain,
! [U_49] :
( ( iext(uri_owl_unionOf,U_49,uri_rdf_nil)
| ? [U_48] : icext(U_49,U_48)
| ~ ic(U_49) )
& ( ( ! [U_47] : ~ icext(U_49,U_47)
& ic(U_49) )
| ~ iext(uri_owl_unionOf,U_49,uri_rdf_nil) ) ),
inference(variable_rename,[status(thm)],[f_6_1]) ).
fof(f_6_3,plain,
( ! [U_51] :
( iext(uri_owl_unionOf,U_51,uri_rdf_nil)
| ? [U_48] : icext(U_51,U_48)
| ~ ic(U_51) )
& ! [U_50] :
( ( ! [U_47] : ~ icext(U_50,U_47)
& ic(U_50) )
| ~ iext(uri_owl_unionOf,U_50,uri_rdf_nil) ) ),
inference(miniscope,[status(thm)],[f_6_2]) ).
fof(f_6_4,plain,
( ! [U_51] :
( iext(uri_owl_unionOf,U_51,uri_rdf_nil)
| icext(U_51,sK9(U_51))
| ~ ic(U_51) )
& ! [U_50] :
( ( ! [U_47] : ~ icext(U_50,U_47)
& ic(U_50) )
| ~ iext(uri_owl_unionOf,U_50,uri_rdf_nil) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK9]),skolemize(U_48,sK9(U_51))],[f_6_3]) ).
cnf(f_6_5,plain,
( ic(U_50)
| ~ iext(uri_owl_unionOf,U_50,uri_rdf_nil) ),
inference(clausify,[status(thm)],[f_6_4]) ).
cnf(f_6_6,plain,
( ~ icext(U_50,U_47)
| ~ iext(uri_owl_unionOf,U_50,uri_rdf_nil) ),
inference(clausify,[status(thm)],[f_6_4]) ).
cnf(f_6_7,plain,
( iext(uri_owl_unionOf,U_51,uri_rdf_nil)
| icext(U_51,sK9(U_51))
| ~ ic(U_51) ),
inference(clausify,[status(thm)],[f_6_4]) ).
fof(f_7_1,plain,
! [Z,S1,C1] :
( ( ( iext(uri_owl_unionOf,Z,S1)
| ? [X] :
( ( ~ icext(Z,X)
& icext(C1,X) )
| ( ~ icext(C1,X)
& icext(Z,X) ) )
| ~ ic(C1)
| ~ ic(Z) )
& ( ( ! [X] :
( ( icext(Z,X)
| ~ icext(C1,X) )
& ( icext(C1,X)
| ~ icext(Z,X) ) )
& ic(C1)
& ic(Z) )
| ~ iext(uri_owl_unionOf,Z,S1) ) )
| ~ iext(uri_rdf_rest,S1,uri_rdf_nil)
| ~ iext(uri_rdf_first,S1,C1) ),
inference(fof_nnf,[status(thm)],[owl_bool_unionof_class_001]) ).
fof(f_7_2,plain,
! [U_56,U_55,U_54] :
( ( ( iext(uri_owl_unionOf,U_56,U_55)
| ? [U_53] :
( ( ~ icext(U_56,U_53)
& icext(U_54,U_53) )
| ( ~ icext(U_54,U_53)
& icext(U_56,U_53) ) )
| ~ ic(U_54)
| ~ ic(U_56) )
& ( ( ! [U_52] :
( ( icext(U_56,U_52)
| ~ icext(U_54,U_52) )
& ( icext(U_54,U_52)
| ~ icext(U_56,U_52) ) )
& ic(U_54)
& ic(U_56) )
| ~ iext(uri_owl_unionOf,U_56,U_55) ) )
| ~ iext(uri_rdf_rest,U_55,uri_rdf_nil)
| ~ iext(uri_rdf_first,U_55,U_54) ),
inference(variable_rename,[status(thm)],[f_7_1]) ).
fof(f_7_3,plain,
! [U_56,U_55,U_54] :
( ( ( iext(uri_owl_unionOf,U_56,U_55)
| ? [U_60] :
( ~ icext(U_56,U_60)
& icext(U_54,U_60) )
| ? [U_59] :
( ~ icext(U_54,U_59)
& icext(U_56,U_59) )
| ~ ic(U_54)
| ~ ic(U_56) )
& ( ( ! [U_58] :
( icext(U_56,U_58)
| ~ icext(U_54,U_58) )
& ! [U_57] :
( icext(U_54,U_57)
| ~ icext(U_56,U_57) )
& ic(U_54)
& ic(U_56) )
| ~ iext(uri_owl_unionOf,U_56,U_55) ) )
| ~ iext(uri_rdf_rest,U_55,uri_rdf_nil)
| ~ iext(uri_rdf_first,U_55,U_54) ),
inference(miniscope,[status(thm)],[f_7_2]) ).
fof(f_7_4,plain,
! [U_56,U_55,U_54] :
( ( ( iext(uri_owl_unionOf,U_56,U_55)
| ? [U_60] :
( ~ icext(U_56,U_60)
& icext(U_54,U_60) )
| ( ~ icext(U_54,sK10(U_56,U_55,U_54))
& icext(U_56,sK10(U_56,U_55,U_54)) )
| ~ ic(U_54)
| ~ ic(U_56) )
& ( ( ! [U_58] :
( icext(U_56,U_58)
| ~ icext(U_54,U_58) )
& ! [U_57] :
( icext(U_54,U_57)
| ~ icext(U_56,U_57) )
& ic(U_54)
& ic(U_56) )
| ~ iext(uri_owl_unionOf,U_56,U_55) ) )
| ~ iext(uri_rdf_rest,U_55,uri_rdf_nil)
| ~ iext(uri_rdf_first,U_55,U_54) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK10]),skolemize(U_59,sK10(U_56,U_55,U_54))],[f_7_3]) ).
fof(f_7_5,plain,
! [U_56,U_55,U_54] :
( ( ( iext(uri_owl_unionOf,U_56,U_55)
| ( ~ icext(U_56,sK11(U_56,U_55,U_54))
& icext(U_54,sK11(U_56,U_55,U_54)) )
| ( ~ icext(U_54,sK10(U_56,U_55,U_54))
& icext(U_56,sK10(U_56,U_55,U_54)) )
| ~ ic(U_54)
| ~ ic(U_56) )
& ( ( ! [U_58] :
( icext(U_56,U_58)
| ~ icext(U_54,U_58) )
& ! [U_57] :
( icext(U_54,U_57)
| ~ icext(U_56,U_57) )
& ic(U_54)
& ic(U_56) )
| ~ iext(uri_owl_unionOf,U_56,U_55) ) )
| ~ iext(uri_rdf_rest,U_55,uri_rdf_nil)
| ~ iext(uri_rdf_first,U_55,U_54) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK11]),skolemize(U_60,sK11(U_56,U_55,U_54))],[f_7_4]) ).
cnf(f_7_6,plain,
( ic(U_56)
| ~ iext(uri_owl_unionOf,U_56,U_55)
| ~ iext(uri_rdf_rest,U_55,uri_rdf_nil)
| ~ iext(uri_rdf_first,U_55,U_54) ),
inference(clausify,[status(thm)],[f_7_5]) ).
cnf(f_7_7,plain,
( ic(U_54)
| ~ iext(uri_owl_unionOf,U_56,U_55)
| ~ iext(uri_rdf_rest,U_55,uri_rdf_nil)
| ~ iext(uri_rdf_first,U_55,U_54) ),
inference(clausify,[status(thm)],[f_7_5]) ).
cnf(f_7_8,plain,
( icext(U_54,U_57)
| ~ icext(U_56,U_57)
| ~ iext(uri_owl_unionOf,U_56,U_55)
| ~ iext(uri_rdf_rest,U_55,uri_rdf_nil)
| ~ iext(uri_rdf_first,U_55,U_54) ),
inference(clausify,[status(thm)],[f_7_5]) ).
cnf(f_7_9,plain,
( icext(U_56,U_58)
| ~ icext(U_54,U_58)
| ~ iext(uri_owl_unionOf,U_56,U_55)
| ~ iext(uri_rdf_rest,U_55,uri_rdf_nil)
| ~ iext(uri_rdf_first,U_55,U_54) ),
inference(clausify,[status(thm)],[f_7_5]) ).
cnf(f_7_10,plain,
( icext(U_54,sK11(U_56,U_55,U_54))
| icext(U_56,sK10(U_56,U_55,U_54))
| ~ ic(U_54)
| ~ ic(U_56)
| iext(uri_owl_unionOf,U_56,U_55)
| ~ iext(uri_rdf_rest,U_55,uri_rdf_nil)
| ~ iext(uri_rdf_first,U_55,U_54) ),
inference(clausify,[status(thm)],[f_7_5]) ).
cnf(f_7_11,plain,
( ~ icext(U_56,sK11(U_56,U_55,U_54))
| icext(U_56,sK10(U_56,U_55,U_54))
| ~ ic(U_54)
| ~ ic(U_56)
| iext(uri_owl_unionOf,U_56,U_55)
| ~ iext(uri_rdf_rest,U_55,uri_rdf_nil)
| ~ iext(uri_rdf_first,U_55,U_54) ),
inference(clausify,[status(thm)],[f_7_5]) ).
cnf(f_7_12,plain,
( icext(U_54,sK11(U_56,U_55,U_54))
| ~ icext(U_54,sK10(U_56,U_55,U_54))
| ~ ic(U_54)
| ~ ic(U_56)
| iext(uri_owl_unionOf,U_56,U_55)
| ~ iext(uri_rdf_rest,U_55,uri_rdf_nil)
| ~ iext(uri_rdf_first,U_55,U_54) ),
inference(clausify,[status(thm)],[f_7_5]) ).
cnf(f_7_13,plain,
( ~ icext(U_56,sK11(U_56,U_55,U_54))
| ~ icext(U_54,sK10(U_56,U_55,U_54))
| ~ ic(U_54)
| ~ ic(U_56)
| iext(uri_owl_unionOf,U_56,U_55)
| ~ iext(uri_rdf_rest,U_55,uri_rdf_nil)
| ~ iext(uri_rdf_first,U_55,U_54) ),
inference(clausify,[status(thm)],[f_7_5]) ).
fof(f_8_1,plain,
! [Z,S1,C1,S2,C2] :
( ( ( iext(uri_owl_unionOf,Z,S1)
| ? [X] :
( ( ~ icext(Z,X)
& ( icext(C2,X)
| icext(C1,X) ) )
| ( ~ icext(C2,X)
& ~ icext(C1,X)
& icext(Z,X) ) )
| ~ ic(C2)
| ~ ic(C1)
| ~ ic(Z) )
& ( ( ! [X] :
( ( icext(Z,X)
| ( ~ icext(C2,X)
& ~ icext(C1,X) ) )
& ( icext(C2,X)
| icext(C1,X)
| ~ icext(Z,X) ) )
& ic(C2)
& ic(C1)
& ic(Z) )
| ~ iext(uri_owl_unionOf,Z,S1) ) )
| ~ iext(uri_rdf_rest,S2,uri_rdf_nil)
| ~ iext(uri_rdf_first,S2,C2)
| ~ iext(uri_rdf_rest,S1,S2)
| ~ iext(uri_rdf_first,S1,C1) ),
inference(fof_nnf,[status(thm)],[owl_bool_unionof_class_002]) ).
fof(f_8_2,plain,
! [U_67,U_66,U_65,U_64,U_63] :
( ( ( iext(uri_owl_unionOf,U_67,U_66)
| ? [U_62] :
( ( ~ icext(U_67,U_62)
& ( icext(U_63,U_62)
| icext(U_65,U_62) ) )
| ( ~ icext(U_63,U_62)
& ~ icext(U_65,U_62)
& icext(U_67,U_62) ) )
| ~ ic(U_63)
| ~ ic(U_65)
| ~ ic(U_67) )
& ( ( ! [U_61] :
( ( icext(U_67,U_61)
| ( ~ icext(U_63,U_61)
& ~ icext(U_65,U_61) ) )
& ( icext(U_63,U_61)
| icext(U_65,U_61)
| ~ icext(U_67,U_61) ) )
& ic(U_63)
& ic(U_65)
& ic(U_67) )
| ~ iext(uri_owl_unionOf,U_67,U_66) ) )
| ~ iext(uri_rdf_rest,U_64,uri_rdf_nil)
| ~ iext(uri_rdf_first,U_64,U_63)
| ~ iext(uri_rdf_rest,U_66,U_64)
| ~ iext(uri_rdf_first,U_66,U_65) ),
inference(variable_rename,[status(thm)],[f_8_1]) ).
fof(f_8_3,plain,
! [U_67,U_66,U_65,U_64,U_63] :
( ( ( iext(uri_owl_unionOf,U_67,U_66)
| ? [U_71] :
( ~ icext(U_67,U_71)
& ( icext(U_63,U_71)
| icext(U_65,U_71) ) )
| ? [U_70] :
( ~ icext(U_63,U_70)
& ~ icext(U_65,U_70)
& icext(U_67,U_70) )
| ~ ic(U_63)
| ~ ic(U_65)
| ~ ic(U_67) )
& ( ( ! [U_69] :
( icext(U_67,U_69)
| ( ~ icext(U_63,U_69)
& ~ icext(U_65,U_69) ) )
& ! [U_68] :
( icext(U_63,U_68)
| icext(U_65,U_68)
| ~ icext(U_67,U_68) )
& ic(U_63)
& ic(U_65)
& ic(U_67) )
| ~ iext(uri_owl_unionOf,U_67,U_66) ) )
| ~ iext(uri_rdf_rest,U_64,uri_rdf_nil)
| ~ iext(uri_rdf_first,U_64,U_63)
| ~ iext(uri_rdf_rest,U_66,U_64)
| ~ iext(uri_rdf_first,U_66,U_65) ),
inference(miniscope,[status(thm)],[f_8_2]) ).
fof(f_8_4,plain,
! [U_67,U_66,U_65,U_64,U_63] :
( ( ( iext(uri_owl_unionOf,U_67,U_66)
| ? [U_71] :
( ~ icext(U_67,U_71)
& ( icext(U_63,U_71)
| icext(U_65,U_71) ) )
| ( ~ icext(U_63,sK12(U_67,U_66,U_65,U_64,U_63))
& ~ icext(U_65,sK12(U_67,U_66,U_65,U_64,U_63))
& icext(U_67,sK12(U_67,U_66,U_65,U_64,U_63)) )
| ~ ic(U_63)
| ~ ic(U_65)
| ~ ic(U_67) )
& ( ( ! [U_69] :
( icext(U_67,U_69)
| ( ~ icext(U_63,U_69)
& ~ icext(U_65,U_69) ) )
& ! [U_68] :
( icext(U_63,U_68)
| icext(U_65,U_68)
| ~ icext(U_67,U_68) )
& ic(U_63)
& ic(U_65)
& ic(U_67) )
| ~ iext(uri_owl_unionOf,U_67,U_66) ) )
| ~ iext(uri_rdf_rest,U_64,uri_rdf_nil)
| ~ iext(uri_rdf_first,U_64,U_63)
| ~ iext(uri_rdf_rest,U_66,U_64)
| ~ iext(uri_rdf_first,U_66,U_65) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK12]),skolemize(U_70,sK12(U_67,U_66,U_65,U_64,U_63))],[f_8_3]) ).
fof(f_8_5,plain,
! [U_67,U_66,U_65,U_64,U_63] :
( ( ( iext(uri_owl_unionOf,U_67,U_66)
| ( ~ icext(U_67,sK13(U_67,U_66,U_65,U_64,U_63))
& ( icext(U_63,sK13(U_67,U_66,U_65,U_64,U_63))
| icext(U_65,sK13(U_67,U_66,U_65,U_64,U_63)) ) )
| ( ~ icext(U_63,sK12(U_67,U_66,U_65,U_64,U_63))
& ~ icext(U_65,sK12(U_67,U_66,U_65,U_64,U_63))
& icext(U_67,sK12(U_67,U_66,U_65,U_64,U_63)) )
| ~ ic(U_63)
| ~ ic(U_65)
| ~ ic(U_67) )
& ( ( ! [U_69] :
( icext(U_67,U_69)
| ( ~ icext(U_63,U_69)
& ~ icext(U_65,U_69) ) )
& ! [U_68] :
( icext(U_63,U_68)
| icext(U_65,U_68)
| ~ icext(U_67,U_68) )
& ic(U_63)
& ic(U_65)
& ic(U_67) )
| ~ iext(uri_owl_unionOf,U_67,U_66) ) )
| ~ iext(uri_rdf_rest,U_64,uri_rdf_nil)
| ~ iext(uri_rdf_first,U_64,U_63)
| ~ iext(uri_rdf_rest,U_66,U_64)
| ~ iext(uri_rdf_first,U_66,U_65) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK13]),skolemize(U_71,sK13(U_67,U_66,U_65,U_64,U_63))],[f_8_4]) ).
cnf(f_8_6,plain,
( ic(U_67)
| ~ iext(uri_owl_unionOf,U_67,U_66)
| ~ iext(uri_rdf_rest,U_64,uri_rdf_nil)
| ~ iext(uri_rdf_first,U_64,U_63)
| ~ iext(uri_rdf_rest,U_66,U_64)
| ~ iext(uri_rdf_first,U_66,U_65) ),
inference(clausify,[status(thm)],[f_8_5]) ).
cnf(f_8_7,plain,
( ic(U_65)
| ~ iext(uri_owl_unionOf,U_67,U_66)
| ~ iext(uri_rdf_rest,U_64,uri_rdf_nil)
| ~ iext(uri_rdf_first,U_64,U_63)
| ~ iext(uri_rdf_rest,U_66,U_64)
| ~ iext(uri_rdf_first,U_66,U_65) ),
inference(clausify,[status(thm)],[f_8_5]) ).
cnf(f_8_8,plain,
( ic(U_63)
| ~ iext(uri_owl_unionOf,U_67,U_66)
| ~ iext(uri_rdf_rest,U_64,uri_rdf_nil)
| ~ iext(uri_rdf_first,U_64,U_63)
| ~ iext(uri_rdf_rest,U_66,U_64)
| ~ iext(uri_rdf_first,U_66,U_65) ),
inference(clausify,[status(thm)],[f_8_5]) ).
cnf(f_8_9,plain,
( icext(U_63,U_68)
| icext(U_65,U_68)
| ~ icext(U_67,U_68)
| ~ iext(uri_owl_unionOf,U_67,U_66)
| ~ iext(uri_rdf_rest,U_64,uri_rdf_nil)
| ~ iext(uri_rdf_first,U_64,U_63)
| ~ iext(uri_rdf_rest,U_66,U_64)
| ~ iext(uri_rdf_first,U_66,U_65) ),
inference(clausify,[status(thm)],[f_8_5]) ).
cnf(f_8_10,plain,
( ~ icext(U_65,U_69)
| icext(U_67,U_69)
| ~ iext(uri_owl_unionOf,U_67,U_66)
| ~ iext(uri_rdf_rest,U_64,uri_rdf_nil)
| ~ iext(uri_rdf_first,U_64,U_63)
| ~ iext(uri_rdf_rest,U_66,U_64)
| ~ iext(uri_rdf_first,U_66,U_65) ),
inference(clausify,[status(thm)],[f_8_5]) ).
cnf(f_8_11,plain,
( ~ icext(U_63,U_69)
| icext(U_67,U_69)
| ~ iext(uri_owl_unionOf,U_67,U_66)
| ~ iext(uri_rdf_rest,U_64,uri_rdf_nil)
| ~ iext(uri_rdf_first,U_64,U_63)
| ~ iext(uri_rdf_rest,U_66,U_64)
| ~ iext(uri_rdf_first,U_66,U_65) ),
inference(clausify,[status(thm)],[f_8_5]) ).
cnf(f_8_12,plain,
( icext(U_63,sK13(U_67,U_66,U_65,U_64,U_63))
| icext(U_65,sK13(U_67,U_66,U_65,U_64,U_63))
| icext(U_67,sK12(U_67,U_66,U_65,U_64,U_63))
| ~ ic(U_63)
| ~ ic(U_65)
| ~ ic(U_67)
| iext(uri_owl_unionOf,U_67,U_66)
| ~ iext(uri_rdf_rest,U_64,uri_rdf_nil)
| ~ iext(uri_rdf_first,U_64,U_63)
| ~ iext(uri_rdf_rest,U_66,U_64)
| ~ iext(uri_rdf_first,U_66,U_65) ),
inference(clausify,[status(thm)],[f_8_5]) ).
cnf(f_8_13,plain,
( ~ icext(U_67,sK13(U_67,U_66,U_65,U_64,U_63))
| icext(U_67,sK12(U_67,U_66,U_65,U_64,U_63))
| ~ ic(U_63)
| ~ ic(U_65)
| ~ ic(U_67)
| iext(uri_owl_unionOf,U_67,U_66)
| ~ iext(uri_rdf_rest,U_64,uri_rdf_nil)
| ~ iext(uri_rdf_first,U_64,U_63)
| ~ iext(uri_rdf_rest,U_66,U_64)
| ~ iext(uri_rdf_first,U_66,U_65) ),
inference(clausify,[status(thm)],[f_8_5]) ).
cnf(f_8_14,plain,
( ~ icext(U_65,sK12(U_67,U_66,U_65,U_64,U_63))
| icext(U_63,sK13(U_67,U_66,U_65,U_64,U_63))
| icext(U_65,sK13(U_67,U_66,U_65,U_64,U_63))
| ~ ic(U_63)
| ~ ic(U_65)
| ~ ic(U_67)
| iext(uri_owl_unionOf,U_67,U_66)
| ~ iext(uri_rdf_rest,U_64,uri_rdf_nil)
| ~ iext(uri_rdf_first,U_64,U_63)
| ~ iext(uri_rdf_rest,U_66,U_64)
| ~ iext(uri_rdf_first,U_66,U_65) ),
inference(clausify,[status(thm)],[f_8_5]) ).
cnf(f_8_15,plain,
( ~ icext(U_63,sK12(U_67,U_66,U_65,U_64,U_63))
| icext(U_63,sK13(U_67,U_66,U_65,U_64,U_63))
| icext(U_65,sK13(U_67,U_66,U_65,U_64,U_63))
| ~ ic(U_63)
| ~ ic(U_65)
| ~ ic(U_67)
| iext(uri_owl_unionOf,U_67,U_66)
| ~ iext(uri_rdf_rest,U_64,uri_rdf_nil)
| ~ iext(uri_rdf_first,U_64,U_63)
| ~ iext(uri_rdf_rest,U_66,U_64)
| ~ iext(uri_rdf_first,U_66,U_65) ),
inference(clausify,[status(thm)],[f_8_5]) ).
cnf(f_8_16,plain,
( ~ icext(U_65,sK12(U_67,U_66,U_65,U_64,U_63))
| ~ icext(U_67,sK13(U_67,U_66,U_65,U_64,U_63))
| ~ ic(U_63)
| ~ ic(U_65)
| ~ ic(U_67)
| iext(uri_owl_unionOf,U_67,U_66)
| ~ iext(uri_rdf_rest,U_64,uri_rdf_nil)
| ~ iext(uri_rdf_first,U_64,U_63)
| ~ iext(uri_rdf_rest,U_66,U_64)
| ~ iext(uri_rdf_first,U_66,U_65) ),
inference(clausify,[status(thm)],[f_8_5]) ).
cnf(f_8_17,plain,
( ~ icext(U_63,sK12(U_67,U_66,U_65,U_64,U_63))
| ~ icext(U_67,sK13(U_67,U_66,U_65,U_64,U_63))
| ~ ic(U_63)
| ~ ic(U_65)
| ~ ic(U_67)
| iext(uri_owl_unionOf,U_67,U_66)
| ~ iext(uri_rdf_rest,U_64,uri_rdf_nil)
| ~ iext(uri_rdf_first,U_64,U_63)
| ~ iext(uri_rdf_rest,U_66,U_64)
| ~ iext(uri_rdf_first,U_66,U_65) ),
inference(clausify,[status(thm)],[f_8_5]) ).
fof(f_9_1,plain,
! [Z,S1,C1,S2,C2,S3,C3] :
( ( ( iext(uri_owl_unionOf,Z,S1)
| ? [X] :
( ( ~ icext(Z,X)
& ( icext(C3,X)
| icext(C2,X)
| icext(C1,X) ) )
| ( ~ icext(C3,X)
& ~ icext(C2,X)
& ~ icext(C1,X)
& icext(Z,X) ) )
| ~ ic(C3)
| ~ ic(C2)
| ~ ic(C1)
| ~ ic(Z) )
& ( ( ! [X] :
( ( icext(Z,X)
| ( ~ icext(C3,X)
& ~ icext(C2,X)
& ~ icext(C1,X) ) )
& ( icext(C3,X)
| icext(C2,X)
| icext(C1,X)
| ~ icext(Z,X) ) )
& ic(C3)
& ic(C2)
& ic(C1)
& ic(Z) )
| ~ iext(uri_owl_unionOf,Z,S1) ) )
| ~ iext(uri_rdf_rest,S3,uri_rdf_nil)
| ~ iext(uri_rdf_first,S3,C3)
| ~ iext(uri_rdf_rest,S2,S3)
| ~ iext(uri_rdf_first,S2,C2)
| ~ iext(uri_rdf_rest,S1,S2)
| ~ iext(uri_rdf_first,S1,C1) ),
inference(fof_nnf,[status(thm)],[owl_bool_unionof_class_003]) ).
fof(f_9_2,plain,
! [U_80,U_79,U_78,U_77,U_76,U_75,U_74] :
( ( ( iext(uri_owl_unionOf,U_80,U_79)
| ? [U_73] :
( ( ~ icext(U_80,U_73)
& ( icext(U_74,U_73)
| icext(U_76,U_73)
| icext(U_78,U_73) ) )
| ( ~ icext(U_74,U_73)
& ~ icext(U_76,U_73)
& ~ icext(U_78,U_73)
& icext(U_80,U_73) ) )
| ~ ic(U_74)
| ~ ic(U_76)
| ~ ic(U_78)
| ~ ic(U_80) )
& ( ( ! [U_72] :
( ( icext(U_80,U_72)
| ( ~ icext(U_74,U_72)
& ~ icext(U_76,U_72)
& ~ icext(U_78,U_72) ) )
& ( icext(U_74,U_72)
| icext(U_76,U_72)
| icext(U_78,U_72)
| ~ icext(U_80,U_72) ) )
& ic(U_74)
& ic(U_76)
& ic(U_78)
& ic(U_80) )
| ~ iext(uri_owl_unionOf,U_80,U_79) ) )
| ~ iext(uri_rdf_rest,U_75,uri_rdf_nil)
| ~ iext(uri_rdf_first,U_75,U_74)
| ~ iext(uri_rdf_rest,U_77,U_75)
| ~ iext(uri_rdf_first,U_77,U_76)
| ~ iext(uri_rdf_rest,U_79,U_77)
| ~ iext(uri_rdf_first,U_79,U_78) ),
inference(variable_rename,[status(thm)],[f_9_1]) ).
fof(f_9_3,plain,
! [U_80,U_79,U_78,U_77,U_76,U_75,U_74] :
( ( ( iext(uri_owl_unionOf,U_80,U_79)
| ? [U_84] :
( ~ icext(U_80,U_84)
& ( icext(U_74,U_84)
| icext(U_76,U_84)
| icext(U_78,U_84) ) )
| ? [U_83] :
( ~ icext(U_74,U_83)
& ~ icext(U_76,U_83)
& ~ icext(U_78,U_83)
& icext(U_80,U_83) )
| ~ ic(U_74)
| ~ ic(U_76)
| ~ ic(U_78)
| ~ ic(U_80) )
& ( ( ! [U_82] :
( icext(U_80,U_82)
| ( ~ icext(U_74,U_82)
& ~ icext(U_76,U_82)
& ~ icext(U_78,U_82) ) )
& ! [U_81] :
( icext(U_74,U_81)
| icext(U_76,U_81)
| icext(U_78,U_81)
| ~ icext(U_80,U_81) )
& ic(U_74)
& ic(U_76)
& ic(U_78)
& ic(U_80) )
| ~ iext(uri_owl_unionOf,U_80,U_79) ) )
| ~ iext(uri_rdf_rest,U_75,uri_rdf_nil)
| ~ iext(uri_rdf_first,U_75,U_74)
| ~ iext(uri_rdf_rest,U_77,U_75)
| ~ iext(uri_rdf_first,U_77,U_76)
| ~ iext(uri_rdf_rest,U_79,U_77)
| ~ iext(uri_rdf_first,U_79,U_78) ),
inference(miniscope,[status(thm)],[f_9_2]) ).
fof(f_9_4,plain,
! [U_80,U_79,U_78,U_77,U_76,U_75,U_74] :
( ( ( iext(uri_owl_unionOf,U_80,U_79)
| ? [U_84] :
( ~ icext(U_80,U_84)
& ( icext(U_74,U_84)
| icext(U_76,U_84)
| icext(U_78,U_84) ) )
| ( ~ icext(U_74,sK14(U_80,U_79,U_78,U_77,U_76,U_75,U_74))
& ~ icext(U_76,sK14(U_80,U_79,U_78,U_77,U_76,U_75,U_74))
& ~ icext(U_78,sK14(U_80,U_79,U_78,U_77,U_76,U_75,U_74))
& icext(U_80,sK14(U_80,U_79,U_78,U_77,U_76,U_75,U_74)) )
| ~ ic(U_74)
| ~ ic(U_76)
| ~ ic(U_78)
| ~ ic(U_80) )
& ( ( ! [U_82] :
( icext(U_80,U_82)
| ( ~ icext(U_74,U_82)
& ~ icext(U_76,U_82)
& ~ icext(U_78,U_82) ) )
& ! [U_81] :
( icext(U_74,U_81)
| icext(U_76,U_81)
| icext(U_78,U_81)
| ~ icext(U_80,U_81) )
& ic(U_74)
& ic(U_76)
& ic(U_78)
& ic(U_80) )
| ~ iext(uri_owl_unionOf,U_80,U_79) ) )
| ~ iext(uri_rdf_rest,U_75,uri_rdf_nil)
| ~ iext(uri_rdf_first,U_75,U_74)
| ~ iext(uri_rdf_rest,U_77,U_75)
| ~ iext(uri_rdf_first,U_77,U_76)
| ~ iext(uri_rdf_rest,U_79,U_77)
| ~ iext(uri_rdf_first,U_79,U_78) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK14]),skolemize(U_83,sK14(U_80,U_79,U_78,U_77,U_76,U_75,U_74))],[f_9_3]) ).
fof(f_9_5,plain,
! [U_80,U_79,U_78,U_77,U_76,U_75,U_74] :
( ( ( iext(uri_owl_unionOf,U_80,U_79)
| ( ~ icext(U_80,sK15(U_80,U_79,U_78,U_77,U_76,U_75,U_74))
& ( icext(U_74,sK15(U_80,U_79,U_78,U_77,U_76,U_75,U_74))
| icext(U_76,sK15(U_80,U_79,U_78,U_77,U_76,U_75,U_74))
| icext(U_78,sK15(U_80,U_79,U_78,U_77,U_76,U_75,U_74)) ) )
| ( ~ icext(U_74,sK14(U_80,U_79,U_78,U_77,U_76,U_75,U_74))
& ~ icext(U_76,sK14(U_80,U_79,U_78,U_77,U_76,U_75,U_74))
& ~ icext(U_78,sK14(U_80,U_79,U_78,U_77,U_76,U_75,U_74))
& icext(U_80,sK14(U_80,U_79,U_78,U_77,U_76,U_75,U_74)) )
| ~ ic(U_74)
| ~ ic(U_76)
| ~ ic(U_78)
| ~ ic(U_80) )
& ( ( ! [U_82] :
( icext(U_80,U_82)
| ( ~ icext(U_74,U_82)
& ~ icext(U_76,U_82)
& ~ icext(U_78,U_82) ) )
& ! [U_81] :
( icext(U_74,U_81)
| icext(U_76,U_81)
| icext(U_78,U_81)
| ~ icext(U_80,U_81) )
& ic(U_74)
& ic(U_76)
& ic(U_78)
& ic(U_80) )
| ~ iext(uri_owl_unionOf,U_80,U_79) ) )
| ~ iext(uri_rdf_rest,U_75,uri_rdf_nil)
| ~ iext(uri_rdf_first,U_75,U_74)
| ~ iext(uri_rdf_rest,U_77,U_75)
| ~ iext(uri_rdf_first,U_77,U_76)
| ~ iext(uri_rdf_rest,U_79,U_77)
| ~ iext(uri_rdf_first,U_79,U_78) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK15]),skolemize(U_84,sK15(U_80,U_79,U_78,U_77,U_76,U_75,U_74))],[f_9_4]) ).
cnf(f_9_6,plain,
( ic(U_80)
| ~ iext(uri_owl_unionOf,U_80,U_79)
| ~ iext(uri_rdf_rest,U_75,uri_rdf_nil)
| ~ iext(uri_rdf_first,U_75,U_74)
| ~ iext(uri_rdf_rest,U_77,U_75)
| ~ iext(uri_rdf_first,U_77,U_76)
| ~ iext(uri_rdf_rest,U_79,U_77)
| ~ iext(uri_rdf_first,U_79,U_78) ),
inference(clausify,[status(thm)],[f_9_5]) ).
cnf(f_9_7,plain,
( ic(U_78)
| ~ iext(uri_owl_unionOf,U_80,U_79)
| ~ iext(uri_rdf_rest,U_75,uri_rdf_nil)
| ~ iext(uri_rdf_first,U_75,U_74)
| ~ iext(uri_rdf_rest,U_77,U_75)
| ~ iext(uri_rdf_first,U_77,U_76)
| ~ iext(uri_rdf_rest,U_79,U_77)
| ~ iext(uri_rdf_first,U_79,U_78) ),
inference(clausify,[status(thm)],[f_9_5]) ).
cnf(f_9_8,plain,
( ic(U_76)
| ~ iext(uri_owl_unionOf,U_80,U_79)
| ~ iext(uri_rdf_rest,U_75,uri_rdf_nil)
| ~ iext(uri_rdf_first,U_75,U_74)
| ~ iext(uri_rdf_rest,U_77,U_75)
| ~ iext(uri_rdf_first,U_77,U_76)
| ~ iext(uri_rdf_rest,U_79,U_77)
| ~ iext(uri_rdf_first,U_79,U_78) ),
inference(clausify,[status(thm)],[f_9_5]) ).
cnf(f_9_9,plain,
( ic(U_74)
| ~ iext(uri_owl_unionOf,U_80,U_79)
| ~ iext(uri_rdf_rest,U_75,uri_rdf_nil)
| ~ iext(uri_rdf_first,U_75,U_74)
| ~ iext(uri_rdf_rest,U_77,U_75)
| ~ iext(uri_rdf_first,U_77,U_76)
| ~ iext(uri_rdf_rest,U_79,U_77)
| ~ iext(uri_rdf_first,U_79,U_78) ),
inference(clausify,[status(thm)],[f_9_5]) ).
cnf(f_9_10,plain,
( icext(U_74,U_81)
| icext(U_76,U_81)
| icext(U_78,U_81)
| ~ icext(U_80,U_81)
| ~ iext(uri_owl_unionOf,U_80,U_79)
| ~ iext(uri_rdf_rest,U_75,uri_rdf_nil)
| ~ iext(uri_rdf_first,U_75,U_74)
| ~ iext(uri_rdf_rest,U_77,U_75)
| ~ iext(uri_rdf_first,U_77,U_76)
| ~ iext(uri_rdf_rest,U_79,U_77)
| ~ iext(uri_rdf_first,U_79,U_78) ),
inference(clausify,[status(thm)],[f_9_5]) ).
cnf(f_9_11,plain,
( ~ icext(U_78,U_82)
| icext(U_80,U_82)
| ~ iext(uri_owl_unionOf,U_80,U_79)
| ~ iext(uri_rdf_rest,U_75,uri_rdf_nil)
| ~ iext(uri_rdf_first,U_75,U_74)
| ~ iext(uri_rdf_rest,U_77,U_75)
| ~ iext(uri_rdf_first,U_77,U_76)
| ~ iext(uri_rdf_rest,U_79,U_77)
| ~ iext(uri_rdf_first,U_79,U_78) ),
inference(clausify,[status(thm)],[f_9_5]) ).
cnf(f_9_12,plain,
( ~ icext(U_76,U_82)
| icext(U_80,U_82)
| ~ iext(uri_owl_unionOf,U_80,U_79)
| ~ iext(uri_rdf_rest,U_75,uri_rdf_nil)
| ~ iext(uri_rdf_first,U_75,U_74)
| ~ iext(uri_rdf_rest,U_77,U_75)
| ~ iext(uri_rdf_first,U_77,U_76)
| ~ iext(uri_rdf_rest,U_79,U_77)
| ~ iext(uri_rdf_first,U_79,U_78) ),
inference(clausify,[status(thm)],[f_9_5]) ).
cnf(f_9_13,plain,
( ~ icext(U_74,U_82)
| icext(U_80,U_82)
| ~ iext(uri_owl_unionOf,U_80,U_79)
| ~ iext(uri_rdf_rest,U_75,uri_rdf_nil)
| ~ iext(uri_rdf_first,U_75,U_74)
| ~ iext(uri_rdf_rest,U_77,U_75)
| ~ iext(uri_rdf_first,U_77,U_76)
| ~ iext(uri_rdf_rest,U_79,U_77)
| ~ iext(uri_rdf_first,U_79,U_78) ),
inference(clausify,[status(thm)],[f_9_5]) ).
cnf(f_9_14,plain,
( icext(U_74,sK15(U_80,U_79,U_78,U_77,U_76,U_75,U_74))
| icext(U_76,sK15(U_80,U_79,U_78,U_77,U_76,U_75,U_74))
| icext(U_78,sK15(U_80,U_79,U_78,U_77,U_76,U_75,U_74))
| icext(U_80,sK14(U_80,U_79,U_78,U_77,U_76,U_75,U_74))
| ~ ic(U_74)
| ~ ic(U_76)
| ~ ic(U_78)
| ~ ic(U_80)
| iext(uri_owl_unionOf,U_80,U_79)
| ~ iext(uri_rdf_rest,U_75,uri_rdf_nil)
| ~ iext(uri_rdf_first,U_75,U_74)
| ~ iext(uri_rdf_rest,U_77,U_75)
| ~ iext(uri_rdf_first,U_77,U_76)
| ~ iext(uri_rdf_rest,U_79,U_77)
| ~ iext(uri_rdf_first,U_79,U_78) ),
inference(clausify,[status(thm)],[f_9_5]) ).
cnf(f_9_15,plain,
( ~ icext(U_80,sK15(U_80,U_79,U_78,U_77,U_76,U_75,U_74))
| icext(U_80,sK14(U_80,U_79,U_78,U_77,U_76,U_75,U_74))
| ~ ic(U_74)
| ~ ic(U_76)
| ~ ic(U_78)
| ~ ic(U_80)
| iext(uri_owl_unionOf,U_80,U_79)
| ~ iext(uri_rdf_rest,U_75,uri_rdf_nil)
| ~ iext(uri_rdf_first,U_75,U_74)
| ~ iext(uri_rdf_rest,U_77,U_75)
| ~ iext(uri_rdf_first,U_77,U_76)
| ~ iext(uri_rdf_rest,U_79,U_77)
| ~ iext(uri_rdf_first,U_79,U_78) ),
inference(clausify,[status(thm)],[f_9_5]) ).
cnf(f_9_16,plain,
( ~ icext(U_78,sK14(U_80,U_79,U_78,U_77,U_76,U_75,U_74))
| icext(U_74,sK15(U_80,U_79,U_78,U_77,U_76,U_75,U_74))
| icext(U_76,sK15(U_80,U_79,U_78,U_77,U_76,U_75,U_74))
| icext(U_78,sK15(U_80,U_79,U_78,U_77,U_76,U_75,U_74))
| ~ ic(U_74)
| ~ ic(U_76)
| ~ ic(U_78)
| ~ ic(U_80)
| iext(uri_owl_unionOf,U_80,U_79)
| ~ iext(uri_rdf_rest,U_75,uri_rdf_nil)
| ~ iext(uri_rdf_first,U_75,U_74)
| ~ iext(uri_rdf_rest,U_77,U_75)
| ~ iext(uri_rdf_first,U_77,U_76)
| ~ iext(uri_rdf_rest,U_79,U_77)
| ~ iext(uri_rdf_first,U_79,U_78) ),
inference(clausify,[status(thm)],[f_9_5]) ).
cnf(f_9_17,plain,
( ~ icext(U_76,sK14(U_80,U_79,U_78,U_77,U_76,U_75,U_74))
| icext(U_74,sK15(U_80,U_79,U_78,U_77,U_76,U_75,U_74))
| icext(U_76,sK15(U_80,U_79,U_78,U_77,U_76,U_75,U_74))
| icext(U_78,sK15(U_80,U_79,U_78,U_77,U_76,U_75,U_74))
| ~ ic(U_74)
| ~ ic(U_76)
| ~ ic(U_78)
| ~ ic(U_80)
| iext(uri_owl_unionOf,U_80,U_79)
| ~ iext(uri_rdf_rest,U_75,uri_rdf_nil)
| ~ iext(uri_rdf_first,U_75,U_74)
| ~ iext(uri_rdf_rest,U_77,U_75)
| ~ iext(uri_rdf_first,U_77,U_76)
| ~ iext(uri_rdf_rest,U_79,U_77)
| ~ iext(uri_rdf_first,U_79,U_78) ),
inference(clausify,[status(thm)],[f_9_5]) ).
cnf(f_9_18,plain,
( ~ icext(U_74,sK14(U_80,U_79,U_78,U_77,U_76,U_75,U_74))
| icext(U_74,sK15(U_80,U_79,U_78,U_77,U_76,U_75,U_74))
| icext(U_76,sK15(U_80,U_79,U_78,U_77,U_76,U_75,U_74))
| icext(U_78,sK15(U_80,U_79,U_78,U_77,U_76,U_75,U_74))
| ~ ic(U_74)
| ~ ic(U_76)
| ~ ic(U_78)
| ~ ic(U_80)
| iext(uri_owl_unionOf,U_80,U_79)
| ~ iext(uri_rdf_rest,U_75,uri_rdf_nil)
| ~ iext(uri_rdf_first,U_75,U_74)
| ~ iext(uri_rdf_rest,U_77,U_75)
| ~ iext(uri_rdf_first,U_77,U_76)
| ~ iext(uri_rdf_rest,U_79,U_77)
| ~ iext(uri_rdf_first,U_79,U_78) ),
inference(clausify,[status(thm)],[f_9_5]) ).
cnf(f_9_19,plain,
( ~ icext(U_78,sK14(U_80,U_79,U_78,U_77,U_76,U_75,U_74))
| ~ icext(U_80,sK15(U_80,U_79,U_78,U_77,U_76,U_75,U_74))
| ~ ic(U_74)
| ~ ic(U_76)
| ~ ic(U_78)
| ~ ic(U_80)
| iext(uri_owl_unionOf,U_80,U_79)
| ~ iext(uri_rdf_rest,U_75,uri_rdf_nil)
| ~ iext(uri_rdf_first,U_75,U_74)
| ~ iext(uri_rdf_rest,U_77,U_75)
| ~ iext(uri_rdf_first,U_77,U_76)
| ~ iext(uri_rdf_rest,U_79,U_77)
| ~ iext(uri_rdf_first,U_79,U_78) ),
inference(clausify,[status(thm)],[f_9_5]) ).
cnf(f_9_20,plain,
( ~ icext(U_76,sK14(U_80,U_79,U_78,U_77,U_76,U_75,U_74))
| ~ icext(U_80,sK15(U_80,U_79,U_78,U_77,U_76,U_75,U_74))
| ~ ic(U_74)
| ~ ic(U_76)
| ~ ic(U_78)
| ~ ic(U_80)
| iext(uri_owl_unionOf,U_80,U_79)
| ~ iext(uri_rdf_rest,U_75,uri_rdf_nil)
| ~ iext(uri_rdf_first,U_75,U_74)
| ~ iext(uri_rdf_rest,U_77,U_75)
| ~ iext(uri_rdf_first,U_77,U_76)
| ~ iext(uri_rdf_rest,U_79,U_77)
| ~ iext(uri_rdf_first,U_79,U_78) ),
inference(clausify,[status(thm)],[f_9_5]) ).
cnf(f_9_21,plain,
( ~ icext(U_74,sK14(U_80,U_79,U_78,U_77,U_76,U_75,U_74))
| ~ icext(U_80,sK15(U_80,U_79,U_78,U_77,U_76,U_75,U_74))
| ~ ic(U_74)
| ~ ic(U_76)
| ~ ic(U_78)
| ~ ic(U_80)
| iext(uri_owl_unionOf,U_80,U_79)
| ~ iext(uri_rdf_rest,U_75,uri_rdf_nil)
| ~ iext(uri_rdf_first,U_75,U_74)
| ~ iext(uri_rdf_rest,U_77,U_75)
| ~ iext(uri_rdf_first,U_77,U_76)
| ~ iext(uri_rdf_rest,U_79,U_77)
| ~ iext(uri_rdf_first,U_79,U_78) ),
inference(clausify,[status(thm)],[f_9_5]) ).
fof(f_10_1,plain,
! [X] : ~ icext(uri_owl_Nothing,X),
inference(fof_nnf,[status(thm)],[owl_class_nothing_ext]) ).
fof(f_10_2,plain,
! [U_85] : ~ icext(uri_owl_Nothing,U_85),
inference(variable_rename,[status(thm)],[f_10_1]) ).
cnf(f_10_3,plain,
~ icext(uri_owl_Nothing,U_85),
inference(clausify,[status(thm)],[f_10_2]) ).
fof(f_11_1,plain,
ic(uri_owl_Nothing),
inference(fof_nnf,[status(thm)],[owl_class_nothing_type]) ).
cnf(f_11_2,plain,
ic(uri_owl_Nothing),
inference(clausify,[status(thm)],[f_11_1]) ).
fof(f_12_1,plain,
! [X] :
( ( icext(uri_owl_Thing,X)
| ~ ir(X) )
& ( ir(X)
| ~ icext(uri_owl_Thing,X) ) ),
inference(fof_nnf,[status(thm)],[owl_class_thing_ext]) ).
fof(f_12_2,plain,
! [U_86] :
( ( icext(uri_owl_Thing,U_86)
| ~ ir(U_86) )
& ( ir(U_86)
| ~ icext(uri_owl_Thing,U_86) ) ),
inference(variable_rename,[status(thm)],[f_12_1]) ).
fof(f_12_3,plain,
( ! [U_88] :
( icext(uri_owl_Thing,U_88)
| ~ ir(U_88) )
& ! [U_87] :
( ir(U_87)
| ~ icext(uri_owl_Thing,U_87) ) ),
inference(miniscope,[status(thm)],[f_12_2]) ).
cnf(f_12_4,plain,
( ir(U_87)
| ~ icext(uri_owl_Thing,U_87) ),
inference(clausify,[status(thm)],[f_12_3]) ).
cnf(f_12_5,plain,
( icext(uri_owl_Thing,U_88)
| ~ ir(U_88) ),
inference(clausify,[status(thm)],[f_12_3]) ).
fof(f_13_1,plain,
ic(uri_owl_Thing),
inference(fof_nnf,[status(thm)],[owl_class_thing_type]) ).
cnf(f_13_2,plain,
ic(uri_owl_Thing),
inference(clausify,[status(thm)],[f_13_1]) ).
fof(f_14_1,plain,
! [X] :
( ! [Y] :
( ir(Y)
| ~ icext(X,Y) )
| ~ ic(X) ),
inference(fof_nnf,[status(thm)],[owl_parts_ic_cond_inst]) ).
fof(f_14_2,plain,
! [U_90] :
( ! [U_89] :
( ir(U_89)
| ~ icext(U_90,U_89) )
| ~ ic(U_90) ),
inference(variable_rename,[status(thm)],[f_14_1]) ).
cnf(f_14_3,plain,
( ir(U_89)
| ~ icext(U_90,U_89)
| ~ ic(U_90) ),
inference(clausify,[status(thm)],[f_14_2]) ).
fof(f_15_1,plain,
! [X] :
( ir(X)
| ~ ic(X) ),
inference(fof_nnf,[status(thm)],[owl_parts_ic_cond_set]) ).
fof(f_15_2,plain,
! [U_91] :
( ir(U_91)
| ~ ic(U_91) ),
inference(variable_rename,[status(thm)],[f_15_1]) ).
cnf(f_15_3,plain,
( ir(U_91)
| ~ ic(U_91) ),
inference(clausify,[status(thm)],[f_15_2]) ).
fof(f_16_1,plain,
! [X] :
( ( ic(X)
| ~ iext(uri_rdf_type,X,uri_rdfs_Class) )
& ( iext(uri_rdf_type,X,uri_rdfs_Class)
| ~ ic(X) ) ),
inference(fof_nnf,[status(thm)],[owl_parts_ic_def]) ).
fof(f_16_2,plain,
! [U_92] :
( ( ic(U_92)
| ~ iext(uri_rdf_type,U_92,uri_rdfs_Class) )
& ( iext(uri_rdf_type,U_92,uri_rdfs_Class)
| ~ ic(U_92) ) ),
inference(variable_rename,[status(thm)],[f_16_1]) ).
fof(f_16_3,plain,
( ! [U_94] :
( ic(U_94)
| ~ iext(uri_rdf_type,U_94,uri_rdfs_Class) )
& ! [U_93] :
( iext(uri_rdf_type,U_93,uri_rdfs_Class)
| ~ ic(U_93) ) ),
inference(miniscope,[status(thm)],[f_16_2]) ).
cnf(f_16_4,plain,
( iext(uri_rdf_type,U_93,uri_rdfs_Class)
| ~ ic(U_93) ),
inference(clausify,[status(thm)],[f_16_3]) ).
cnf(f_16_5,plain,
( ic(U_94)
| ~ iext(uri_rdf_type,U_94,uri_rdfs_Class) ),
inference(clausify,[status(thm)],[f_16_3]) ).
fof(f_17_1,plain,
! [X] :
( ! [Y] :
( lv(Y)
| ~ icext(X,Y) )
| ~ idc(X) ),
inference(fof_nnf,[status(thm)],[owl_parts_idc_cond_inst]) ).
fof(f_17_2,plain,
! [U_96] :
( ! [U_95] :
( lv(U_95)
| ~ icext(U_96,U_95) )
| ~ idc(U_96) ),
inference(variable_rename,[status(thm)],[f_17_1]) ).
cnf(f_17_3,plain,
( lv(U_95)
| ~ icext(U_96,U_95)
| ~ idc(U_96) ),
inference(clausify,[status(thm)],[f_17_2]) ).
fof(f_18_1,plain,
! [X] :
( ic(X)
| ~ idc(X) ),
inference(fof_nnf,[status(thm)],[owl_parts_idc_cond_set]) ).
fof(f_18_2,plain,
! [U_97] :
( ic(U_97)
| ~ idc(U_97) ),
inference(variable_rename,[status(thm)],[f_18_1]) ).
cnf(f_18_3,plain,
( ic(U_97)
| ~ idc(U_97) ),
inference(clausify,[status(thm)],[f_18_2]) ).
fof(f_19_1,plain,
! [X] :
( ( idc(X)
| ~ iext(uri_rdf_type,X,uri_rdfs_Datatype) )
& ( iext(uri_rdf_type,X,uri_rdfs_Datatype)
| ~ idc(X) ) ),
inference(fof_nnf,[status(thm)],[owl_parts_idc_def]) ).
fof(f_19_2,plain,
! [U_98] :
( ( idc(U_98)
| ~ iext(uri_rdf_type,U_98,uri_rdfs_Datatype) )
& ( iext(uri_rdf_type,U_98,uri_rdfs_Datatype)
| ~ idc(U_98) ) ),
inference(variable_rename,[status(thm)],[f_19_1]) ).
fof(f_19_3,plain,
( ! [U_100] :
( idc(U_100)
| ~ iext(uri_rdf_type,U_100,uri_rdfs_Datatype) )
& ! [U_99] :
( iext(uri_rdf_type,U_99,uri_rdfs_Datatype)
| ~ idc(U_99) ) ),
inference(miniscope,[status(thm)],[f_19_2]) ).
cnf(f_19_4,plain,
( iext(uri_rdf_type,U_99,uri_rdfs_Datatype)
| ~ idc(U_99) ),
inference(clausify,[status(thm)],[f_19_3]) ).
cnf(f_19_5,plain,
( idc(U_100)
| ~ iext(uri_rdf_type,U_100,uri_rdfs_Datatype) ),
inference(clausify,[status(thm)],[f_19_3]) ).
fof(f_20_1,plain,
! [X] :
( ! [Y,Z] :
( ( ir(Z)
& ir(Y) )
| ~ iext(X,Y,Z) )
| ~ ioap(X) ),
inference(fof_nnf,[status(thm)],[owl_parts_ioap_cond_inst]) ).
fof(f_20_2,plain,
! [U_103] :
( ! [U_102,U_101] :
( ( ir(U_101)
& ir(U_102) )
| ~ iext(U_103,U_102,U_101) )
| ~ ioap(U_103) ),
inference(variable_rename,[status(thm)],[f_20_1]) ).
cnf(f_20_3,plain,
( ir(U_102)
| ~ iext(U_103,U_102,U_101)
| ~ ioap(U_103) ),
inference(clausify,[status(thm)],[f_20_2]) ).
cnf(f_20_4,plain,
( ir(U_101)
| ~ iext(U_103,U_102,U_101)
| ~ ioap(U_103) ),
inference(clausify,[status(thm)],[f_20_2]) ).
fof(f_21_1,plain,
! [X] :
( ip(X)
| ~ ioap(X) ),
inference(fof_nnf,[status(thm)],[owl_parts_ioap_cond_set]) ).
fof(f_21_2,plain,
! [U_104] :
( ip(U_104)
| ~ ioap(U_104) ),
inference(variable_rename,[status(thm)],[f_21_1]) ).
cnf(f_21_3,plain,
( ip(U_104)
| ~ ioap(U_104) ),
inference(clausify,[status(thm)],[f_21_2]) ).
fof(f_22_1,plain,
! [X] :
( ( ioap(X)
| ~ iext(uri_rdf_type,X,uri_owl_AnnotationProperty) )
& ( iext(uri_rdf_type,X,uri_owl_AnnotationProperty)
| ~ ioap(X) ) ),
inference(fof_nnf,[status(thm)],[owl_parts_ioap_def]) ).
fof(f_22_2,plain,
! [U_105] :
( ( ioap(U_105)
| ~ iext(uri_rdf_type,U_105,uri_owl_AnnotationProperty) )
& ( iext(uri_rdf_type,U_105,uri_owl_AnnotationProperty)
| ~ ioap(U_105) ) ),
inference(variable_rename,[status(thm)],[f_22_1]) ).
fof(f_22_3,plain,
( ! [U_107] :
( ioap(U_107)
| ~ iext(uri_rdf_type,U_107,uri_owl_AnnotationProperty) )
& ! [U_106] :
( iext(uri_rdf_type,U_106,uri_owl_AnnotationProperty)
| ~ ioap(U_106) ) ),
inference(miniscope,[status(thm)],[f_22_2]) ).
cnf(f_22_4,plain,
( iext(uri_rdf_type,U_106,uri_owl_AnnotationProperty)
| ~ ioap(U_106) ),
inference(clausify,[status(thm)],[f_22_3]) ).
cnf(f_22_5,plain,
( ioap(U_107)
| ~ iext(uri_rdf_type,U_107,uri_owl_AnnotationProperty) ),
inference(clausify,[status(thm)],[f_22_3]) ).
fof(f_23_1,plain,
! [X] :
( ! [Y,Z] :
( ( lv(Z)
& ir(Y) )
| ~ iext(X,Y,Z) )
| ~ iodp(X) ),
inference(fof_nnf,[status(thm)],[owl_parts_iodp_cond_inst]) ).
fof(f_23_2,plain,
! [U_110] :
( ! [U_109,U_108] :
( ( lv(U_108)
& ir(U_109) )
| ~ iext(U_110,U_109,U_108) )
| ~ iodp(U_110) ),
inference(variable_rename,[status(thm)],[f_23_1]) ).
cnf(f_23_3,plain,
( ir(U_109)
| ~ iext(U_110,U_109,U_108)
| ~ iodp(U_110) ),
inference(clausify,[status(thm)],[f_23_2]) ).
cnf(f_23_4,plain,
( lv(U_108)
| ~ iext(U_110,U_109,U_108)
| ~ iodp(U_110) ),
inference(clausify,[status(thm)],[f_23_2]) ).
fof(f_24_1,plain,
! [X] :
( ip(X)
| ~ iodp(X) ),
inference(fof_nnf,[status(thm)],[owl_parts_iodp_cond_set]) ).
fof(f_24_2,plain,
! [U_111] :
( ip(U_111)
| ~ iodp(U_111) ),
inference(variable_rename,[status(thm)],[f_24_1]) ).
cnf(f_24_3,plain,
( ip(U_111)
| ~ iodp(U_111) ),
inference(clausify,[status(thm)],[f_24_2]) ).
fof(f_25_1,plain,
! [X] :
( ( iodp(X)
| ~ iext(uri_rdf_type,X,uri_owl_DatatypeProperty) )
& ( iext(uri_rdf_type,X,uri_owl_DatatypeProperty)
| ~ iodp(X) ) ),
inference(fof_nnf,[status(thm)],[owl_parts_iodp_def]) ).
fof(f_25_2,plain,
! [U_112] :
( ( iodp(U_112)
| ~ iext(uri_rdf_type,U_112,uri_owl_DatatypeProperty) )
& ( iext(uri_rdf_type,U_112,uri_owl_DatatypeProperty)
| ~ iodp(U_112) ) ),
inference(variable_rename,[status(thm)],[f_25_1]) ).
fof(f_25_3,plain,
( ! [U_114] :
( iodp(U_114)
| ~ iext(uri_rdf_type,U_114,uri_owl_DatatypeProperty) )
& ! [U_113] :
( iext(uri_rdf_type,U_113,uri_owl_DatatypeProperty)
| ~ iodp(U_113) ) ),
inference(miniscope,[status(thm)],[f_25_2]) ).
cnf(f_25_4,plain,
( iext(uri_rdf_type,U_113,uri_owl_DatatypeProperty)
| ~ iodp(U_113) ),
inference(clausify,[status(thm)],[f_25_3]) ).
cnf(f_25_5,plain,
( iodp(U_114)
| ~ iext(uri_rdf_type,U_114,uri_owl_DatatypeProperty) ),
inference(clausify,[status(thm)],[f_25_3]) ).
fof(f_26_1,plain,
! [X] :
( ! [Y,Z] :
( ( ix(Z)
& ix(Y) )
| ~ iext(X,Y,Z) )
| ~ ioxp(X) ),
inference(fof_nnf,[status(thm)],[owl_parts_ioxp_cond_inst]) ).
fof(f_26_2,plain,
! [U_117] :
( ! [U_116,U_115] :
( ( ix(U_115)
& ix(U_116) )
| ~ iext(U_117,U_116,U_115) )
| ~ ioxp(U_117) ),
inference(variable_rename,[status(thm)],[f_26_1]) ).
cnf(f_26_3,plain,
( ix(U_116)
| ~ iext(U_117,U_116,U_115)
| ~ ioxp(U_117) ),
inference(clausify,[status(thm)],[f_26_2]) ).
cnf(f_26_4,plain,
( ix(U_115)
| ~ iext(U_117,U_116,U_115)
| ~ ioxp(U_117) ),
inference(clausify,[status(thm)],[f_26_2]) ).
fof(f_27_1,plain,
! [X] :
( ip(X)
| ~ ioxp(X) ),
inference(fof_nnf,[status(thm)],[owl_parts_ioxp_cond_set]) ).
fof(f_27_2,plain,
! [U_118] :
( ip(U_118)
| ~ ioxp(U_118) ),
inference(variable_rename,[status(thm)],[f_27_1]) ).
cnf(f_27_3,plain,
( ip(U_118)
| ~ ioxp(U_118) ),
inference(clausify,[status(thm)],[f_27_2]) ).
fof(f_28_1,plain,
! [X] :
( ( ioxp(X)
| ~ iext(uri_rdf_type,X,uri_owl_OntologyProperty) )
& ( iext(uri_rdf_type,X,uri_owl_OntologyProperty)
| ~ ioxp(X) ) ),
inference(fof_nnf,[status(thm)],[owl_parts_ioxp_def]) ).
fof(f_28_2,plain,
! [U_119] :
( ( ioxp(U_119)
| ~ iext(uri_rdf_type,U_119,uri_owl_OntologyProperty) )
& ( iext(uri_rdf_type,U_119,uri_owl_OntologyProperty)
| ~ ioxp(U_119) ) ),
inference(variable_rename,[status(thm)],[f_28_1]) ).
fof(f_28_3,plain,
( ! [U_121] :
( ioxp(U_121)
| ~ iext(uri_rdf_type,U_121,uri_owl_OntologyProperty) )
& ! [U_120] :
( iext(uri_rdf_type,U_120,uri_owl_OntologyProperty)
| ~ ioxp(U_120) ) ),
inference(miniscope,[status(thm)],[f_28_2]) ).
cnf(f_28_4,plain,
( iext(uri_rdf_type,U_120,uri_owl_OntologyProperty)
| ~ ioxp(U_120) ),
inference(clausify,[status(thm)],[f_28_3]) ).
cnf(f_28_5,plain,
( ioxp(U_121)
| ~ iext(uri_rdf_type,U_121,uri_owl_OntologyProperty) ),
inference(clausify,[status(thm)],[f_28_3]) ).
fof(f_29_1,plain,
! [X] :
( ! [Y,Z] :
( ( ir(Z)
& ir(Y) )
| ~ iext(X,Y,Z) )
| ~ ip(X) ),
inference(fof_nnf,[status(thm)],[owl_parts_ip_cond_inst]) ).
fof(f_29_2,plain,
! [U_124] :
( ! [U_123,U_122] :
( ( ir(U_122)
& ir(U_123) )
| ~ iext(U_124,U_123,U_122) )
| ~ ip(U_124) ),
inference(variable_rename,[status(thm)],[f_29_1]) ).
cnf(f_29_3,plain,
( ir(U_123)
| ~ iext(U_124,U_123,U_122)
| ~ ip(U_124) ),
inference(clausify,[status(thm)],[f_29_2]) ).
cnf(f_29_4,plain,
( ir(U_122)
| ~ iext(U_124,U_123,U_122)
| ~ ip(U_124) ),
inference(clausify,[status(thm)],[f_29_2]) ).
fof(f_30_1,plain,
! [X] :
( ir(X)
| ~ ip(X) ),
inference(fof_nnf,[status(thm)],[owl_parts_ip_cond_set]) ).
fof(f_30_2,plain,
! [U_125] :
( ir(U_125)
| ~ ip(U_125) ),
inference(variable_rename,[status(thm)],[f_30_1]) ).
cnf(f_30_3,plain,
( ir(U_125)
| ~ ip(U_125) ),
inference(clausify,[status(thm)],[f_30_2]) ).
fof(f_31_1,plain,
! [X] :
( ( ip(X)
| ~ iext(uri_rdf_type,X,uri_rdf_Property) )
& ( iext(uri_rdf_type,X,uri_rdf_Property)
| ~ ip(X) ) ),
inference(fof_nnf,[status(thm)],[owl_parts_ip_def]) ).
fof(f_31_2,plain,
! [U_126] :
( ( ip(U_126)
| ~ iext(uri_rdf_type,U_126,uri_rdf_Property) )
& ( iext(uri_rdf_type,U_126,uri_rdf_Property)
| ~ ip(U_126) ) ),
inference(variable_rename,[status(thm)],[f_31_1]) ).
fof(f_31_3,plain,
( ! [U_128] :
( ip(U_128)
| ~ iext(uri_rdf_type,U_128,uri_rdf_Property) )
& ! [U_127] :
( iext(uri_rdf_type,U_127,uri_rdf_Property)
| ~ ip(U_127) ) ),
inference(miniscope,[status(thm)],[f_31_2]) ).
cnf(f_31_4,plain,
( iext(uri_rdf_type,U_127,uri_rdf_Property)
| ~ ip(U_127) ),
inference(clausify,[status(thm)],[f_31_3]) ).
cnf(f_31_5,plain,
( ip(U_128)
| ~ iext(uri_rdf_type,U_128,uri_rdf_Property) ),
inference(clausify,[status(thm)],[f_31_3]) ).
fof(f_32_1,plain,
? [X] : ir(X),
inference(fof_nnf,[status(thm)],[owl_parts_ir_cond_set]) ).
fof(f_32_2,plain,
? [U_129] : ir(U_129),
inference(variable_rename,[status(thm)],[f_32_1]) ).
fof(f_32_3,plain,
ir(sK16),
inference(skolemize,[status(esa),new_symbols(skolem,[sK16]),skolemize(U_129,sK16)],[f_32_2]) ).
cnf(f_32_4,plain,
ir(sK16),
inference(clausify,[status(thm)],[f_32_3]) ).
fof(f_33_1,plain,
! [X] :
( ( ir(X)
| ~ iext(uri_rdf_type,X,uri_rdfs_Resource) )
& ( iext(uri_rdf_type,X,uri_rdfs_Resource)
| ~ ir(X) ) ),
inference(fof_nnf,[status(thm)],[owl_parts_ir_def]) ).
fof(f_33_2,plain,
! [U_130] :
( ( ir(U_130)
| ~ iext(uri_rdf_type,U_130,uri_rdfs_Resource) )
& ( iext(uri_rdf_type,U_130,uri_rdfs_Resource)
| ~ ir(U_130) ) ),
inference(variable_rename,[status(thm)],[f_33_1]) ).
fof(f_33_3,plain,
( ! [U_132] :
( ir(U_132)
| ~ iext(uri_rdf_type,U_132,uri_rdfs_Resource) )
& ! [U_131] :
( iext(uri_rdf_type,U_131,uri_rdfs_Resource)
| ~ ir(U_131) ) ),
inference(miniscope,[status(thm)],[f_33_2]) ).
cnf(f_33_4,plain,
( iext(uri_rdf_type,U_131,uri_rdfs_Resource)
| ~ ir(U_131) ),
inference(clausify,[status(thm)],[f_33_3]) ).
cnf(f_33_5,plain,
( ir(U_132)
| ~ iext(uri_rdf_type,U_132,uri_rdfs_Resource) ),
inference(clausify,[status(thm)],[f_33_3]) ).
fof(f_34_1,plain,
! [X] :
( ir(X)
| ~ ix(X) ),
inference(fof_nnf,[status(thm)],[owl_parts_ix_cond_set]) ).
fof(f_34_2,plain,
! [U_133] :
( ir(U_133)
| ~ ix(U_133) ),
inference(variable_rename,[status(thm)],[f_34_1]) ).
cnf(f_34_3,plain,
( ir(U_133)
| ~ ix(U_133) ),
inference(clausify,[status(thm)],[f_34_2]) ).
fof(f_35_1,plain,
! [X] :
( ( ix(X)
| ~ iext(uri_rdf_type,X,uri_owl_Ontology) )
& ( iext(uri_rdf_type,X,uri_owl_Ontology)
| ~ ix(X) ) ),
inference(fof_nnf,[status(thm)],[owl_parts_ix_def]) ).
fof(f_35_2,plain,
! [U_134] :
( ( ix(U_134)
| ~ iext(uri_rdf_type,U_134,uri_owl_Ontology) )
& ( iext(uri_rdf_type,U_134,uri_owl_Ontology)
| ~ ix(U_134) ) ),
inference(variable_rename,[status(thm)],[f_35_1]) ).
fof(f_35_3,plain,
( ! [U_136] :
( ix(U_136)
| ~ iext(uri_rdf_type,U_136,uri_owl_Ontology) )
& ! [U_135] :
( iext(uri_rdf_type,U_135,uri_owl_Ontology)
| ~ ix(U_135) ) ),
inference(miniscope,[status(thm)],[f_35_2]) ).
cnf(f_35_4,plain,
( iext(uri_rdf_type,U_135,uri_owl_Ontology)
| ~ ix(U_135) ),
inference(clausify,[status(thm)],[f_35_3]) ).
cnf(f_35_5,plain,
( ix(U_136)
| ~ iext(uri_rdf_type,U_136,uri_owl_Ontology) ),
inference(clausify,[status(thm)],[f_35_3]) ).
fof(f_36_1,plain,
! [X] :
( ir(X)
| ~ lv(X) ),
inference(fof_nnf,[status(thm)],[owl_parts_lv_cond_set]) ).
fof(f_36_2,plain,
! [U_137] :
( ir(U_137)
| ~ lv(U_137) ),
inference(variable_rename,[status(thm)],[f_36_1]) ).
cnf(f_36_3,plain,
( ir(U_137)
| ~ lv(U_137) ),
inference(clausify,[status(thm)],[f_36_2]) ).
fof(f_37_1,plain,
! [X] :
( ( lv(X)
| ~ iext(uri_rdf_type,X,uri_rdfs_Literal) )
& ( iext(uri_rdf_type,X,uri_rdfs_Literal)
| ~ lv(X) ) ),
inference(fof_nnf,[status(thm)],[owl_parts_lv_def]) ).
fof(f_37_2,plain,
! [U_138] :
( ( lv(U_138)
| ~ iext(uri_rdf_type,U_138,uri_rdfs_Literal) )
& ( iext(uri_rdf_type,U_138,uri_rdfs_Literal)
| ~ lv(U_138) ) ),
inference(variable_rename,[status(thm)],[f_37_1]) ).
fof(f_37_3,plain,
( ! [U_140] :
( lv(U_140)
| ~ iext(uri_rdf_type,U_140,uri_rdfs_Literal) )
& ! [U_139] :
( iext(uri_rdf_type,U_139,uri_rdfs_Literal)
| ~ lv(U_139) ) ),
inference(miniscope,[status(thm)],[f_37_2]) ).
cnf(f_37_4,plain,
( iext(uri_rdf_type,U_139,uri_rdfs_Literal)
| ~ lv(U_139) ),
inference(clausify,[status(thm)],[f_37_3]) ).
cnf(f_37_5,plain,
( lv(U_140)
| ~ iext(uri_rdf_type,U_140,uri_rdfs_Literal) ),
inference(clausify,[status(thm)],[f_37_3]) ).
fof(f_38_1,plain,
! [X,Y] :
( ( ic(Y)
& icext(uri_owl_Restriction,X) )
| ~ iext(uri_owl_allValuesFrom,X,Y) ),
inference(fof_nnf,[status(thm)],[owl_prop_allvaluesfrom_ext]) ).
fof(f_38_2,plain,
! [U_142,U_141] :
( ( ic(U_141)
& icext(uri_owl_Restriction,U_142) )
| ~ iext(uri_owl_allValuesFrom,U_142,U_141) ),
inference(variable_rename,[status(thm)],[f_38_1]) ).
cnf(f_38_3,plain,
( icext(uri_owl_Restriction,U_142)
| ~ iext(uri_owl_allValuesFrom,U_142,U_141) ),
inference(clausify,[status(thm)],[f_38_2]) ).
cnf(f_38_4,plain,
( ic(U_141)
| ~ iext(uri_owl_allValuesFrom,U_142,U_141) ),
inference(clausify,[status(thm)],[f_38_2]) ).
fof(f_39_1,plain,
ip(uri_owl_allValuesFrom),
inference(fof_nnf,[status(thm)],[owl_prop_allvaluesfrom_type]) ).
cnf(f_39_2,plain,
ip(uri_owl_allValuesFrom),
inference(clausify,[status(thm)],[f_39_1]) ).
fof(f_40_1,plain,
! [X,Y] :
( ( ic(Y)
& ic(X) )
| ~ iext(uri_owl_complementOf,X,Y) ),
inference(fof_nnf,[status(thm)],[owl_prop_complementof_ext]) ).
fof(f_40_2,plain,
! [U_144,U_143] :
( ( ic(U_143)
& ic(U_144) )
| ~ iext(uri_owl_complementOf,U_144,U_143) ),
inference(variable_rename,[status(thm)],[f_40_1]) ).
cnf(f_40_3,plain,
( ic(U_144)
| ~ iext(uri_owl_complementOf,U_144,U_143) ),
inference(clausify,[status(thm)],[f_40_2]) ).
cnf(f_40_4,plain,
( ic(U_143)
| ~ iext(uri_owl_complementOf,U_144,U_143) ),
inference(clausify,[status(thm)],[f_40_2]) ).
fof(f_41_1,plain,
ip(uri_owl_complementOf),
inference(fof_nnf,[status(thm)],[owl_prop_complementof_type]) ).
cnf(f_41_2,plain,
ip(uri_owl_complementOf),
inference(clausify,[status(thm)],[f_41_1]) ).
fof(f_42_1,plain,
! [X,Y] :
( ( ir(Y)
& icext(uri_owl_Restriction,X) )
| ~ iext(uri_owl_hasValue,X,Y) ),
inference(fof_nnf,[status(thm)],[owl_prop_hasvalue_ext]) ).
fof(f_42_2,plain,
! [U_146,U_145] :
( ( ir(U_145)
& icext(uri_owl_Restriction,U_146) )
| ~ iext(uri_owl_hasValue,U_146,U_145) ),
inference(variable_rename,[status(thm)],[f_42_1]) ).
cnf(f_42_3,plain,
( icext(uri_owl_Restriction,U_146)
| ~ iext(uri_owl_hasValue,U_146,U_145) ),
inference(clausify,[status(thm)],[f_42_2]) ).
cnf(f_42_4,plain,
( ir(U_145)
| ~ iext(uri_owl_hasValue,U_146,U_145) ),
inference(clausify,[status(thm)],[f_42_2]) ).
fof(f_43_1,plain,
ip(uri_owl_hasValue),
inference(fof_nnf,[status(thm)],[owl_prop_hasvalue_type]) ).
cnf(f_43_2,plain,
ip(uri_owl_hasValue),
inference(clausify,[status(thm)],[f_43_1]) ).
fof(f_44_1,plain,
! [X,Y] :
( ( icext(uri_rdf_List,Y)
& ic(X) )
| ~ iext(uri_owl_intersectionOf,X,Y) ),
inference(fof_nnf,[status(thm)],[owl_prop_intersectionof_ext]) ).
fof(f_44_2,plain,
! [U_148,U_147] :
( ( icext(uri_rdf_List,U_147)
& ic(U_148) )
| ~ iext(uri_owl_intersectionOf,U_148,U_147) ),
inference(variable_rename,[status(thm)],[f_44_1]) ).
cnf(f_44_3,plain,
( ic(U_148)
| ~ iext(uri_owl_intersectionOf,U_148,U_147) ),
inference(clausify,[status(thm)],[f_44_2]) ).
cnf(f_44_4,plain,
( icext(uri_rdf_List,U_147)
| ~ iext(uri_owl_intersectionOf,U_148,U_147) ),
inference(clausify,[status(thm)],[f_44_2]) ).
fof(f_45_1,plain,
ip(uri_owl_intersectionOf),
inference(fof_nnf,[status(thm)],[owl_prop_intersectionof_type]) ).
cnf(f_45_2,plain,
ip(uri_owl_intersectionOf),
inference(clausify,[status(thm)],[f_45_1]) ).
fof(f_46_1,plain,
! [X,Y] :
( ( ip(Y)
& icext(uri_owl_Restriction,X) )
| ~ iext(uri_owl_onProperty,X,Y) ),
inference(fof_nnf,[status(thm)],[owl_prop_onproperty_ext]) ).
fof(f_46_2,plain,
! [U_150,U_149] :
( ( ip(U_149)
& icext(uri_owl_Restriction,U_150) )
| ~ iext(uri_owl_onProperty,U_150,U_149) ),
inference(variable_rename,[status(thm)],[f_46_1]) ).
cnf(f_46_3,plain,
( icext(uri_owl_Restriction,U_150)
| ~ iext(uri_owl_onProperty,U_150,U_149) ),
inference(clausify,[status(thm)],[f_46_2]) ).
cnf(f_46_4,plain,
( ip(U_149)
| ~ iext(uri_owl_onProperty,U_150,U_149) ),
inference(clausify,[status(thm)],[f_46_2]) ).
fof(f_47_1,plain,
ip(uri_owl_onProperty),
inference(fof_nnf,[status(thm)],[owl_prop_onproperty_type]) ).
cnf(f_47_2,plain,
ip(uri_owl_onProperty),
inference(clausify,[status(thm)],[f_47_1]) ).
fof(f_48_1,plain,
! [X,Y] :
( ( ic(Y)
& icext(uri_owl_Restriction,X) )
| ~ iext(uri_owl_someValuesFrom,X,Y) ),
inference(fof_nnf,[status(thm)],[owl_prop_somevaluesfrom_ext]) ).
fof(f_48_2,plain,
! [U_152,U_151] :
( ( ic(U_151)
& icext(uri_owl_Restriction,U_152) )
| ~ iext(uri_owl_someValuesFrom,U_152,U_151) ),
inference(variable_rename,[status(thm)],[f_48_1]) ).
cnf(f_48_3,plain,
( icext(uri_owl_Restriction,U_152)
| ~ iext(uri_owl_someValuesFrom,U_152,U_151) ),
inference(clausify,[status(thm)],[f_48_2]) ).
cnf(f_48_4,plain,
( ic(U_151)
| ~ iext(uri_owl_someValuesFrom,U_152,U_151) ),
inference(clausify,[status(thm)],[f_48_2]) ).
fof(f_49_1,plain,
ip(uri_owl_someValuesFrom),
inference(fof_nnf,[status(thm)],[owl_prop_somevaluesfrom_type]) ).
cnf(f_49_2,plain,
ip(uri_owl_someValuesFrom),
inference(clausify,[status(thm)],[f_49_1]) ).
fof(f_50_1,plain,
! [X,Y] :
( ( icext(uri_rdf_List,Y)
& ic(X) )
| ~ iext(uri_owl_unionOf,X,Y) ),
inference(fof_nnf,[status(thm)],[owl_prop_unionof_ext]) ).
fof(f_50_2,plain,
! [U_154,U_153] :
( ( icext(uri_rdf_List,U_153)
& ic(U_154) )
| ~ iext(uri_owl_unionOf,U_154,U_153) ),
inference(variable_rename,[status(thm)],[f_50_1]) ).
cnf(f_50_3,plain,
( ic(U_154)
| ~ iext(uri_owl_unionOf,U_154,U_153) ),
inference(clausify,[status(thm)],[f_50_2]) ).
cnf(f_50_4,plain,
( icext(uri_rdf_List,U_153)
| ~ iext(uri_owl_unionOf,U_154,U_153) ),
inference(clausify,[status(thm)],[f_50_2]) ).
fof(f_51_1,plain,
ip(uri_owl_unionOf),
inference(fof_nnf,[status(thm)],[owl_prop_unionof_type]) ).
cnf(f_51_2,plain,
ip(uri_owl_unionOf),
inference(clausify,[status(thm)],[f_51_1]) ).
fof(f_52_1,plain,
! [P,C] :
( ( iext(uri_rdfs_domain,P,C)
| ? [X,Y] :
( ~ icext(C,X)
& iext(P,X,Y) )
| ~ ic(C)
| ~ ip(P) )
& ( ( ! [X,Y] :
( icext(C,X)
| ~ iext(P,X,Y) )
& ic(C)
& ip(P) )
| ~ iext(uri_rdfs_domain,P,C) ) ),
inference(fof_nnf,[status(thm)],[owl_rdfsext_domain]) ).
fof(f_52_2,plain,
! [U_160,U_159] :
( ( iext(uri_rdfs_domain,U_160,U_159)
| ? [U_158,U_157] :
( ~ icext(U_159,U_158)
& iext(U_160,U_158,U_157) )
| ~ ic(U_159)
| ~ ip(U_160) )
& ( ( ! [U_156,U_155] :
( icext(U_159,U_156)
| ~ iext(U_160,U_156,U_155) )
& ic(U_159)
& ip(U_160) )
| ~ iext(uri_rdfs_domain,U_160,U_159) ) ),
inference(variable_rename,[status(thm)],[f_52_1]) ).
fof(f_52_3,plain,
( ! [U_164,U_162] :
( iext(uri_rdfs_domain,U_164,U_162)
| ? [U_158] :
( ? [U_157] : iext(U_164,U_158,U_157)
& ~ icext(U_162,U_158) )
| ~ ic(U_162)
| ~ ip(U_164) )
& ! [U_163,U_161] :
( ( ! [U_156] :
( ! [U_155] : ~ iext(U_163,U_156,U_155)
| icext(U_161,U_156) )
& ic(U_161)
& ip(U_163) )
| ~ iext(uri_rdfs_domain,U_163,U_161) ) ),
inference(miniscope,[status(thm)],[f_52_2]) ).
fof(f_52_4,plain,
( ! [U_164,U_162] :
( iext(uri_rdfs_domain,U_164,U_162)
| ( ? [U_157] : iext(U_164,sK17(U_164,U_162),U_157)
& ~ icext(U_162,sK17(U_164,U_162)) )
| ~ ic(U_162)
| ~ ip(U_164) )
& ! [U_163,U_161] :
( ( ! [U_156] :
( ! [U_155] : ~ iext(U_163,U_156,U_155)
| icext(U_161,U_156) )
& ic(U_161)
& ip(U_163) )
| ~ iext(uri_rdfs_domain,U_163,U_161) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK17]),skolemize(U_158,sK17(U_164,U_162))],[f_52_3]) ).
fof(f_52_5,plain,
( ! [U_164,U_162] :
( iext(uri_rdfs_domain,U_164,U_162)
| ( iext(U_164,sK17(U_164,U_162),sK18(U_164,U_162))
& ~ icext(U_162,sK17(U_164,U_162)) )
| ~ ic(U_162)
| ~ ip(U_164) )
& ! [U_163,U_161] :
( ( ! [U_156] :
( ! [U_155] : ~ iext(U_163,U_156,U_155)
| icext(U_161,U_156) )
& ic(U_161)
& ip(U_163) )
| ~ iext(uri_rdfs_domain,U_163,U_161) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK18]),skolemize(U_157,sK18(U_164,U_162))],[f_52_4]) ).
cnf(f_52_6,plain,
( ip(U_163)
| ~ iext(uri_rdfs_domain,U_163,U_161) ),
inference(clausify,[status(thm)],[f_52_5]) ).
cnf(f_52_7,plain,
( ic(U_161)
| ~ iext(uri_rdfs_domain,U_163,U_161) ),
inference(clausify,[status(thm)],[f_52_5]) ).
cnf(f_52_8,plain,
( ~ iext(U_163,U_156,U_155)
| icext(U_161,U_156)
| ~ iext(uri_rdfs_domain,U_163,U_161) ),
inference(clausify,[status(thm)],[f_52_5]) ).
cnf(f_52_9,plain,
( ~ icext(U_162,sK17(U_164,U_162))
| ~ ic(U_162)
| ~ ip(U_164)
| iext(uri_rdfs_domain,U_164,U_162) ),
inference(clausify,[status(thm)],[f_52_5]) ).
cnf(f_52_10,plain,
( iext(U_164,sK17(U_164,U_162),sK18(U_164,U_162))
| ~ ic(U_162)
| ~ ip(U_164)
| iext(uri_rdfs_domain,U_164,U_162) ),
inference(clausify,[status(thm)],[f_52_5]) ).
fof(f_53_1,plain,
! [P,C] :
( ( iext(uri_rdfs_range,P,C)
| ? [X,Y] :
( ~ icext(C,Y)
& iext(P,X,Y) )
| ~ ip(C)
| ~ ip(P) )
& ( ( ! [X,Y] :
( icext(C,Y)
| ~ iext(P,X,Y) )
& ip(C)
& ip(P) )
| ~ iext(uri_rdfs_range,P,C) ) ),
inference(fof_nnf,[status(thm)],[owl_rdfsext_range]) ).
fof(f_53_2,plain,
! [U_170,U_169] :
( ( iext(uri_rdfs_range,U_170,U_169)
| ? [U_168,U_167] :
( ~ icext(U_169,U_167)
& iext(U_170,U_168,U_167) )
| ~ ip(U_169)
| ~ ip(U_170) )
& ( ( ! [U_166,U_165] :
( icext(U_169,U_165)
| ~ iext(U_170,U_166,U_165) )
& ip(U_169)
& ip(U_170) )
| ~ iext(uri_rdfs_range,U_170,U_169) ) ),
inference(variable_rename,[status(thm)],[f_53_1]) ).
fof(f_53_3,plain,
( ! [U_174,U_172] :
( iext(uri_rdfs_range,U_174,U_172)
| ? [U_168,U_167] :
( ~ icext(U_172,U_167)
& iext(U_174,U_168,U_167) )
| ~ ip(U_172)
| ~ ip(U_174) )
& ! [U_173,U_171] :
( ( ! [U_166,U_165] :
( icext(U_171,U_165)
| ~ iext(U_173,U_166,U_165) )
& ip(U_171)
& ip(U_173) )
| ~ iext(uri_rdfs_range,U_173,U_171) ) ),
inference(miniscope,[status(thm)],[f_53_2]) ).
fof(f_53_4,plain,
( ! [U_174,U_172] :
( iext(uri_rdfs_range,U_174,U_172)
| ? [U_167] :
( ~ icext(U_172,U_167)
& iext(U_174,sK19(U_174,U_172),U_167) )
| ~ ip(U_172)
| ~ ip(U_174) )
& ! [U_173,U_171] :
( ( ! [U_166,U_165] :
( icext(U_171,U_165)
| ~ iext(U_173,U_166,U_165) )
& ip(U_171)
& ip(U_173) )
| ~ iext(uri_rdfs_range,U_173,U_171) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK19]),skolemize(U_168,sK19(U_174,U_172))],[f_53_3]) ).
fof(f_53_5,plain,
( ! [U_174,U_172] :
( iext(uri_rdfs_range,U_174,U_172)
| ( ~ icext(U_172,sK20(U_174,U_172))
& iext(U_174,sK19(U_174,U_172),sK20(U_174,U_172)) )
| ~ ip(U_172)
| ~ ip(U_174) )
& ! [U_173,U_171] :
( ( ! [U_166,U_165] :
( icext(U_171,U_165)
| ~ iext(U_173,U_166,U_165) )
& ip(U_171)
& ip(U_173) )
| ~ iext(uri_rdfs_range,U_173,U_171) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK20]),skolemize(U_167,sK20(U_174,U_172))],[f_53_4]) ).
cnf(f_53_6,plain,
( ip(U_173)
| ~ iext(uri_rdfs_range,U_173,U_171) ),
inference(clausify,[status(thm)],[f_53_5]) ).
cnf(f_53_7,plain,
( ip(U_171)
| ~ iext(uri_rdfs_range,U_173,U_171) ),
inference(clausify,[status(thm)],[f_53_5]) ).
cnf(f_53_8,plain,
( icext(U_171,U_165)
| ~ iext(U_173,U_166,U_165)
| ~ iext(uri_rdfs_range,U_173,U_171) ),
inference(clausify,[status(thm)],[f_53_5]) ).
cnf(f_53_9,plain,
( iext(U_174,sK19(U_174,U_172),sK20(U_174,U_172))
| ~ ip(U_172)
| ~ ip(U_174)
| iext(uri_rdfs_range,U_174,U_172) ),
inference(clausify,[status(thm)],[f_53_5]) ).
cnf(f_53_10,plain,
( ~ icext(U_172,sK20(U_174,U_172))
| ~ ip(U_172)
| ~ ip(U_174)
| iext(uri_rdfs_range,U_174,U_172) ),
inference(clausify,[status(thm)],[f_53_5]) ).
fof(f_54_1,plain,
! [C1,C2] :
( ( iext(uri_rdfs_subClassOf,C1,C2)
| ? [X] :
( ~ icext(C2,X)
& icext(C1,X) )
| ~ ic(C2)
| ~ ic(C1) )
& ( ( ! [X] :
( icext(C2,X)
| ~ icext(C1,X) )
& ic(C2)
& ic(C1) )
| ~ iext(uri_rdfs_subClassOf,C1,C2) ) ),
inference(fof_nnf,[status(thm)],[owl_rdfsext_subclassof]) ).
fof(f_54_2,plain,
! [U_178,U_177] :
( ( iext(uri_rdfs_subClassOf,U_178,U_177)
| ? [U_176] :
( ~ icext(U_177,U_176)
& icext(U_178,U_176) )
| ~ ic(U_177)
| ~ ic(U_178) )
& ( ( ! [U_175] :
( icext(U_177,U_175)
| ~ icext(U_178,U_175) )
& ic(U_177)
& ic(U_178) )
| ~ iext(uri_rdfs_subClassOf,U_178,U_177) ) ),
inference(variable_rename,[status(thm)],[f_54_1]) ).
fof(f_54_3,plain,
( ! [U_182,U_180] :
( iext(uri_rdfs_subClassOf,U_182,U_180)
| ? [U_176] :
( ~ icext(U_180,U_176)
& icext(U_182,U_176) )
| ~ ic(U_180)
| ~ ic(U_182) )
& ! [U_181,U_179] :
( ( ! [U_175] :
( icext(U_179,U_175)
| ~ icext(U_181,U_175) )
& ic(U_179)
& ic(U_181) )
| ~ iext(uri_rdfs_subClassOf,U_181,U_179) ) ),
inference(miniscope,[status(thm)],[f_54_2]) ).
fof(f_54_4,plain,
( ! [U_182,U_180] :
( iext(uri_rdfs_subClassOf,U_182,U_180)
| ( ~ icext(U_180,sK21(U_182,U_180))
& icext(U_182,sK21(U_182,U_180)) )
| ~ ic(U_180)
| ~ ic(U_182) )
& ! [U_181,U_179] :
( ( ! [U_175] :
( icext(U_179,U_175)
| ~ icext(U_181,U_175) )
& ic(U_179)
& ic(U_181) )
| ~ iext(uri_rdfs_subClassOf,U_181,U_179) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK21]),skolemize(U_176,sK21(U_182,U_180))],[f_54_3]) ).
cnf(f_54_5,plain,
( ic(U_181)
| ~ iext(uri_rdfs_subClassOf,U_181,U_179) ),
inference(clausify,[status(thm)],[f_54_4]) ).
cnf(f_54_6,plain,
( ic(U_179)
| ~ iext(uri_rdfs_subClassOf,U_181,U_179) ),
inference(clausify,[status(thm)],[f_54_4]) ).
cnf(f_54_7,plain,
( icext(U_179,U_175)
| ~ icext(U_181,U_175)
| ~ iext(uri_rdfs_subClassOf,U_181,U_179) ),
inference(clausify,[status(thm)],[f_54_4]) ).
cnf(f_54_8,plain,
( icext(U_182,sK21(U_182,U_180))
| ~ ic(U_180)
| ~ ic(U_182)
| iext(uri_rdfs_subClassOf,U_182,U_180) ),
inference(clausify,[status(thm)],[f_54_4]) ).
cnf(f_54_9,plain,
( ~ icext(U_180,sK21(U_182,U_180))
| ~ ic(U_180)
| ~ ic(U_182)
| iext(uri_rdfs_subClassOf,U_182,U_180) ),
inference(clausify,[status(thm)],[f_54_4]) ).
fof(f_55_1,plain,
! [P1,P2] :
( ( iext(uri_rdfs_subPropertyOf,P1,P2)
| ? [X,Y] :
( ~ iext(P2,X,Y)
& iext(P1,X,Y) )
| ~ ip(P2)
| ~ ip(P1) )
& ( ( ! [X,Y] :
( iext(P2,X,Y)
| ~ iext(P1,X,Y) )
& ip(P2)
& ip(P1) )
| ~ iext(uri_rdfs_subPropertyOf,P1,P2) ) ),
inference(fof_nnf,[status(thm)],[owl_rdfsext_subpropertyof]) ).
fof(f_55_2,plain,
! [U_188,U_187] :
( ( iext(uri_rdfs_subPropertyOf,U_188,U_187)
| ? [U_186,U_185] :
( ~ iext(U_187,U_186,U_185)
& iext(U_188,U_186,U_185) )
| ~ ip(U_187)
| ~ ip(U_188) )
& ( ( ! [U_184,U_183] :
( iext(U_187,U_184,U_183)
| ~ iext(U_188,U_184,U_183) )
& ip(U_187)
& ip(U_188) )
| ~ iext(uri_rdfs_subPropertyOf,U_188,U_187) ) ),
inference(variable_rename,[status(thm)],[f_55_1]) ).
fof(f_55_3,plain,
( ! [U_192,U_190] :
( iext(uri_rdfs_subPropertyOf,U_192,U_190)
| ? [U_186,U_185] :
( ~ iext(U_190,U_186,U_185)
& iext(U_192,U_186,U_185) )
| ~ ip(U_190)
| ~ ip(U_192) )
& ! [U_191,U_189] :
( ( ! [U_184,U_183] :
( iext(U_189,U_184,U_183)
| ~ iext(U_191,U_184,U_183) )
& ip(U_189)
& ip(U_191) )
| ~ iext(uri_rdfs_subPropertyOf,U_191,U_189) ) ),
inference(miniscope,[status(thm)],[f_55_2]) ).
fof(f_55_4,plain,
( ! [U_192,U_190] :
( iext(uri_rdfs_subPropertyOf,U_192,U_190)
| ? [U_185] :
( ~ iext(U_190,sK22(U_192,U_190),U_185)
& iext(U_192,sK22(U_192,U_190),U_185) )
| ~ ip(U_190)
| ~ ip(U_192) )
& ! [U_191,U_189] :
( ( ! [U_184,U_183] :
( iext(U_189,U_184,U_183)
| ~ iext(U_191,U_184,U_183) )
& ip(U_189)
& ip(U_191) )
| ~ iext(uri_rdfs_subPropertyOf,U_191,U_189) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK22]),skolemize(U_186,sK22(U_192,U_190))],[f_55_3]) ).
fof(f_55_5,plain,
( ! [U_192,U_190] :
( iext(uri_rdfs_subPropertyOf,U_192,U_190)
| ( ~ iext(U_190,sK22(U_192,U_190),sK23(U_192,U_190))
& iext(U_192,sK22(U_192,U_190),sK23(U_192,U_190)) )
| ~ ip(U_190)
| ~ ip(U_192) )
& ! [U_191,U_189] :
( ( ! [U_184,U_183] :
( iext(U_189,U_184,U_183)
| ~ iext(U_191,U_184,U_183) )
& ip(U_189)
& ip(U_191) )
| ~ iext(uri_rdfs_subPropertyOf,U_191,U_189) ) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK23]),skolemize(U_185,sK23(U_192,U_190))],[f_55_4]) ).
cnf(f_55_6,plain,
( ip(U_191)
| ~ iext(uri_rdfs_subPropertyOf,U_191,U_189) ),
inference(clausify,[status(thm)],[f_55_5]) ).
cnf(f_55_7,plain,
( ip(U_189)
| ~ iext(uri_rdfs_subPropertyOf,U_191,U_189) ),
inference(clausify,[status(thm)],[f_55_5]) ).
cnf(f_55_8,plain,
( iext(U_189,U_184,U_183)
| ~ iext(U_191,U_184,U_183)
| ~ iext(uri_rdfs_subPropertyOf,U_191,U_189) ),
inference(clausify,[status(thm)],[f_55_5]) ).
cnf(f_55_9,plain,
( iext(U_192,sK22(U_192,U_190),sK23(U_192,U_190))
| ~ ip(U_190)
| ~ ip(U_192)
| iext(uri_rdfs_subPropertyOf,U_192,U_190) ),
inference(clausify,[status(thm)],[f_55_5]) ).
cnf(f_55_10,plain,
( ~ iext(U_190,sK22(U_192,U_190),sK23(U_192,U_190))
| ~ ip(U_190)
| ~ ip(U_192)
| iext(uri_rdfs_subPropertyOf,U_192,U_190) ),
inference(clausify,[status(thm)],[f_55_5]) ).
fof(f_56_1,plain,
! [Z,P,C] :
( ! [X] :
( ( icext(Z,X)
| ? [Y] :
( ~ icext(C,Y)
& iext(P,X,Y) ) )
& ( ! [Y] :
( icext(C,Y)
| ~ iext(P,X,Y) )
| ~ icext(Z,X) ) )
| ~ iext(uri_owl_onProperty,Z,P)
| ~ iext(uri_owl_allValuesFrom,Z,C) ),
inference(fof_nnf,[status(thm)],[owl_restrict_allvaluesfrom]) ).
fof(f_56_2,plain,
! [U_198,U_197,U_196] :
( ! [U_195] :
( ( icext(U_198,U_195)
| ? [U_194] :
( ~ icext(U_196,U_194)
& iext(U_197,U_195,U_194) ) )
& ( ! [U_193] :
( icext(U_196,U_193)
| ~ iext(U_197,U_195,U_193) )
| ~ icext(U_198,U_195) ) )
| ~ iext(uri_owl_onProperty,U_198,U_197)
| ~ iext(uri_owl_allValuesFrom,U_198,U_196) ),
inference(variable_rename,[status(thm)],[f_56_1]) ).
fof(f_56_3,plain,
! [U_198,U_197,U_196] :
( ( ! [U_200] :
( icext(U_198,U_200)
| ? [U_194] :
( ~ icext(U_196,U_194)
& iext(U_197,U_200,U_194) ) )
& ! [U_199] :
( ! [U_193] :
( icext(U_196,U_193)
| ~ iext(U_197,U_199,U_193) )
| ~ icext(U_198,U_199) ) )
| ~ iext(uri_owl_onProperty,U_198,U_197)
| ~ iext(uri_owl_allValuesFrom,U_198,U_196) ),
inference(miniscope,[status(thm)],[f_56_2]) ).
fof(f_56_4,plain,
! [U_198,U_197,U_196] :
( ( ! [U_200] :
( icext(U_198,U_200)
| ( ~ icext(U_196,sK24(U_198,U_197,U_196,U_200))
& iext(U_197,U_200,sK24(U_198,U_197,U_196,U_200)) ) )
& ! [U_199] :
( ! [U_193] :
( icext(U_196,U_193)
| ~ iext(U_197,U_199,U_193) )
| ~ icext(U_198,U_199) ) )
| ~ iext(uri_owl_onProperty,U_198,U_197)
| ~ iext(uri_owl_allValuesFrom,U_198,U_196) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK24]),skolemize(U_194,sK24(U_198,U_197,U_196,U_200))],[f_56_3]) ).
cnf(f_56_5,plain,
( icext(U_196,U_193)
| ~ iext(U_197,U_199,U_193)
| ~ icext(U_198,U_199)
| ~ iext(uri_owl_onProperty,U_198,U_197)
| ~ iext(uri_owl_allValuesFrom,U_198,U_196) ),
inference(clausify,[status(thm)],[f_56_4]) ).
cnf(f_56_6,plain,
( iext(U_197,U_200,sK24(U_198,U_197,U_196,U_200))
| icext(U_198,U_200)
| ~ iext(uri_owl_onProperty,U_198,U_197)
| ~ iext(uri_owl_allValuesFrom,U_198,U_196) ),
inference(clausify,[status(thm)],[f_56_4]) ).
cnf(f_56_7,plain,
( ~ icext(U_196,sK24(U_198,U_197,U_196,U_200))
| icext(U_198,U_200)
| ~ iext(uri_owl_onProperty,U_198,U_197)
| ~ iext(uri_owl_allValuesFrom,U_198,U_196) ),
inference(clausify,[status(thm)],[f_56_4]) ).
fof(f_57_1,plain,
! [Z,P,A] :
( ! [X] :
( ( icext(Z,X)
| ~ iext(P,X,A) )
& ( iext(P,X,A)
| ~ icext(Z,X) ) )
| ~ iext(uri_owl_onProperty,Z,P)
| ~ iext(uri_owl_hasValue,Z,A) ),
inference(fof_nnf,[status(thm)],[owl_restrict_hasvalue]) ).
fof(f_57_2,plain,
! [U_204,U_203,U_202] :
( ! [U_201] :
( ( icext(U_204,U_201)
| ~ iext(U_203,U_201,U_202) )
& ( iext(U_203,U_201,U_202)
| ~ icext(U_204,U_201) ) )
| ~ iext(uri_owl_onProperty,U_204,U_203)
| ~ iext(uri_owl_hasValue,U_204,U_202) ),
inference(variable_rename,[status(thm)],[f_57_1]) ).
fof(f_57_3,plain,
! [U_204,U_203,U_202] :
( ( ! [U_206] :
( icext(U_204,U_206)
| ~ iext(U_203,U_206,U_202) )
& ! [U_205] :
( iext(U_203,U_205,U_202)
| ~ icext(U_204,U_205) ) )
| ~ iext(uri_owl_onProperty,U_204,U_203)
| ~ iext(uri_owl_hasValue,U_204,U_202) ),
inference(miniscope,[status(thm)],[f_57_2]) ).
cnf(f_57_4,plain,
( iext(U_203,U_205,U_202)
| ~ icext(U_204,U_205)
| ~ iext(uri_owl_onProperty,U_204,U_203)
| ~ iext(uri_owl_hasValue,U_204,U_202) ),
inference(clausify,[status(thm)],[f_57_3]) ).
cnf(f_57_5,plain,
( icext(U_204,U_206)
| ~ iext(U_203,U_206,U_202)
| ~ iext(uri_owl_onProperty,U_204,U_203)
| ~ iext(uri_owl_hasValue,U_204,U_202) ),
inference(clausify,[status(thm)],[f_57_3]) ).
fof(f_58_1,plain,
! [Z,P,C] :
( ! [X] :
( ( icext(Z,X)
| ! [Y] :
( ~ icext(C,Y)
| ~ iext(P,X,Y) ) )
& ( ? [Y] :
( icext(C,Y)
& iext(P,X,Y) )
| ~ icext(Z,X) ) )
| ~ iext(uri_owl_onProperty,Z,P)
| ~ iext(uri_owl_someValuesFrom,Z,C) ),
inference(fof_nnf,[status(thm)],[owl_restrict_somevaluesfrom]) ).
fof(f_58_2,plain,
! [U_212,U_211,U_210] :
( ! [U_209] :
( ( icext(U_212,U_209)
| ! [U_208] :
( ~ icext(U_210,U_208)
| ~ iext(U_211,U_209,U_208) ) )
& ( ? [U_207] :
( icext(U_210,U_207)
& iext(U_211,U_209,U_207) )
| ~ icext(U_212,U_209) ) )
| ~ iext(uri_owl_onProperty,U_212,U_211)
| ~ iext(uri_owl_someValuesFrom,U_212,U_210) ),
inference(variable_rename,[status(thm)],[f_58_1]) ).
fof(f_58_3,plain,
! [U_212,U_211,U_210] :
( ( ! [U_214] :
( icext(U_212,U_214)
| ! [U_208] :
( ~ icext(U_210,U_208)
| ~ iext(U_211,U_214,U_208) ) )
& ! [U_213] :
( ? [U_207] :
( icext(U_210,U_207)
& iext(U_211,U_213,U_207) )
| ~ icext(U_212,U_213) ) )
| ~ iext(uri_owl_onProperty,U_212,U_211)
| ~ iext(uri_owl_someValuesFrom,U_212,U_210) ),
inference(miniscope,[status(thm)],[f_58_2]) ).
fof(f_58_4,plain,
! [U_212,U_211,U_210] :
( ( ! [U_214] :
( icext(U_212,U_214)
| ! [U_208] :
( ~ icext(U_210,U_208)
| ~ iext(U_211,U_214,U_208) ) )
& ! [U_213] :
( ( icext(U_210,sK25(U_212,U_211,U_210,U_213))
& iext(U_211,U_213,sK25(U_212,U_211,U_210,U_213)) )
| ~ icext(U_212,U_213) ) )
| ~ iext(uri_owl_onProperty,U_212,U_211)
| ~ iext(uri_owl_someValuesFrom,U_212,U_210) ),
inference(skolemize,[status(esa),new_symbols(skolem,[sK25]),skolemize(U_207,sK25(U_212,U_211,U_210,U_213))],[f_58_3]) ).
cnf(f_58_5,plain,
( iext(U_211,U_213,sK25(U_212,U_211,U_210,U_213))
| ~ icext(U_212,U_213)
| ~ iext(uri_owl_onProperty,U_212,U_211)
| ~ iext(uri_owl_someValuesFrom,U_212,U_210) ),
inference(clausify,[status(thm)],[f_58_4]) ).
cnf(f_58_6,plain,
( icext(U_210,sK25(U_212,U_211,U_210,U_213))
| ~ icext(U_212,U_213)
| ~ iext(uri_owl_onProperty,U_212,U_211)
| ~ iext(uri_owl_someValuesFrom,U_212,U_210) ),
inference(clausify,[status(thm)],[f_58_4]) ).
cnf(f_58_7,plain,
( icext(U_212,U_214)
| ~ icext(U_210,U_208)
| ~ iext(U_211,U_214,U_208)
| ~ iext(uri_owl_onProperty,U_212,U_211)
| ~ iext(uri_owl_someValuesFrom,U_212,U_210) ),
inference(clausify,[status(thm)],[f_58_4]) ).
fof(f_59_1,plain,
iext(uri_rdf_type,uri_rdf_first,uri_rdf_Property),
inference(fof_nnf,[status(thm)],[rdf_collection_first_type]) ).
cnf(f_59_2,plain,
iext(uri_rdf_type,uri_rdf_first,uri_rdf_Property),
inference(clausify,[status(thm)],[f_59_1]) ).
fof(f_60_1,plain,
iext(uri_rdf_type,uri_rdf_nil,uri_rdf_List),
inference(fof_nnf,[status(thm)],[rdf_collection_nil_type]) ).
cnf(f_60_2,plain,
iext(uri_rdf_type,uri_rdf_nil,uri_rdf_List),
inference(clausify,[status(thm)],[f_60_1]) ).
fof(f_61_1,plain,
iext(uri_rdf_type,uri_rdf_rest,uri_rdf_Property),
inference(fof_nnf,[status(thm)],[rdf_collection_rest_type]) ).
cnf(f_61_2,plain,
iext(uri_rdf_type,uri_rdf_rest,uri_rdf_Property),
inference(clausify,[status(thm)],[f_61_1]) ).
fof(f_62_1,plain,
iext(uri_rdf_type,uri_rdf__1,uri_rdf_Property),
inference(fof_nnf,[status(thm)],[rdf_container_n_type_001]) ).
cnf(f_62_2,plain,
iext(uri_rdf_type,uri_rdf__1,uri_rdf_Property),
inference(clausify,[status(thm)],[f_62_1]) ).
fof(f_63_1,plain,
iext(uri_rdf_type,uri_rdf__2,uri_rdf_Property),
inference(fof_nnf,[status(thm)],[rdf_container_n_type_002]) ).
cnf(f_63_2,plain,
iext(uri_rdf_type,uri_rdf__2,uri_rdf_Property),
inference(clausify,[status(thm)],[f_63_1]) ).
fof(f_64_1,plain,
iext(uri_rdf_type,uri_rdf__3,uri_rdf_Property),
inference(fof_nnf,[status(thm)],[rdf_container_n_type_003]) ).
cnf(f_64_2,plain,
iext(uri_rdf_type,uri_rdf__3,uri_rdf_Property),
inference(clausify,[status(thm)],[f_64_1]) ).
fof(f_65_1,plain,
iext(uri_rdf_type,uri_rdf_object,uri_rdf_Property),
inference(fof_nnf,[status(thm)],[rdf_reification_object_type]) ).
cnf(f_65_2,plain,
iext(uri_rdf_type,uri_rdf_object,uri_rdf_Property),
inference(clausify,[status(thm)],[f_65_1]) ).
fof(f_66_1,plain,
iext(uri_rdf_type,uri_rdf_value,uri_rdf_Property),
inference(fof_nnf,[status(thm)],[rdf_reification_predicate_type]) ).
cnf(f_66_2,plain,
iext(uri_rdf_type,uri_rdf_value,uri_rdf_Property),
inference(clausify,[status(thm)],[f_66_1]) ).
fof(f_67_1,plain,
iext(uri_rdf_type,uri_rdf_subject,uri_rdf_Property),
inference(fof_nnf,[status(thm)],[rdf_reification_subject_type]) ).
cnf(f_67_2,plain,
iext(uri_rdf_type,uri_rdf_subject,uri_rdf_Property),
inference(clausify,[status(thm)],[f_67_1]) ).
fof(f_68_1,plain,
! [P] :
( ( iext(uri_rdf_type,P,uri_rdf_Property)
| ~ ip(P) )
& ( ip(P)
| ~ iext(uri_rdf_type,P,uri_rdf_Property) ) ),
inference(fof_nnf,[status(thm)],[rdf_type_ip]) ).
fof(f_68_2,plain,
! [U_215] :
( ( iext(uri_rdf_type,U_215,uri_rdf_Property)
| ~ ip(U_215) )
& ( ip(U_215)
| ~ iext(uri_rdf_type,U_215,uri_rdf_Property) ) ),
inference(variable_rename,[status(thm)],[f_68_1]) ).
fof(f_68_3,plain,
( ! [U_217] :
( iext(uri_rdf_type,U_217,uri_rdf_Property)
| ~ ip(U_217) )
& ! [U_216] :
( ip(U_216)
| ~ iext(uri_rdf_type,U_216,uri_rdf_Property) ) ),
inference(miniscope,[status(thm)],[f_68_2]) ).
cnf(f_68_4,plain,
( ip(U_216)
| ~ iext(uri_rdf_type,U_216,uri_rdf_Property) ),
inference(clausify,[status(thm)],[f_68_3]) ).
cnf(f_68_5,plain,
( iext(uri_rdf_type,U_217,uri_rdf_Property)
| ~ ip(U_217) ),
inference(clausify,[status(thm)],[f_68_3]) ).
fof(f_69_1,plain,
iext(uri_rdf_type,uri_rdf_type,uri_rdf_Property),
inference(fof_nnf,[status(thm)],[rdf_type_type]) ).
cnf(f_69_2,plain,
iext(uri_rdf_type,uri_rdf_type,uri_rdf_Property),
inference(clausify,[status(thm)],[f_69_1]) ).
fof(f_70_1,plain,
iext(uri_rdf_type,uri_rdf_type,uri_rdf_Property),
inference(fof_nnf,[status(thm)],[rdf_value_type]) ).
cnf(f_70_2,plain,
iext(uri_rdf_type,uri_rdf_type,uri_rdf_Property),
inference(clausify,[status(thm)],[f_70_1]) ).
fof(f_71_1,plain,
iext(uri_rdfs_domain,uri_rdfs_comment,uri_rdfs_Resource),
inference(fof_nnf,[status(thm)],[rdfs_annotation_comment_domain]) ).
cnf(f_71_2,plain,
iext(uri_rdfs_domain,uri_rdfs_comment,uri_rdfs_Resource),
inference(clausify,[status(thm)],[f_71_1]) ).
fof(f_72_1,plain,
iext(uri_rdfs_range,uri_rdfs_comment,uri_rdfs_Literal),
inference(fof_nnf,[status(thm)],[rdfs_annotation_comment_range]) ).
cnf(f_72_2,plain,
iext(uri_rdfs_range,uri_rdfs_comment,uri_rdfs_Literal),
inference(clausify,[status(thm)],[f_72_1]) ).
fof(f_73_1,plain,
iext(uri_rdfs_domain,uri_rdfs_isDefinedBy,uri_rdfs_Resource),
inference(fof_nnf,[status(thm)],[rdfs_annotation_isdefinedby_domain]) ).
cnf(f_73_2,plain,
iext(uri_rdfs_domain,uri_rdfs_isDefinedBy,uri_rdfs_Resource),
inference(clausify,[status(thm)],[f_73_1]) ).
fof(f_74_1,plain,
iext(uri_rdfs_range,uri_rdfs_isDefinedBy,uri_rdfs_Resource),
inference(fof_nnf,[status(thm)],[rdfs_annotation_isdefinedby_range]) ).
cnf(f_74_2,plain,
iext(uri_rdfs_range,uri_rdfs_isDefinedBy,uri_rdfs_Resource),
inference(clausify,[status(thm)],[f_74_1]) ).
fof(f_75_1,plain,
iext(uri_rdfs_subPropertyOf,uri_rdfs_isDefinedBy,uri_rdfs_seeAlso),
inference(fof_nnf,[status(thm)],[rdfs_annotation_isdefinedby_sub]) ).
cnf(f_75_2,plain,
iext(uri_rdfs_subPropertyOf,uri_rdfs_isDefinedBy,uri_rdfs_seeAlso),
inference(clausify,[status(thm)],[f_75_1]) ).
fof(f_76_1,plain,
iext(uri_rdfs_domain,uri_rdfs_label,uri_rdfs_Resource),
inference(fof_nnf,[status(thm)],[rdfs_annotation_label_domain]) ).
cnf(f_76_2,plain,
iext(uri_rdfs_domain,uri_rdfs_label,uri_rdfs_Resource),
inference(clausify,[status(thm)],[f_76_1]) ).
fof(f_77_1,plain,
iext(uri_rdfs_range,uri_rdfs_label,uri_rdfs_Literal),
inference(fof_nnf,[status(thm)],[rdfs_annotation_label_range]) ).
cnf(f_77_2,plain,
iext(uri_rdfs_range,uri_rdfs_label,uri_rdfs_Literal),
inference(clausify,[status(thm)],[f_77_1]) ).
fof(f_78_1,plain,
iext(uri_rdfs_domain,uri_rdfs_seeAlso,uri_rdfs_Resource),
inference(fof_nnf,[status(thm)],[rdfs_annotation_seealso_domain]) ).
cnf(f_78_2,plain,
iext(uri_rdfs_domain,uri_rdfs_seeAlso,uri_rdfs_Resource),
inference(clausify,[status(thm)],[f_78_1]) ).
fof(f_79_1,plain,
iext(uri_rdfs_range,uri_rdfs_seeAlso,uri_rdfs_Resource),
inference(fof_nnf,[status(thm)],[rdfs_annotation_seealso_range]) ).
cnf(f_79_2,plain,
iext(uri_rdfs_range,uri_rdfs_seeAlso,uri_rdfs_Resource),
inference(clausify,[status(thm)],[f_79_1]) ).
fof(f_80_1,plain,
! [X,C] :
( ( iext(uri_rdf_type,X,C)
| ~ icext(C,X) )
& ( icext(C,X)
| ~ iext(uri_rdf_type,X,C) ) ),
inference(fof_nnf,[status(thm)],[rdfs_cext_def]) ).
fof(f_80_2,plain,
! [U_219,U_218] :
( ( iext(uri_rdf_type,U_219,U_218)
| ~ icext(U_218,U_219) )
& ( icext(U_218,U_219)
| ~ iext(uri_rdf_type,U_219,U_218) ) ),
inference(variable_rename,[status(thm)],[f_80_1]) ).
fof(f_80_3,plain,
( ! [U_223,U_221] :
( iext(uri_rdf_type,U_223,U_221)
| ~ icext(U_221,U_223) )
& ! [U_222,U_220] :
( icext(U_220,U_222)
| ~ iext(uri_rdf_type,U_222,U_220) ) ),
inference(miniscope,[status(thm)],[f_80_2]) ).
cnf(f_80_4,plain,
( icext(U_220,U_222)
| ~ iext(uri_rdf_type,U_222,U_220) ),
inference(clausify,[status(thm)],[f_80_3]) ).
cnf(f_80_5,plain,
( iext(uri_rdf_type,U_223,U_221)
| ~ icext(U_221,U_223) ),
inference(clausify,[status(thm)],[f_80_3]) ).
fof(f_81_1,plain,
! [C] :
( iext(uri_rdfs_subClassOf,C,uri_rdfs_Resource)
| ~ ic(C) ),
inference(fof_nnf,[status(thm)],[rdfs_class_instsub_resource]) ).
fof(f_81_2,plain,
! [U_224] :
( iext(uri_rdfs_subClassOf,U_224,uri_rdfs_Resource)
| ~ ic(U_224) ),
inference(variable_rename,[status(thm)],[f_81_1]) ).
cnf(f_81_3,plain,
( iext(uri_rdfs_subClassOf,U_224,uri_rdfs_Resource)
| ~ ic(U_224) ),
inference(clausify,[status(thm)],[f_81_2]) ).
fof(f_82_1,plain,
iext(uri_rdfs_domain,uri_rdf_first,uri_rdf_List),
inference(fof_nnf,[status(thm)],[rdfs_collection_first_domain]) ).
cnf(f_82_2,plain,
iext(uri_rdfs_domain,uri_rdf_first,uri_rdf_List),
inference(clausify,[status(thm)],[f_82_1]) ).
fof(f_83_1,plain,
iext(uri_rdfs_range,uri_rdf_first,uri_rdfs_Resource),
inference(fof_nnf,[status(thm)],[rdfs_collection_first_range]) ).
cnf(f_83_2,plain,
iext(uri_rdfs_range,uri_rdf_first,uri_rdfs_Resource),
inference(clausify,[status(thm)],[f_83_1]) ).
fof(f_84_1,plain,
iext(uri_rdfs_domain,uri_rdf_rest,uri_rdf_List),
inference(fof_nnf,[status(thm)],[rdfs_collection_rest_domain]) ).
cnf(f_84_2,plain,
iext(uri_rdfs_domain,uri_rdf_rest,uri_rdf_List),
inference(clausify,[status(thm)],[f_84_1]) ).
fof(f_85_1,plain,
iext(uri_rdfs_range,uri_rdf_rest,uri_rdf_List),
inference(fof_nnf,[status(thm)],[rdfs_collection_rest_range]) ).
cnf(f_85_2,plain,
iext(uri_rdfs_range,uri_rdf_rest,uri_rdf_List),
inference(clausify,[status(thm)],[f_85_1]) ).
fof(f_86_1,plain,
iext(uri_rdfs_subClassOf,uri_rdf_Alt,uri_rdfs_Container),
inference(fof_nnf,[status(thm)],[rdfs_container_alt_sub]) ).
cnf(f_86_2,plain,
iext(uri_rdfs_subClassOf,uri_rdf_Alt,uri_rdfs_Container),
inference(clausify,[status(thm)],[f_86_1]) ).
fof(f_87_1,plain,
iext(uri_rdfs_subClassOf,uri_rdf_Bag,uri_rdfs_Container),
inference(fof_nnf,[status(thm)],[rdfs_container_bag_sub]) ).
cnf(f_87_2,plain,
iext(uri_rdfs_subClassOf,uri_rdf_Bag,uri_rdfs_Container),
inference(clausify,[status(thm)],[f_87_1]) ).
fof(f_88_1,plain,
! [P] :
( iext(uri_rdfs_subPropertyOf,P,uri_rdfs_member)
| ~ icext(uri_rdfs_ContainerMembershipProperty,P) ),
inference(fof_nnf,[status(thm)],[rdfs_container_containermembershipproperty_instsub_member]) ).
fof(f_88_2,plain,
! [U_225] :
( iext(uri_rdfs_subPropertyOf,U_225,uri_rdfs_member)
| ~ icext(uri_rdfs_ContainerMembershipProperty,U_225) ),
inference(variable_rename,[status(thm)],[f_88_1]) ).
cnf(f_88_3,plain,
( iext(uri_rdfs_subPropertyOf,U_225,uri_rdfs_member)
| ~ icext(uri_rdfs_ContainerMembershipProperty,U_225) ),
inference(clausify,[status(thm)],[f_88_2]) ).
fof(f_89_1,plain,
iext(uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty,uri_rdf_Property),
inference(fof_nnf,[status(thm)],[rdfs_container_containermembershipproperty_sub]) ).
cnf(f_89_2,plain,
iext(uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty,uri_rdf_Property),
inference(clausify,[status(thm)],[f_89_1]) ).
fof(f_90_1,plain,
iext(uri_rdfs_domain,uri_rdfs_member,uri_rdfs_Resource),
inference(fof_nnf,[status(thm)],[rdfs_container_member_domain]) ).
cnf(f_90_2,plain,
iext(uri_rdfs_domain,uri_rdfs_member,uri_rdfs_Resource),
inference(clausify,[status(thm)],[f_90_1]) ).
fof(f_91_1,plain,
iext(uri_rdfs_range,uri_rdfs_member,uri_rdfs_Resource),
inference(fof_nnf,[status(thm)],[rdfs_container_member_range]) ).
cnf(f_91_2,plain,
iext(uri_rdfs_range,uri_rdfs_member,uri_rdfs_Resource),
inference(clausify,[status(thm)],[f_91_1]) ).
fof(f_92_1,plain,
iext(uri_rdfs_domain,uri_rdf__1,uri_rdfs_Resource),
inference(fof_nnf,[status(thm)],[rdfs_container_n_domain_001]) ).
cnf(f_92_2,plain,
iext(uri_rdfs_domain,uri_rdf__1,uri_rdfs_Resource),
inference(clausify,[status(thm)],[f_92_1]) ).
fof(f_93_1,plain,
iext(uri_rdfs_domain,uri_rdf__2,uri_rdfs_Resource),
inference(fof_nnf,[status(thm)],[rdfs_container_n_domain_002]) ).
cnf(f_93_2,plain,
iext(uri_rdfs_domain,uri_rdf__2,uri_rdfs_Resource),
inference(clausify,[status(thm)],[f_93_1]) ).
fof(f_94_1,plain,
iext(uri_rdfs_domain,uri_rdf__3,uri_rdfs_Resource),
inference(fof_nnf,[status(thm)],[rdfs_container_n_domain_003]) ).
cnf(f_94_2,plain,
iext(uri_rdfs_domain,uri_rdf__3,uri_rdfs_Resource),
inference(clausify,[status(thm)],[f_94_1]) ).
fof(f_95_1,plain,
iext(uri_rdfs_range,uri_rdf__1,uri_rdfs_Resource),
inference(fof_nnf,[status(thm)],[rdfs_container_n_range_001]) ).
cnf(f_95_2,plain,
iext(uri_rdfs_range,uri_rdf__1,uri_rdfs_Resource),
inference(clausify,[status(thm)],[f_95_1]) ).
fof(f_96_1,plain,
iext(uri_rdfs_range,uri_rdf__2,uri_rdfs_Resource),
inference(fof_nnf,[status(thm)],[rdfs_container_n_range_002]) ).
cnf(f_96_2,plain,
iext(uri_rdfs_range,uri_rdf__2,uri_rdfs_Resource),
inference(clausify,[status(thm)],[f_96_1]) ).
fof(f_97_1,plain,
iext(uri_rdfs_range,uri_rdf__3,uri_rdfs_Resource),
inference(fof_nnf,[status(thm)],[rdfs_container_n_range_003]) ).
cnf(f_97_2,plain,
iext(uri_rdfs_range,uri_rdf__3,uri_rdfs_Resource),
inference(clausify,[status(thm)],[f_97_1]) ).
fof(f_98_1,plain,
iext(uri_rdf_type,uri_rdf__1,uri_rdfs_ContainerMembershipProperty),
inference(fof_nnf,[status(thm)],[rdfs_container_n_type_001]) ).
cnf(f_98_2,plain,
iext(uri_rdf_type,uri_rdf__1,uri_rdfs_ContainerMembershipProperty),
inference(clausify,[status(thm)],[f_98_1]) ).
fof(f_99_1,plain,
iext(uri_rdf_type,uri_rdf__2,uri_rdfs_ContainerMembershipProperty),
inference(fof_nnf,[status(thm)],[rdfs_container_n_type_002]) ).
cnf(f_99_2,plain,
iext(uri_rdf_type,uri_rdf__2,uri_rdfs_ContainerMembershipProperty),
inference(clausify,[status(thm)],[f_99_1]) ).
fof(f_100_1,plain,
iext(uri_rdf_type,uri_rdf__3,uri_rdfs_ContainerMembershipProperty),
inference(fof_nnf,[status(thm)],[rdfs_container_n_type_003]) ).
cnf(f_100_2,plain,
iext(uri_rdf_type,uri_rdf__3,uri_rdfs_ContainerMembershipProperty),
inference(clausify,[status(thm)],[f_100_1]) ).
fof(f_101_1,plain,
iext(uri_rdfs_subClassOf,uri_rdfs_Seq,uri_rdfs_Container),
inference(fof_nnf,[status(thm)],[rdfs_container_seq_sub]) ).
cnf(f_101_2,plain,
iext(uri_rdfs_subClassOf,uri_rdfs_Seq,uri_rdfs_Container),
inference(clausify,[status(thm)],[f_101_1]) ).
fof(f_102_1,plain,
iext(uri_rdfs_subClassOf,uri_rdf_XMLLiteral,uri_rdfs_Literal),
inference(fof_nnf,[status(thm)],[rdfs_dat_xmlliteral_sub]) ).
cnf(f_102_2,plain,
iext(uri_rdfs_subClassOf,uri_rdf_XMLLiteral,uri_rdfs_Literal),
inference(clausify,[status(thm)],[f_102_1]) ).
fof(f_103_1,plain,
iext(uri_rdf_type,uri_rdf_XMLLiteral,uri_rdfs_Datatype),
inference(fof_nnf,[status(thm)],[rdfs_dat_xmlliteral_type]) ).
cnf(f_103_2,plain,
iext(uri_rdf_type,uri_rdf_XMLLiteral,uri_rdfs_Datatype),
inference(clausify,[status(thm)],[f_103_1]) ).
fof(f_104_1,plain,
! [D] :
( iext(uri_rdfs_subClassOf,D,uri_rdfs_Literal)
| ~ icext(uri_rdfs_Datatype,D) ),
inference(fof_nnf,[status(thm)],[rdfs_datatype_instsub_literal]) ).
fof(f_104_2,plain,
! [U_226] :
( iext(uri_rdfs_subClassOf,U_226,uri_rdfs_Literal)
| ~ icext(uri_rdfs_Datatype,U_226) ),
inference(variable_rename,[status(thm)],[f_104_1]) ).
cnf(f_104_3,plain,
( iext(uri_rdfs_subClassOf,U_226,uri_rdfs_Literal)
| ~ icext(uri_rdfs_Datatype,U_226) ),
inference(clausify,[status(thm)],[f_104_2]) ).
fof(f_105_1,plain,
iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,uri_rdfs_Class),
inference(fof_nnf,[status(thm)],[rdfs_datatype_sub]) ).
cnf(f_105_2,plain,
iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,uri_rdfs_Class),
inference(clausify,[status(thm)],[f_105_1]) ).
fof(f_106_1,plain,
iext(uri_rdfs_domain,uri_rdfs_domain,uri_rdf_Property),
inference(fof_nnf,[status(thm)],[rdfs_domain_domain]) ).
cnf(f_106_2,plain,
iext(uri_rdfs_domain,uri_rdfs_domain,uri_rdf_Property),
inference(clausify,[status(thm)],[f_106_1]) ).
fof(f_107_1,plain,
! [P,C,X,Y] :
( icext(C,X)
| ~ iext(P,X,Y)
| ~ iext(uri_rdfs_domain,P,C) ),
inference(fof_nnf,[status(thm)],[rdfs_domain_main]) ).
fof(f_107_2,plain,
! [U_230,U_229,U_228,U_227] :
( icext(U_229,U_228)
| ~ iext(U_230,U_228,U_227)
| ~ iext(uri_rdfs_domain,U_230,U_229) ),
inference(variable_rename,[status(thm)],[f_107_1]) ).
fof(f_107_3,plain,
! [U_230,U_229,U_228] :
( ! [U_227] : ~ iext(U_230,U_228,U_227)
| ~ iext(uri_rdfs_domain,U_230,U_229)
| icext(U_229,U_228) ),
inference(miniscope,[status(thm)],[f_107_2]) ).
cnf(f_107_4,plain,
( ~ iext(U_230,U_228,U_227)
| ~ iext(uri_rdfs_domain,U_230,U_229)
| icext(U_229,U_228) ),
inference(clausify,[status(thm)],[f_107_3]) ).
fof(f_108_1,plain,
iext(uri_rdfs_range,uri_rdfs_domain,uri_rdfs_Class),
inference(fof_nnf,[status(thm)],[rdfs_domain_range]) ).
cnf(f_108_2,plain,
iext(uri_rdfs_range,uri_rdfs_domain,uri_rdfs_Class),
inference(clausify,[status(thm)],[f_108_1]) ).
fof(f_109_1,plain,
! [X] :
( ( ic(X)
| ~ icext(uri_rdfs_Class,X) )
& ( icext(uri_rdfs_Class,X)
| ~ ic(X) ) ),
inference(fof_nnf,[status(thm)],[rdfs_ic_def]) ).
fof(f_109_2,plain,
! [U_231] :
( ( ic(U_231)
| ~ icext(uri_rdfs_Class,U_231) )
& ( icext(uri_rdfs_Class,U_231)
| ~ ic(U_231) ) ),
inference(variable_rename,[status(thm)],[f_109_1]) ).
fof(f_109_3,plain,
( ! [U_233] :
( ic(U_233)
| ~ icext(uri_rdfs_Class,U_233) )
& ! [U_232] :
( icext(uri_rdfs_Class,U_232)
| ~ ic(U_232) ) ),
inference(miniscope,[status(thm)],[f_109_2]) ).
cnf(f_109_4,plain,
( icext(uri_rdfs_Class,U_232)
| ~ ic(U_232) ),
inference(clausify,[status(thm)],[f_109_3]) ).
cnf(f_109_5,plain,
( ic(U_233)
| ~ icext(uri_rdfs_Class,U_233) ),
inference(clausify,[status(thm)],[f_109_3]) ).
fof(f_110_1,plain,
! [X] :
( ( ir(X)
| ~ icext(uri_rdfs_Resource,X) )
& ( icext(uri_rdfs_Resource,X)
| ~ ir(X) ) ),
inference(fof_nnf,[status(thm)],[rdfs_ir_def]) ).
fof(f_110_2,plain,
! [U_234] :
( ( ir(U_234)
| ~ icext(uri_rdfs_Resource,U_234) )
& ( icext(uri_rdfs_Resource,U_234)
| ~ ir(U_234) ) ),
inference(variable_rename,[status(thm)],[f_110_1]) ).
fof(f_110_3,plain,
( ! [U_236] :
( ir(U_236)
| ~ icext(uri_rdfs_Resource,U_236) )
& ! [U_235] :
( icext(uri_rdfs_Resource,U_235)
| ~ ir(U_235) ) ),
inference(miniscope,[status(thm)],[f_110_2]) ).
cnf(f_110_4,plain,
( icext(uri_rdfs_Resource,U_235)
| ~ ir(U_235) ),
inference(clausify,[status(thm)],[f_110_3]) ).
cnf(f_110_5,plain,
( ir(U_236)
| ~ icext(uri_rdfs_Resource,U_236) ),
inference(clausify,[status(thm)],[f_110_3]) ).
fof(f_111_1,plain,
! [X] :
( ( lv(X)
| ~ icext(uri_rdfs_Literal,X) )
& ( icext(uri_rdfs_Literal,X)
| ~ lv(X) ) ),
inference(fof_nnf,[status(thm)],[rdfs_lv_def]) ).
fof(f_111_2,plain,
! [U_237] :
( ( lv(U_237)
| ~ icext(uri_rdfs_Literal,U_237) )
& ( icext(uri_rdfs_Literal,U_237)
| ~ lv(U_237) ) ),
inference(variable_rename,[status(thm)],[f_111_1]) ).
fof(f_111_3,plain,
( ! [U_239] :
( lv(U_239)
| ~ icext(uri_rdfs_Literal,U_239) )
& ! [U_238] :
( icext(uri_rdfs_Literal,U_238)
| ~ lv(U_238) ) ),
inference(miniscope,[status(thm)],[f_111_2]) ).
cnf(f_111_4,plain,
( icext(uri_rdfs_Literal,U_238)
| ~ lv(U_238) ),
inference(clausify,[status(thm)],[f_111_3]) ).
cnf(f_111_5,plain,
( lv(U_239)
| ~ icext(uri_rdfs_Literal,U_239) ),
inference(clausify,[status(thm)],[f_111_3]) ).
fof(f_112_1,plain,
iext(uri_rdf_type,uri_rdf_Property,uri_rdfs_Class),
inference(fof_nnf,[status(thm)],[rdfs_property_type]) ).
cnf(f_112_2,plain,
iext(uri_rdf_type,uri_rdf_Property,uri_rdfs_Class),
inference(clausify,[status(thm)],[f_112_1]) ).
fof(f_113_1,plain,
iext(uri_rdfs_domain,uri_rdfs_range,uri_rdf_Property),
inference(fof_nnf,[status(thm)],[rdfs_range_domain]) ).
cnf(f_113_2,plain,
iext(uri_rdfs_domain,uri_rdfs_range,uri_rdf_Property),
inference(clausify,[status(thm)],[f_113_1]) ).
fof(f_114_1,plain,
! [P,C,X,Y] :
( icext(C,Y)
| ~ iext(P,X,Y)
| ~ iext(uri_rdfs_range,P,C) ),
inference(fof_nnf,[status(thm)],[rdfs_range_main]) ).
fof(f_114_2,plain,
! [U_243,U_242,U_241,U_240] :
( icext(U_242,U_240)
| ~ iext(U_243,U_241,U_240)
| ~ iext(uri_rdfs_range,U_243,U_242) ),
inference(variable_rename,[status(thm)],[f_114_1]) ).
cnf(f_114_3,plain,
( icext(U_242,U_240)
| ~ iext(U_243,U_241,U_240)
| ~ iext(uri_rdfs_range,U_243,U_242) ),
inference(clausify,[status(thm)],[f_114_2]) ).
fof(f_115_1,plain,
iext(uri_rdfs_range,uri_rdfs_range,uri_rdfs_Class),
inference(fof_nnf,[status(thm)],[rdfs_range_range]) ).
cnf(f_115_2,plain,
iext(uri_rdfs_range,uri_rdfs_range,uri_rdfs_Class),
inference(clausify,[status(thm)],[f_115_1]) ).
fof(f_116_1,plain,
iext(uri_rdfs_domain,uri_rdf_object,uri_rdfs_Statement),
inference(fof_nnf,[status(thm)],[rdfs_reification_object_domain]) ).
cnf(f_116_2,plain,
iext(uri_rdfs_domain,uri_rdf_object,uri_rdfs_Statement),
inference(clausify,[status(thm)],[f_116_1]) ).
fof(f_117_1,plain,
iext(uri_rdfs_range,uri_rdf_predicate,uri_rdfs_Resource),
inference(fof_nnf,[status(thm)],[rdfs_reification_object_range]) ).
cnf(f_117_2,plain,
iext(uri_rdfs_range,uri_rdf_predicate,uri_rdfs_Resource),
inference(clausify,[status(thm)],[f_117_1]) ).
fof(f_118_1,plain,
iext(uri_rdfs_domain,uri_rdf_predicate,uri_rdfs_Statement),
inference(fof_nnf,[status(thm)],[rdfs_reification_predicate_domain]) ).
cnf(f_118_2,plain,
iext(uri_rdfs_domain,uri_rdf_predicate,uri_rdfs_Statement),
inference(clausify,[status(thm)],[f_118_1]) ).
fof(f_119_1,plain,
iext(uri_rdfs_range,uri_rdf_predicate,uri_rdfs_Resource),
inference(fof_nnf,[status(thm)],[rdfs_reification_predicate_range]) ).
cnf(f_119_2,plain,
iext(uri_rdfs_range,uri_rdf_predicate,uri_rdfs_Resource),
inference(clausify,[status(thm)],[f_119_1]) ).
fof(f_120_1,plain,
iext(uri_rdfs_domain,uri_rdf_subject,uri_rdfs_Statement),
inference(fof_nnf,[status(thm)],[rdfs_reification_subject_domain]) ).
cnf(f_120_2,plain,
iext(uri_rdfs_domain,uri_rdf_subject,uri_rdfs_Statement),
inference(clausify,[status(thm)],[f_120_1]) ).
fof(f_121_1,plain,
iext(uri_rdfs_range,uri_rdf_subject,uri_rdfs_Resource),
inference(fof_nnf,[status(thm)],[rdfs_reification_subject_range]) ).
cnf(f_121_2,plain,
iext(uri_rdfs_range,uri_rdf_subject,uri_rdfs_Resource),
inference(clausify,[status(thm)],[f_121_1]) ).
fof(f_122_1,plain,
iext(uri_rdfs_domain,uri_rdfs_subClassOf,uri_rdfs_Class),
inference(fof_nnf,[status(thm)],[rdfs_subclassof_domain]) ).
cnf(f_122_2,plain,
iext(uri_rdfs_domain,uri_rdfs_subClassOf,uri_rdfs_Class),
inference(clausify,[status(thm)],[f_122_1]) ).
fof(f_123_1,plain,
! [C,D] :
( ( ! [X] :
( icext(D,X)
| ~ icext(C,X) )
& ic(D)
& ic(C) )
| ~ iext(uri_rdfs_subClassOf,C,D) ),
inference(fof_nnf,[status(thm)],[rdfs_subclassof_main]) ).
fof(f_123_2,plain,
! [U_246,U_245] :
( ( ! [U_244] :
( icext(U_245,U_244)
| ~ icext(U_246,U_244) )
& ic(U_245)
& ic(U_246) )
| ~ iext(uri_rdfs_subClassOf,U_246,U_245) ),
inference(variable_rename,[status(thm)],[f_123_1]) ).
cnf(f_123_3,plain,
( ic(U_246)
| ~ iext(uri_rdfs_subClassOf,U_246,U_245) ),
inference(clausify,[status(thm)],[f_123_2]) ).
cnf(f_123_4,plain,
( ic(U_245)
| ~ iext(uri_rdfs_subClassOf,U_246,U_245) ),
inference(clausify,[status(thm)],[f_123_2]) ).
cnf(f_123_5,plain,
( icext(U_245,U_244)
| ~ icext(U_246,U_244)
| ~ iext(uri_rdfs_subClassOf,U_246,U_245) ),
inference(clausify,[status(thm)],[f_123_2]) ).
fof(f_124_1,plain,
iext(uri_rdfs_range,uri_rdfs_subClassOf,uri_rdfs_Class),
inference(fof_nnf,[status(thm)],[rdfs_subclassof_range]) ).
cnf(f_124_2,plain,
iext(uri_rdfs_range,uri_rdfs_subClassOf,uri_rdfs_Class),
inference(clausify,[status(thm)],[f_124_1]) ).
fof(f_125_1,plain,
! [C] :
( iext(uri_rdfs_subClassOf,C,C)
| ~ ic(C) ),
inference(fof_nnf,[status(thm)],[rdfs_subclassof_reflex]) ).
fof(f_125_2,plain,
! [U_247] :
( iext(uri_rdfs_subClassOf,U_247,U_247)
| ~ ic(U_247) ),
inference(variable_rename,[status(thm)],[f_125_1]) ).
cnf(f_125_3,plain,
( iext(uri_rdfs_subClassOf,U_247,U_247)
| ~ ic(U_247) ),
inference(clausify,[status(thm)],[f_125_2]) ).
fof(f_126_1,plain,
! [C,D,E] :
( iext(uri_rdfs_subClassOf,C,E)
| ~ iext(uri_rdfs_subClassOf,D,E)
| ~ iext(uri_rdfs_subClassOf,C,D) ),
inference(fof_nnf,[status(thm)],[rdfs_subclassof_trans]) ).
fof(f_126_2,plain,
! [U_250,U_249,U_248] :
( iext(uri_rdfs_subClassOf,U_250,U_248)
| ~ iext(uri_rdfs_subClassOf,U_249,U_248)
| ~ iext(uri_rdfs_subClassOf,U_250,U_249) ),
inference(variable_rename,[status(thm)],[f_126_1]) ).
cnf(f_126_3,plain,
( iext(uri_rdfs_subClassOf,U_250,U_248)
| ~ iext(uri_rdfs_subClassOf,U_249,U_248)
| ~ iext(uri_rdfs_subClassOf,U_250,U_249) ),
inference(clausify,[status(thm)],[f_126_2]) ).
fof(f_127_1,plain,
iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,uri_rdf_Property),
inference(fof_nnf,[status(thm)],[rdfs_subpropertyof_domain]) ).
cnf(f_127_2,plain,
iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,uri_rdf_Property),
inference(clausify,[status(thm)],[f_127_1]) ).
fof(f_128_1,plain,
! [P,Q] :
( ( ! [X,Y] :
( iext(Q,X,Y)
| ~ iext(P,X,Y) )
& ip(Q)
& ip(P) )
| ~ iext(uri_rdfs_subPropertyOf,P,Q) ),
inference(fof_nnf,[status(thm)],[rdfs_subpropertyof_main]) ).
fof(f_128_2,plain,
! [U_254,U_253] :
( ( ! [U_252,U_251] :
( iext(U_253,U_252,U_251)
| ~ iext(U_254,U_252,U_251) )
& ip(U_253)
& ip(U_254) )
| ~ iext(uri_rdfs_subPropertyOf,U_254,U_253) ),
inference(variable_rename,[status(thm)],[f_128_1]) ).
cnf(f_128_3,plain,
( ip(U_254)
| ~ iext(uri_rdfs_subPropertyOf,U_254,U_253) ),
inference(clausify,[status(thm)],[f_128_2]) ).
cnf(f_128_4,plain,
( ip(U_253)
| ~ iext(uri_rdfs_subPropertyOf,U_254,U_253) ),
inference(clausify,[status(thm)],[f_128_2]) ).
cnf(f_128_5,plain,
( iext(U_253,U_252,U_251)
| ~ iext(U_254,U_252,U_251)
| ~ iext(uri_rdfs_subPropertyOf,U_254,U_253) ),
inference(clausify,[status(thm)],[f_128_2]) ).
fof(f_129_1,plain,
iext(uri_rdfs_range,uri_rdfs_subPropertyOf,uri_rdf_Property),
inference(fof_nnf,[status(thm)],[rdfs_subpropertyof_range]) ).
cnf(f_129_2,plain,
iext(uri_rdfs_range,uri_rdfs_subPropertyOf,uri_rdf_Property),
inference(clausify,[status(thm)],[f_129_1]) ).
fof(f_130_1,plain,
! [P] :
( iext(uri_rdfs_subPropertyOf,P,P)
| ~ ip(P) ),
inference(fof_nnf,[status(thm)],[rdfs_subpropertyof_reflex]) ).
fof(f_130_2,plain,
! [U_255] :
( iext(uri_rdfs_subPropertyOf,U_255,U_255)
| ~ ip(U_255) ),
inference(variable_rename,[status(thm)],[f_130_1]) ).
cnf(f_130_3,plain,
( iext(uri_rdfs_subPropertyOf,U_255,U_255)
| ~ ip(U_255) ),
inference(clausify,[status(thm)],[f_130_2]) ).
fof(f_131_1,plain,
! [P,Q,R] :
( iext(uri_rdfs_subPropertyOf,P,R)
| ~ iext(uri_rdfs_subPropertyOf,Q,R)
| ~ iext(uri_rdfs_subPropertyOf,P,Q) ),
inference(fof_nnf,[status(thm)],[rdfs_subpropertyof_trans]) ).
fof(f_131_2,plain,
! [U_258,U_257,U_256] :
( iext(uri_rdfs_subPropertyOf,U_258,U_256)
| ~ iext(uri_rdfs_subPropertyOf,U_257,U_256)
| ~ iext(uri_rdfs_subPropertyOf,U_258,U_257) ),
inference(variable_rename,[status(thm)],[f_131_1]) ).
cnf(f_131_3,plain,
( iext(uri_rdfs_subPropertyOf,U_258,U_256)
| ~ iext(uri_rdfs_subPropertyOf,U_257,U_256)
| ~ iext(uri_rdfs_subPropertyOf,U_258,U_257) ),
inference(clausify,[status(thm)],[f_131_2]) ).
fof(f_132_1,plain,
iext(uri_rdfs_domain,uri_rdf_type,uri_rdfs_Resource),
inference(fof_nnf,[status(thm)],[rdfs_type_domain]) ).
cnf(f_132_2,plain,
iext(uri_rdfs_domain,uri_rdf_type,uri_rdfs_Resource),
inference(clausify,[status(thm)],[f_132_1]) ).
fof(f_133_1,plain,
iext(uri_rdfs_range,uri_rdf_type,uri_rdfs_Class),
inference(fof_nnf,[status(thm)],[rdfs_type_range]) ).
cnf(f_133_2,plain,
iext(uri_rdfs_range,uri_rdf_type,uri_rdfs_Class),
inference(clausify,[status(thm)],[f_133_1]) ).
fof(f_134_1,plain,
iext(uri_rdfs_domain,uri_rdf_value,uri_rdfs_Resource),
inference(fof_nnf,[status(thm)],[rdfs_value_domain]) ).
cnf(f_134_2,plain,
iext(uri_rdfs_domain,uri_rdf_value,uri_rdfs_Resource),
inference(clausify,[status(thm)],[f_134_1]) ).
fof(f_135_1,plain,
iext(uri_rdfs_range,uri_rdf_value,uri_rdfs_Resource),
inference(fof_nnf,[status(thm)],[rdfs_value_range]) ).
cnf(f_135_2,plain,
iext(uri_rdfs_range,uri_rdf_value,uri_rdfs_Resource),
inference(clausify,[status(thm)],[f_135_1]) ).
fof(f_136_1,plain,
! [S,P,O] :
( ip(P)
| ~ iext(P,S,O) ),
inference(fof_nnf,[status(thm)],[simple_iext_property]) ).
fof(f_136_2,plain,
! [U_261,U_260,U_259] :
( ip(U_260)
| ~ iext(U_260,U_261,U_259) ),
inference(variable_rename,[status(thm)],[f_136_1]) ).
fof(f_136_3,plain,
! [U_261,U_260] :
( ! [U_259] : ~ iext(U_260,U_261,U_259)
| ip(U_260) ),
inference(miniscope,[status(thm)],[f_136_2]) ).
cnf(f_136_4,plain,
( ~ iext(U_260,U_261,U_259)
| ip(U_260) ),
inference(clausify,[status(thm)],[f_136_3]) ).
fof(f_137_1,plain,
! [X] : ir(X),
inference(fof_nnf,[status(thm)],[simple_ir]) ).
fof(f_137_2,plain,
! [U_262] : ir(U_262),
inference(variable_rename,[status(thm)],[f_137_1]) ).
cnf(f_137_3,plain,
ir(U_262),
inference(clausify,[status(thm)],[f_137_2]) ).
fof(f_138_1,plain,
! [X] :
( ir(X)
| ~ lv(X) ),
inference(fof_nnf,[status(thm)],[simple_lv]) ).
fof(f_138_2,plain,
! [U_263] :
( ir(U_263)
| ~ lv(U_263) ),
inference(variable_rename,[status(thm)],[f_138_1]) ).
cnf(f_138_3,plain,
( ir(U_263)
| ~ lv(U_263) ),
inference(clausify,[status(thm)],[f_138_2]) ).
fof(f_139_1,negated_conjecture,
~ ( iext(uri_owl_onProperty,uri_ex_r,uri_ex_p)
& iext(uri_rdf_type,uri_ex_r,uri_owl_Restriction) ),
inference(negate,[status(cth)],[testcase_conclusion_fullish_001_Subgraph_Entailment]) ).
fof(f_139_2,negated_conjecture,
( ~ iext(uri_owl_onProperty,uri_ex_r,uri_ex_p)
| ~ iext(uri_rdf_type,uri_ex_r,uri_owl_Restriction) ),
inference(fof_nnf,[status(thm)],[f_139_1]) ).
fof(f_139_3,negated_conjecture,
( ~ iext(uri_owl_onProperty,uri_ex_r,uri_ex_p)
| ~ iext(uri_rdf_type,uri_ex_r,uri_owl_Restriction) ),
inference(definitional_conversion,[status(esa)],[f_139_2]) ).
cnf(f_139_4,negated_conjecture,
( ~ iext(uri_owl_onProperty,uri_ex_r,uri_ex_p)
| ~ iext(uri_rdf_type,uri_ex_r,uri_owl_Restriction) ),
inference(clausify,[status(thm)],[f_139_3]) ).
fof(f_140_1,plain,
( iext(uri_owl_someValuesFrom,uri_ex_r,uri_ex_d)
& iext(uri_owl_onProperty,uri_ex_r,uri_ex_p)
& iext(uri_rdf_type,uri_ex_r,uri_owl_Restriction)
& iext(uri_rdfs_subClassOf,uri_ex_c,uri_ex_r) ),
inference(fof_nnf,[status(thm)],[testcase_premise_fullish_001_Subgraph_Entailment]) ).
cnf(f_140_2,plain,
iext(uri_rdfs_subClassOf,uri_ex_c,uri_ex_r),
inference(clausify,[status(thm)],[f_140_1]) ).
cnf(f_140_3,plain,
iext(uri_rdf_type,uri_ex_r,uri_owl_Restriction),
inference(clausify,[status(thm)],[f_140_1]) ).
cnf(f_140_4,plain,
iext(uri_owl_onProperty,uri_ex_r,uri_ex_p),
inference(clausify,[status(thm)],[f_140_1]) ).
cnf(f_140_5,plain,
iext(uri_owl_someValuesFrom,uri_ex_r,uri_ex_d),
inference(clausify,[status(thm)],[f_140_1]) ).
cnf(sat_proved,plain,
$false,
inference(cadical,[status(thm)],[]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.02 % Problem : SWB001+3 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.03 This is a FOF_THM_RFO_NEQ problem
% 0.00/0.04 % Command : /export/starexec/sandbox2/solver/bin/connect++ --verbosity 1 --no-colour --tptp-proof --schedule default --timeout 300 /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.36 % Computer : n009.cluster.edu
% 0.09/0.36 % Model : x86_64 x86_64
% 0.09/0.36 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.36 % Memory : 8046.5625MB
% 0.09/0.36 % OS : Linux 6.8.0-71-generic
% 0.09/0.36 % CPULimit : 300
% 0.09/0.36 % WCLimit : 300
% 0.09/0.36 % DateTime : Sun Sep 20 01:03:12 UTC 2026
% 0.09/0.36 % CPUTime :
% 0.25/0.53 % SZS status Theorem for theBenchmark
% 0.25/0.53 % SZS output start Proof for theBenchmark
% See solution above
%------------------------------------------------------------------------------