%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : SWB001+3 : TPTP v9.2.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox2/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox2/solver/bin/cse --final-prover /export/starexec/sandbox2/solver/bin/eprover --proof-time %d --global-time-limit %d
% Computer : n028.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8042.1875MB
% OS : Linux 3.10.0-693.el7.x86_64
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Tue May 5 05:16:31 PM UTC 2026
% Result : Theorem 0.33s 1.62s
% Output : CNFRefutation 0.33s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named c_0_172)
% Comments :
%------------------------------------------------------------------------------
fof(testcase_conclusion_fullish_001_Subgraph_Entailment,conjecture,
( iext(uri_rdf_type,uri_ex_r,uri_owl_Restriction)
& iext(uri_owl_onProperty,uri_ex_r,uri_ex_p) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',testcase_conclusion_fullish_001_Subgraph_Entailment) ).
fof(owl_bool_complementof_class,axiom,
! [X1,X2] :
( iext(uri_owl_complementOf,X1,X2)
=> ( ic(X1)
& ic(X2)
& ! [X3] :
( icext(X1,X3)
<=> ~ icext(X2,X3) ) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB002+0.ax',owl_bool_complementof_class) ).
fof(owl_bool_unionof_class_000,axiom,
! [X1] :
( iext(uri_owl_unionOf,X1,uri_rdf_nil)
<=> ( ic(X1)
& ! [X3] : ~ icext(X1,X3) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB002+0.ax',owl_bool_unionof_class_000) ).
fof(owl_bool_intersectionof_class_000,axiom,
! [X1] :
( iext(uri_owl_intersectionOf,X1,uri_rdf_nil)
<=> ( ic(X1)
& ! [X3] :
( icext(X1,X3)
<=> ir(X3) ) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB002+0.ax',owl_bool_intersectionof_class_000) ).
fof(simple_ir,axiom,
! [X3] : ir(X3),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB002+0.ax',simple_ir) ).
fof(owl_parts_ir_def,axiom,
! [X3] :
( ir(X3)
<=> iext(uri_rdf_type,X3,uri_rdfs_Resource) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB002+0.ax',owl_parts_ir_def) ).
fof(owl_class_nothing_ext,axiom,
! [X3] : ~ icext(uri_owl_Nothing,X3),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB002+0.ax',owl_class_nothing_ext) ).
fof(rdfs_ir_def,axiom,
! [X3] :
( ir(X3)
<=> icext(uri_rdfs_Resource,X3) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB002+0.ax',rdfs_ir_def) ).
fof(owl_class_thing_ext,axiom,
! [X3] :
( icext(uri_owl_Thing,X3)
<=> ir(X3) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB002+0.ax',owl_class_thing_ext) ).
fof(owl_bool_intersectionof_class_003,axiom,
! [X1,X4,X5,X6,X7,X8,X9] :
( ( iext(uri_rdf_first,X4,X5)
& iext(uri_rdf_rest,X4,X6)
& iext(uri_rdf_first,X6,X7)
& iext(uri_rdf_rest,X6,X8)
& iext(uri_rdf_first,X8,X9)
& iext(uri_rdf_rest,X8,uri_rdf_nil) )
=> ( iext(uri_owl_intersectionOf,X1,X4)
<=> ( ic(X1)
& ic(X5)
& ic(X7)
& ic(X9)
& ! [X3] :
( icext(X1,X3)
<=> ( icext(X5,X3)
& icext(X7,X3)
& icext(X9,X3) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB002+0.ax',owl_bool_intersectionof_class_003) ).
fof(owl_bool_unionof_class_003,axiom,
! [X1,X4,X5,X6,X7,X8,X9] :
( ( iext(uri_rdf_first,X4,X5)
& iext(uri_rdf_rest,X4,X6)
& iext(uri_rdf_first,X6,X7)
& iext(uri_rdf_rest,X6,X8)
& iext(uri_rdf_first,X8,X9)
& iext(uri_rdf_rest,X8,uri_rdf_nil) )
=> ( iext(uri_owl_unionOf,X1,X4)
<=> ( ic(X1)
& ic(X5)
& ic(X7)
& ic(X9)
& ! [X3] :
( icext(X1,X3)
<=> ( icext(X5,X3)
| icext(X7,X3)
| icext(X9,X3) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB002+0.ax',owl_bool_unionof_class_003) ).
fof(owl_bool_intersectionof_class_002,axiom,
! [X1,X4,X5,X6,X7] :
( ( iext(uri_rdf_first,X4,X5)
& iext(uri_rdf_rest,X4,X6)
& iext(uri_rdf_first,X6,X7)
& iext(uri_rdf_rest,X6,uri_rdf_nil) )
=> ( iext(uri_owl_intersectionOf,X1,X4)
<=> ( ic(X1)
& ic(X5)
& ic(X7)
& ! [X3] :
( icext(X1,X3)
<=> ( icext(X5,X3)
& icext(X7,X3) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB002+0.ax',owl_bool_intersectionof_class_002) ).
fof(owl_bool_unionof_class_002,axiom,
! [X1,X4,X5,X6,X7] :
( ( iext(uri_rdf_first,X4,X5)
& iext(uri_rdf_rest,X4,X6)
& iext(uri_rdf_first,X6,X7)
& iext(uri_rdf_rest,X6,uri_rdf_nil) )
=> ( iext(uri_owl_unionOf,X1,X4)
<=> ( ic(X1)
& ic(X5)
& ic(X7)
& ! [X3] :
( icext(X1,X3)
<=> ( icext(X5,X3)
| icext(X7,X3) ) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB002+0.ax',owl_bool_unionof_class_002) ).
fof(owl_restrict_allvaluesfrom,axiom,
! [X1,X11,X2] :
( ( iext(uri_owl_allValuesFrom,X1,X2)
& iext(uri_owl_onProperty,X1,X11) )
=> ! [X3] :
( icext(X1,X3)
<=> ! [X10] :
( iext(X11,X3,X10)
=> icext(X2,X10) ) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB002+0.ax',owl_restrict_allvaluesfrom) ).
fof(owl_restrict_somevaluesfrom,axiom,
! [X1,X11,X2] :
( ( iext(uri_owl_someValuesFrom,X1,X2)
& iext(uri_owl_onProperty,X1,X11) )
=> ! [X3] :
( icext(X1,X3)
<=> ? [X10] :
( iext(X11,X3,X10)
& icext(X2,X10) ) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB002+0.ax',owl_restrict_somevaluesfrom) ).
fof(owl_bool_unionof_class_001,axiom,
! [X1,X4,X5] :
( ( iext(uri_rdf_first,X4,X5)
& iext(uri_rdf_rest,X4,uri_rdf_nil) )
=> ( iext(uri_owl_unionOf,X1,X4)
<=> ( ic(X1)
& ic(X5)
& ! [X3] :
( icext(X1,X3)
<=> icext(X5,X3) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB002+0.ax',owl_bool_unionof_class_001) ).
fof(owl_bool_intersectionof_class_001,axiom,
! [X1,X4,X5] :
( ( iext(uri_rdf_first,X4,X5)
& iext(uri_rdf_rest,X4,uri_rdf_nil) )
=> ( iext(uri_owl_intersectionOf,X1,X4)
<=> ( ic(X1)
& ic(X5)
& ! [X3] :
( icext(X1,X3)
<=> icext(X5,X3) ) ) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB002+0.ax',owl_bool_intersectionof_class_001) ).
fof(owl_restrict_hasvalue,axiom,
! [X1,X11,X14] :
( ( iext(uri_owl_hasValue,X1,X14)
& iext(uri_owl_onProperty,X1,X11) )
=> ! [X3] :
( icext(X1,X3)
<=> iext(X11,X3,X14) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB002+0.ax',owl_restrict_hasvalue) ).
fof(owl_rdfsext_subpropertyof,axiom,
! [X12,X13] :
( iext(uri_rdfs_subPropertyOf,X12,X13)
<=> ( ip(X12)
& ip(X13)
& ! [X3,X10] :
( iext(X12,X3,X10)
=> iext(X13,X3,X10) ) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB002+0.ax',owl_rdfsext_subpropertyof) ).
fof(rdfs_subpropertyof_main,axiom,
! [X11,X17] :
( iext(uri_rdfs_subPropertyOf,X11,X17)
=> ( ip(X11)
& ip(X17)
& ! [X3,X10] :
( iext(X11,X3,X10)
=> iext(X17,X3,X10) ) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB002+0.ax',rdfs_subpropertyof_main) ).
fof(rdfs_subpropertyof_trans,axiom,
! [X11,X17,X18] :
( ( iext(uri_rdfs_subPropertyOf,X11,X17)
& iext(uri_rdfs_subPropertyOf,X17,X18) )
=> iext(uri_rdfs_subPropertyOf,X11,X18) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB002+0.ax',rdfs_subpropertyof_trans) ).
fof(rdfs_subclassof_trans,axiom,
! [X2,X15,X16] :
( ( iext(uri_rdfs_subClassOf,X2,X15)
& iext(uri_rdfs_subClassOf,X15,X16) )
=> iext(uri_rdfs_subClassOf,X2,X16) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB002+0.ax',rdfs_subclassof_trans) ).
fof(rdfs_domain_main,axiom,
! [X11,X2,X3,X10] :
( ( iext(uri_rdfs_domain,X11,X2)
& iext(X11,X3,X10) )
=> icext(X2,X3) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB002+0.ax',rdfs_domain_main) ).
fof(rdfs_range_main,axiom,
! [X11,X2,X3,X10] :
( ( iext(uri_rdfs_range,X11,X2)
& iext(X11,X3,X10) )
=> icext(X2,X10) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB002+0.ax',rdfs_range_main) ).
fof(owl_rdfsext_domain,axiom,
! [X11,X2] :
( iext(uri_rdfs_domain,X11,X2)
<=> ( ip(X11)
& ic(X2)
& ! [X3,X10] :
( iext(X11,X3,X10)
=> icext(X2,X3) ) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB002+0.ax',owl_rdfsext_domain) ).
fof(owl_rdfsext_range,axiom,
! [X11,X2] :
( iext(uri_rdfs_range,X11,X2)
<=> ( ip(X11)
& ip(X2)
& ! [X3,X10] :
( iext(X11,X3,X10)
=> icext(X2,X10) ) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB002+0.ax',owl_rdfsext_range) ).
fof(owl_rdfsext_subclassof,axiom,
! [X5,X7] :
( iext(uri_rdfs_subClassOf,X5,X7)
<=> ( ic(X5)
& ic(X7)
& ! [X3] :
( icext(X5,X3)
=> icext(X7,X3) ) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB002+0.ax',owl_rdfsext_subclassof) ).
fof(rdfs_subclassof_main,axiom,
! [X2,X15] :
( iext(uri_rdfs_subClassOf,X2,X15)
=> ( ic(X2)
& ic(X15)
& ! [X3] :
( icext(X2,X3)
=> icext(X15,X3) ) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB002+0.ax',rdfs_subclassof_main) ).
fof(rdfs_cext_def,axiom,
! [X3,X2] :
( iext(uri_rdf_type,X3,X2)
<=> icext(X2,X3) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB002+0.ax',rdfs_cext_def) ).
fof(owl_parts_ioxp_cond_inst,axiom,
! [X3] :
( ioxp(X3)
=> ! [X10,X1] :
( iext(X3,X10,X1)
=> ( ix(X10)
& ix(X1) ) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB002+0.ax',owl_parts_ioxp_cond_inst) ).
fof(owl_parts_iodp_cond_inst,axiom,
! [X3] :
( iodp(X3)
=> ! [X10,X1] :
( iext(X3,X10,X1)
=> ( ir(X10)
& lv(X1) ) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB002+0.ax',owl_parts_iodp_cond_inst) ).
fof(owl_prop_unionof_ext,axiom,
! [X3,X10] :
( iext(uri_owl_unionOf,X3,X10)
=> ( ic(X3)
& icext(uri_rdf_List,X10) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB002+0.ax',owl_prop_unionof_ext) ).
fof(owl_prop_intersectionof_ext,axiom,
! [X3,X10] :
( iext(uri_owl_intersectionOf,X3,X10)
=> ( ic(X3)
& icext(uri_rdf_List,X10) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB002+0.ax',owl_prop_intersectionof_ext) ).
fof(owl_prop_somevaluesfrom_ext,axiom,
! [X3,X10] :
( iext(uri_owl_someValuesFrom,X3,X10)
=> ( icext(uri_owl_Restriction,X3)
& ic(X10) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB002+0.ax',owl_prop_somevaluesfrom_ext) ).
fof(owl_prop_onproperty_ext,axiom,
! [X3,X10] :
( iext(uri_owl_onProperty,X3,X10)
=> ( icext(uri_owl_Restriction,X3)
& ip(X10) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB002+0.ax',owl_prop_onproperty_ext) ).
fof(owl_prop_hasvalue_ext,axiom,
! [X3,X10] :
( iext(uri_owl_hasValue,X3,X10)
=> ( icext(uri_owl_Restriction,X3)
& ir(X10) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB002+0.ax',owl_prop_hasvalue_ext) ).
fof(owl_prop_allvaluesfrom_ext,axiom,
! [X3,X10] :
( iext(uri_owl_allValuesFrom,X3,X10)
=> ( icext(uri_owl_Restriction,X3)
& ic(X10) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB002+0.ax',owl_prop_allvaluesfrom_ext) ).
fof(simple_iext_property,axiom,
! [X19,X11,X20] :
( iext(X11,X19,X20)
=> ip(X11) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB002+0.ax',simple_iext_property) ).
fof(owl_prop_complementof_ext,axiom,
! [X3,X10] :
( iext(uri_owl_complementOf,X3,X10)
=> ( ic(X3)
& ic(X10) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB002+0.ax',owl_prop_complementof_ext) ).
fof(owl_parts_ix_def,axiom,
! [X3] :
( ix(X3)
<=> iext(uri_rdf_type,X3,uri_owl_Ontology) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB002+0.ax',owl_parts_ix_def) ).
fof(owl_parts_ioxp_def,axiom,
! [X3] :
( ioxp(X3)
<=> iext(uri_rdf_type,X3,uri_owl_OntologyProperty) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB002+0.ax',owl_parts_ioxp_def) ).
fof(owl_parts_iodp_def,axiom,
! [X3] :
( iodp(X3)
<=> iext(uri_rdf_type,X3,uri_owl_DatatypeProperty) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB002+0.ax',owl_parts_iodp_def) ).
fof(rdf_type_ip,axiom,
! [X11] :
( iext(uri_rdf_type,X11,uri_rdf_Property)
<=> ip(X11) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB002+0.ax',rdf_type_ip) ).
fof(owl_parts_ip_def,axiom,
! [X3] :
( ip(X3)
<=> iext(uri_rdf_type,X3,uri_rdf_Property) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB002+0.ax',owl_parts_ip_def) ).
fof(owl_parts_ioap_def,axiom,
! [X3] :
( ioap(X3)
<=> iext(uri_rdf_type,X3,uri_owl_AnnotationProperty) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB002+0.ax',owl_parts_ioap_def) ).
fof(owl_parts_lv_def,axiom,
! [X3] :
( lv(X3)
<=> iext(uri_rdf_type,X3,uri_rdfs_Literal) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB002+0.ax',owl_parts_lv_def) ).
fof(owl_parts_idc_def,axiom,
! [X3] :
( idc(X3)
<=> iext(uri_rdf_type,X3,uri_rdfs_Datatype) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB002+0.ax',owl_parts_idc_def) ).
fof(owl_parts_ic_def,axiom,
! [X3] :
( ic(X3)
<=> iext(uri_rdf_type,X3,uri_rdfs_Class) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB002+0.ax',owl_parts_ic_def) ).
fof(rdfs_container_containermembershipproperty_instsub_member,axiom,
! [X11] :
( icext(uri_rdfs_ContainerMembershipProperty,X11)
=> iext(uri_rdfs_subPropertyOf,X11,uri_rdfs_member) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB002+0.ax',rdfs_container_containermembershipproperty_instsub_member) ).
fof(rdfs_datatype_instsub_literal,axiom,
! [X15] :
( icext(uri_rdfs_Datatype,X15)
=> iext(uri_rdfs_subClassOf,X15,uri_rdfs_Literal) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB002+0.ax',rdfs_datatype_instsub_literal) ).
fof(rdfs_subpropertyof_reflex,axiom,
! [X11] :
( ip(X11)
=> iext(uri_rdfs_subPropertyOf,X11,X11) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB002+0.ax',rdfs_subpropertyof_reflex) ).
fof(rdfs_subclassof_reflex,axiom,
! [X2] :
( ic(X2)
=> iext(uri_rdfs_subClassOf,X2,X2) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB002+0.ax',rdfs_subclassof_reflex) ).
fof(rdfs_class_instsub_resource,axiom,
! [X2] :
( ic(X2)
=> iext(uri_rdfs_subClassOf,X2,uri_rdfs_Resource) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB002+0.ax',rdfs_class_instsub_resource) ).
fof(owl_parts_idc_cond_inst,axiom,
! [X3] :
( idc(X3)
=> ! [X10] :
( icext(X3,X10)
=> lv(X10) ) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB002+0.ax',owl_parts_idc_cond_inst) ).
fof(rdfs_lv_def,axiom,
! [X3] :
( lv(X3)
<=> icext(uri_rdfs_Literal,X3) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB002+0.ax',rdfs_lv_def) ).
fof(rdfs_ic_def,axiom,
! [X3] :
( ic(X3)
<=> icext(uri_rdfs_Class,X3) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB002+0.ax',rdfs_ic_def) ).
fof(owl_parts_ioxp_cond_set,axiom,
! [X3] :
( ioxp(X3)
=> ip(X3) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB002+0.ax',owl_parts_ioxp_cond_set) ).
fof(owl_parts_iodp_cond_set,axiom,
! [X3] :
( iodp(X3)
=> ip(X3) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB002+0.ax',owl_parts_iodp_cond_set) ).
fof(owl_parts_ioap_cond_set,axiom,
! [X3] :
( ioap(X3)
=> ip(X3) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB002+0.ax',owl_parts_ioap_cond_set) ).
fof(owl_parts_idc_cond_set,axiom,
! [X3] :
( idc(X3)
=> ic(X3) ),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB002+0.ax',owl_parts_idc_cond_set) ).
fof(rdfs_annotation_isdefinedby_sub,axiom,
iext(uri_rdfs_subPropertyOf,uri_rdfs_isDefinedBy,uri_rdfs_seeAlso),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB002+0.ax',rdfs_annotation_isdefinedby_sub) ).
fof(testcase_premise_fullish_001_Subgraph_Entailment,axiom,
( iext(uri_rdfs_subClassOf,uri_ex_c,uri_ex_r)
& iext(uri_rdf_type,uri_ex_r,uri_owl_Restriction)
& iext(uri_owl_onProperty,uri_ex_r,uri_ex_p)
& iext(uri_owl_someValuesFrom,uri_ex_r,uri_ex_d) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',testcase_premise_fullish_001_Subgraph_Entailment) ).
fof(rdfs_dat_xmlliteral_sub,axiom,
iext(uri_rdfs_subClassOf,uri_rdf_XMLLiteral,uri_rdfs_Literal),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB002+0.ax',rdfs_dat_xmlliteral_sub) ).
fof(rdfs_container_seq_sub,axiom,
iext(uri_rdfs_subClassOf,uri_rdfs_Seq,uri_rdfs_Container),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB002+0.ax',rdfs_container_seq_sub) ).
fof(rdfs_container_containermembershipproperty_sub,axiom,
iext(uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty,uri_rdf_Property),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB002+0.ax',rdfs_container_containermembershipproperty_sub) ).
fof(rdfs_container_bag_sub,axiom,
iext(uri_rdfs_subClassOf,uri_rdf_Bag,uri_rdfs_Container),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB002+0.ax',rdfs_container_bag_sub) ).
fof(rdfs_container_alt_sub,axiom,
iext(uri_rdfs_subClassOf,uri_rdf_Alt,uri_rdfs_Container),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB002+0.ax',rdfs_container_alt_sub) ).
fof(rdfs_datatype_sub,axiom,
iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,uri_rdfs_Class),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB002+0.ax',rdfs_datatype_sub) ).
fof(rdfs_reification_predicate_range,axiom,
iext(uri_rdfs_range,uri_rdf_predicate,uri_rdfs_Resource),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB002+0.ax',rdfs_reification_predicate_range) ).
fof(rdfs_reification_object_range,axiom,
iext(uri_rdfs_range,uri_rdf_predicate,uri_rdfs_Resource),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB002+0.ax',rdfs_reification_object_range) ).
fof(rdfs_container_member_range,axiom,
iext(uri_rdfs_range,uri_rdfs_member,uri_rdfs_Resource),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB002+0.ax',rdfs_container_member_range) ).
fof(rdfs_annotation_label_range,axiom,
iext(uri_rdfs_range,uri_rdfs_label,uri_rdfs_Literal),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB002+0.ax',rdfs_annotation_label_range) ).
fof(rdfs_annotation_seealso_range,axiom,
iext(uri_rdfs_range,uri_rdfs_seeAlso,uri_rdfs_Resource),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB002+0.ax',rdfs_annotation_seealso_range) ).
fof(rdfs_annotation_isdefinedby_range,axiom,
iext(uri_rdfs_range,uri_rdfs_isDefinedBy,uri_rdfs_Resource),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB002+0.ax',rdfs_annotation_isdefinedby_range) ).
fof(rdfs_annotation_comment_range,axiom,
iext(uri_rdfs_range,uri_rdfs_comment,uri_rdfs_Literal),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB002+0.ax',rdfs_annotation_comment_range) ).
fof(rdfs_reification_subject_range,axiom,
iext(uri_rdfs_range,uri_rdf_subject,uri_rdfs_Resource),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB002+0.ax',rdfs_reification_subject_range) ).
fof(rdfs_value_range,axiom,
iext(uri_rdfs_range,uri_rdf_value,uri_rdfs_Resource),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB002+0.ax',rdfs_value_range) ).
fof(rdfs_container_n_range_003,axiom,
iext(uri_rdfs_range,uri_rdf__3,uri_rdfs_Resource),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB002+0.ax',rdfs_container_n_range_003) ).
fof(rdfs_container_n_range_002,axiom,
iext(uri_rdfs_range,uri_rdf__2,uri_rdfs_Resource),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB002+0.ax',rdfs_container_n_range_002) ).
fof(rdfs_container_n_range_001,axiom,
iext(uri_rdfs_range,uri_rdf__1,uri_rdfs_Resource),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB002+0.ax',rdfs_container_n_range_001) ).
fof(rdfs_subpropertyof_range,axiom,
iext(uri_rdfs_range,uri_rdfs_subPropertyOf,uri_rdf_Property),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB002+0.ax',rdfs_subpropertyof_range) ).
fof(rdfs_subclassof_range,axiom,
iext(uri_rdfs_range,uri_rdfs_subClassOf,uri_rdfs_Class),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB002+0.ax',rdfs_subclassof_range) ).
fof(rdfs_range_range,axiom,
iext(uri_rdfs_range,uri_rdfs_range,uri_rdfs_Class),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB002+0.ax',rdfs_range_range) ).
fof(rdfs_domain_range,axiom,
iext(uri_rdfs_range,uri_rdfs_domain,uri_rdfs_Class),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB002+0.ax',rdfs_domain_range) ).
fof(rdfs_type_range,axiom,
iext(uri_rdfs_range,uri_rdf_type,uri_rdfs_Class),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB002+0.ax',rdfs_type_range) ).
fof(rdfs_collection_rest_range,axiom,
iext(uri_rdfs_range,uri_rdf_rest,uri_rdf_List),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB002+0.ax',rdfs_collection_rest_range) ).
fof(rdfs_collection_first_range,axiom,
iext(uri_rdfs_range,uri_rdf_first,uri_rdfs_Resource),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB002+0.ax',rdfs_collection_first_range) ).
fof(rdfs_reification_predicate_domain,axiom,
iext(uri_rdfs_domain,uri_rdf_predicate,uri_rdfs_Statement),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB002+0.ax',rdfs_reification_predicate_domain) ).
fof(rdfs_container_member_domain,axiom,
iext(uri_rdfs_domain,uri_rdfs_member,uri_rdfs_Resource),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB002+0.ax',rdfs_container_member_domain) ).
fof(rdfs_annotation_label_domain,axiom,
iext(uri_rdfs_domain,uri_rdfs_label,uri_rdfs_Resource),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB002+0.ax',rdfs_annotation_label_domain) ).
fof(rdfs_annotation_seealso_domain,axiom,
iext(uri_rdfs_domain,uri_rdfs_seeAlso,uri_rdfs_Resource),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB002+0.ax',rdfs_annotation_seealso_domain) ).
fof(rdfs_annotation_isdefinedby_domain,axiom,
iext(uri_rdfs_domain,uri_rdfs_isDefinedBy,uri_rdfs_Resource),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB002+0.ax',rdfs_annotation_isdefinedby_domain) ).
fof(rdfs_annotation_comment_domain,axiom,
iext(uri_rdfs_domain,uri_rdfs_comment,uri_rdfs_Resource),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB002+0.ax',rdfs_annotation_comment_domain) ).
fof(rdfs_reification_subject_domain,axiom,
iext(uri_rdfs_domain,uri_rdf_subject,uri_rdfs_Statement),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB002+0.ax',rdfs_reification_subject_domain) ).
fof(rdfs_value_domain,axiom,
iext(uri_rdfs_domain,uri_rdf_value,uri_rdfs_Resource),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB002+0.ax',rdfs_value_domain) ).
fof(rdfs_reification_object_domain,axiom,
iext(uri_rdfs_domain,uri_rdf_object,uri_rdfs_Statement),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB002+0.ax',rdfs_reification_object_domain) ).
fof(rdfs_container_n_domain_003,axiom,
iext(uri_rdfs_domain,uri_rdf__3,uri_rdfs_Resource),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB002+0.ax',rdfs_container_n_domain_003) ).
fof(rdfs_container_n_domain_002,axiom,
iext(uri_rdfs_domain,uri_rdf__2,uri_rdfs_Resource),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB002+0.ax',rdfs_container_n_domain_002) ).
fof(rdfs_container_n_domain_001,axiom,
iext(uri_rdfs_domain,uri_rdf__1,uri_rdfs_Resource),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB002+0.ax',rdfs_container_n_domain_001) ).
fof(rdfs_subpropertyof_domain,axiom,
iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,uri_rdf_Property),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB002+0.ax',rdfs_subpropertyof_domain) ).
fof(rdfs_subclassof_domain,axiom,
iext(uri_rdfs_domain,uri_rdfs_subClassOf,uri_rdfs_Class),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB002+0.ax',rdfs_subclassof_domain) ).
fof(rdfs_range_domain,axiom,
iext(uri_rdfs_domain,uri_rdfs_range,uri_rdf_Property),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB002+0.ax',rdfs_range_domain) ).
fof(rdfs_domain_domain,axiom,
iext(uri_rdfs_domain,uri_rdfs_domain,uri_rdf_Property),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB002+0.ax',rdfs_domain_domain) ).
fof(rdfs_type_domain,axiom,
iext(uri_rdfs_domain,uri_rdf_type,uri_rdfs_Resource),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB002+0.ax',rdfs_type_domain) ).
fof(rdfs_collection_rest_domain,axiom,
iext(uri_rdfs_domain,uri_rdf_rest,uri_rdf_List),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB002+0.ax',rdfs_collection_rest_domain) ).
fof(rdfs_collection_first_domain,axiom,
iext(uri_rdfs_domain,uri_rdf_first,uri_rdf_List),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB002+0.ax',rdfs_collection_first_domain) ).
fof(rdfs_dat_xmlliteral_type,axiom,
iext(uri_rdf_type,uri_rdf_XMLLiteral,uri_rdfs_Datatype),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB002+0.ax',rdfs_dat_xmlliteral_type) ).
fof(rdf_reification_subject_type,axiom,
iext(uri_rdf_type,uri_rdf_subject,uri_rdf_Property),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB002+0.ax',rdf_reification_subject_type) ).
fof(rdf_reification_predicate_type,axiom,
iext(uri_rdf_type,uri_rdf_value,uri_rdf_Property),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB002+0.ax',rdf_reification_predicate_type) ).
fof(rdf_reification_object_type,axiom,
iext(uri_rdf_type,uri_rdf_object,uri_rdf_Property),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB002+0.ax',rdf_reification_object_type) ).
fof(rdfs_container_n_type_003,axiom,
iext(uri_rdf_type,uri_rdf__3,uri_rdfs_ContainerMembershipProperty),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB002+0.ax',rdfs_container_n_type_003) ).
fof(rdf_container_n_type_003,axiom,
iext(uri_rdf_type,uri_rdf__3,uri_rdf_Property),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB002+0.ax',rdf_container_n_type_003) ).
fof(rdfs_container_n_type_002,axiom,
iext(uri_rdf_type,uri_rdf__2,uri_rdfs_ContainerMembershipProperty),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB002+0.ax',rdfs_container_n_type_002) ).
fof(rdf_container_n_type_002,axiom,
iext(uri_rdf_type,uri_rdf__2,uri_rdf_Property),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB002+0.ax',rdf_container_n_type_002) ).
fof(rdfs_container_n_type_001,axiom,
iext(uri_rdf_type,uri_rdf__1,uri_rdfs_ContainerMembershipProperty),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB002+0.ax',rdfs_container_n_type_001) ).
fof(rdf_container_n_type_001,axiom,
iext(uri_rdf_type,uri_rdf__1,uri_rdf_Property),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB002+0.ax',rdf_container_n_type_001) ).
fof(rdfs_property_type,axiom,
iext(uri_rdf_type,uri_rdf_Property,uri_rdfs_Class),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB002+0.ax',rdfs_property_type) ).
fof(rdf_value_type,axiom,
iext(uri_rdf_type,uri_rdf_type,uri_rdf_Property),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB002+0.ax',rdf_value_type) ).
fof(rdf_type_type,axiom,
iext(uri_rdf_type,uri_rdf_type,uri_rdf_Property),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB002+0.ax',rdf_type_type) ).
fof(rdf_collection_rest_type,axiom,
iext(uri_rdf_type,uri_rdf_rest,uri_rdf_Property),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB002+0.ax',rdf_collection_rest_type) ).
fof(rdf_collection_first_type,axiom,
iext(uri_rdf_type,uri_rdf_first,uri_rdf_Property),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB002+0.ax',rdf_collection_first_type) ).
fof(rdf_collection_nil_type,axiom,
iext(uri_rdf_type,uri_rdf_nil,uri_rdf_List),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB002+0.ax',rdf_collection_nil_type) ).
fof(owl_prop_somevaluesfrom_type,axiom,
ip(uri_owl_someValuesFrom),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB002+0.ax',owl_prop_somevaluesfrom_type) ).
fof(owl_prop_onproperty_type,axiom,
ip(uri_owl_onProperty),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB002+0.ax',owl_prop_onproperty_type) ).
fof(owl_prop_hasvalue_type,axiom,
ip(uri_owl_hasValue),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB002+0.ax',owl_prop_hasvalue_type) ).
fof(owl_prop_allvaluesfrom_type,axiom,
ip(uri_owl_allValuesFrom),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB002+0.ax',owl_prop_allvaluesfrom_type) ).
fof(owl_prop_unionof_type,axiom,
ip(uri_owl_unionOf),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB002+0.ax',owl_prop_unionof_type) ).
fof(owl_prop_intersectionof_type,axiom,
ip(uri_owl_intersectionOf),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB002+0.ax',owl_prop_intersectionof_type) ).
fof(owl_prop_complementof_type,axiom,
ip(uri_owl_complementOf),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB002+0.ax',owl_prop_complementof_type) ).
fof(owl_class_thing_type,axiom,
ic(uri_owl_Thing),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB002+0.ax',owl_class_thing_type) ).
fof(owl_class_nothing_type,axiom,
ic(uri_owl_Nothing),
file('/export/starexec/sandbox2/benchmark/Axioms/SWB002+0.ax',owl_class_nothing_type) ).
fof(i_0_131,negated_conjecture,
~ ( iext(uri_rdf_type,uri_ex_r,uri_owl_Restriction)
& iext(uri_owl_onProperty,uri_ex_r,uri_ex_p) ),
inference(assume_negation,[status(cth)],[testcase_conclusion_fullish_001_Subgraph_Entailment]) ).
fof(i_0_132,plain,
! [X1,X2] :
( iext(uri_owl_complementOf,X1,X2)
=> ( ic(X1)
& ic(X2)
& ! [X3] :
( icext(X1,X3)
<=> ~ icext(X2,X3) ) ) ),
inference(fof_simplification,[status(thm)],[owl_bool_complementof_class]) ).
fof(i_0_133,plain,
! [X1] :
( iext(uri_owl_unionOf,X1,uri_rdf_nil)
<=> ( ic(X1)
& ! [X3] : ~ icext(X1,X3) ) ),
inference(fof_simplification,[status(thm)],[owl_bool_unionof_class_000]) ).
fof(i_0_134,plain,
! [X183,X184,X185,X186] :
( ( ic(X183)
| ~ iext(uri_owl_intersectionOf,X183,uri_rdf_nil) )
& ( ~ icext(X183,X184)
| ir(X184)
| ~ iext(uri_owl_intersectionOf,X183,uri_rdf_nil) )
& ( ~ ir(X185)
| icext(X183,X185)
| ~ iext(uri_owl_intersectionOf,X183,uri_rdf_nil) )
& ( ~ icext(X186,esk1_1(X186))
| ~ ir(esk1_1(X186))
| ~ ic(X186)
| iext(uri_owl_intersectionOf,X186,uri_rdf_nil) )
& ( icext(X186,esk1_1(X186))
| ir(esk1_1(X186))
| ~ ic(X186)
| iext(uri_owl_intersectionOf,X186,uri_rdf_nil) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[owl_bool_intersectionof_class_000])])])])])]) ).
fof(i_0_135,plain,
! [X373] : ir(X373),
inference(variable_rename,[status(thm)],[simple_ir]) ).
fof(i_0_136,plain,
! [X271] :
( ( ~ ir(X271)
| iext(uri_rdf_type,X271,uri_rdfs_Resource) )
& ( ~ iext(uri_rdf_type,X271,uri_rdfs_Resource)
| ir(X271) ) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[owl_parts_ir_def])]) ).
fof(i_0_137,plain,
! [X3] : ~ icext(uri_owl_Nothing,X3),
inference(fof_simplification,[status(thm)],[owl_class_nothing_ext]) ).
fof(i_0_138,plain,
! [X349] :
( ( ~ ir(X349)
| icext(uri_rdfs_Resource,X349) )
& ( ~ icext(uri_rdfs_Resource,X349)
| ir(X349) ) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[rdfs_ir_def])]) ).
fof(i_0_139,plain,
! [X241] :
( ( ~ icext(uri_owl_Thing,X241)
| ir(X241) )
& ( ~ ir(X241)
| icext(uri_owl_Thing,X241) ) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[owl_class_thing_ext])]) ).
fof(i_0_140,plain,
! [X202,X203,X204,X205,X206,X207,X208,X209,X210] :
( ( ic(X202)
| ~ iext(uri_owl_intersectionOf,X202,X203)
| ~ iext(uri_rdf_first,X203,X204)
| ~ iext(uri_rdf_rest,X203,X205)
| ~ iext(uri_rdf_first,X205,X206)
| ~ iext(uri_rdf_rest,X205,X207)
| ~ iext(uri_rdf_first,X207,X208)
| ~ iext(uri_rdf_rest,X207,uri_rdf_nil) )
& ( ic(X204)
| ~ iext(uri_owl_intersectionOf,X202,X203)
| ~ iext(uri_rdf_first,X203,X204)
| ~ iext(uri_rdf_rest,X203,X205)
| ~ iext(uri_rdf_first,X205,X206)
| ~ iext(uri_rdf_rest,X205,X207)
| ~ iext(uri_rdf_first,X207,X208)
| ~ iext(uri_rdf_rest,X207,uri_rdf_nil) )
& ( ic(X206)
| ~ iext(uri_owl_intersectionOf,X202,X203)
| ~ iext(uri_rdf_first,X203,X204)
| ~ iext(uri_rdf_rest,X203,X205)
| ~ iext(uri_rdf_first,X205,X206)
| ~ iext(uri_rdf_rest,X205,X207)
| ~ iext(uri_rdf_first,X207,X208)
| ~ iext(uri_rdf_rest,X207,uri_rdf_nil) )
& ( ic(X208)
| ~ iext(uri_owl_intersectionOf,X202,X203)
| ~ iext(uri_rdf_first,X203,X204)
| ~ iext(uri_rdf_rest,X203,X205)
| ~ iext(uri_rdf_first,X205,X206)
| ~ iext(uri_rdf_rest,X205,X207)
| ~ iext(uri_rdf_first,X207,X208)
| ~ iext(uri_rdf_rest,X207,uri_rdf_nil) )
& ( icext(X204,X209)
| ~ icext(X202,X209)
| ~ iext(uri_owl_intersectionOf,X202,X203)
| ~ iext(uri_rdf_first,X203,X204)
| ~ iext(uri_rdf_rest,X203,X205)
| ~ iext(uri_rdf_first,X205,X206)
| ~ iext(uri_rdf_rest,X205,X207)
| ~ iext(uri_rdf_first,X207,X208)
| ~ iext(uri_rdf_rest,X207,uri_rdf_nil) )
& ( icext(X206,X209)
| ~ icext(X202,X209)
| ~ iext(uri_owl_intersectionOf,X202,X203)
| ~ iext(uri_rdf_first,X203,X204)
| ~ iext(uri_rdf_rest,X203,X205)
| ~ iext(uri_rdf_first,X205,X206)
| ~ iext(uri_rdf_rest,X205,X207)
| ~ iext(uri_rdf_first,X207,X208)
| ~ iext(uri_rdf_rest,X207,uri_rdf_nil) )
& ( icext(X208,X209)
| ~ icext(X202,X209)
| ~ iext(uri_owl_intersectionOf,X202,X203)
| ~ iext(uri_rdf_first,X203,X204)
| ~ iext(uri_rdf_rest,X203,X205)
| ~ iext(uri_rdf_first,X205,X206)
| ~ iext(uri_rdf_rest,X205,X207)
| ~ iext(uri_rdf_first,X207,X208)
| ~ iext(uri_rdf_rest,X207,uri_rdf_nil) )
& ( ~ icext(X204,X210)
| ~ icext(X206,X210)
| ~ icext(X208,X210)
| icext(X202,X210)
| ~ iext(uri_owl_intersectionOf,X202,X203)
| ~ iext(uri_rdf_first,X203,X204)
| ~ iext(uri_rdf_rest,X203,X205)
| ~ iext(uri_rdf_first,X205,X206)
| ~ iext(uri_rdf_rest,X205,X207)
| ~ iext(uri_rdf_first,X207,X208)
| ~ iext(uri_rdf_rest,X207,uri_rdf_nil) )
& ( ~ icext(X202,esk4_7(X202,X203,X204,X205,X206,X207,X208))
| ~ icext(X204,esk4_7(X202,X203,X204,X205,X206,X207,X208))
| ~ icext(X206,esk4_7(X202,X203,X204,X205,X206,X207,X208))
| ~ icext(X208,esk4_7(X202,X203,X204,X205,X206,X207,X208))
| ~ ic(X202)
| ~ ic(X204)
| ~ ic(X206)
| ~ ic(X208)
| iext(uri_owl_intersectionOf,X202,X203)
| ~ iext(uri_rdf_first,X203,X204)
| ~ iext(uri_rdf_rest,X203,X205)
| ~ iext(uri_rdf_first,X205,X206)
| ~ iext(uri_rdf_rest,X205,X207)
| ~ iext(uri_rdf_first,X207,X208)
| ~ iext(uri_rdf_rest,X207,uri_rdf_nil) )
& ( icext(X204,esk4_7(X202,X203,X204,X205,X206,X207,X208))
| icext(X202,esk4_7(X202,X203,X204,X205,X206,X207,X208))
| ~ ic(X202)
| ~ ic(X204)
| ~ ic(X206)
| ~ ic(X208)
| iext(uri_owl_intersectionOf,X202,X203)
| ~ iext(uri_rdf_first,X203,X204)
| ~ iext(uri_rdf_rest,X203,X205)
| ~ iext(uri_rdf_first,X205,X206)
| ~ iext(uri_rdf_rest,X205,X207)
| ~ iext(uri_rdf_first,X207,X208)
| ~ iext(uri_rdf_rest,X207,uri_rdf_nil) )
& ( icext(X206,esk4_7(X202,X203,X204,X205,X206,X207,X208))
| icext(X202,esk4_7(X202,X203,X204,X205,X206,X207,X208))
| ~ ic(X202)
| ~ ic(X204)
| ~ ic(X206)
| ~ ic(X208)
| iext(uri_owl_intersectionOf,X202,X203)
| ~ iext(uri_rdf_first,X203,X204)
| ~ iext(uri_rdf_rest,X203,X205)
| ~ iext(uri_rdf_first,X205,X206)
| ~ iext(uri_rdf_rest,X205,X207)
| ~ iext(uri_rdf_first,X207,X208)
| ~ iext(uri_rdf_rest,X207,uri_rdf_nil) )
& ( icext(X208,esk4_7(X202,X203,X204,X205,X206,X207,X208))
| icext(X202,esk4_7(X202,X203,X204,X205,X206,X207,X208))
| ~ ic(X202)
| ~ ic(X204)
| ~ ic(X206)
| ~ ic(X208)
| iext(uri_owl_intersectionOf,X202,X203)
| ~ iext(uri_rdf_first,X203,X204)
| ~ iext(uri_rdf_rest,X203,X205)
| ~ iext(uri_rdf_first,X205,X206)
| ~ iext(uri_rdf_rest,X205,X207)
| ~ iext(uri_rdf_first,X207,X208)
| ~ iext(uri_rdf_rest,X207,uri_rdf_nil) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[owl_bool_intersectionof_class_003])])])])])]) ).
fof(i_0_141,plain,
! [X230,X231,X232,X233,X234,X235,X236,X237,X238] :
( ( ic(X230)
| ~ iext(uri_owl_unionOf,X230,X231)
| ~ iext(uri_rdf_first,X231,X232)
| ~ iext(uri_rdf_rest,X231,X233)
| ~ iext(uri_rdf_first,X233,X234)
| ~ iext(uri_rdf_rest,X233,X235)
| ~ iext(uri_rdf_first,X235,X236)
| ~ iext(uri_rdf_rest,X235,uri_rdf_nil) )
& ( ic(X232)
| ~ iext(uri_owl_unionOf,X230,X231)
| ~ iext(uri_rdf_first,X231,X232)
| ~ iext(uri_rdf_rest,X231,X233)
| ~ iext(uri_rdf_first,X233,X234)
| ~ iext(uri_rdf_rest,X233,X235)
| ~ iext(uri_rdf_first,X235,X236)
| ~ iext(uri_rdf_rest,X235,uri_rdf_nil) )
& ( ic(X234)
| ~ iext(uri_owl_unionOf,X230,X231)
| ~ iext(uri_rdf_first,X231,X232)
| ~ iext(uri_rdf_rest,X231,X233)
| ~ iext(uri_rdf_first,X233,X234)
| ~ iext(uri_rdf_rest,X233,X235)
| ~ iext(uri_rdf_first,X235,X236)
| ~ iext(uri_rdf_rest,X235,uri_rdf_nil) )
& ( ic(X236)
| ~ iext(uri_owl_unionOf,X230,X231)
| ~ iext(uri_rdf_first,X231,X232)
| ~ iext(uri_rdf_rest,X231,X233)
| ~ iext(uri_rdf_first,X233,X234)
| ~ iext(uri_rdf_rest,X233,X235)
| ~ iext(uri_rdf_first,X235,X236)
| ~ iext(uri_rdf_rest,X235,uri_rdf_nil) )
& ( ~ icext(X230,X237)
| icext(X232,X237)
| icext(X234,X237)
| icext(X236,X237)
| ~ iext(uri_owl_unionOf,X230,X231)
| ~ iext(uri_rdf_first,X231,X232)
| ~ iext(uri_rdf_rest,X231,X233)
| ~ iext(uri_rdf_first,X233,X234)
| ~ iext(uri_rdf_rest,X233,X235)
| ~ iext(uri_rdf_first,X235,X236)
| ~ iext(uri_rdf_rest,X235,uri_rdf_nil) )
& ( ~ icext(X232,X238)
| icext(X230,X238)
| ~ iext(uri_owl_unionOf,X230,X231)
| ~ iext(uri_rdf_first,X231,X232)
| ~ iext(uri_rdf_rest,X231,X233)
| ~ iext(uri_rdf_first,X233,X234)
| ~ iext(uri_rdf_rest,X233,X235)
| ~ iext(uri_rdf_first,X235,X236)
| ~ iext(uri_rdf_rest,X235,uri_rdf_nil) )
& ( ~ icext(X234,X238)
| icext(X230,X238)
| ~ iext(uri_owl_unionOf,X230,X231)
| ~ iext(uri_rdf_first,X231,X232)
| ~ iext(uri_rdf_rest,X231,X233)
| ~ iext(uri_rdf_first,X233,X234)
| ~ iext(uri_rdf_rest,X233,X235)
| ~ iext(uri_rdf_first,X235,X236)
| ~ iext(uri_rdf_rest,X235,uri_rdf_nil) )
& ( ~ icext(X236,X238)
| icext(X230,X238)
| ~ iext(uri_owl_unionOf,X230,X231)
| ~ iext(uri_rdf_first,X231,X232)
| ~ iext(uri_rdf_rest,X231,X233)
| ~ iext(uri_rdf_first,X233,X234)
| ~ iext(uri_rdf_rest,X233,X235)
| ~ iext(uri_rdf_first,X235,X236)
| ~ iext(uri_rdf_rest,X235,uri_rdf_nil) )
& ( ~ icext(X232,esk8_7(X230,X231,X232,X233,X234,X235,X236))
| ~ icext(X230,esk8_7(X230,X231,X232,X233,X234,X235,X236))
| ~ ic(X230)
| ~ ic(X232)
| ~ ic(X234)
| ~ ic(X236)
| iext(uri_owl_unionOf,X230,X231)
| ~ iext(uri_rdf_first,X231,X232)
| ~ iext(uri_rdf_rest,X231,X233)
| ~ iext(uri_rdf_first,X233,X234)
| ~ iext(uri_rdf_rest,X233,X235)
| ~ iext(uri_rdf_first,X235,X236)
| ~ iext(uri_rdf_rest,X235,uri_rdf_nil) )
& ( ~ icext(X234,esk8_7(X230,X231,X232,X233,X234,X235,X236))
| ~ icext(X230,esk8_7(X230,X231,X232,X233,X234,X235,X236))
| ~ ic(X230)
| ~ ic(X232)
| ~ ic(X234)
| ~ ic(X236)
| iext(uri_owl_unionOf,X230,X231)
| ~ iext(uri_rdf_first,X231,X232)
| ~ iext(uri_rdf_rest,X231,X233)
| ~ iext(uri_rdf_first,X233,X234)
| ~ iext(uri_rdf_rest,X233,X235)
| ~ iext(uri_rdf_first,X235,X236)
| ~ iext(uri_rdf_rest,X235,uri_rdf_nil) )
& ( ~ icext(X236,esk8_7(X230,X231,X232,X233,X234,X235,X236))
| ~ icext(X230,esk8_7(X230,X231,X232,X233,X234,X235,X236))
| ~ ic(X230)
| ~ ic(X232)
| ~ ic(X234)
| ~ ic(X236)
| iext(uri_owl_unionOf,X230,X231)
| ~ iext(uri_rdf_first,X231,X232)
| ~ iext(uri_rdf_rest,X231,X233)
| ~ iext(uri_rdf_first,X233,X234)
| ~ iext(uri_rdf_rest,X233,X235)
| ~ iext(uri_rdf_first,X235,X236)
| ~ iext(uri_rdf_rest,X235,uri_rdf_nil) )
& ( icext(X230,esk8_7(X230,X231,X232,X233,X234,X235,X236))
| icext(X232,esk8_7(X230,X231,X232,X233,X234,X235,X236))
| icext(X234,esk8_7(X230,X231,X232,X233,X234,X235,X236))
| icext(X236,esk8_7(X230,X231,X232,X233,X234,X235,X236))
| ~ ic(X230)
| ~ ic(X232)
| ~ ic(X234)
| ~ ic(X236)
| iext(uri_owl_unionOf,X230,X231)
| ~ iext(uri_rdf_first,X231,X232)
| ~ iext(uri_rdf_rest,X231,X233)
| ~ iext(uri_rdf_first,X233,X234)
| ~ iext(uri_rdf_rest,X233,X235)
| ~ iext(uri_rdf_first,X235,X236)
| ~ iext(uri_rdf_rest,X235,uri_rdf_nil) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[owl_bool_unionof_class_003])])])])])]) ).
fof(i_0_142,plain,
! [X194,X195,X196,X197,X198,X199,X200] :
( ( ic(X194)
| ~ iext(uri_owl_intersectionOf,X194,X195)
| ~ iext(uri_rdf_first,X195,X196)
| ~ iext(uri_rdf_rest,X195,X197)
| ~ iext(uri_rdf_first,X197,X198)
| ~ iext(uri_rdf_rest,X197,uri_rdf_nil) )
& ( ic(X196)
| ~ iext(uri_owl_intersectionOf,X194,X195)
| ~ iext(uri_rdf_first,X195,X196)
| ~ iext(uri_rdf_rest,X195,X197)
| ~ iext(uri_rdf_first,X197,X198)
| ~ iext(uri_rdf_rest,X197,uri_rdf_nil) )
& ( ic(X198)
| ~ iext(uri_owl_intersectionOf,X194,X195)
| ~ iext(uri_rdf_first,X195,X196)
| ~ iext(uri_rdf_rest,X195,X197)
| ~ iext(uri_rdf_first,X197,X198)
| ~ iext(uri_rdf_rest,X197,uri_rdf_nil) )
& ( icext(X196,X199)
| ~ icext(X194,X199)
| ~ iext(uri_owl_intersectionOf,X194,X195)
| ~ iext(uri_rdf_first,X195,X196)
| ~ iext(uri_rdf_rest,X195,X197)
| ~ iext(uri_rdf_first,X197,X198)
| ~ iext(uri_rdf_rest,X197,uri_rdf_nil) )
& ( icext(X198,X199)
| ~ icext(X194,X199)
| ~ iext(uri_owl_intersectionOf,X194,X195)
| ~ iext(uri_rdf_first,X195,X196)
| ~ iext(uri_rdf_rest,X195,X197)
| ~ iext(uri_rdf_first,X197,X198)
| ~ iext(uri_rdf_rest,X197,uri_rdf_nil) )
& ( ~ icext(X196,X200)
| ~ icext(X198,X200)
| icext(X194,X200)
| ~ iext(uri_owl_intersectionOf,X194,X195)
| ~ iext(uri_rdf_first,X195,X196)
| ~ iext(uri_rdf_rest,X195,X197)
| ~ iext(uri_rdf_first,X197,X198)
| ~ iext(uri_rdf_rest,X197,uri_rdf_nil) )
& ( ~ icext(X194,esk3_5(X194,X195,X196,X197,X198))
| ~ icext(X196,esk3_5(X194,X195,X196,X197,X198))
| ~ icext(X198,esk3_5(X194,X195,X196,X197,X198))
| ~ ic(X194)
| ~ ic(X196)
| ~ ic(X198)
| iext(uri_owl_intersectionOf,X194,X195)
| ~ iext(uri_rdf_first,X195,X196)
| ~ iext(uri_rdf_rest,X195,X197)
| ~ iext(uri_rdf_first,X197,X198)
| ~ iext(uri_rdf_rest,X197,uri_rdf_nil) )
& ( icext(X196,esk3_5(X194,X195,X196,X197,X198))
| icext(X194,esk3_5(X194,X195,X196,X197,X198))
| ~ ic(X194)
| ~ ic(X196)
| ~ ic(X198)
| iext(uri_owl_intersectionOf,X194,X195)
| ~ iext(uri_rdf_first,X195,X196)
| ~ iext(uri_rdf_rest,X195,X197)
| ~ iext(uri_rdf_first,X197,X198)
| ~ iext(uri_rdf_rest,X197,uri_rdf_nil) )
& ( icext(X198,esk3_5(X194,X195,X196,X197,X198))
| icext(X194,esk3_5(X194,X195,X196,X197,X198))
| ~ ic(X194)
| ~ ic(X196)
| ~ ic(X198)
| iext(uri_owl_intersectionOf,X194,X195)
| ~ iext(uri_rdf_first,X195,X196)
| ~ iext(uri_rdf_rest,X195,X197)
| ~ iext(uri_rdf_first,X197,X198)
| ~ iext(uri_rdf_rest,X197,uri_rdf_nil) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[owl_bool_intersectionof_class_002])])])])])]) ).
fof(i_0_143,plain,
! [X222,X223,X224,X225,X226,X227,X228] :
( ( ic(X222)
| ~ iext(uri_owl_unionOf,X222,X223)
| ~ iext(uri_rdf_first,X223,X224)
| ~ iext(uri_rdf_rest,X223,X225)
| ~ iext(uri_rdf_first,X225,X226)
| ~ iext(uri_rdf_rest,X225,uri_rdf_nil) )
& ( ic(X224)
| ~ iext(uri_owl_unionOf,X222,X223)
| ~ iext(uri_rdf_first,X223,X224)
| ~ iext(uri_rdf_rest,X223,X225)
| ~ iext(uri_rdf_first,X225,X226)
| ~ iext(uri_rdf_rest,X225,uri_rdf_nil) )
& ( ic(X226)
| ~ iext(uri_owl_unionOf,X222,X223)
| ~ iext(uri_rdf_first,X223,X224)
| ~ iext(uri_rdf_rest,X223,X225)
| ~ iext(uri_rdf_first,X225,X226)
| ~ iext(uri_rdf_rest,X225,uri_rdf_nil) )
& ( ~ icext(X222,X227)
| icext(X224,X227)
| icext(X226,X227)
| ~ iext(uri_owl_unionOf,X222,X223)
| ~ iext(uri_rdf_first,X223,X224)
| ~ iext(uri_rdf_rest,X223,X225)
| ~ iext(uri_rdf_first,X225,X226)
| ~ iext(uri_rdf_rest,X225,uri_rdf_nil) )
& ( ~ icext(X224,X228)
| icext(X222,X228)
| ~ iext(uri_owl_unionOf,X222,X223)
| ~ iext(uri_rdf_first,X223,X224)
| ~ iext(uri_rdf_rest,X223,X225)
| ~ iext(uri_rdf_first,X225,X226)
| ~ iext(uri_rdf_rest,X225,uri_rdf_nil) )
& ( ~ icext(X226,X228)
| icext(X222,X228)
| ~ iext(uri_owl_unionOf,X222,X223)
| ~ iext(uri_rdf_first,X223,X224)
| ~ iext(uri_rdf_rest,X223,X225)
| ~ iext(uri_rdf_first,X225,X226)
| ~ iext(uri_rdf_rest,X225,uri_rdf_nil) )
& ( ~ icext(X224,esk7_5(X222,X223,X224,X225,X226))
| ~ icext(X222,esk7_5(X222,X223,X224,X225,X226))
| ~ ic(X222)
| ~ ic(X224)
| ~ ic(X226)
| iext(uri_owl_unionOf,X222,X223)
| ~ iext(uri_rdf_first,X223,X224)
| ~ iext(uri_rdf_rest,X223,X225)
| ~ iext(uri_rdf_first,X225,X226)
| ~ iext(uri_rdf_rest,X225,uri_rdf_nil) )
& ( ~ icext(X226,esk7_5(X222,X223,X224,X225,X226))
| ~ icext(X222,esk7_5(X222,X223,X224,X225,X226))
| ~ ic(X222)
| ~ ic(X224)
| ~ ic(X226)
| iext(uri_owl_unionOf,X222,X223)
| ~ iext(uri_rdf_first,X223,X224)
| ~ iext(uri_rdf_rest,X223,X225)
| ~ iext(uri_rdf_first,X225,X226)
| ~ iext(uri_rdf_rest,X225,uri_rdf_nil) )
& ( icext(X222,esk7_5(X222,X223,X224,X225,X226))
| icext(X224,esk7_5(X222,X223,X224,X225,X226))
| icext(X226,esk7_5(X222,X223,X224,X225,X226))
| ~ ic(X222)
| ~ ic(X224)
| ~ ic(X226)
| iext(uri_owl_unionOf,X222,X223)
| ~ iext(uri_rdf_first,X223,X224)
| ~ iext(uri_rdf_rest,X223,X225)
| ~ iext(uri_rdf_first,X225,X226)
| ~ iext(uri_rdf_rest,X225,uri_rdf_nil) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[owl_bool_unionof_class_002])])])])])]) ).
fof(i_0_144,plain,
! [X320,X321,X322,X323,X324,X325] :
( ( ~ icext(X320,X323)
| ~ iext(X321,X323,X324)
| icext(X322,X324)
| ~ iext(uri_owl_allValuesFrom,X320,X322)
| ~ iext(uri_owl_onProperty,X320,X321) )
& ( iext(X321,X325,esk17_4(X320,X321,X322,X325))
| icext(X320,X325)
| ~ iext(uri_owl_allValuesFrom,X320,X322)
| ~ iext(uri_owl_onProperty,X320,X321) )
& ( ~ icext(X322,esk17_4(X320,X321,X322,X325))
| icext(X320,X325)
| ~ iext(uri_owl_allValuesFrom,X320,X322)
| ~ iext(uri_owl_onProperty,X320,X321) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[owl_restrict_allvaluesfrom])])])])])]) ).
fof(i_0_145,plain,
! [X331,X332,X333,X334,X336,X337] :
( ( iext(X332,X334,esk18_4(X331,X332,X333,X334))
| ~ icext(X331,X334)
| ~ iext(uri_owl_someValuesFrom,X331,X333)
| ~ iext(uri_owl_onProperty,X331,X332) )
& ( icext(X333,esk18_4(X331,X332,X333,X334))
| ~ icext(X331,X334)
| ~ iext(uri_owl_someValuesFrom,X331,X333)
| ~ iext(uri_owl_onProperty,X331,X332) )
& ( ~ iext(X332,X336,X337)
| ~ icext(X333,X337)
| icext(X331,X336)
| ~ iext(uri_owl_someValuesFrom,X331,X333)
| ~ iext(uri_owl_onProperty,X331,X332) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[owl_restrict_somevaluesfrom])])])])])]) ).
fof(i_0_146,plain,
! [X216,X217,X218,X219,X220] :
( ( ic(X216)
| ~ iext(uri_owl_unionOf,X216,X217)
| ~ iext(uri_rdf_first,X217,X218)
| ~ iext(uri_rdf_rest,X217,uri_rdf_nil) )
& ( ic(X218)
| ~ iext(uri_owl_unionOf,X216,X217)
| ~ iext(uri_rdf_first,X217,X218)
| ~ iext(uri_rdf_rest,X217,uri_rdf_nil) )
& ( ~ icext(X216,X219)
| icext(X218,X219)
| ~ iext(uri_owl_unionOf,X216,X217)
| ~ iext(uri_rdf_first,X217,X218)
| ~ iext(uri_rdf_rest,X217,uri_rdf_nil) )
& ( ~ icext(X218,X220)
| icext(X216,X220)
| ~ iext(uri_owl_unionOf,X216,X217)
| ~ iext(uri_rdf_first,X217,X218)
| ~ iext(uri_rdf_rest,X217,uri_rdf_nil) )
& ( ~ icext(X216,esk6_3(X216,X217,X218))
| ~ icext(X218,esk6_3(X216,X217,X218))
| ~ ic(X216)
| ~ ic(X218)
| iext(uri_owl_unionOf,X216,X217)
| ~ iext(uri_rdf_first,X217,X218)
| ~ iext(uri_rdf_rest,X217,uri_rdf_nil) )
& ( icext(X216,esk6_3(X216,X217,X218))
| icext(X218,esk6_3(X216,X217,X218))
| ~ ic(X216)
| ~ ic(X218)
| iext(uri_owl_unionOf,X216,X217)
| ~ iext(uri_rdf_first,X217,X218)
| ~ iext(uri_rdf_rest,X217,uri_rdf_nil) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[owl_bool_unionof_class_001])])])])])]) ).
fof(i_0_147,plain,
! [X188,X189,X190,X191,X192] :
( ( ic(X188)
| ~ iext(uri_owl_intersectionOf,X188,X189)
| ~ iext(uri_rdf_first,X189,X190)
| ~ iext(uri_rdf_rest,X189,uri_rdf_nil) )
& ( ic(X190)
| ~ iext(uri_owl_intersectionOf,X188,X189)
| ~ iext(uri_rdf_first,X189,X190)
| ~ iext(uri_rdf_rest,X189,uri_rdf_nil) )
& ( ~ icext(X188,X191)
| icext(X190,X191)
| ~ iext(uri_owl_intersectionOf,X188,X189)
| ~ iext(uri_rdf_first,X189,X190)
| ~ iext(uri_rdf_rest,X189,uri_rdf_nil) )
& ( ~ icext(X190,X192)
| icext(X188,X192)
| ~ iext(uri_owl_intersectionOf,X188,X189)
| ~ iext(uri_rdf_first,X189,X190)
| ~ iext(uri_rdf_rest,X189,uri_rdf_nil) )
& ( ~ icext(X188,esk2_3(X188,X189,X190))
| ~ icext(X190,esk2_3(X188,X189,X190))
| ~ ic(X188)
| ~ ic(X190)
| iext(uri_owl_intersectionOf,X188,X189)
| ~ iext(uri_rdf_first,X189,X190)
| ~ iext(uri_rdf_rest,X189,uri_rdf_nil) )
& ( icext(X188,esk2_3(X188,X189,X190))
| icext(X190,esk2_3(X188,X189,X190))
| ~ ic(X188)
| ~ ic(X190)
| iext(uri_owl_intersectionOf,X188,X189)
| ~ iext(uri_rdf_first,X189,X190)
| ~ iext(uri_rdf_rest,X189,uri_rdf_nil) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[owl_bool_intersectionof_class_001])])])])])]) ).
fof(i_0_148,plain,
! [X327,X328,X329,X330] :
( ( ~ icext(X327,X330)
| iext(X328,X330,X329)
| ~ iext(uri_owl_hasValue,X327,X329)
| ~ iext(uri_owl_onProperty,X327,X328) )
& ( ~ iext(X328,X330,X329)
| icext(X327,X330)
| ~ iext(uri_owl_hasValue,X327,X329)
| ~ iext(uri_owl_onProperty,X327,X328) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[owl_restrict_hasvalue])])])]) ).
fof(i_0_149,plain,
! [X312,X313,X314,X315,X316,X317] :
( ( ip(X312)
| ~ iext(uri_rdfs_subPropertyOf,X312,X313) )
& ( ip(X313)
| ~ iext(uri_rdfs_subPropertyOf,X312,X313) )
& ( ~ iext(X312,X314,X315)
| iext(X313,X314,X315)
| ~ iext(uri_rdfs_subPropertyOf,X312,X313) )
& ( iext(X316,esk15_2(X316,X317),esk16_2(X316,X317))
| ~ ip(X316)
| ~ ip(X317)
| iext(uri_rdfs_subPropertyOf,X316,X317) )
& ( ~ iext(X317,esk15_2(X316,X317),esk16_2(X316,X317))
| ~ ip(X316)
| ~ ip(X317)
| iext(uri_rdfs_subPropertyOf,X316,X317) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[owl_rdfsext_subpropertyof])])])])])]) ).
fof(i_0_150,plain,
! [X362,X363,X364,X365] :
( ( ip(X362)
| ~ iext(uri_rdfs_subPropertyOf,X362,X363) )
& ( ip(X363)
| ~ iext(uri_rdfs_subPropertyOf,X362,X363) )
& ( ~ iext(X362,X364,X365)
| iext(X363,X364,X365)
| ~ iext(uri_rdfs_subPropertyOf,X362,X363) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[rdfs_subpropertyof_main])])])]) ).
fof(i_0_151,plain,
! [X367,X368,X369] :
( ~ iext(uri_rdfs_subPropertyOf,X367,X368)
| ~ iext(uri_rdfs_subPropertyOf,X368,X369)
| iext(uri_rdfs_subPropertyOf,X367,X369) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[rdfs_subpropertyof_trans])]) ).
fof(i_0_152,plain,
! [X359,X360,X361] :
( ~ iext(uri_rdfs_subClassOf,X359,X360)
| ~ iext(uri_rdfs_subClassOf,X360,X361)
| iext(uri_rdfs_subClassOf,X359,X361) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[rdfs_subclassof_trans])]) ).
fof(i_0_153,plain,
! [X344,X345,X346,X347] :
( ~ iext(uri_rdfs_domain,X344,X345)
| ~ iext(X344,X346,X347)
| icext(X345,X346) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[rdfs_domain_main])]) ).
fof(i_0_154,plain,
! [X351,X352,X353,X354] :
( ~ iext(uri_rdfs_range,X351,X352)
| ~ iext(X351,X353,X354)
| icext(X352,X354) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[rdfs_range_main])]) ).
fof(i_0_155,plain,
! [X290,X291,X292,X293,X294,X295] :
( ( ip(X290)
| ~ iext(uri_rdfs_domain,X290,X291) )
& ( ic(X291)
| ~ iext(uri_rdfs_domain,X290,X291) )
& ( ~ iext(X290,X292,X293)
| icext(X291,X292)
| ~ iext(uri_rdfs_domain,X290,X291) )
& ( iext(X294,esk10_2(X294,X295),esk11_2(X294,X295))
| ~ ip(X294)
| ~ ic(X295)
| iext(uri_rdfs_domain,X294,X295) )
& ( ~ icext(X295,esk10_2(X294,X295))
| ~ ip(X294)
| ~ ic(X295)
| iext(uri_rdfs_domain,X294,X295) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[owl_rdfsext_domain])])])])])]) ).
fof(i_0_156,plain,
! [X298,X299,X300,X301,X302,X303] :
( ( ip(X298)
| ~ iext(uri_rdfs_range,X298,X299) )
& ( ip(X299)
| ~ iext(uri_rdfs_range,X298,X299) )
& ( ~ iext(X298,X300,X301)
| icext(X299,X301)
| ~ iext(uri_rdfs_range,X298,X299) )
& ( iext(X302,esk12_2(X302,X303),esk13_2(X302,X303))
| ~ ip(X302)
| ~ ip(X303)
| iext(uri_rdfs_range,X302,X303) )
& ( ~ icext(X303,esk13_2(X302,X303))
| ~ ip(X302)
| ~ ip(X303)
| iext(uri_rdfs_range,X302,X303) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[owl_rdfsext_range])])])])])]) ).
fof(i_0_157,negated_conjecture,
( ~ iext(uri_rdf_type,uri_ex_r,uri_owl_Restriction)
| ~ iext(uri_owl_onProperty,uri_ex_r,uri_ex_p) ),
inference(fof_nnf,[status(thm)],[i_0_131]) ).
fof(i_0_158,plain,
! [X306,X307,X308,X309,X310] :
( ( ic(X306)
| ~ iext(uri_rdfs_subClassOf,X306,X307) )
& ( ic(X307)
| ~ iext(uri_rdfs_subClassOf,X306,X307) )
& ( ~ icext(X306,X308)
| icext(X307,X308)
| ~ iext(uri_rdfs_subClassOf,X306,X307) )
& ( icext(X309,esk14_2(X309,X310))
| ~ ic(X309)
| ~ ic(X310)
| iext(uri_rdfs_subClassOf,X309,X310) )
& ( ~ icext(X310,esk14_2(X309,X310))
| ~ ic(X309)
| ~ ic(X310)
| iext(uri_rdfs_subClassOf,X309,X310) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[owl_rdfsext_subclassof])])])])])]) ).
fof(i_0_159,plain,
! [X180,X181,X182] :
( ( ic(X180)
| ~ iext(uri_owl_complementOf,X180,X181) )
& ( ic(X181)
| ~ iext(uri_owl_complementOf,X180,X181) )
& ( ~ icext(X180,X182)
| ~ icext(X181,X182)
| ~ iext(uri_owl_complementOf,X180,X181) )
& ( icext(X181,X182)
| icext(X180,X182)
| ~ iext(uri_owl_complementOf,X180,X181) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_132])])])]) ).
fof(i_0_160,plain,
! [X355,X356,X357] :
( ( ic(X355)
| ~ iext(uri_rdfs_subClassOf,X355,X356) )
& ( ic(X356)
| ~ iext(uri_rdfs_subClassOf,X355,X356) )
& ( ~ icext(X355,X357)
| icext(X356,X357)
| ~ iext(uri_rdfs_subClassOf,X355,X356) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[rdfs_subclassof_main])])])]) ).
fof(i_0_161,plain,
! [X212,X213,X214] :
( ( ic(X212)
| ~ iext(uri_owl_unionOf,X212,uri_rdf_nil) )
& ( ~ icext(X212,X213)
| ~ iext(uri_owl_unionOf,X212,uri_rdf_nil) )
& ( ~ ic(X214)
| icext(X214,esk5_1(X214))
| iext(uri_owl_unionOf,X214,uri_rdf_nil) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_133])])])])])]) ).
fof(i_0_162,plain,
! [X339,X340] :
( ( ~ iext(uri_rdf_type,X339,X340)
| icext(X340,X339) )
& ( ~ icext(X340,X339)
| iext(uri_rdf_type,X339,X340) ) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[rdfs_cext_def])]) ).
fof(i_0_163,plain,
! [X260,X261,X262] :
( ( ix(X261)
| ~ iext(X260,X261,X262)
| ~ ioxp(X260) )
& ( ix(X262)
| ~ iext(X260,X261,X262)
| ~ ioxp(X260) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[owl_parts_ioxp_cond_inst])])])]) ).
fof(i_0_164,plain,
! [X255,X256,X257] :
( ( ir(X256)
| ~ iext(X255,X256,X257)
| ~ iodp(X255) )
& ( lv(X257)
| ~ iext(X255,X256,X257)
| ~ iodp(X255) ) ),
inference(distribute,[status(thm)],[inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[owl_parts_iodp_cond_inst])])])]) ).
fof(i_0_165,plain,
! [X288,X289] :
( ( ic(X288)
| ~ iext(uri_owl_unionOf,X288,X289) )
& ( icext(uri_rdf_List,X289)
| ~ iext(uri_owl_unionOf,X288,X289) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[owl_prop_unionof_ext])])]) ).
fof(i_0_166,plain,
! [X282,X283] :
( ( ic(X282)
| ~ iext(uri_owl_intersectionOf,X282,X283) )
& ( icext(uri_rdf_List,X283)
| ~ iext(uri_owl_intersectionOf,X282,X283) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[owl_prop_intersectionof_ext])])]) ).
fof(i_0_167,plain,
! [X286,X287] :
( ( icext(uri_owl_Restriction,X286)
| ~ iext(uri_owl_someValuesFrom,X286,X287) )
& ( ic(X287)
| ~ iext(uri_owl_someValuesFrom,X286,X287) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[owl_prop_somevaluesfrom_ext])])]) ).
fof(i_0_168,plain,
! [X284,X285] :
( ( icext(uri_owl_Restriction,X284)
| ~ iext(uri_owl_onProperty,X284,X285) )
& ( ip(X285)
| ~ iext(uri_owl_onProperty,X284,X285) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[owl_prop_onproperty_ext])])]) ).
fof(i_0_169,plain,
! [X280,X281] :
( ( icext(uri_owl_Restriction,X280)
| ~ iext(uri_owl_hasValue,X280,X281) )
& ( ir(X281)
| ~ iext(uri_owl_hasValue,X280,X281) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[owl_prop_hasvalue_ext])])]) ).
fof(i_0_170,plain,
! [X276,X277] :
( ( icext(uri_owl_Restriction,X276)
| ~ iext(uri_owl_allValuesFrom,X276,X277) )
& ( ic(X277)
| ~ iext(uri_owl_allValuesFrom,X276,X277) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[owl_prop_allvaluesfrom_ext])])]) ).
cnf(i_0_171,plain,
( icext(X2,X1)
| ~ ir(X1)
| ~ iext(uri_owl_intersectionOf,X2,uri_rdf_nil) ),
inference(split_conjunct,[status(thm)],[i_0_134]) ).
cnf(i_0_172,plain,
ir(X1),
inference(split_conjunct,[status(thm)],[i_0_135]) ).
cnf(i_0_173,plain,
( iext(uri_owl_intersectionOf,X1,uri_rdf_nil)
| ~ icext(X1,esk1_1(X1))
| ~ ir(esk1_1(X1))
| ~ ic(X1) ),
inference(split_conjunct,[status(thm)],[i_0_134]) ).
fof(i_0_174,plain,
! [X370,X371,X372] :
( ~ iext(X371,X370,X372)
| ip(X371) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[simple_iext_property])]) ).
fof(i_0_175,plain,
! [X278,X279] :
( ( ic(X278)
| ~ iext(uri_owl_complementOf,X278,X279) )
& ( ic(X279)
| ~ iext(uri_owl_complementOf,X278,X279) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[owl_prop_complementof_ext])])]) ).
fof(i_0_176,plain,
! [X273] :
( ( ~ ix(X273)
| iext(uri_rdf_type,X273,uri_owl_Ontology) )
& ( ~ iext(uri_rdf_type,X273,uri_owl_Ontology)
| ix(X273) ) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[owl_parts_ix_def])]) ).
fof(i_0_177,plain,
! [X264] :
( ( ~ ioxp(X264)
| iext(uri_rdf_type,X264,uri_owl_OntologyProperty) )
& ( ~ iext(uri_rdf_type,X264,uri_owl_OntologyProperty)
| ioxp(X264) ) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[owl_parts_ioxp_def])]) ).
fof(i_0_178,plain,
! [X259] :
( ( ~ iodp(X259)
| iext(uri_rdf_type,X259,uri_owl_DatatypeProperty) )
& ( ~ iext(uri_rdf_type,X259,uri_owl_DatatypeProperty)
| iodp(X259) ) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[owl_parts_iodp_def])]) ).
fof(i_0_179,plain,
! [X338] :
( ( ~ iext(uri_rdf_type,X338,uri_rdf_Property)
| ip(X338) )
& ( ~ ip(X338)
| iext(uri_rdf_type,X338,uri_rdf_Property) ) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[rdf_type_ip])]) ).
fof(i_0_180,plain,
! [X269] :
( ( ~ ip(X269)
| iext(uri_rdf_type,X269,uri_rdf_Property) )
& ( ~ iext(uri_rdf_type,X269,uri_rdf_Property)
| ip(X269) ) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[owl_parts_ip_def])]) ).
fof(i_0_181,plain,
! [X254] :
( ( ~ ioap(X254)
| iext(uri_rdf_type,X254,uri_owl_AnnotationProperty) )
& ( ~ iext(uri_rdf_type,X254,uri_owl_AnnotationProperty)
| ioap(X254) ) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[owl_parts_ioap_def])]) ).
fof(i_0_182,plain,
! [X275] :
( ( ~ lv(X275)
| iext(uri_rdf_type,X275,uri_rdfs_Literal) )
& ( ~ iext(uri_rdf_type,X275,uri_rdfs_Literal)
| lv(X275) ) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[owl_parts_lv_def])]) ).
fof(i_0_183,plain,
! [X249] :
( ( ~ idc(X249)
| iext(uri_rdf_type,X249,uri_rdfs_Datatype) )
& ( ~ iext(uri_rdf_type,X249,uri_rdfs_Datatype)
| idc(X249) ) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[owl_parts_idc_def])]) ).
fof(i_0_184,plain,
! [X245] :
( ( ~ ic(X245)
| iext(uri_rdf_type,X245,uri_rdfs_Class) )
& ( ~ iext(uri_rdf_type,X245,uri_rdfs_Class)
| ic(X245) ) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[owl_parts_ic_def])]) ).
fof(i_0_185,plain,
! [X342] :
( ~ icext(uri_rdfs_ContainerMembershipProperty,X342)
| iext(uri_rdfs_subPropertyOf,X342,uri_rdfs_member) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[rdfs_container_containermembershipproperty_instsub_member])]) ).
fof(i_0_186,plain,
! [X343] :
( ~ icext(uri_rdfs_Datatype,X343)
| iext(uri_rdfs_subClassOf,X343,uri_rdfs_Literal) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[rdfs_datatype_instsub_literal])]) ).
fof(i_0_187,plain,
! [X366] :
( ~ ip(X366)
| iext(uri_rdfs_subPropertyOf,X366,X366) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[rdfs_subpropertyof_reflex])]) ).
fof(i_0_188,plain,
! [X358] :
( ~ ic(X358)
| iext(uri_rdfs_subClassOf,X358,X358) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[rdfs_subclassof_reflex])]) ).
fof(i_0_189,plain,
! [X341] :
( ~ ic(X341)
| iext(uri_rdfs_subClassOf,X341,uri_rdfs_Resource) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[rdfs_class_instsub_resource])]) ).
cnf(i_0_190,plain,
( iext(uri_rdf_type,X1,uri_rdfs_Resource)
| ~ ir(X1) ),
inference(split_conjunct,[status(thm)],[i_0_136]) ).
fof(i_0_191,plain,
! [X246,X247] :
( ~ idc(X246)
| ~ icext(X246,X247)
| lv(X247) ),
inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[owl_parts_idc_cond_inst])])]) ).
fof(i_0_192,plain,
! [X350] :
( ( ~ lv(X350)
| icext(uri_rdfs_Literal,X350) )
& ( ~ icext(uri_rdfs_Literal,X350)
| lv(X350) ) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[rdfs_lv_def])]) ).
fof(i_0_193,plain,
! [X348] :
( ( ~ ic(X348)
| icext(uri_rdfs_Class,X348) )
& ( ~ icext(uri_rdfs_Class,X348)
| ic(X348) ) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[rdfs_ic_def])]) ).
fof(i_0_194,plain,
! [X240] : ~ icext(uri_owl_Nothing,X240),
inference(variable_rename,[status(thm)],[i_0_137]) ).
cnf(i_0_195,plain,
( icext(uri_rdfs_Resource,X1)
| ~ ir(X1) ),
inference(split_conjunct,[status(thm)],[i_0_138]) ).
cnf(i_0_196,plain,
( icext(uri_owl_Thing,X1)
| ~ ir(X1) ),
inference(split_conjunct,[status(thm)],[i_0_139]) ).
fof(i_0_197,plain,
! [X263] :
( ~ ioxp(X263)
| ip(X263) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[owl_parts_ioxp_cond_set])]) ).
fof(i_0_198,plain,
! [X258] :
( ~ iodp(X258)
| ip(X258) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[owl_parts_iodp_cond_set])]) ).
fof(i_0_199,plain,
! [X253] :
( ~ ioap(X253)
| ip(X253) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[owl_parts_ioap_cond_set])]) ).
fof(i_0_200,plain,
! [X248] :
( ~ idc(X248)
| ic(X248) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[owl_parts_idc_cond_set])]) ).
cnf(i_0_201,plain,
( iext(uri_owl_intersectionOf,X1,X2)
| ~ icext(X1,esk4_7(X1,X2,X3,X4,X5,X6,X7))
| ~ icext(X3,esk4_7(X1,X2,X3,X4,X5,X6,X7))
| ~ icext(X5,esk4_7(X1,X2,X3,X4,X5,X6,X7))
| ~ icext(X7,esk4_7(X1,X2,X3,X4,X5,X6,X7))
| ~ ic(X1)
| ~ ic(X3)
| ~ ic(X5)
| ~ ic(X7)
| ~ iext(uri_rdf_first,X2,X3)
| ~ iext(uri_rdf_rest,X2,X4)
| ~ iext(uri_rdf_first,X4,X5)
| ~ iext(uri_rdf_rest,X4,X6)
| ~ iext(uri_rdf_first,X6,X7)
| ~ iext(uri_rdf_rest,X6,uri_rdf_nil) ),
inference(split_conjunct,[status(thm)],[i_0_140]),
[final] ).
cnf(i_0_202,plain,
( icext(X1,esk8_7(X1,X2,X3,X4,X5,X6,X7))
| icext(X3,esk8_7(X1,X2,X3,X4,X5,X6,X7))
| icext(X5,esk8_7(X1,X2,X3,X4,X5,X6,X7))
| icext(X7,esk8_7(X1,X2,X3,X4,X5,X6,X7))
| iext(uri_owl_unionOf,X1,X2)
| ~ ic(X1)
| ~ ic(X3)
| ~ ic(X5)
| ~ ic(X7)
| ~ iext(uri_rdf_first,X2,X3)
| ~ iext(uri_rdf_rest,X2,X4)
| ~ iext(uri_rdf_first,X4,X5)
| ~ iext(uri_rdf_rest,X4,X6)
| ~ iext(uri_rdf_first,X6,X7)
| ~ iext(uri_rdf_rest,X6,uri_rdf_nil) ),
inference(split_conjunct,[status(thm)],[i_0_141]),
[final] ).
cnf(i_0_203,plain,
( iext(uri_owl_unionOf,X2,X3)
| ~ icext(X1,esk8_7(X2,X3,X4,X5,X6,X7,X1))
| ~ icext(X2,esk8_7(X2,X3,X4,X5,X6,X7,X1))
| ~ ic(X2)
| ~ ic(X4)
| ~ ic(X6)
| ~ ic(X1)
| ~ iext(uri_rdf_first,X3,X4)
| ~ iext(uri_rdf_rest,X3,X5)
| ~ iext(uri_rdf_first,X5,X6)
| ~ iext(uri_rdf_rest,X5,X7)
| ~ iext(uri_rdf_first,X7,X1)
| ~ iext(uri_rdf_rest,X7,uri_rdf_nil) ),
inference(split_conjunct,[status(thm)],[i_0_141]),
[final] ).
cnf(i_0_204,plain,
( iext(uri_owl_unionOf,X2,X3)
| ~ icext(X1,esk8_7(X2,X3,X4,X5,X1,X6,X7))
| ~ icext(X2,esk8_7(X2,X3,X4,X5,X1,X6,X7))
| ~ ic(X2)
| ~ ic(X4)
| ~ ic(X1)
| ~ ic(X7)
| ~ iext(uri_rdf_first,X3,X4)
| ~ iext(uri_rdf_rest,X3,X5)
| ~ iext(uri_rdf_first,X5,X1)
| ~ iext(uri_rdf_rest,X5,X6)
| ~ iext(uri_rdf_first,X6,X7)
| ~ iext(uri_rdf_rest,X6,uri_rdf_nil) ),
inference(split_conjunct,[status(thm)],[i_0_141]),
[final] ).
cnf(i_0_205,plain,
( iext(uri_owl_unionOf,X2,X3)
| ~ icext(X1,esk8_7(X2,X3,X1,X4,X5,X6,X7))
| ~ icext(X2,esk8_7(X2,X3,X1,X4,X5,X6,X7))
| ~ ic(X2)
| ~ ic(X1)
| ~ ic(X5)
| ~ ic(X7)
| ~ iext(uri_rdf_first,X3,X1)
| ~ iext(uri_rdf_rest,X3,X4)
| ~ iext(uri_rdf_first,X4,X5)
| ~ iext(uri_rdf_rest,X4,X6)
| ~ iext(uri_rdf_first,X6,X7)
| ~ iext(uri_rdf_rest,X6,uri_rdf_nil) ),
inference(split_conjunct,[status(thm)],[i_0_141]),
[final] ).
cnf(i_0_206,plain,
( icext(X1,esk4_7(X2,X3,X1,X4,X5,X6,X7))
| icext(X2,esk4_7(X2,X3,X1,X4,X5,X6,X7))
| iext(uri_owl_intersectionOf,X2,X3)
| ~ ic(X2)
| ~ ic(X1)
| ~ ic(X5)
| ~ ic(X7)
| ~ iext(uri_rdf_first,X3,X1)
| ~ iext(uri_rdf_rest,X3,X4)
| ~ iext(uri_rdf_first,X4,X5)
| ~ iext(uri_rdf_rest,X4,X6)
| ~ iext(uri_rdf_first,X6,X7)
| ~ iext(uri_rdf_rest,X6,uri_rdf_nil) ),
inference(split_conjunct,[status(thm)],[i_0_140]),
[final] ).
cnf(i_0_207,plain,
( icext(X1,esk4_7(X2,X3,X4,X5,X1,X6,X7))
| icext(X2,esk4_7(X2,X3,X4,X5,X1,X6,X7))
| iext(uri_owl_intersectionOf,X2,X3)
| ~ ic(X2)
| ~ ic(X4)
| ~ ic(X1)
| ~ ic(X7)
| ~ iext(uri_rdf_first,X3,X4)
| ~ iext(uri_rdf_rest,X3,X5)
| ~ iext(uri_rdf_first,X5,X1)
| ~ iext(uri_rdf_rest,X5,X6)
| ~ iext(uri_rdf_first,X6,X7)
| ~ iext(uri_rdf_rest,X6,uri_rdf_nil) ),
inference(split_conjunct,[status(thm)],[i_0_140]),
[final] ).
cnf(i_0_208,plain,
( icext(X1,esk4_7(X2,X3,X4,X5,X6,X7,X1))
| icext(X2,esk4_7(X2,X3,X4,X5,X6,X7,X1))
| iext(uri_owl_intersectionOf,X2,X3)
| ~ ic(X2)
| ~ ic(X4)
| ~ ic(X6)
| ~ ic(X1)
| ~ iext(uri_rdf_first,X3,X4)
| ~ iext(uri_rdf_rest,X3,X5)
| ~ iext(uri_rdf_first,X5,X6)
| ~ iext(uri_rdf_rest,X5,X7)
| ~ iext(uri_rdf_first,X7,X1)
| ~ iext(uri_rdf_rest,X7,uri_rdf_nil) ),
inference(split_conjunct,[status(thm)],[i_0_140]),
[final] ).
cnf(i_0_209,plain,
( iext(uri_owl_intersectionOf,X1,X2)
| ~ icext(X1,esk3_5(X1,X2,X3,X4,X5))
| ~ icext(X3,esk3_5(X1,X2,X3,X4,X5))
| ~ icext(X5,esk3_5(X1,X2,X3,X4,X5))
| ~ ic(X1)
| ~ ic(X3)
| ~ ic(X5)
| ~ iext(uri_rdf_first,X2,X3)
| ~ iext(uri_rdf_rest,X2,X4)
| ~ iext(uri_rdf_first,X4,X5)
| ~ iext(uri_rdf_rest,X4,uri_rdf_nil) ),
inference(split_conjunct,[status(thm)],[i_0_142]),
[final] ).
cnf(i_0_210,plain,
( iext(uri_owl_unionOf,X2,X3)
| ~ icext(X1,esk7_5(X2,X3,X4,X5,X1))
| ~ icext(X2,esk7_5(X2,X3,X4,X5,X1))
| ~ ic(X2)
| ~ ic(X4)
| ~ ic(X1)
| ~ iext(uri_rdf_first,X3,X4)
| ~ iext(uri_rdf_rest,X3,X5)
| ~ iext(uri_rdf_first,X5,X1)
| ~ iext(uri_rdf_rest,X5,uri_rdf_nil) ),
inference(split_conjunct,[status(thm)],[i_0_143]),
[final] ).
cnf(i_0_211,plain,
( iext(uri_owl_unionOf,X2,X3)
| ~ icext(X1,esk7_5(X2,X3,X1,X4,X5))
| ~ icext(X2,esk7_5(X2,X3,X1,X4,X5))
| ~ ic(X2)
| ~ ic(X1)
| ~ ic(X5)
| ~ iext(uri_rdf_first,X3,X1)
| ~ iext(uri_rdf_rest,X3,X4)
| ~ iext(uri_rdf_first,X4,X5)
| ~ iext(uri_rdf_rest,X4,uri_rdf_nil) ),
inference(split_conjunct,[status(thm)],[i_0_143]),
[final] ).
cnf(i_0_212,plain,
( icext(X1,esk7_5(X1,X2,X3,X4,X5))
| icext(X3,esk7_5(X1,X2,X3,X4,X5))
| icext(X5,esk7_5(X1,X2,X3,X4,X5))
| iext(uri_owl_unionOf,X1,X2)
| ~ ic(X1)
| ~ ic(X3)
| ~ ic(X5)
| ~ iext(uri_rdf_first,X2,X3)
| ~ iext(uri_rdf_rest,X2,X4)
| ~ iext(uri_rdf_first,X4,X5)
| ~ iext(uri_rdf_rest,X4,uri_rdf_nil) ),
inference(split_conjunct,[status(thm)],[i_0_143]),
[final] ).
cnf(i_0_213,plain,
( icext(X1,esk3_5(X2,X3,X1,X4,X5))
| icext(X2,esk3_5(X2,X3,X1,X4,X5))
| iext(uri_owl_intersectionOf,X2,X3)
| ~ ic(X2)
| ~ ic(X1)
| ~ ic(X5)
| ~ iext(uri_rdf_first,X3,X1)
| ~ iext(uri_rdf_rest,X3,X4)
| ~ iext(uri_rdf_first,X4,X5)
| ~ iext(uri_rdf_rest,X4,uri_rdf_nil) ),
inference(split_conjunct,[status(thm)],[i_0_142]),
[final] ).
cnf(i_0_214,plain,
( icext(X1,esk3_5(X2,X3,X4,X5,X1))
| icext(X2,esk3_5(X2,X3,X4,X5,X1))
| iext(uri_owl_intersectionOf,X2,X3)
| ~ ic(X2)
| ~ ic(X4)
| ~ ic(X1)
| ~ iext(uri_rdf_first,X3,X4)
| ~ iext(uri_rdf_rest,X3,X5)
| ~ iext(uri_rdf_first,X5,X1)
| ~ iext(uri_rdf_rest,X5,uri_rdf_nil) ),
inference(split_conjunct,[status(thm)],[i_0_142]),
[final] ).
cnf(i_0_215,plain,
( icext(X2,X4)
| ~ icext(X1,esk17_4(X2,X3,X1,X4))
| ~ iext(uri_owl_allValuesFrom,X2,X1)
| ~ iext(uri_owl_onProperty,X2,X3) ),
inference(split_conjunct,[status(thm)],[i_0_144]),
[final] ).
cnf(i_0_216,plain,
( iext(X1,X2,esk18_4(X3,X1,X4,X2))
| ~ icext(X3,X2)
| ~ iext(uri_owl_someValuesFrom,X3,X4)
| ~ iext(uri_owl_onProperty,X3,X1) ),
inference(split_conjunct,[status(thm)],[i_0_145]),
[final] ).
cnf(i_0_217,plain,
( iext(X1,X2,esk17_4(X3,X1,X4,X2))
| icext(X3,X2)
| ~ iext(uri_owl_allValuesFrom,X3,X4)
| ~ iext(uri_owl_onProperty,X3,X1) ),
inference(split_conjunct,[status(thm)],[i_0_144]),
[final] ).
cnf(i_0_218,plain,
( icext(X1,esk18_4(X2,X3,X1,X4))
| ~ icext(X2,X4)
| ~ iext(uri_owl_someValuesFrom,X2,X1)
| ~ iext(uri_owl_onProperty,X2,X3) ),
inference(split_conjunct,[status(thm)],[i_0_145]),
[final] ).
cnf(i_0_219,plain,
( icext(X5,X2)
| ~ icext(X1,X2)
| ~ icext(X3,X2)
| ~ icext(X4,X2)
| ~ iext(uri_owl_intersectionOf,X5,X6)
| ~ iext(uri_rdf_first,X6,X1)
| ~ iext(uri_rdf_rest,X6,X7)
| ~ iext(uri_rdf_first,X7,X3)
| ~ iext(uri_rdf_rest,X7,X8)
| ~ iext(uri_rdf_first,X8,X4)
| ~ iext(uri_rdf_rest,X8,uri_rdf_nil) ),
inference(split_conjunct,[status(thm)],[i_0_140]),
[final] ).
cnf(i_0_220,plain,
( icext(X3,X2)
| icext(X4,X2)
| icext(X5,X2)
| ~ icext(X1,X2)
| ~ iext(uri_owl_unionOf,X1,X6)
| ~ iext(uri_rdf_first,X6,X3)
| ~ iext(uri_rdf_rest,X6,X7)
| ~ iext(uri_rdf_first,X7,X4)
| ~ iext(uri_rdf_rest,X7,X8)
| ~ iext(uri_rdf_first,X8,X5)
| ~ iext(uri_rdf_rest,X8,uri_rdf_nil) ),
inference(split_conjunct,[status(thm)],[i_0_141]),
[final] ).
cnf(i_0_221,plain,
( icext(X1,X2)
| ~ icext(X3,X2)
| ~ iext(uri_owl_intersectionOf,X3,X4)
| ~ iext(uri_rdf_first,X4,X1)
| ~ iext(uri_rdf_rest,X4,X5)
| ~ iext(uri_rdf_first,X5,X6)
| ~ iext(uri_rdf_rest,X5,X7)
| ~ iext(uri_rdf_first,X7,X8)
| ~ iext(uri_rdf_rest,X7,uri_rdf_nil) ),
inference(split_conjunct,[status(thm)],[i_0_140]),
[final] ).
cnf(i_0_222,plain,
( icext(X1,X2)
| ~ icext(X3,X2)
| ~ iext(uri_owl_intersectionOf,X3,X4)
| ~ iext(uri_rdf_first,X4,X5)
| ~ iext(uri_rdf_rest,X4,X6)
| ~ iext(uri_rdf_first,X6,X1)
| ~ iext(uri_rdf_rest,X6,X7)
| ~ iext(uri_rdf_first,X7,X8)
| ~ iext(uri_rdf_rest,X7,uri_rdf_nil) ),
inference(split_conjunct,[status(thm)],[i_0_140]),
[final] ).
cnf(i_0_223,plain,
( icext(X1,X2)
| ~ icext(X3,X2)
| ~ iext(uri_owl_intersectionOf,X3,X4)
| ~ iext(uri_rdf_first,X4,X5)
| ~ iext(uri_rdf_rest,X4,X6)
| ~ iext(uri_rdf_first,X6,X7)
| ~ iext(uri_rdf_rest,X6,X8)
| ~ iext(uri_rdf_first,X8,X1)
| ~ iext(uri_rdf_rest,X8,uri_rdf_nil) ),
inference(split_conjunct,[status(thm)],[i_0_140]),
[final] ).
cnf(i_0_224,plain,
( icext(X3,X2)
| ~ icext(X1,X2)
| ~ iext(uri_owl_unionOf,X3,X4)
| ~ iext(uri_rdf_first,X4,X1)
| ~ iext(uri_rdf_rest,X4,X5)
| ~ iext(uri_rdf_first,X5,X6)
| ~ iext(uri_rdf_rest,X5,X7)
| ~ iext(uri_rdf_first,X7,X8)
| ~ iext(uri_rdf_rest,X7,uri_rdf_nil) ),
inference(split_conjunct,[status(thm)],[i_0_141]),
[final] ).
cnf(i_0_225,plain,
( icext(X3,X2)
| ~ icext(X1,X2)
| ~ iext(uri_owl_unionOf,X3,X4)
| ~ iext(uri_rdf_first,X4,X5)
| ~ iext(uri_rdf_rest,X4,X6)
| ~ iext(uri_rdf_first,X6,X1)
| ~ iext(uri_rdf_rest,X6,X7)
| ~ iext(uri_rdf_first,X7,X8)
| ~ iext(uri_rdf_rest,X7,uri_rdf_nil) ),
inference(split_conjunct,[status(thm)],[i_0_141]),
[final] ).
cnf(i_0_226,plain,
( icext(X3,X2)
| ~ icext(X1,X2)
| ~ iext(uri_owl_unionOf,X3,X4)
| ~ iext(uri_rdf_first,X4,X5)
| ~ iext(uri_rdf_rest,X4,X6)
| ~ iext(uri_rdf_first,X6,X7)
| ~ iext(uri_rdf_rest,X6,X8)
| ~ iext(uri_rdf_first,X8,X1)
| ~ iext(uri_rdf_rest,X8,uri_rdf_nil) ),
inference(split_conjunct,[status(thm)],[i_0_141]),
[final] ).
cnf(i_0_227,plain,
( iext(uri_owl_unionOf,X1,X2)
| ~ icext(X1,esk6_3(X1,X2,X3))
| ~ icext(X3,esk6_3(X1,X2,X3))
| ~ ic(X1)
| ~ ic(X3)
| ~ iext(uri_rdf_first,X2,X3)
| ~ iext(uri_rdf_rest,X2,uri_rdf_nil) ),
inference(split_conjunct,[status(thm)],[i_0_146]),
[final] ).
cnf(i_0_228,plain,
( iext(uri_owl_intersectionOf,X1,X2)
| ~ icext(X1,esk2_3(X1,X2,X3))
| ~ icext(X3,esk2_3(X1,X2,X3))
| ~ ic(X1)
| ~ ic(X3)
| ~ iext(uri_rdf_first,X2,X3)
| ~ iext(uri_rdf_rest,X2,uri_rdf_nil) ),
inference(split_conjunct,[status(thm)],[i_0_147]),
[final] ).
cnf(i_0_229,plain,
( ic(X1)
| ~ iext(uri_owl_unionOf,X1,X2)
| ~ iext(uri_rdf_first,X2,X3)
| ~ iext(uri_rdf_rest,X2,X4)
| ~ iext(uri_rdf_first,X4,X5)
| ~ iext(uri_rdf_rest,X4,X6)
| ~ iext(uri_rdf_first,X6,X7)
| ~ iext(uri_rdf_rest,X6,uri_rdf_nil) ),
inference(split_conjunct,[status(thm)],[i_0_141]),
[final] ).
cnf(i_0_230,plain,
( ic(X1)
| ~ iext(uri_owl_unionOf,X2,X3)
| ~ iext(uri_rdf_first,X3,X1)
| ~ iext(uri_rdf_rest,X3,X4)
| ~ iext(uri_rdf_first,X4,X5)
| ~ iext(uri_rdf_rest,X4,X6)
| ~ iext(uri_rdf_first,X6,X7)
| ~ iext(uri_rdf_rest,X6,uri_rdf_nil) ),
inference(split_conjunct,[status(thm)],[i_0_141]),
[final] ).
cnf(i_0_231,plain,
( ic(X1)
| ~ iext(uri_owl_unionOf,X2,X3)
| ~ iext(uri_rdf_first,X3,X4)
| ~ iext(uri_rdf_rest,X3,X5)
| ~ iext(uri_rdf_first,X5,X1)
| ~ iext(uri_rdf_rest,X5,X6)
| ~ iext(uri_rdf_first,X6,X7)
| ~ iext(uri_rdf_rest,X6,uri_rdf_nil) ),
inference(split_conjunct,[status(thm)],[i_0_141]),
[final] ).
cnf(i_0_232,plain,
( ic(X1)
| ~ iext(uri_owl_unionOf,X2,X3)
| ~ iext(uri_rdf_first,X3,X4)
| ~ iext(uri_rdf_rest,X3,X5)
| ~ iext(uri_rdf_first,X5,X6)
| ~ iext(uri_rdf_rest,X5,X7)
| ~ iext(uri_rdf_first,X7,X1)
| ~ iext(uri_rdf_rest,X7,uri_rdf_nil) ),
inference(split_conjunct,[status(thm)],[i_0_141]),
[final] ).
cnf(i_0_233,plain,
( ic(X1)
| ~ iext(uri_owl_intersectionOf,X1,X2)
| ~ iext(uri_rdf_first,X2,X3)
| ~ iext(uri_rdf_rest,X2,X4)
| ~ iext(uri_rdf_first,X4,X5)
| ~ iext(uri_rdf_rest,X4,X6)
| ~ iext(uri_rdf_first,X6,X7)
| ~ iext(uri_rdf_rest,X6,uri_rdf_nil) ),
inference(split_conjunct,[status(thm)],[i_0_140]),
[final] ).
cnf(i_0_234,plain,
( ic(X1)
| ~ iext(uri_owl_intersectionOf,X2,X3)
| ~ iext(uri_rdf_first,X3,X1)
| ~ iext(uri_rdf_rest,X3,X4)
| ~ iext(uri_rdf_first,X4,X5)
| ~ iext(uri_rdf_rest,X4,X6)
| ~ iext(uri_rdf_first,X6,X7)
| ~ iext(uri_rdf_rest,X6,uri_rdf_nil) ),
inference(split_conjunct,[status(thm)],[i_0_140]),
[final] ).
cnf(i_0_235,plain,
( ic(X1)
| ~ iext(uri_owl_intersectionOf,X2,X3)
| ~ iext(uri_rdf_first,X3,X4)
| ~ iext(uri_rdf_rest,X3,X5)
| ~ iext(uri_rdf_first,X5,X1)
| ~ iext(uri_rdf_rest,X5,X6)
| ~ iext(uri_rdf_first,X6,X7)
| ~ iext(uri_rdf_rest,X6,uri_rdf_nil) ),
inference(split_conjunct,[status(thm)],[i_0_140]),
[final] ).
cnf(i_0_236,plain,
( ic(X1)
| ~ iext(uri_owl_intersectionOf,X2,X3)
| ~ iext(uri_rdf_first,X3,X4)
| ~ iext(uri_rdf_rest,X3,X5)
| ~ iext(uri_rdf_first,X5,X6)
| ~ iext(uri_rdf_rest,X5,X7)
| ~ iext(uri_rdf_first,X7,X1)
| ~ iext(uri_rdf_rest,X7,uri_rdf_nil) ),
inference(split_conjunct,[status(thm)],[i_0_140]),
[final] ).
cnf(i_0_237,plain,
( icext(X4,X2)
| ~ icext(X1,X2)
| ~ icext(X3,X2)
| ~ iext(uri_owl_intersectionOf,X4,X5)
| ~ iext(uri_rdf_first,X5,X1)
| ~ iext(uri_rdf_rest,X5,X6)
| ~ iext(uri_rdf_first,X6,X3)
| ~ iext(uri_rdf_rest,X6,uri_rdf_nil) ),
inference(split_conjunct,[status(thm)],[i_0_142]),
[final] ).
cnf(i_0_238,plain,
( icext(X1,esk6_3(X1,X2,X3))
| icext(X3,esk6_3(X1,X2,X3))
| iext(uri_owl_unionOf,X1,X2)
| ~ ic(X1)
| ~ ic(X3)
| ~ iext(uri_rdf_first,X2,X3)
| ~ iext(uri_rdf_rest,X2,uri_rdf_nil) ),
inference(split_conjunct,[status(thm)],[i_0_146]),
[final] ).
cnf(i_0_239,plain,
( icext(X1,esk2_3(X1,X2,X3))
| icext(X3,esk2_3(X1,X2,X3))
| iext(uri_owl_intersectionOf,X1,X2)
| ~ ic(X1)
| ~ ic(X3)
| ~ iext(uri_rdf_first,X2,X3)
| ~ iext(uri_rdf_rest,X2,uri_rdf_nil) ),
inference(split_conjunct,[status(thm)],[i_0_147]),
[final] ).
cnf(i_0_240,plain,
( icext(X3,X2)
| icext(X4,X2)
| ~ icext(X1,X2)
| ~ iext(uri_owl_unionOf,X1,X5)
| ~ iext(uri_rdf_first,X5,X3)
| ~ iext(uri_rdf_rest,X5,X6)
| ~ iext(uri_rdf_first,X6,X4)
| ~ iext(uri_rdf_rest,X6,uri_rdf_nil) ),
inference(split_conjunct,[status(thm)],[i_0_143]),
[final] ).
cnf(i_0_241,plain,
( icext(X1,X2)
| ~ icext(X3,X2)
| ~ iext(uri_owl_intersectionOf,X3,X4)
| ~ iext(uri_rdf_first,X4,X1)
| ~ iext(uri_rdf_rest,X4,X5)
| ~ iext(uri_rdf_first,X5,X6)
| ~ iext(uri_rdf_rest,X5,uri_rdf_nil) ),
inference(split_conjunct,[status(thm)],[i_0_142]),
[final] ).
cnf(i_0_242,plain,
( icext(X1,X2)
| ~ icext(X3,X2)
| ~ iext(uri_owl_intersectionOf,X3,X4)
| ~ iext(uri_rdf_first,X4,X5)
| ~ iext(uri_rdf_rest,X4,X6)
| ~ iext(uri_rdf_first,X6,X1)
| ~ iext(uri_rdf_rest,X6,uri_rdf_nil) ),
inference(split_conjunct,[status(thm)],[i_0_142]),
[final] ).
cnf(i_0_243,plain,
( icext(X3,X2)
| ~ icext(X1,X2)
| ~ iext(uri_owl_unionOf,X3,X4)
| ~ iext(uri_rdf_first,X4,X1)
| ~ iext(uri_rdf_rest,X4,X5)
| ~ iext(uri_rdf_first,X5,X6)
| ~ iext(uri_rdf_rest,X5,uri_rdf_nil) ),
inference(split_conjunct,[status(thm)],[i_0_143]),
[final] ).
cnf(i_0_244,plain,
( icext(X3,X2)
| ~ icext(X1,X2)
| ~ iext(uri_owl_unionOf,X3,X4)
| ~ iext(uri_rdf_first,X4,X5)
| ~ iext(uri_rdf_rest,X4,X6)
| ~ iext(uri_rdf_first,X6,X1)
| ~ iext(uri_rdf_rest,X6,uri_rdf_nil) ),
inference(split_conjunct,[status(thm)],[i_0_143]),
[final] ).
cnf(i_0_245,plain,
( ic(X1)
| ~ iext(uri_owl_unionOf,X1,X2)
| ~ iext(uri_rdf_first,X2,X3)
| ~ iext(uri_rdf_rest,X2,X4)
| ~ iext(uri_rdf_first,X4,X5)
| ~ iext(uri_rdf_rest,X4,uri_rdf_nil) ),
inference(split_conjunct,[status(thm)],[i_0_143]),
[final] ).
cnf(i_0_246,plain,
( ic(X1)
| ~ iext(uri_owl_unionOf,X2,X3)
| ~ iext(uri_rdf_first,X3,X1)
| ~ iext(uri_rdf_rest,X3,X4)
| ~ iext(uri_rdf_first,X4,X5)
| ~ iext(uri_rdf_rest,X4,uri_rdf_nil) ),
inference(split_conjunct,[status(thm)],[i_0_143]),
[final] ).
cnf(i_0_247,plain,
( ic(X1)
| ~ iext(uri_owl_unionOf,X2,X3)
| ~ iext(uri_rdf_first,X3,X4)
| ~ iext(uri_rdf_rest,X3,X5)
| ~ iext(uri_rdf_first,X5,X1)
| ~ iext(uri_rdf_rest,X5,uri_rdf_nil) ),
inference(split_conjunct,[status(thm)],[i_0_143]),
[final] ).
cnf(i_0_248,plain,
( ic(X1)
| ~ iext(uri_owl_intersectionOf,X1,X2)
| ~ iext(uri_rdf_first,X2,X3)
| ~ iext(uri_rdf_rest,X2,X4)
| ~ iext(uri_rdf_first,X4,X5)
| ~ iext(uri_rdf_rest,X4,uri_rdf_nil) ),
inference(split_conjunct,[status(thm)],[i_0_142]),
[final] ).
cnf(i_0_249,plain,
( ic(X1)
| ~ iext(uri_owl_intersectionOf,X2,X3)
| ~ iext(uri_rdf_first,X3,X1)
| ~ iext(uri_rdf_rest,X3,X4)
| ~ iext(uri_rdf_first,X4,X5)
| ~ iext(uri_rdf_rest,X4,uri_rdf_nil) ),
inference(split_conjunct,[status(thm)],[i_0_142]),
[final] ).
cnf(i_0_250,plain,
( ic(X1)
| ~ iext(uri_owl_intersectionOf,X2,X3)
| ~ iext(uri_rdf_first,X3,X4)
| ~ iext(uri_rdf_rest,X3,X5)
| ~ iext(uri_rdf_first,X5,X1)
| ~ iext(uri_rdf_rest,X5,uri_rdf_nil) ),
inference(split_conjunct,[status(thm)],[i_0_142]),
[final] ).
cnf(i_0_251,plain,
( icext(X5,X2)
| ~ iext(X1,X2,X3)
| ~ icext(X4,X3)
| ~ iext(uri_owl_someValuesFrom,X5,X4)
| ~ iext(uri_owl_onProperty,X5,X1) ),
inference(split_conjunct,[status(thm)],[i_0_145]),
[final] ).
cnf(i_0_252,plain,
( icext(X5,X4)
| ~ icext(X1,X2)
| ~ iext(X3,X2,X4)
| ~ iext(uri_owl_allValuesFrom,X1,X5)
| ~ iext(uri_owl_onProperty,X1,X3) ),
inference(split_conjunct,[status(thm)],[i_0_144]),
[final] ).
cnf(i_0_253,plain,
( icext(X3,X2)
| ~ icext(X1,X2)
| ~ iext(uri_owl_unionOf,X3,X4)
| ~ iext(uri_rdf_first,X4,X1)
| ~ iext(uri_rdf_rest,X4,uri_rdf_nil) ),
inference(split_conjunct,[status(thm)],[i_0_146]),
[final] ).
cnf(i_0_254,plain,
( icext(X3,X2)
| ~ icext(X1,X2)
| ~ iext(uri_owl_unionOf,X1,X4)
| ~ iext(uri_rdf_first,X4,X3)
| ~ iext(uri_rdf_rest,X4,uri_rdf_nil) ),
inference(split_conjunct,[status(thm)],[i_0_146]),
[final] ).
cnf(i_0_255,plain,
( icext(X3,X2)
| ~ icext(X1,X2)
| ~ iext(uri_owl_intersectionOf,X1,X4)
| ~ iext(uri_rdf_first,X4,X3)
| ~ iext(uri_rdf_rest,X4,uri_rdf_nil) ),
inference(split_conjunct,[status(thm)],[i_0_147]),
[final] ).
cnf(i_0_256,plain,
( icext(X3,X2)
| ~ icext(X1,X2)
| ~ iext(uri_owl_intersectionOf,X3,X4)
| ~ iext(uri_rdf_first,X4,X1)
| ~ iext(uri_rdf_rest,X4,uri_rdf_nil) ),
inference(split_conjunct,[status(thm)],[i_0_147]),
[final] ).
cnf(i_0_257,plain,
( icext(X4,X2)
| ~ iext(X1,X2,X3)
| ~ iext(uri_owl_hasValue,X4,X3)
| ~ iext(uri_owl_onProperty,X4,X1) ),
inference(split_conjunct,[status(thm)],[i_0_148]),
[final] ).
cnf(i_0_258,plain,
( ic(X1)
| ~ iext(uri_owl_unionOf,X1,X2)
| ~ iext(uri_rdf_first,X2,X3)
| ~ iext(uri_rdf_rest,X2,uri_rdf_nil) ),
inference(split_conjunct,[status(thm)],[i_0_146]),
[final] ).
cnf(i_0_259,plain,
( ic(X1)
| ~ iext(uri_owl_unionOf,X2,X3)
| ~ iext(uri_rdf_first,X3,X1)
| ~ iext(uri_rdf_rest,X3,uri_rdf_nil) ),
inference(split_conjunct,[status(thm)],[i_0_146]),
[final] ).
cnf(i_0_260,plain,
( ic(X1)
| ~ iext(uri_owl_intersectionOf,X1,X2)
| ~ iext(uri_rdf_first,X2,X3)
| ~ iext(uri_rdf_rest,X2,uri_rdf_nil) ),
inference(split_conjunct,[status(thm)],[i_0_147]),
[final] ).
cnf(i_0_261,plain,
( ic(X1)
| ~ iext(uri_owl_intersectionOf,X2,X3)
| ~ iext(uri_rdf_first,X3,X1)
| ~ iext(uri_rdf_rest,X3,uri_rdf_nil) ),
inference(split_conjunct,[status(thm)],[i_0_147]),
[final] ).
cnf(i_0_262,plain,
( iext(X3,X2,X4)
| ~ icext(X1,X2)
| ~ iext(uri_owl_hasValue,X1,X4)
| ~ iext(uri_owl_onProperty,X1,X3) ),
inference(split_conjunct,[status(thm)],[i_0_148]),
[final] ).
cnf(i_0_263,plain,
( iext(uri_rdfs_subPropertyOf,X2,X1)
| ~ iext(X1,esk15_2(X2,X1),esk16_2(X2,X1))
| ~ ip(X2)
| ~ ip(X1) ),
inference(split_conjunct,[status(thm)],[i_0_149]),
[final] ).
cnf(i_0_264,plain,
( iext(X4,X2,X3)
| ~ iext(X1,X2,X3)
| ~ iext(uri_rdfs_subPropertyOf,X1,X4) ),
inference(split_conjunct,[status(thm)],[i_0_150]),
[final] ).
cnf(i_0_265,plain,
( iext(X4,X2,X3)
| ~ iext(X1,X2,X3)
| ~ iext(uri_rdfs_subPropertyOf,X1,X4) ),
inference(split_conjunct,[status(thm)],[i_0_149]),
[final] ).
cnf(i_0_266,plain,
( iext(uri_rdfs_subPropertyOf,X1,X3)
| ~ iext(uri_rdfs_subPropertyOf,X1,X2)
| ~ iext(uri_rdfs_subPropertyOf,X2,X3) ),
inference(split_conjunct,[status(thm)],[i_0_151]),
[final] ).
cnf(i_0_267,plain,
( iext(uri_rdfs_subClassOf,X1,X3)
| ~ iext(uri_rdfs_subClassOf,X1,X2)
| ~ iext(uri_rdfs_subClassOf,X2,X3) ),
inference(split_conjunct,[status(thm)],[i_0_152]),
[final] ).
cnf(i_0_268,plain,
( icext(X2,X3)
| ~ iext(uri_rdfs_domain,X1,X2)
| ~ iext(X1,X3,X4) ),
inference(split_conjunct,[status(thm)],[i_0_153]),
[final] ).
cnf(i_0_269,plain,
( icext(X2,X4)
| ~ iext(uri_rdfs_range,X1,X2)
| ~ iext(X1,X3,X4) ),
inference(split_conjunct,[status(thm)],[i_0_154]),
[final] ).
cnf(i_0_270,plain,
( icext(X4,X2)
| ~ iext(X1,X2,X3)
| ~ iext(uri_rdfs_domain,X1,X4) ),
inference(split_conjunct,[status(thm)],[i_0_155]),
[final] ).
cnf(i_0_271,plain,
( icext(X4,X3)
| ~ iext(X1,X2,X3)
| ~ iext(uri_rdfs_range,X1,X4) ),
inference(split_conjunct,[status(thm)],[i_0_156]),
[final] ).
cnf(i_0_272,plain,
( iext(X1,esk15_2(X1,X2),esk16_2(X1,X2))
| iext(uri_rdfs_subPropertyOf,X1,X2)
| ~ ip(X1)
| ~ ip(X2) ),
inference(split_conjunct,[status(thm)],[i_0_149]),
[final] ).
cnf(i_0_273,plain,
( iext(X1,esk12_2(X1,X2),esk13_2(X1,X2))
| iext(uri_rdfs_range,X1,X2)
| ~ ip(X1)
| ~ ip(X2) ),
inference(split_conjunct,[status(thm)],[i_0_156]),
[final] ).
cnf(i_0_274,plain,
( iext(X1,esk10_2(X1,X2),esk11_2(X1,X2))
| iext(uri_rdfs_domain,X1,X2)
| ~ ip(X1)
| ~ ic(X2) ),
inference(split_conjunct,[status(thm)],[i_0_155]),
[final] ).
cnf(i_0_275,negated_conjecture,
( ~ iext(uri_rdf_type,uri_ex_r,uri_owl_Restriction)
| ~ iext(uri_owl_onProperty,uri_ex_r,uri_ex_p) ),
inference(split_conjunct,[status(thm)],[i_0_157]),
[final] ).
cnf(i_0_276,plain,
( iext(uri_rdfs_subClassOf,X2,X1)
| ~ icext(X1,esk14_2(X2,X1))
| ~ ic(X2)
| ~ ic(X1) ),
inference(split_conjunct,[status(thm)],[i_0_158]),
[final] ).
cnf(i_0_277,plain,
( iext(uri_rdfs_range,X2,X1)
| ~ icext(X1,esk13_2(X2,X1))
| ~ ip(X2)
| ~ ip(X1) ),
inference(split_conjunct,[status(thm)],[i_0_156]),
[final] ).
cnf(i_0_278,plain,
( iext(uri_rdfs_domain,X2,X1)
| ~ icext(X1,esk10_2(X2,X1))
| ~ ip(X2)
| ~ ic(X1) ),
inference(split_conjunct,[status(thm)],[i_0_155]),
[final] ).
cnf(i_0_279,plain,
( ~ icext(X1,X2)
| ~ icext(X3,X2)
| ~ iext(uri_owl_complementOf,X1,X3) ),
inference(split_conjunct,[status(thm)],[i_0_159]),
[final] ).
cnf(i_0_280,plain,
( icext(X3,X2)
| ~ icext(X1,X2)
| ~ iext(uri_rdfs_subClassOf,X1,X3) ),
inference(split_conjunct,[status(thm)],[i_0_160]),
[final] ).
cnf(i_0_281,plain,
( icext(X3,X2)
| ~ icext(X1,X2)
| ~ iext(uri_rdfs_subClassOf,X1,X3) ),
inference(split_conjunct,[status(thm)],[i_0_158]),
[final] ).
cnf(i_0_282,plain,
( icext(X1,X2)
| icext(X3,X2)
| ~ iext(uri_owl_complementOf,X3,X1) ),
inference(split_conjunct,[status(thm)],[i_0_159]),
[final] ).
cnf(i_0_283,plain,
( icext(X1,esk14_2(X1,X2))
| iext(uri_rdfs_subClassOf,X1,X2)
| ~ ic(X1)
| ~ ic(X2) ),
inference(split_conjunct,[status(thm)],[i_0_158]),
[final] ).
cnf(i_0_284,plain,
( ~ icext(X1,X2)
| ~ iext(uri_owl_unionOf,X1,uri_rdf_nil) ),
inference(split_conjunct,[status(thm)],[i_0_161]),
[final] ).
cnf(i_0_285,plain,
( icext(X2,X1)
| ~ iext(uri_rdf_type,X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_162]),
[final] ).
cnf(i_0_286,plain,
( ix(X1)
| ~ iext(X2,X1,X3)
| ~ ioxp(X2) ),
inference(split_conjunct,[status(thm)],[i_0_163]),
[final] ).
cnf(i_0_287,plain,
( ix(X1)
| ~ iext(X2,X3,X1)
| ~ ioxp(X2) ),
inference(split_conjunct,[status(thm)],[i_0_163]),
[final] ).
cnf(i_0_288,plain,
( lv(X1)
| ~ iext(X2,X3,X1)
| ~ iodp(X2) ),
inference(split_conjunct,[status(thm)],[i_0_164]),
[final] ).
cnf(i_0_289,plain,
( icext(uri_rdf_List,X1)
| ~ iext(uri_owl_unionOf,X2,X1) ),
inference(split_conjunct,[status(thm)],[i_0_165]),
[final] ).
cnf(i_0_290,plain,
( icext(uri_rdf_List,X1)
| ~ iext(uri_owl_intersectionOf,X2,X1) ),
inference(split_conjunct,[status(thm)],[i_0_166]),
[final] ).
cnf(i_0_291,plain,
( icext(uri_owl_Restriction,X1)
| ~ iext(uri_owl_someValuesFrom,X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_167]),
[final] ).
cnf(i_0_292,plain,
( icext(uri_owl_Restriction,X1)
| ~ iext(uri_owl_onProperty,X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_168]),
[final] ).
cnf(i_0_293,plain,
( icext(uri_owl_Restriction,X1)
| ~ iext(uri_owl_hasValue,X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_169]),
[final] ).
cnf(i_0_294,plain,
( icext(uri_owl_Restriction,X1)
| ~ iext(uri_owl_allValuesFrom,X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_170]),
[final] ).
cnf(i_0_295,plain,
( icext(X2,X1)
| ~ iext(uri_owl_intersectionOf,X2,uri_rdf_nil) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[i_0_171,c_0_172])]),
[final] ).
cnf(i_0_296,plain,
( iext(uri_owl_intersectionOf,X1,uri_rdf_nil)
| ~ ic(X1)
| ~ icext(X1,esk1_1(X1)) ),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[i_0_173,c_0_172])]),
[final] ).
cnf(i_0_297,plain,
( ip(X1)
| ~ iext(X1,X2,X3) ),
inference(split_conjunct,[status(thm)],[i_0_174]),
[final] ).
cnf(i_0_298,plain,
( ip(X1)
| ~ iext(uri_rdfs_subPropertyOf,X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_150]),
[final] ).
cnf(i_0_299,plain,
( ip(X1)
| ~ iext(uri_rdfs_subPropertyOf,X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_149]),
[final] ).
cnf(i_0_300,plain,
( ip(X1)
| ~ iext(uri_rdfs_subPropertyOf,X2,X1) ),
inference(split_conjunct,[status(thm)],[i_0_150]),
[final] ).
cnf(i_0_301,plain,
( ip(X1)
| ~ iext(uri_rdfs_subPropertyOf,X2,X1) ),
inference(split_conjunct,[status(thm)],[i_0_149]),
[final] ).
cnf(i_0_302,plain,
( ip(X1)
| ~ iext(uri_rdfs_range,X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_156]),
[final] ).
cnf(i_0_303,plain,
( ip(X1)
| ~ iext(uri_rdfs_range,X2,X1) ),
inference(split_conjunct,[status(thm)],[i_0_156]),
[final] ).
cnf(i_0_304,plain,
( ip(X1)
| ~ iext(uri_rdfs_domain,X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_155]),
[final] ).
cnf(i_0_305,plain,
( ip(X1)
| ~ iext(uri_owl_onProperty,X2,X1) ),
inference(split_conjunct,[status(thm)],[i_0_168]),
[final] ).
cnf(i_0_306,plain,
( ic(X1)
| ~ iext(uri_rdfs_subClassOf,X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_160]),
[final] ).
cnf(i_0_307,plain,
( ic(X1)
| ~ iext(uri_rdfs_subClassOf,X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_158]),
[final] ).
cnf(i_0_308,plain,
( ic(X1)
| ~ iext(uri_rdfs_subClassOf,X2,X1) ),
inference(split_conjunct,[status(thm)],[i_0_160]),
[final] ).
cnf(i_0_309,plain,
( ic(X1)
| ~ iext(uri_rdfs_subClassOf,X2,X1) ),
inference(split_conjunct,[status(thm)],[i_0_158]),
[final] ).
cnf(i_0_310,plain,
( ic(X1)
| ~ iext(uri_rdfs_domain,X2,X1) ),
inference(split_conjunct,[status(thm)],[i_0_155]),
[final] ).
cnf(i_0_311,plain,
( ic(X1)
| ~ iext(uri_owl_someValuesFrom,X2,X1) ),
inference(split_conjunct,[status(thm)],[i_0_167]),
[final] ).
cnf(i_0_312,plain,
( ic(X1)
| ~ iext(uri_owl_allValuesFrom,X2,X1) ),
inference(split_conjunct,[status(thm)],[i_0_170]),
[final] ).
cnf(i_0_313,plain,
( ic(X1)
| ~ iext(uri_owl_unionOf,X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_165]),
[final] ).
cnf(i_0_314,plain,
( ic(X1)
| ~ iext(uri_owl_intersectionOf,X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_166]),
[final] ).
cnf(i_0_315,plain,
( ic(X1)
| ~ iext(uri_owl_complementOf,X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_175]),
[final] ).
cnf(i_0_316,plain,
( ic(X1)
| ~ iext(uri_owl_complementOf,X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_159]),
[final] ).
cnf(i_0_317,plain,
( ic(X1)
| ~ iext(uri_owl_complementOf,X2,X1) ),
inference(split_conjunct,[status(thm)],[i_0_175]),
[final] ).
cnf(i_0_318,plain,
( ic(X1)
| ~ iext(uri_owl_complementOf,X2,X1) ),
inference(split_conjunct,[status(thm)],[i_0_159]),
[final] ).
cnf(i_0_319,plain,
( ix(X1)
| ~ iext(uri_rdf_type,X1,uri_owl_Ontology) ),
inference(split_conjunct,[status(thm)],[i_0_176]),
[final] ).
cnf(i_0_320,plain,
( ioxp(X1)
| ~ iext(uri_rdf_type,X1,uri_owl_OntologyProperty) ),
inference(split_conjunct,[status(thm)],[i_0_177]),
[final] ).
cnf(i_0_321,plain,
( iodp(X1)
| ~ iext(uri_rdf_type,X1,uri_owl_DatatypeProperty) ),
inference(split_conjunct,[status(thm)],[i_0_178]),
[final] ).
cnf(i_0_322,plain,
( ip(X1)
| ~ iext(uri_rdf_type,X1,uri_rdf_Property) ),
inference(split_conjunct,[status(thm)],[i_0_179]),
[final] ).
cnf(i_0_323,plain,
( ip(X1)
| ~ iext(uri_rdf_type,X1,uri_rdf_Property) ),
inference(split_conjunct,[status(thm)],[i_0_180]),
[final] ).
cnf(i_0_324,plain,
( ioap(X1)
| ~ iext(uri_rdf_type,X1,uri_owl_AnnotationProperty) ),
inference(split_conjunct,[status(thm)],[i_0_181]),
[final] ).
cnf(i_0_325,plain,
( lv(X1)
| ~ iext(uri_rdf_type,X1,uri_rdfs_Literal) ),
inference(split_conjunct,[status(thm)],[i_0_182]),
[final] ).
cnf(i_0_326,plain,
( idc(X1)
| ~ iext(uri_rdf_type,X1,uri_rdfs_Datatype) ),
inference(split_conjunct,[status(thm)],[i_0_183]),
[final] ).
cnf(i_0_327,plain,
( ic(X1)
| ~ iext(uri_rdf_type,X1,uri_rdfs_Class) ),
inference(split_conjunct,[status(thm)],[i_0_184]),
[final] ).
cnf(i_0_328,plain,
( ic(X1)
| ~ iext(uri_owl_unionOf,X1,uri_rdf_nil) ),
inference(split_conjunct,[status(thm)],[i_0_161]),
[final] ).
cnf(i_0_329,plain,
( ic(X1)
| ~ iext(uri_owl_intersectionOf,X1,uri_rdf_nil) ),
inference(split_conjunct,[status(thm)],[i_0_134]),
[final] ).
cnf(i_0_330,plain,
( icext(X1,esk5_1(X1))
| iext(uri_owl_unionOf,X1,uri_rdf_nil)
| ~ ic(X1) ),
inference(split_conjunct,[status(thm)],[i_0_161]),
[final] ).
cnf(i_0_331,plain,
( iext(uri_rdf_type,X2,X1)
| ~ icext(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_162]),
[final] ).
cnf(i_0_332,plain,
( iext(uri_rdfs_subPropertyOf,X1,uri_rdfs_member)
| ~ icext(uri_rdfs_ContainerMembershipProperty,X1) ),
inference(split_conjunct,[status(thm)],[i_0_185]),
[final] ).
cnf(i_0_333,plain,
( iext(uri_rdfs_subClassOf,X1,uri_rdfs_Literal)
| ~ icext(uri_rdfs_Datatype,X1) ),
inference(split_conjunct,[status(thm)],[i_0_186]),
[final] ).
cnf(i_0_334,plain,
( iext(uri_rdfs_subPropertyOf,X1,X1)
| ~ ip(X1) ),
inference(split_conjunct,[status(thm)],[i_0_187]),
[final] ).
cnf(i_0_335,plain,
( iext(uri_rdfs_subClassOf,X1,X1)
| ~ ic(X1) ),
inference(split_conjunct,[status(thm)],[i_0_188]),
[final] ).
cnf(i_0_336,plain,
( iext(uri_rdfs_subClassOf,X1,uri_rdfs_Resource)
| ~ ic(X1) ),
inference(split_conjunct,[status(thm)],[i_0_189]),
[final] ).
cnf(i_0_337,plain,
( iext(uri_rdf_type,X1,uri_rdfs_Literal)
| ~ lv(X1) ),
inference(split_conjunct,[status(thm)],[i_0_182]),
[final] ).
cnf(i_0_338,plain,
( iext(uri_rdf_type,X1,uri_owl_Ontology)
| ~ ix(X1) ),
inference(split_conjunct,[status(thm)],[i_0_176]),
[final] ).
cnf(i_0_339,plain,
( iext(uri_rdf_type,X1,uri_rdf_Property)
| ~ ip(X1) ),
inference(split_conjunct,[status(thm)],[i_0_179]),
[final] ).
cnf(i_0_340,plain,
( iext(uri_rdf_type,X1,uri_rdf_Property)
| ~ ip(X1) ),
inference(split_conjunct,[status(thm)],[i_0_180]),
[final] ).
cnf(i_0_341,plain,
( iext(uri_rdf_type,X1,uri_owl_OntologyProperty)
| ~ ioxp(X1) ),
inference(split_conjunct,[status(thm)],[i_0_177]),
[final] ).
cnf(i_0_342,plain,
( iext(uri_rdf_type,X1,uri_owl_DatatypeProperty)
| ~ iodp(X1) ),
inference(split_conjunct,[status(thm)],[i_0_178]),
[final] ).
cnf(i_0_343,plain,
( iext(uri_rdf_type,X1,uri_owl_AnnotationProperty)
| ~ ioap(X1) ),
inference(split_conjunct,[status(thm)],[i_0_181]),
[final] ).
cnf(i_0_344,plain,
( iext(uri_rdf_type,X1,uri_rdfs_Datatype)
| ~ idc(X1) ),
inference(split_conjunct,[status(thm)],[i_0_183]),
[final] ).
cnf(i_0_345,plain,
( iext(uri_rdf_type,X1,uri_rdfs_Class)
| ~ ic(X1) ),
inference(split_conjunct,[status(thm)],[i_0_184]),
[final] ).
cnf(i_0_346,plain,
iext(uri_rdf_type,X1,uri_rdfs_Resource),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[i_0_190,c_0_172])]),
[final] ).
cnf(i_0_347,plain,
iext(uri_rdfs_subPropertyOf,uri_rdfs_isDefinedBy,uri_rdfs_seeAlso),
inference(split_conjunct,[status(thm)],[rdfs_annotation_isdefinedby_sub]),
[final] ).
cnf(i_0_348,plain,
iext(uri_rdfs_subClassOf,uri_ex_c,uri_ex_r),
inference(split_conjunct,[status(thm)],[testcase_premise_fullish_001_Subgraph_Entailment]),
[final] ).
cnf(i_0_349,plain,
iext(uri_rdfs_subClassOf,uri_rdf_XMLLiteral,uri_rdfs_Literal),
inference(split_conjunct,[status(thm)],[rdfs_dat_xmlliteral_sub]),
[final] ).
cnf(i_0_350,plain,
iext(uri_rdfs_subClassOf,uri_rdfs_Seq,uri_rdfs_Container),
inference(split_conjunct,[status(thm)],[rdfs_container_seq_sub]),
[final] ).
cnf(i_0_351,plain,
iext(uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty,uri_rdf_Property),
inference(split_conjunct,[status(thm)],[rdfs_container_containermembershipproperty_sub]),
[final] ).
cnf(i_0_352,plain,
iext(uri_rdfs_subClassOf,uri_rdf_Bag,uri_rdfs_Container),
inference(split_conjunct,[status(thm)],[rdfs_container_bag_sub]),
[final] ).
cnf(i_0_353,plain,
iext(uri_rdfs_subClassOf,uri_rdf_Alt,uri_rdfs_Container),
inference(split_conjunct,[status(thm)],[rdfs_container_alt_sub]),
[final] ).
cnf(i_0_354,plain,
iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,uri_rdfs_Class),
inference(split_conjunct,[status(thm)],[rdfs_datatype_sub]),
[final] ).
cnf(i_0_355,plain,
iext(uri_rdfs_range,uri_rdf_predicate,uri_rdfs_Resource),
inference(split_conjunct,[status(thm)],[rdfs_reification_predicate_range]),
[final] ).
cnf(i_0_356,plain,
iext(uri_rdfs_range,uri_rdf_predicate,uri_rdfs_Resource),
inference(split_conjunct,[status(thm)],[rdfs_reification_object_range]),
[final] ).
cnf(i_0_357,plain,
iext(uri_rdfs_range,uri_rdfs_member,uri_rdfs_Resource),
inference(split_conjunct,[status(thm)],[rdfs_container_member_range]),
[final] ).
cnf(i_0_358,plain,
iext(uri_rdfs_range,uri_rdfs_label,uri_rdfs_Literal),
inference(split_conjunct,[status(thm)],[rdfs_annotation_label_range]),
[final] ).
cnf(i_0_359,plain,
iext(uri_rdfs_range,uri_rdfs_seeAlso,uri_rdfs_Resource),
inference(split_conjunct,[status(thm)],[rdfs_annotation_seealso_range]),
[final] ).
cnf(i_0_360,plain,
iext(uri_rdfs_range,uri_rdfs_isDefinedBy,uri_rdfs_Resource),
inference(split_conjunct,[status(thm)],[rdfs_annotation_isdefinedby_range]),
[final] ).
cnf(i_0_361,plain,
iext(uri_rdfs_range,uri_rdfs_comment,uri_rdfs_Literal),
inference(split_conjunct,[status(thm)],[rdfs_annotation_comment_range]),
[final] ).
cnf(i_0_362,plain,
iext(uri_rdfs_range,uri_rdf_subject,uri_rdfs_Resource),
inference(split_conjunct,[status(thm)],[rdfs_reification_subject_range]),
[final] ).
cnf(i_0_363,plain,
iext(uri_rdfs_range,uri_rdf_value,uri_rdfs_Resource),
inference(split_conjunct,[status(thm)],[rdfs_value_range]),
[final] ).
cnf(i_0_364,plain,
iext(uri_rdfs_range,uri_rdf__3,uri_rdfs_Resource),
inference(split_conjunct,[status(thm)],[rdfs_container_n_range_003]),
[final] ).
cnf(i_0_365,plain,
iext(uri_rdfs_range,uri_rdf__2,uri_rdfs_Resource),
inference(split_conjunct,[status(thm)],[rdfs_container_n_range_002]),
[final] ).
cnf(i_0_366,plain,
iext(uri_rdfs_range,uri_rdf__1,uri_rdfs_Resource),
inference(split_conjunct,[status(thm)],[rdfs_container_n_range_001]),
[final] ).
cnf(i_0_367,plain,
iext(uri_rdfs_range,uri_rdfs_subPropertyOf,uri_rdf_Property),
inference(split_conjunct,[status(thm)],[rdfs_subpropertyof_range]),
[final] ).
cnf(i_0_368,plain,
iext(uri_rdfs_range,uri_rdfs_subClassOf,uri_rdfs_Class),
inference(split_conjunct,[status(thm)],[rdfs_subclassof_range]),
[final] ).
cnf(i_0_369,plain,
iext(uri_rdfs_range,uri_rdfs_range,uri_rdfs_Class),
inference(split_conjunct,[status(thm)],[rdfs_range_range]),
[final] ).
cnf(i_0_370,plain,
iext(uri_rdfs_range,uri_rdfs_domain,uri_rdfs_Class),
inference(split_conjunct,[status(thm)],[rdfs_domain_range]),
[final] ).
cnf(i_0_371,plain,
iext(uri_rdfs_range,uri_rdf_type,uri_rdfs_Class),
inference(split_conjunct,[status(thm)],[rdfs_type_range]),
[final] ).
cnf(i_0_372,plain,
iext(uri_rdfs_range,uri_rdf_rest,uri_rdf_List),
inference(split_conjunct,[status(thm)],[rdfs_collection_rest_range]),
[final] ).
cnf(i_0_373,plain,
iext(uri_rdfs_range,uri_rdf_first,uri_rdfs_Resource),
inference(split_conjunct,[status(thm)],[rdfs_collection_first_range]),
[final] ).
cnf(i_0_374,plain,
iext(uri_rdfs_domain,uri_rdf_predicate,uri_rdfs_Statement),
inference(split_conjunct,[status(thm)],[rdfs_reification_predicate_domain]),
[final] ).
cnf(i_0_375,plain,
iext(uri_rdfs_domain,uri_rdfs_member,uri_rdfs_Resource),
inference(split_conjunct,[status(thm)],[rdfs_container_member_domain]),
[final] ).
cnf(i_0_376,plain,
iext(uri_rdfs_domain,uri_rdfs_label,uri_rdfs_Resource),
inference(split_conjunct,[status(thm)],[rdfs_annotation_label_domain]),
[final] ).
cnf(i_0_377,plain,
iext(uri_rdfs_domain,uri_rdfs_seeAlso,uri_rdfs_Resource),
inference(split_conjunct,[status(thm)],[rdfs_annotation_seealso_domain]),
[final] ).
cnf(i_0_378,plain,
iext(uri_rdfs_domain,uri_rdfs_isDefinedBy,uri_rdfs_Resource),
inference(split_conjunct,[status(thm)],[rdfs_annotation_isdefinedby_domain]),
[final] ).
cnf(i_0_379,plain,
iext(uri_rdfs_domain,uri_rdfs_comment,uri_rdfs_Resource),
inference(split_conjunct,[status(thm)],[rdfs_annotation_comment_domain]),
[final] ).
cnf(i_0_380,plain,
iext(uri_rdfs_domain,uri_rdf_subject,uri_rdfs_Statement),
inference(split_conjunct,[status(thm)],[rdfs_reification_subject_domain]),
[final] ).
cnf(i_0_381,plain,
iext(uri_rdfs_domain,uri_rdf_value,uri_rdfs_Resource),
inference(split_conjunct,[status(thm)],[rdfs_value_domain]),
[final] ).
cnf(i_0_382,plain,
iext(uri_rdfs_domain,uri_rdf_object,uri_rdfs_Statement),
inference(split_conjunct,[status(thm)],[rdfs_reification_object_domain]),
[final] ).
cnf(i_0_383,plain,
iext(uri_rdfs_domain,uri_rdf__3,uri_rdfs_Resource),
inference(split_conjunct,[status(thm)],[rdfs_container_n_domain_003]),
[final] ).
cnf(i_0_384,plain,
iext(uri_rdfs_domain,uri_rdf__2,uri_rdfs_Resource),
inference(split_conjunct,[status(thm)],[rdfs_container_n_domain_002]),
[final] ).
cnf(i_0_385,plain,
iext(uri_rdfs_domain,uri_rdf__1,uri_rdfs_Resource),
inference(split_conjunct,[status(thm)],[rdfs_container_n_domain_001]),
[final] ).
cnf(i_0_386,plain,
iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,uri_rdf_Property),
inference(split_conjunct,[status(thm)],[rdfs_subpropertyof_domain]),
[final] ).
cnf(i_0_387,plain,
iext(uri_rdfs_domain,uri_rdfs_subClassOf,uri_rdfs_Class),
inference(split_conjunct,[status(thm)],[rdfs_subclassof_domain]),
[final] ).
cnf(i_0_388,plain,
iext(uri_rdfs_domain,uri_rdfs_range,uri_rdf_Property),
inference(split_conjunct,[status(thm)],[rdfs_range_domain]),
[final] ).
cnf(i_0_389,plain,
iext(uri_rdfs_domain,uri_rdfs_domain,uri_rdf_Property),
inference(split_conjunct,[status(thm)],[rdfs_domain_domain]),
[final] ).
cnf(i_0_390,plain,
iext(uri_rdfs_domain,uri_rdf_type,uri_rdfs_Resource),
inference(split_conjunct,[status(thm)],[rdfs_type_domain]),
[final] ).
cnf(i_0_391,plain,
iext(uri_rdfs_domain,uri_rdf_rest,uri_rdf_List),
inference(split_conjunct,[status(thm)],[rdfs_collection_rest_domain]),
[final] ).
cnf(i_0_392,plain,
iext(uri_rdfs_domain,uri_rdf_first,uri_rdf_List),
inference(split_conjunct,[status(thm)],[rdfs_collection_first_domain]),
[final] ).
cnf(i_0_393,plain,
iext(uri_owl_someValuesFrom,uri_ex_r,uri_ex_d),
inference(split_conjunct,[status(thm)],[testcase_premise_fullish_001_Subgraph_Entailment]),
[final] ).
cnf(i_0_394,plain,
iext(uri_owl_onProperty,uri_ex_r,uri_ex_p),
inference(split_conjunct,[status(thm)],[testcase_premise_fullish_001_Subgraph_Entailment]),
[final] ).
cnf(i_0_395,plain,
iext(uri_rdf_type,uri_ex_r,uri_owl_Restriction),
inference(split_conjunct,[status(thm)],[testcase_premise_fullish_001_Subgraph_Entailment]),
[final] ).
cnf(i_0_396,plain,
iext(uri_rdf_type,uri_rdf_XMLLiteral,uri_rdfs_Datatype),
inference(split_conjunct,[status(thm)],[rdfs_dat_xmlliteral_type]),
[final] ).
cnf(i_0_397,plain,
iext(uri_rdf_type,uri_rdf_subject,uri_rdf_Property),
inference(split_conjunct,[status(thm)],[rdf_reification_subject_type]),
[final] ).
cnf(i_0_398,plain,
iext(uri_rdf_type,uri_rdf_value,uri_rdf_Property),
inference(split_conjunct,[status(thm)],[rdf_reification_predicate_type]),
[final] ).
cnf(i_0_399,plain,
iext(uri_rdf_type,uri_rdf_object,uri_rdf_Property),
inference(split_conjunct,[status(thm)],[rdf_reification_object_type]),
[final] ).
cnf(i_0_400,plain,
iext(uri_rdf_type,uri_rdf__3,uri_rdfs_ContainerMembershipProperty),
inference(split_conjunct,[status(thm)],[rdfs_container_n_type_003]),
[final] ).
cnf(i_0_401,plain,
iext(uri_rdf_type,uri_rdf__3,uri_rdf_Property),
inference(split_conjunct,[status(thm)],[rdf_container_n_type_003]),
[final] ).
cnf(i_0_402,plain,
iext(uri_rdf_type,uri_rdf__2,uri_rdfs_ContainerMembershipProperty),
inference(split_conjunct,[status(thm)],[rdfs_container_n_type_002]),
[final] ).
cnf(i_0_403,plain,
iext(uri_rdf_type,uri_rdf__2,uri_rdf_Property),
inference(split_conjunct,[status(thm)],[rdf_container_n_type_002]),
[final] ).
cnf(i_0_404,plain,
iext(uri_rdf_type,uri_rdf__1,uri_rdfs_ContainerMembershipProperty),
inference(split_conjunct,[status(thm)],[rdfs_container_n_type_001]),
[final] ).
cnf(i_0_405,plain,
iext(uri_rdf_type,uri_rdf__1,uri_rdf_Property),
inference(split_conjunct,[status(thm)],[rdf_container_n_type_001]),
[final] ).
cnf(i_0_406,plain,
iext(uri_rdf_type,uri_rdf_Property,uri_rdfs_Class),
inference(split_conjunct,[status(thm)],[rdfs_property_type]),
[final] ).
cnf(i_0_407,plain,
iext(uri_rdf_type,uri_rdf_type,uri_rdf_Property),
inference(split_conjunct,[status(thm)],[rdf_value_type]),
[final] ).
cnf(i_0_408,plain,
iext(uri_rdf_type,uri_rdf_type,uri_rdf_Property),
inference(split_conjunct,[status(thm)],[rdf_type_type]),
[final] ).
cnf(i_0_409,plain,
iext(uri_rdf_type,uri_rdf_rest,uri_rdf_Property),
inference(split_conjunct,[status(thm)],[rdf_collection_rest_type]),
[final] ).
cnf(i_0_410,plain,
iext(uri_rdf_type,uri_rdf_first,uri_rdf_Property),
inference(split_conjunct,[status(thm)],[rdf_collection_first_type]),
[final] ).
cnf(i_0_411,plain,
iext(uri_rdf_type,uri_rdf_nil,uri_rdf_List),
inference(split_conjunct,[status(thm)],[rdf_collection_nil_type]),
[final] ).
cnf(i_0_412,plain,
( lv(X2)
| ~ idc(X1)
| ~ icext(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_191]),
[final] ).
cnf(i_0_413,plain,
( lv(X1)
| ~ icext(uri_rdfs_Literal,X1) ),
inference(split_conjunct,[status(thm)],[i_0_192]),
[final] ).
cnf(i_0_414,plain,
( ic(X1)
| ~ icext(uri_rdfs_Class,X1) ),
inference(split_conjunct,[status(thm)],[i_0_193]),
[final] ).
cnf(i_0_415,plain,
~ icext(uri_owl_Nothing,X1),
inference(split_conjunct,[status(thm)],[i_0_194]),
[final] ).
cnf(i_0_416,plain,
( icext(uri_rdfs_Literal,X1)
| ~ lv(X1) ),
inference(split_conjunct,[status(thm)],[i_0_192]),
[final] ).
cnf(i_0_417,plain,
( icext(uri_rdfs_Class,X1)
| ~ ic(X1) ),
inference(split_conjunct,[status(thm)],[i_0_193]),
[final] ).
cnf(i_0_418,plain,
icext(uri_rdfs_Resource,X1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[i_0_195,c_0_172])]),
[final] ).
cnf(i_0_419,plain,
icext(uri_owl_Thing,X1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[i_0_196,c_0_172])]),
[final] ).
cnf(i_0_420,plain,
( ip(X1)
| ~ ioxp(X1) ),
inference(split_conjunct,[status(thm)],[i_0_197]),
[final] ).
cnf(i_0_421,plain,
( ip(X1)
| ~ iodp(X1) ),
inference(split_conjunct,[status(thm)],[i_0_198]),
[final] ).
cnf(i_0_422,plain,
( ip(X1)
| ~ ioap(X1) ),
inference(split_conjunct,[status(thm)],[i_0_199]),
[final] ).
cnf(i_0_423,plain,
( ic(X1)
| ~ idc(X1) ),
inference(split_conjunct,[status(thm)],[i_0_200]),
[final] ).
cnf(i_0_424,plain,
ip(uri_owl_someValuesFrom),
inference(split_conjunct,[status(thm)],[owl_prop_somevaluesfrom_type]),
[final] ).
cnf(i_0_425,plain,
ip(uri_owl_onProperty),
inference(split_conjunct,[status(thm)],[owl_prop_onproperty_type]),
[final] ).
cnf(i_0_426,plain,
ip(uri_owl_hasValue),
inference(split_conjunct,[status(thm)],[owl_prop_hasvalue_type]),
[final] ).
cnf(i_0_427,plain,
ip(uri_owl_allValuesFrom),
inference(split_conjunct,[status(thm)],[owl_prop_allvaluesfrom_type]),
[final] ).
cnf(i_0_428,plain,
ip(uri_owl_unionOf),
inference(split_conjunct,[status(thm)],[owl_prop_unionof_type]),
[final] ).
cnf(i_0_429,plain,
ip(uri_owl_intersectionOf),
inference(split_conjunct,[status(thm)],[owl_prop_intersectionof_type]),
[final] ).
cnf(i_0_430,plain,
ip(uri_owl_complementOf),
inference(split_conjunct,[status(thm)],[owl_prop_complementof_type]),
[final] ).
cnf(i_0_431,plain,
ic(uri_owl_Thing),
inference(split_conjunct,[status(thm)],[owl_class_thing_type]),
[final] ).
cnf(i_0_432,plain,
ic(uri_owl_Nothing),
inference(split_conjunct,[status(thm)],[owl_class_nothing_type]),
[final] ).
cnf(i_0_433,plain,
$false,
inference(scs_inference,[],[i_0_395,i_0_394,i_0_275]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SWB001+3 : TPTP v9.2.1. Released v5.2.0.
% 0.00/0.12 % Command : /export/starexec/sandbox2/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox2/solver/bin/cse --final-prover /export/starexec/sandbox2/solver/bin/eprover --proof-time %d --global-time-limit %d
% 0.16/0.33 % Computer : n028.cluster.edu
% 0.16/0.33 % Model : x86_64 x86_64
% 0.16/0.33 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.16/0.33 % Memory : 8042.1875MB
% 0.16/0.33 % OS : Linux 3.10.0-693.el7.x86_64
% 0.16/0.33 % CPULimit : 300
% 0.16/0.33 % WCLimit : 300
% 0.16/0.33 % DateTime : Tue May 5 04:06:01 EDT 2026
% 0.16/0.33 % CPUTime :
% 0.16/0.34 % start to proof: theBenchmark
% 0.33/1.62 % Version : CSE_E---1.7
% 0.33/1.62 % Problem : theBenchmark.p
% 0.33/1.62 % SZS status Theorem for theBenchmark.p
% 0.33/1.62 % SZS output start CNFRefutation
% See solution above
% 0.33/1.63 % Total time : 1.273s
%------------------------------------------------------------------------------