%------------------------------------------------------------------------------
% File : CSE_E---1.7
% Problem : SWB002+3 : TPTP v9.2.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : /export/starexec/sandbox/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox/solver/bin/cse --final-prover /export/starexec/sandbox/solver/bin/eprover --proof-time %d --global-time-limit %d
% Computer : n010.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:32 PM UTC 2026
% Result : Theorem 0.38s 1.62s
% Output : CNFRefutation 0.38s
% Verified :
% SZS Type : ERROR: Analysing output (Could not find formula named c_0_172)
% Comments :
%------------------------------------------------------------------------------
fof(testcase_conclusion_fullish_002_Existential_Blank_Nodes,conjecture,
? [X21,X22] :
( iext(uri_ex_p,X21,X22)
& iext(uri_ex_q,X22,X21) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',testcase_conclusion_fullish_002_Existential_Blank_Nodes) ).
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/sandbox/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/sandbox/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/sandbox/benchmark/Axioms/SWB002+0.ax',owl_bool_intersectionof_class_000) ).
fof(simple_ir,axiom,
! [X3] : ir(X3),
file('/export/starexec/sandbox/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/sandbox/benchmark/Axioms/SWB002+0.ax',owl_parts_ir_def) ).
fof(owl_class_nothing_ext,axiom,
! [X3] : ~ icext(uri_owl_Nothing,X3),
file('/export/starexec/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/benchmark/Axioms/SWB002+0.ax',rdfs_class_instsub_resource) ).
fof(testcase_premise_fullish_002_Existential_Blank_Nodes,axiom,
? [X23] :
( iext(uri_ex_p,uri_ex_s,X23)
& iext(uri_ex_q,X23,uri_ex_s) ),
file('/export/starexec/sandbox/benchmark/theBenchmark.p',testcase_premise_fullish_002_Existential_Blank_Nodes) ).
fof(owl_parts_idc_cond_inst,axiom,
! [X3] :
( idc(X3)
=> ! [X10] :
( icext(X3,X10)
=> lv(X10) ) ),
file('/export/starexec/sandbox/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/sandbox/benchmark/Axioms/SWB002+0.ax',rdfs_lv_def) ).
fof(rdfs_ic_def,axiom,
! [X3] :
( ic(X3)
<=> icext(uri_rdfs_Class,X3) ),
file('/export/starexec/sandbox/benchmark/Axioms/SWB002+0.ax',rdfs_ic_def) ).
fof(owl_parts_ioxp_cond_set,axiom,
! [X3] :
( ioxp(X3)
=> ip(X3) ),
file('/export/starexec/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/benchmark/Axioms/SWB002+0.ax',rdfs_annotation_isdefinedby_sub) ).
fof(rdfs_dat_xmlliteral_sub,axiom,
iext(uri_rdfs_subClassOf,uri_rdf_XMLLiteral,uri_rdfs_Literal),
file('/export/starexec/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/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/sandbox/benchmark/Axioms/SWB002+0.ax',rdf_collection_nil_type) ).
fof(owl_prop_somevaluesfrom_type,axiom,
ip(uri_owl_someValuesFrom),
file('/export/starexec/sandbox/benchmark/Axioms/SWB002+0.ax',owl_prop_somevaluesfrom_type) ).
fof(owl_prop_onproperty_type,axiom,
ip(uri_owl_onProperty),
file('/export/starexec/sandbox/benchmark/Axioms/SWB002+0.ax',owl_prop_onproperty_type) ).
fof(owl_prop_hasvalue_type,axiom,
ip(uri_owl_hasValue),
file('/export/starexec/sandbox/benchmark/Axioms/SWB002+0.ax',owl_prop_hasvalue_type) ).
fof(owl_prop_allvaluesfrom_type,axiom,
ip(uri_owl_allValuesFrom),
file('/export/starexec/sandbox/benchmark/Axioms/SWB002+0.ax',owl_prop_allvaluesfrom_type) ).
fof(owl_prop_unionof_type,axiom,
ip(uri_owl_unionOf),
file('/export/starexec/sandbox/benchmark/Axioms/SWB002+0.ax',owl_prop_unionof_type) ).
fof(owl_prop_intersectionof_type,axiom,
ip(uri_owl_intersectionOf),
file('/export/starexec/sandbox/benchmark/Axioms/SWB002+0.ax',owl_prop_intersectionof_type) ).
fof(owl_prop_complementof_type,axiom,
ip(uri_owl_complementOf),
file('/export/starexec/sandbox/benchmark/Axioms/SWB002+0.ax',owl_prop_complementof_type) ).
fof(owl_class_thing_type,axiom,
ic(uri_owl_Thing),
file('/export/starexec/sandbox/benchmark/Axioms/SWB002+0.ax',owl_class_thing_type) ).
fof(owl_class_nothing_type,axiom,
ic(uri_owl_Nothing),
file('/export/starexec/sandbox/benchmark/Axioms/SWB002+0.ax',owl_class_nothing_type) ).
fof(i_0_131,negated_conjecture,
~ ? [X21,X22] :
( iext(uri_ex_p,X21,X22)
& iext(uri_ex_q,X22,X21) ),
inference(assume_negation,[status(cth)],[testcase_conclusion_fullish_002_Existential_Blank_Nodes]) ).
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,
! [X189,X190,X191,X192] :
( ( ic(X189)
| ~ iext(uri_owl_intersectionOf,X189,uri_rdf_nil) )
& ( ~ icext(X189,X190)
| ir(X190)
| ~ iext(uri_owl_intersectionOf,X189,uri_rdf_nil) )
& ( ~ ir(X191)
| icext(X189,X191)
| ~ iext(uri_owl_intersectionOf,X189,uri_rdf_nil) )
& ( ~ icext(X192,esk1_1(X192))
| ~ ir(esk1_1(X192))
| ~ ic(X192)
| iext(uri_owl_intersectionOf,X192,uri_rdf_nil) )
& ( icext(X192,esk1_1(X192))
| ir(esk1_1(X192))
| ~ ic(X192)
| iext(uri_owl_intersectionOf,X192,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,
! [X379] : ir(X379),
inference(variable_rename,[status(thm)],[simple_ir]) ).
fof(i_0_136,plain,
! [X277] :
( ( ~ ir(X277)
| iext(uri_rdf_type,X277,uri_rdfs_Resource) )
& ( ~ iext(uri_rdf_type,X277,uri_rdfs_Resource)
| ir(X277) ) ),
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,
! [X355] :
( ( ~ ir(X355)
| icext(uri_rdfs_Resource,X355) )
& ( ~ icext(uri_rdfs_Resource,X355)
| ir(X355) ) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[rdfs_ir_def])]) ).
fof(i_0_139,plain,
! [X247] :
( ( ~ icext(uri_owl_Thing,X247)
| ir(X247) )
& ( ~ ir(X247)
| icext(uri_owl_Thing,X247) ) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[owl_class_thing_ext])]) ).
fof(i_0_140,plain,
! [X208,X209,X210,X211,X212,X213,X214,X215,X216] :
( ( ic(X208)
| ~ iext(uri_owl_intersectionOf,X208,X209)
| ~ iext(uri_rdf_first,X209,X210)
| ~ iext(uri_rdf_rest,X209,X211)
| ~ iext(uri_rdf_first,X211,X212)
| ~ iext(uri_rdf_rest,X211,X213)
| ~ iext(uri_rdf_first,X213,X214)
| ~ iext(uri_rdf_rest,X213,uri_rdf_nil) )
& ( ic(X210)
| ~ iext(uri_owl_intersectionOf,X208,X209)
| ~ iext(uri_rdf_first,X209,X210)
| ~ iext(uri_rdf_rest,X209,X211)
| ~ iext(uri_rdf_first,X211,X212)
| ~ iext(uri_rdf_rest,X211,X213)
| ~ iext(uri_rdf_first,X213,X214)
| ~ iext(uri_rdf_rest,X213,uri_rdf_nil) )
& ( ic(X212)
| ~ iext(uri_owl_intersectionOf,X208,X209)
| ~ iext(uri_rdf_first,X209,X210)
| ~ iext(uri_rdf_rest,X209,X211)
| ~ iext(uri_rdf_first,X211,X212)
| ~ iext(uri_rdf_rest,X211,X213)
| ~ iext(uri_rdf_first,X213,X214)
| ~ iext(uri_rdf_rest,X213,uri_rdf_nil) )
& ( ic(X214)
| ~ iext(uri_owl_intersectionOf,X208,X209)
| ~ iext(uri_rdf_first,X209,X210)
| ~ iext(uri_rdf_rest,X209,X211)
| ~ iext(uri_rdf_first,X211,X212)
| ~ iext(uri_rdf_rest,X211,X213)
| ~ iext(uri_rdf_first,X213,X214)
| ~ iext(uri_rdf_rest,X213,uri_rdf_nil) )
& ( icext(X210,X215)
| ~ icext(X208,X215)
| ~ iext(uri_owl_intersectionOf,X208,X209)
| ~ iext(uri_rdf_first,X209,X210)
| ~ iext(uri_rdf_rest,X209,X211)
| ~ iext(uri_rdf_first,X211,X212)
| ~ iext(uri_rdf_rest,X211,X213)
| ~ iext(uri_rdf_first,X213,X214)
| ~ iext(uri_rdf_rest,X213,uri_rdf_nil) )
& ( icext(X212,X215)
| ~ icext(X208,X215)
| ~ iext(uri_owl_intersectionOf,X208,X209)
| ~ iext(uri_rdf_first,X209,X210)
| ~ iext(uri_rdf_rest,X209,X211)
| ~ iext(uri_rdf_first,X211,X212)
| ~ iext(uri_rdf_rest,X211,X213)
| ~ iext(uri_rdf_first,X213,X214)
| ~ iext(uri_rdf_rest,X213,uri_rdf_nil) )
& ( icext(X214,X215)
| ~ icext(X208,X215)
| ~ iext(uri_owl_intersectionOf,X208,X209)
| ~ iext(uri_rdf_first,X209,X210)
| ~ iext(uri_rdf_rest,X209,X211)
| ~ iext(uri_rdf_first,X211,X212)
| ~ iext(uri_rdf_rest,X211,X213)
| ~ iext(uri_rdf_first,X213,X214)
| ~ iext(uri_rdf_rest,X213,uri_rdf_nil) )
& ( ~ icext(X210,X216)
| ~ icext(X212,X216)
| ~ icext(X214,X216)
| icext(X208,X216)
| ~ iext(uri_owl_intersectionOf,X208,X209)
| ~ iext(uri_rdf_first,X209,X210)
| ~ iext(uri_rdf_rest,X209,X211)
| ~ iext(uri_rdf_first,X211,X212)
| ~ iext(uri_rdf_rest,X211,X213)
| ~ iext(uri_rdf_first,X213,X214)
| ~ iext(uri_rdf_rest,X213,uri_rdf_nil) )
& ( ~ icext(X208,esk4_7(X208,X209,X210,X211,X212,X213,X214))
| ~ icext(X210,esk4_7(X208,X209,X210,X211,X212,X213,X214))
| ~ icext(X212,esk4_7(X208,X209,X210,X211,X212,X213,X214))
| ~ icext(X214,esk4_7(X208,X209,X210,X211,X212,X213,X214))
| ~ ic(X208)
| ~ ic(X210)
| ~ ic(X212)
| ~ ic(X214)
| iext(uri_owl_intersectionOf,X208,X209)
| ~ iext(uri_rdf_first,X209,X210)
| ~ iext(uri_rdf_rest,X209,X211)
| ~ iext(uri_rdf_first,X211,X212)
| ~ iext(uri_rdf_rest,X211,X213)
| ~ iext(uri_rdf_first,X213,X214)
| ~ iext(uri_rdf_rest,X213,uri_rdf_nil) )
& ( icext(X210,esk4_7(X208,X209,X210,X211,X212,X213,X214))
| icext(X208,esk4_7(X208,X209,X210,X211,X212,X213,X214))
| ~ ic(X208)
| ~ ic(X210)
| ~ ic(X212)
| ~ ic(X214)
| iext(uri_owl_intersectionOf,X208,X209)
| ~ iext(uri_rdf_first,X209,X210)
| ~ iext(uri_rdf_rest,X209,X211)
| ~ iext(uri_rdf_first,X211,X212)
| ~ iext(uri_rdf_rest,X211,X213)
| ~ iext(uri_rdf_first,X213,X214)
| ~ iext(uri_rdf_rest,X213,uri_rdf_nil) )
& ( icext(X212,esk4_7(X208,X209,X210,X211,X212,X213,X214))
| icext(X208,esk4_7(X208,X209,X210,X211,X212,X213,X214))
| ~ ic(X208)
| ~ ic(X210)
| ~ ic(X212)
| ~ ic(X214)
| iext(uri_owl_intersectionOf,X208,X209)
| ~ iext(uri_rdf_first,X209,X210)
| ~ iext(uri_rdf_rest,X209,X211)
| ~ iext(uri_rdf_first,X211,X212)
| ~ iext(uri_rdf_rest,X211,X213)
| ~ iext(uri_rdf_first,X213,X214)
| ~ iext(uri_rdf_rest,X213,uri_rdf_nil) )
& ( icext(X214,esk4_7(X208,X209,X210,X211,X212,X213,X214))
| icext(X208,esk4_7(X208,X209,X210,X211,X212,X213,X214))
| ~ ic(X208)
| ~ ic(X210)
| ~ ic(X212)
| ~ ic(X214)
| iext(uri_owl_intersectionOf,X208,X209)
| ~ iext(uri_rdf_first,X209,X210)
| ~ iext(uri_rdf_rest,X209,X211)
| ~ iext(uri_rdf_first,X211,X212)
| ~ iext(uri_rdf_rest,X211,X213)
| ~ iext(uri_rdf_first,X213,X214)
| ~ iext(uri_rdf_rest,X213,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,
! [X236,X237,X238,X239,X240,X241,X242,X243,X244] :
( ( ic(X236)
| ~ iext(uri_owl_unionOf,X236,X237)
| ~ iext(uri_rdf_first,X237,X238)
| ~ iext(uri_rdf_rest,X237,X239)
| ~ iext(uri_rdf_first,X239,X240)
| ~ iext(uri_rdf_rest,X239,X241)
| ~ iext(uri_rdf_first,X241,X242)
| ~ iext(uri_rdf_rest,X241,uri_rdf_nil) )
& ( ic(X238)
| ~ iext(uri_owl_unionOf,X236,X237)
| ~ iext(uri_rdf_first,X237,X238)
| ~ iext(uri_rdf_rest,X237,X239)
| ~ iext(uri_rdf_first,X239,X240)
| ~ iext(uri_rdf_rest,X239,X241)
| ~ iext(uri_rdf_first,X241,X242)
| ~ iext(uri_rdf_rest,X241,uri_rdf_nil) )
& ( ic(X240)
| ~ iext(uri_owl_unionOf,X236,X237)
| ~ iext(uri_rdf_first,X237,X238)
| ~ iext(uri_rdf_rest,X237,X239)
| ~ iext(uri_rdf_first,X239,X240)
| ~ iext(uri_rdf_rest,X239,X241)
| ~ iext(uri_rdf_first,X241,X242)
| ~ iext(uri_rdf_rest,X241,uri_rdf_nil) )
& ( ic(X242)
| ~ iext(uri_owl_unionOf,X236,X237)
| ~ iext(uri_rdf_first,X237,X238)
| ~ iext(uri_rdf_rest,X237,X239)
| ~ iext(uri_rdf_first,X239,X240)
| ~ iext(uri_rdf_rest,X239,X241)
| ~ iext(uri_rdf_first,X241,X242)
| ~ iext(uri_rdf_rest,X241,uri_rdf_nil) )
& ( ~ icext(X236,X243)
| icext(X238,X243)
| icext(X240,X243)
| icext(X242,X243)
| ~ iext(uri_owl_unionOf,X236,X237)
| ~ iext(uri_rdf_first,X237,X238)
| ~ iext(uri_rdf_rest,X237,X239)
| ~ iext(uri_rdf_first,X239,X240)
| ~ iext(uri_rdf_rest,X239,X241)
| ~ iext(uri_rdf_first,X241,X242)
| ~ iext(uri_rdf_rest,X241,uri_rdf_nil) )
& ( ~ icext(X238,X244)
| icext(X236,X244)
| ~ iext(uri_owl_unionOf,X236,X237)
| ~ iext(uri_rdf_first,X237,X238)
| ~ iext(uri_rdf_rest,X237,X239)
| ~ iext(uri_rdf_first,X239,X240)
| ~ iext(uri_rdf_rest,X239,X241)
| ~ iext(uri_rdf_first,X241,X242)
| ~ iext(uri_rdf_rest,X241,uri_rdf_nil) )
& ( ~ icext(X240,X244)
| icext(X236,X244)
| ~ iext(uri_owl_unionOf,X236,X237)
| ~ iext(uri_rdf_first,X237,X238)
| ~ iext(uri_rdf_rest,X237,X239)
| ~ iext(uri_rdf_first,X239,X240)
| ~ iext(uri_rdf_rest,X239,X241)
| ~ iext(uri_rdf_first,X241,X242)
| ~ iext(uri_rdf_rest,X241,uri_rdf_nil) )
& ( ~ icext(X242,X244)
| icext(X236,X244)
| ~ iext(uri_owl_unionOf,X236,X237)
| ~ iext(uri_rdf_first,X237,X238)
| ~ iext(uri_rdf_rest,X237,X239)
| ~ iext(uri_rdf_first,X239,X240)
| ~ iext(uri_rdf_rest,X239,X241)
| ~ iext(uri_rdf_first,X241,X242)
| ~ iext(uri_rdf_rest,X241,uri_rdf_nil) )
& ( ~ icext(X238,esk8_7(X236,X237,X238,X239,X240,X241,X242))
| ~ icext(X236,esk8_7(X236,X237,X238,X239,X240,X241,X242))
| ~ ic(X236)
| ~ ic(X238)
| ~ ic(X240)
| ~ ic(X242)
| iext(uri_owl_unionOf,X236,X237)
| ~ iext(uri_rdf_first,X237,X238)
| ~ iext(uri_rdf_rest,X237,X239)
| ~ iext(uri_rdf_first,X239,X240)
| ~ iext(uri_rdf_rest,X239,X241)
| ~ iext(uri_rdf_first,X241,X242)
| ~ iext(uri_rdf_rest,X241,uri_rdf_nil) )
& ( ~ icext(X240,esk8_7(X236,X237,X238,X239,X240,X241,X242))
| ~ icext(X236,esk8_7(X236,X237,X238,X239,X240,X241,X242))
| ~ ic(X236)
| ~ ic(X238)
| ~ ic(X240)
| ~ ic(X242)
| iext(uri_owl_unionOf,X236,X237)
| ~ iext(uri_rdf_first,X237,X238)
| ~ iext(uri_rdf_rest,X237,X239)
| ~ iext(uri_rdf_first,X239,X240)
| ~ iext(uri_rdf_rest,X239,X241)
| ~ iext(uri_rdf_first,X241,X242)
| ~ iext(uri_rdf_rest,X241,uri_rdf_nil) )
& ( ~ icext(X242,esk8_7(X236,X237,X238,X239,X240,X241,X242))
| ~ icext(X236,esk8_7(X236,X237,X238,X239,X240,X241,X242))
| ~ ic(X236)
| ~ ic(X238)
| ~ ic(X240)
| ~ ic(X242)
| iext(uri_owl_unionOf,X236,X237)
| ~ iext(uri_rdf_first,X237,X238)
| ~ iext(uri_rdf_rest,X237,X239)
| ~ iext(uri_rdf_first,X239,X240)
| ~ iext(uri_rdf_rest,X239,X241)
| ~ iext(uri_rdf_first,X241,X242)
| ~ iext(uri_rdf_rest,X241,uri_rdf_nil) )
& ( icext(X236,esk8_7(X236,X237,X238,X239,X240,X241,X242))
| icext(X238,esk8_7(X236,X237,X238,X239,X240,X241,X242))
| icext(X240,esk8_7(X236,X237,X238,X239,X240,X241,X242))
| icext(X242,esk8_7(X236,X237,X238,X239,X240,X241,X242))
| ~ ic(X236)
| ~ ic(X238)
| ~ ic(X240)
| ~ ic(X242)
| iext(uri_owl_unionOf,X236,X237)
| ~ iext(uri_rdf_first,X237,X238)
| ~ iext(uri_rdf_rest,X237,X239)
| ~ iext(uri_rdf_first,X239,X240)
| ~ iext(uri_rdf_rest,X239,X241)
| ~ iext(uri_rdf_first,X241,X242)
| ~ iext(uri_rdf_rest,X241,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,
! [X200,X201,X202,X203,X204,X205,X206] :
( ( ic(X200)
| ~ iext(uri_owl_intersectionOf,X200,X201)
| ~ iext(uri_rdf_first,X201,X202)
| ~ iext(uri_rdf_rest,X201,X203)
| ~ iext(uri_rdf_first,X203,X204)
| ~ iext(uri_rdf_rest,X203,uri_rdf_nil) )
& ( ic(X202)
| ~ iext(uri_owl_intersectionOf,X200,X201)
| ~ iext(uri_rdf_first,X201,X202)
| ~ iext(uri_rdf_rest,X201,X203)
| ~ iext(uri_rdf_first,X203,X204)
| ~ iext(uri_rdf_rest,X203,uri_rdf_nil) )
& ( ic(X204)
| ~ iext(uri_owl_intersectionOf,X200,X201)
| ~ iext(uri_rdf_first,X201,X202)
| ~ iext(uri_rdf_rest,X201,X203)
| ~ iext(uri_rdf_first,X203,X204)
| ~ iext(uri_rdf_rest,X203,uri_rdf_nil) )
& ( icext(X202,X205)
| ~ icext(X200,X205)
| ~ iext(uri_owl_intersectionOf,X200,X201)
| ~ iext(uri_rdf_first,X201,X202)
| ~ iext(uri_rdf_rest,X201,X203)
| ~ iext(uri_rdf_first,X203,X204)
| ~ iext(uri_rdf_rest,X203,uri_rdf_nil) )
& ( icext(X204,X205)
| ~ icext(X200,X205)
| ~ iext(uri_owl_intersectionOf,X200,X201)
| ~ iext(uri_rdf_first,X201,X202)
| ~ iext(uri_rdf_rest,X201,X203)
| ~ iext(uri_rdf_first,X203,X204)
| ~ iext(uri_rdf_rest,X203,uri_rdf_nil) )
& ( ~ icext(X202,X206)
| ~ icext(X204,X206)
| icext(X200,X206)
| ~ iext(uri_owl_intersectionOf,X200,X201)
| ~ iext(uri_rdf_first,X201,X202)
| ~ iext(uri_rdf_rest,X201,X203)
| ~ iext(uri_rdf_first,X203,X204)
| ~ iext(uri_rdf_rest,X203,uri_rdf_nil) )
& ( ~ icext(X200,esk3_5(X200,X201,X202,X203,X204))
| ~ icext(X202,esk3_5(X200,X201,X202,X203,X204))
| ~ icext(X204,esk3_5(X200,X201,X202,X203,X204))
| ~ ic(X200)
| ~ ic(X202)
| ~ ic(X204)
| iext(uri_owl_intersectionOf,X200,X201)
| ~ iext(uri_rdf_first,X201,X202)
| ~ iext(uri_rdf_rest,X201,X203)
| ~ iext(uri_rdf_first,X203,X204)
| ~ iext(uri_rdf_rest,X203,uri_rdf_nil) )
& ( icext(X202,esk3_5(X200,X201,X202,X203,X204))
| icext(X200,esk3_5(X200,X201,X202,X203,X204))
| ~ ic(X200)
| ~ ic(X202)
| ~ ic(X204)
| iext(uri_owl_intersectionOf,X200,X201)
| ~ iext(uri_rdf_first,X201,X202)
| ~ iext(uri_rdf_rest,X201,X203)
| ~ iext(uri_rdf_first,X203,X204)
| ~ iext(uri_rdf_rest,X203,uri_rdf_nil) )
& ( icext(X204,esk3_5(X200,X201,X202,X203,X204))
| icext(X200,esk3_5(X200,X201,X202,X203,X204))
| ~ ic(X200)
| ~ ic(X202)
| ~ ic(X204)
| iext(uri_owl_intersectionOf,X200,X201)
| ~ iext(uri_rdf_first,X201,X202)
| ~ iext(uri_rdf_rest,X201,X203)
| ~ iext(uri_rdf_first,X203,X204)
| ~ iext(uri_rdf_rest,X203,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,
! [X228,X229,X230,X231,X232,X233,X234] :
( ( ic(X228)
| ~ iext(uri_owl_unionOf,X228,X229)
| ~ iext(uri_rdf_first,X229,X230)
| ~ iext(uri_rdf_rest,X229,X231)
| ~ iext(uri_rdf_first,X231,X232)
| ~ iext(uri_rdf_rest,X231,uri_rdf_nil) )
& ( ic(X230)
| ~ iext(uri_owl_unionOf,X228,X229)
| ~ iext(uri_rdf_first,X229,X230)
| ~ iext(uri_rdf_rest,X229,X231)
| ~ iext(uri_rdf_first,X231,X232)
| ~ iext(uri_rdf_rest,X231,uri_rdf_nil) )
& ( ic(X232)
| ~ iext(uri_owl_unionOf,X228,X229)
| ~ iext(uri_rdf_first,X229,X230)
| ~ iext(uri_rdf_rest,X229,X231)
| ~ iext(uri_rdf_first,X231,X232)
| ~ iext(uri_rdf_rest,X231,uri_rdf_nil) )
& ( ~ icext(X228,X233)
| icext(X230,X233)
| icext(X232,X233)
| ~ iext(uri_owl_unionOf,X228,X229)
| ~ iext(uri_rdf_first,X229,X230)
| ~ iext(uri_rdf_rest,X229,X231)
| ~ iext(uri_rdf_first,X231,X232)
| ~ iext(uri_rdf_rest,X231,uri_rdf_nil) )
& ( ~ icext(X230,X234)
| icext(X228,X234)
| ~ iext(uri_owl_unionOf,X228,X229)
| ~ iext(uri_rdf_first,X229,X230)
| ~ iext(uri_rdf_rest,X229,X231)
| ~ iext(uri_rdf_first,X231,X232)
| ~ iext(uri_rdf_rest,X231,uri_rdf_nil) )
& ( ~ icext(X232,X234)
| icext(X228,X234)
| ~ iext(uri_owl_unionOf,X228,X229)
| ~ iext(uri_rdf_first,X229,X230)
| ~ iext(uri_rdf_rest,X229,X231)
| ~ iext(uri_rdf_first,X231,X232)
| ~ iext(uri_rdf_rest,X231,uri_rdf_nil) )
& ( ~ icext(X230,esk7_5(X228,X229,X230,X231,X232))
| ~ icext(X228,esk7_5(X228,X229,X230,X231,X232))
| ~ ic(X228)
| ~ ic(X230)
| ~ ic(X232)
| iext(uri_owl_unionOf,X228,X229)
| ~ iext(uri_rdf_first,X229,X230)
| ~ iext(uri_rdf_rest,X229,X231)
| ~ iext(uri_rdf_first,X231,X232)
| ~ iext(uri_rdf_rest,X231,uri_rdf_nil) )
& ( ~ icext(X232,esk7_5(X228,X229,X230,X231,X232))
| ~ icext(X228,esk7_5(X228,X229,X230,X231,X232))
| ~ ic(X228)
| ~ ic(X230)
| ~ ic(X232)
| iext(uri_owl_unionOf,X228,X229)
| ~ iext(uri_rdf_first,X229,X230)
| ~ iext(uri_rdf_rest,X229,X231)
| ~ iext(uri_rdf_first,X231,X232)
| ~ iext(uri_rdf_rest,X231,uri_rdf_nil) )
& ( icext(X228,esk7_5(X228,X229,X230,X231,X232))
| icext(X230,esk7_5(X228,X229,X230,X231,X232))
| icext(X232,esk7_5(X228,X229,X230,X231,X232))
| ~ ic(X228)
| ~ ic(X230)
| ~ ic(X232)
| iext(uri_owl_unionOf,X228,X229)
| ~ iext(uri_rdf_first,X229,X230)
| ~ iext(uri_rdf_rest,X229,X231)
| ~ iext(uri_rdf_first,X231,X232)
| ~ iext(uri_rdf_rest,X231,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,
! [X326,X327,X328,X329,X330,X331] :
( ( ~ icext(X326,X329)
| ~ iext(X327,X329,X330)
| icext(X328,X330)
| ~ iext(uri_owl_allValuesFrom,X326,X328)
| ~ iext(uri_owl_onProperty,X326,X327) )
& ( iext(X327,X331,esk17_4(X326,X327,X328,X331))
| icext(X326,X331)
| ~ iext(uri_owl_allValuesFrom,X326,X328)
| ~ iext(uri_owl_onProperty,X326,X327) )
& ( ~ icext(X328,esk17_4(X326,X327,X328,X331))
| icext(X326,X331)
| ~ iext(uri_owl_allValuesFrom,X326,X328)
| ~ iext(uri_owl_onProperty,X326,X327) ) ),
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,
! [X337,X338,X339,X340,X342,X343] :
( ( iext(X338,X340,esk18_4(X337,X338,X339,X340))
| ~ icext(X337,X340)
| ~ iext(uri_owl_someValuesFrom,X337,X339)
| ~ iext(uri_owl_onProperty,X337,X338) )
& ( icext(X339,esk18_4(X337,X338,X339,X340))
| ~ icext(X337,X340)
| ~ iext(uri_owl_someValuesFrom,X337,X339)
| ~ iext(uri_owl_onProperty,X337,X338) )
& ( ~ iext(X338,X342,X343)
| ~ icext(X339,X343)
| icext(X337,X342)
| ~ iext(uri_owl_someValuesFrom,X337,X339)
| ~ iext(uri_owl_onProperty,X337,X338) ) ),
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,
! [X222,X223,X224,X225,X226] :
( ( ic(X222)
| ~ iext(uri_owl_unionOf,X222,X223)
| ~ iext(uri_rdf_first,X223,X224)
| ~ iext(uri_rdf_rest,X223,uri_rdf_nil) )
& ( ic(X224)
| ~ iext(uri_owl_unionOf,X222,X223)
| ~ iext(uri_rdf_first,X223,X224)
| ~ iext(uri_rdf_rest,X223,uri_rdf_nil) )
& ( ~ icext(X222,X225)
| icext(X224,X225)
| ~ iext(uri_owl_unionOf,X222,X223)
| ~ iext(uri_rdf_first,X223,X224)
| ~ iext(uri_rdf_rest,X223,uri_rdf_nil) )
& ( ~ icext(X224,X226)
| icext(X222,X226)
| ~ iext(uri_owl_unionOf,X222,X223)
| ~ iext(uri_rdf_first,X223,X224)
| ~ iext(uri_rdf_rest,X223,uri_rdf_nil) )
& ( ~ icext(X222,esk6_3(X222,X223,X224))
| ~ icext(X224,esk6_3(X222,X223,X224))
| ~ ic(X222)
| ~ ic(X224)
| iext(uri_owl_unionOf,X222,X223)
| ~ iext(uri_rdf_first,X223,X224)
| ~ iext(uri_rdf_rest,X223,uri_rdf_nil) )
& ( icext(X222,esk6_3(X222,X223,X224))
| icext(X224,esk6_3(X222,X223,X224))
| ~ ic(X222)
| ~ ic(X224)
| iext(uri_owl_unionOf,X222,X223)
| ~ iext(uri_rdf_first,X223,X224)
| ~ iext(uri_rdf_rest,X223,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,
! [X194,X195,X196,X197,X198] :
( ( ic(X194)
| ~ iext(uri_owl_intersectionOf,X194,X195)
| ~ iext(uri_rdf_first,X195,X196)
| ~ iext(uri_rdf_rest,X195,uri_rdf_nil) )
& ( ic(X196)
| ~ iext(uri_owl_intersectionOf,X194,X195)
| ~ iext(uri_rdf_first,X195,X196)
| ~ iext(uri_rdf_rest,X195,uri_rdf_nil) )
& ( ~ icext(X194,X197)
| icext(X196,X197)
| ~ iext(uri_owl_intersectionOf,X194,X195)
| ~ iext(uri_rdf_first,X195,X196)
| ~ iext(uri_rdf_rest,X195,uri_rdf_nil) )
& ( ~ icext(X196,X198)
| icext(X194,X198)
| ~ iext(uri_owl_intersectionOf,X194,X195)
| ~ iext(uri_rdf_first,X195,X196)
| ~ iext(uri_rdf_rest,X195,uri_rdf_nil) )
& ( ~ icext(X194,esk2_3(X194,X195,X196))
| ~ icext(X196,esk2_3(X194,X195,X196))
| ~ ic(X194)
| ~ ic(X196)
| iext(uri_owl_intersectionOf,X194,X195)
| ~ iext(uri_rdf_first,X195,X196)
| ~ iext(uri_rdf_rest,X195,uri_rdf_nil) )
& ( icext(X194,esk2_3(X194,X195,X196))
| icext(X196,esk2_3(X194,X195,X196))
| ~ ic(X194)
| ~ ic(X196)
| iext(uri_owl_intersectionOf,X194,X195)
| ~ iext(uri_rdf_first,X195,X196)
| ~ iext(uri_rdf_rest,X195,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,
! [X333,X334,X335,X336] :
( ( ~ icext(X333,X336)
| iext(X334,X336,X335)
| ~ iext(uri_owl_hasValue,X333,X335)
| ~ iext(uri_owl_onProperty,X333,X334) )
& ( ~ iext(X334,X336,X335)
| icext(X333,X336)
| ~ iext(uri_owl_hasValue,X333,X335)
| ~ iext(uri_owl_onProperty,X333,X334) ) ),
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,
! [X318,X319,X320,X321,X322,X323] :
( ( ip(X318)
| ~ iext(uri_rdfs_subPropertyOf,X318,X319) )
& ( ip(X319)
| ~ iext(uri_rdfs_subPropertyOf,X318,X319) )
& ( ~ iext(X318,X320,X321)
| iext(X319,X320,X321)
| ~ iext(uri_rdfs_subPropertyOf,X318,X319) )
& ( iext(X322,esk15_2(X322,X323),esk16_2(X322,X323))
| ~ ip(X322)
| ~ ip(X323)
| iext(uri_rdfs_subPropertyOf,X322,X323) )
& ( ~ iext(X323,esk15_2(X322,X323),esk16_2(X322,X323))
| ~ ip(X322)
| ~ ip(X323)
| iext(uri_rdfs_subPropertyOf,X322,X323) ) ),
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,
! [X368,X369,X370,X371] :
( ( ip(X368)
| ~ iext(uri_rdfs_subPropertyOf,X368,X369) )
& ( ip(X369)
| ~ iext(uri_rdfs_subPropertyOf,X368,X369) )
& ( ~ iext(X368,X370,X371)
| iext(X369,X370,X371)
| ~ iext(uri_rdfs_subPropertyOf,X368,X369) ) ),
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,
! [X373,X374,X375] :
( ~ iext(uri_rdfs_subPropertyOf,X373,X374)
| ~ iext(uri_rdfs_subPropertyOf,X374,X375)
| iext(uri_rdfs_subPropertyOf,X373,X375) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[rdfs_subpropertyof_trans])]) ).
fof(i_0_152,plain,
! [X365,X366,X367] :
( ~ iext(uri_rdfs_subClassOf,X365,X366)
| ~ iext(uri_rdfs_subClassOf,X366,X367)
| iext(uri_rdfs_subClassOf,X365,X367) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[rdfs_subclassof_trans])]) ).
fof(i_0_153,plain,
! [X350,X351,X352,X353] :
( ~ iext(uri_rdfs_domain,X350,X351)
| ~ iext(X350,X352,X353)
| icext(X351,X352) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[rdfs_domain_main])]) ).
fof(i_0_154,plain,
! [X357,X358,X359,X360] :
( ~ iext(uri_rdfs_range,X357,X358)
| ~ iext(X357,X359,X360)
| icext(X358,X360) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[rdfs_range_main])]) ).
fof(i_0_155,plain,
! [X296,X297,X298,X299,X300,X301] :
( ( ip(X296)
| ~ iext(uri_rdfs_domain,X296,X297) )
& ( ic(X297)
| ~ iext(uri_rdfs_domain,X296,X297) )
& ( ~ iext(X296,X298,X299)
| icext(X297,X298)
| ~ iext(uri_rdfs_domain,X296,X297) )
& ( iext(X300,esk10_2(X300,X301),esk11_2(X300,X301))
| ~ ip(X300)
| ~ ic(X301)
| iext(uri_rdfs_domain,X300,X301) )
& ( ~ icext(X301,esk10_2(X300,X301))
| ~ ip(X300)
| ~ ic(X301)
| iext(uri_rdfs_domain,X300,X301) ) ),
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,
! [X304,X305,X306,X307,X308,X309] :
( ( ip(X304)
| ~ iext(uri_rdfs_range,X304,X305) )
& ( ip(X305)
| ~ iext(uri_rdfs_range,X304,X305) )
& ( ~ iext(X304,X306,X307)
| icext(X305,X307)
| ~ iext(uri_rdfs_range,X304,X305) )
& ( iext(X308,esk12_2(X308,X309),esk13_2(X308,X309))
| ~ ip(X308)
| ~ ip(X309)
| iext(uri_rdfs_range,X308,X309) )
& ( ~ icext(X309,esk13_2(X308,X309))
| ~ ip(X308)
| ~ ip(X309)
| iext(uri_rdfs_range,X308,X309) ) ),
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,
! [X381,X382] :
( ~ iext(uri_ex_p,X381,X382)
| ~ iext(uri_ex_q,X382,X381) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[i_0_131])]) ).
fof(i_0_158,plain,
! [X312,X313,X314,X315,X316] :
( ( ic(X312)
| ~ iext(uri_rdfs_subClassOf,X312,X313) )
& ( ic(X313)
| ~ iext(uri_rdfs_subClassOf,X312,X313) )
& ( ~ icext(X312,X314)
| icext(X313,X314)
| ~ iext(uri_rdfs_subClassOf,X312,X313) )
& ( icext(X315,esk14_2(X315,X316))
| ~ ic(X315)
| ~ ic(X316)
| iext(uri_rdfs_subClassOf,X315,X316) )
& ( ~ icext(X316,esk14_2(X315,X316))
| ~ ic(X315)
| ~ ic(X316)
| iext(uri_rdfs_subClassOf,X315,X316) ) ),
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,
! [X186,X187,X188] :
( ( ic(X186)
| ~ iext(uri_owl_complementOf,X186,X187) )
& ( ic(X187)
| ~ iext(uri_owl_complementOf,X186,X187) )
& ( ~ icext(X186,X188)
| ~ icext(X187,X188)
| ~ iext(uri_owl_complementOf,X186,X187) )
& ( icext(X187,X188)
| icext(X186,X188)
| ~ iext(uri_owl_complementOf,X186,X187) ) ),
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,
! [X361,X362,X363] :
( ( ic(X361)
| ~ iext(uri_rdfs_subClassOf,X361,X362) )
& ( ic(X362)
| ~ iext(uri_rdfs_subClassOf,X361,X362) )
& ( ~ icext(X361,X363)
| icext(X362,X363)
| ~ iext(uri_rdfs_subClassOf,X361,X362) ) ),
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,
! [X218,X219,X220] :
( ( ic(X218)
| ~ iext(uri_owl_unionOf,X218,uri_rdf_nil) )
& ( ~ icext(X218,X219)
| ~ iext(uri_owl_unionOf,X218,uri_rdf_nil) )
& ( ~ ic(X220)
| icext(X220,esk5_1(X220))
| iext(uri_owl_unionOf,X220,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,
! [X345,X346] :
( ( ~ iext(uri_rdf_type,X345,X346)
| icext(X346,X345) )
& ( ~ icext(X346,X345)
| iext(uri_rdf_type,X345,X346) ) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[rdfs_cext_def])]) ).
fof(i_0_163,plain,
! [X266,X267,X268] :
( ( ix(X267)
| ~ iext(X266,X267,X268)
| ~ ioxp(X266) )
& ( ix(X268)
| ~ iext(X266,X267,X268)
| ~ ioxp(X266) ) ),
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,
! [X261,X262,X263] :
( ( ir(X262)
| ~ iext(X261,X262,X263)
| ~ iodp(X261) )
& ( lv(X263)
| ~ iext(X261,X262,X263)
| ~ iodp(X261) ) ),
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,
! [X294,X295] :
( ( ic(X294)
| ~ iext(uri_owl_unionOf,X294,X295) )
& ( icext(uri_rdf_List,X295)
| ~ iext(uri_owl_unionOf,X294,X295) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[owl_prop_unionof_ext])])]) ).
fof(i_0_166,plain,
! [X288,X289] :
( ( ic(X288)
| ~ iext(uri_owl_intersectionOf,X288,X289) )
& ( icext(uri_rdf_List,X289)
| ~ iext(uri_owl_intersectionOf,X288,X289) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[owl_prop_intersectionof_ext])])]) ).
fof(i_0_167,plain,
! [X292,X293] :
( ( icext(uri_owl_Restriction,X292)
| ~ iext(uri_owl_someValuesFrom,X292,X293) )
& ( ic(X293)
| ~ iext(uri_owl_someValuesFrom,X292,X293) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[owl_prop_somevaluesfrom_ext])])]) ).
fof(i_0_168,plain,
! [X290,X291] :
( ( icext(uri_owl_Restriction,X290)
| ~ iext(uri_owl_onProperty,X290,X291) )
& ( ip(X291)
| ~ iext(uri_owl_onProperty,X290,X291) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[owl_prop_onproperty_ext])])]) ).
fof(i_0_169,plain,
! [X286,X287] :
( ( icext(uri_owl_Restriction,X286)
| ~ iext(uri_owl_hasValue,X286,X287) )
& ( ir(X287)
| ~ iext(uri_owl_hasValue,X286,X287) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[owl_prop_hasvalue_ext])])]) ).
fof(i_0_170,plain,
! [X282,X283] :
( ( icext(uri_owl_Restriction,X282)
| ~ iext(uri_owl_allValuesFrom,X282,X283) )
& ( ic(X283)
| ~ iext(uri_owl_allValuesFrom,X282,X283) ) ),
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,
! [X376,X377,X378] :
( ~ iext(X377,X376,X378)
| ip(X377) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[simple_iext_property])]) ).
fof(i_0_175,plain,
! [X284,X285] :
( ( ic(X284)
| ~ iext(uri_owl_complementOf,X284,X285) )
& ( ic(X285)
| ~ iext(uri_owl_complementOf,X284,X285) ) ),
inference(distribute,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[owl_prop_complementof_ext])])]) ).
fof(i_0_176,plain,
! [X279] :
( ( ~ ix(X279)
| iext(uri_rdf_type,X279,uri_owl_Ontology) )
& ( ~ iext(uri_rdf_type,X279,uri_owl_Ontology)
| ix(X279) ) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[owl_parts_ix_def])]) ).
fof(i_0_177,plain,
! [X270] :
( ( ~ ioxp(X270)
| iext(uri_rdf_type,X270,uri_owl_OntologyProperty) )
& ( ~ iext(uri_rdf_type,X270,uri_owl_OntologyProperty)
| ioxp(X270) ) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[owl_parts_ioxp_def])]) ).
fof(i_0_178,plain,
! [X265] :
( ( ~ iodp(X265)
| iext(uri_rdf_type,X265,uri_owl_DatatypeProperty) )
& ( ~ iext(uri_rdf_type,X265,uri_owl_DatatypeProperty)
| iodp(X265) ) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[owl_parts_iodp_def])]) ).
fof(i_0_179,plain,
! [X344] :
( ( ~ iext(uri_rdf_type,X344,uri_rdf_Property)
| ip(X344) )
& ( ~ ip(X344)
| iext(uri_rdf_type,X344,uri_rdf_Property) ) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[rdf_type_ip])]) ).
fof(i_0_180,plain,
! [X275] :
( ( ~ ip(X275)
| iext(uri_rdf_type,X275,uri_rdf_Property) )
& ( ~ iext(uri_rdf_type,X275,uri_rdf_Property)
| ip(X275) ) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[owl_parts_ip_def])]) ).
fof(i_0_181,plain,
! [X260] :
( ( ~ ioap(X260)
| iext(uri_rdf_type,X260,uri_owl_AnnotationProperty) )
& ( ~ iext(uri_rdf_type,X260,uri_owl_AnnotationProperty)
| ioap(X260) ) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[owl_parts_ioap_def])]) ).
fof(i_0_182,plain,
! [X281] :
( ( ~ lv(X281)
| iext(uri_rdf_type,X281,uri_rdfs_Literal) )
& ( ~ iext(uri_rdf_type,X281,uri_rdfs_Literal)
| lv(X281) ) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[owl_parts_lv_def])]) ).
fof(i_0_183,plain,
! [X255] :
( ( ~ idc(X255)
| iext(uri_rdf_type,X255,uri_rdfs_Datatype) )
& ( ~ iext(uri_rdf_type,X255,uri_rdfs_Datatype)
| idc(X255) ) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[owl_parts_idc_def])]) ).
fof(i_0_184,plain,
! [X251] :
( ( ~ ic(X251)
| iext(uri_rdf_type,X251,uri_rdfs_Class) )
& ( ~ iext(uri_rdf_type,X251,uri_rdfs_Class)
| ic(X251) ) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[owl_parts_ic_def])]) ).
fof(i_0_185,plain,
! [X348] :
( ~ icext(uri_rdfs_ContainerMembershipProperty,X348)
| iext(uri_rdfs_subPropertyOf,X348,uri_rdfs_member) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[rdfs_container_containermembershipproperty_instsub_member])]) ).
fof(i_0_186,plain,
! [X349] :
( ~ icext(uri_rdfs_Datatype,X349)
| iext(uri_rdfs_subClassOf,X349,uri_rdfs_Literal) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[rdfs_datatype_instsub_literal])]) ).
fof(i_0_187,plain,
! [X372] :
( ~ ip(X372)
| iext(uri_rdfs_subPropertyOf,X372,X372) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[rdfs_subpropertyof_reflex])]) ).
fof(i_0_188,plain,
! [X364] :
( ~ ic(X364)
| iext(uri_rdfs_subClassOf,X364,X364) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[rdfs_subclassof_reflex])]) ).
fof(i_0_189,plain,
! [X347] :
( ~ ic(X347)
| iext(uri_rdfs_subClassOf,X347,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,
( iext(uri_ex_p,uri_ex_s,esk19_0)
& iext(uri_ex_q,esk19_0,uri_ex_s) ),
inference(skolemize,[status(esa)],[inference(variable_rename,[status(thm)],[testcase_premise_fullish_002_Existential_Blank_Nodes])]) ).
fof(i_0_192,plain,
! [X252,X253] :
( ~ idc(X252)
| ~ icext(X252,X253)
| lv(X253) ),
inference(shift_quantors,[status(thm)],[inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[owl_parts_idc_cond_inst])])]) ).
fof(i_0_193,plain,
! [X356] :
( ( ~ lv(X356)
| icext(uri_rdfs_Literal,X356) )
& ( ~ icext(uri_rdfs_Literal,X356)
| lv(X356) ) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[rdfs_lv_def])]) ).
fof(i_0_194,plain,
! [X354] :
( ( ~ ic(X354)
| icext(uri_rdfs_Class,X354) )
& ( ~ icext(uri_rdfs_Class,X354)
| ic(X354) ) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[rdfs_ic_def])]) ).
fof(i_0_195,plain,
! [X246] : ~ icext(uri_owl_Nothing,X246),
inference(variable_rename,[status(thm)],[i_0_137]) ).
cnf(i_0_196,plain,
( icext(uri_rdfs_Resource,X1)
| ~ ir(X1) ),
inference(split_conjunct,[status(thm)],[i_0_138]) ).
cnf(i_0_197,plain,
( icext(uri_owl_Thing,X1)
| ~ ir(X1) ),
inference(split_conjunct,[status(thm)],[i_0_139]) ).
fof(i_0_198,plain,
! [X269] :
( ~ ioxp(X269)
| ip(X269) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[owl_parts_ioxp_cond_set])]) ).
fof(i_0_199,plain,
! [X264] :
( ~ iodp(X264)
| ip(X264) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[owl_parts_iodp_cond_set])]) ).
fof(i_0_200,plain,
! [X259] :
( ~ ioap(X259)
| ip(X259) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[owl_parts_ioap_cond_set])]) ).
fof(i_0_201,plain,
! [X254] :
( ~ idc(X254)
| ic(X254) ),
inference(variable_rename,[status(thm)],[inference(fof_nnf,[status(thm)],[owl_parts_idc_cond_set])]) ).
cnf(i_0_202,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_203,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_204,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_205,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_206,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_207,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_208,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_209,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_210,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_211,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_212,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_213,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_214,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_215,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_216,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_217,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_218,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_219,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_220,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_221,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_222,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_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,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_224,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_225,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_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,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_227,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_228,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_229,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_230,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_231,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_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,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_233,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_234,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_235,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_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,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_237,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_238,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_239,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_240,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_241,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_242,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_243,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_244,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_245,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_246,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_247,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_248,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_249,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_250,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_251,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_252,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_253,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_254,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_255,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_256,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_257,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_258,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_259,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_260,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_261,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_262,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_263,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_264,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_265,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_266,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_267,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_268,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_269,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_270,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_271,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_272,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_273,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_274,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_275,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_276,negated_conjecture,
( ~ iext(uri_ex_p,X1,X2)
| ~ iext(uri_ex_q,X2,X1) ),
inference(split_conjunct,[status(thm)],[i_0_157]),
[final] ).
cnf(i_0_277,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_278,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_279,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_280,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_281,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_282,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_283,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_284,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_285,plain,
( ~ icext(X1,X2)
| ~ iext(uri_owl_unionOf,X1,uri_rdf_nil) ),
inference(split_conjunct,[status(thm)],[i_0_161]),
[final] ).
cnf(i_0_286,plain,
( icext(X2,X1)
| ~ iext(uri_rdf_type,X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_162]),
[final] ).
cnf(i_0_287,plain,
( ix(X1)
| ~ iext(X2,X1,X3)
| ~ ioxp(X2) ),
inference(split_conjunct,[status(thm)],[i_0_163]),
[final] ).
cnf(i_0_288,plain,
( ix(X1)
| ~ iext(X2,X3,X1)
| ~ ioxp(X2) ),
inference(split_conjunct,[status(thm)],[i_0_163]),
[final] ).
cnf(i_0_289,plain,
( lv(X1)
| ~ iext(X2,X3,X1)
| ~ iodp(X2) ),
inference(split_conjunct,[status(thm)],[i_0_164]),
[final] ).
cnf(i_0_290,plain,
( icext(uri_rdf_List,X1)
| ~ iext(uri_owl_unionOf,X2,X1) ),
inference(split_conjunct,[status(thm)],[i_0_165]),
[final] ).
cnf(i_0_291,plain,
( icext(uri_rdf_List,X1)
| ~ iext(uri_owl_intersectionOf,X2,X1) ),
inference(split_conjunct,[status(thm)],[i_0_166]),
[final] ).
cnf(i_0_292,plain,
( icext(uri_owl_Restriction,X1)
| ~ iext(uri_owl_someValuesFrom,X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_167]),
[final] ).
cnf(i_0_293,plain,
( icext(uri_owl_Restriction,X1)
| ~ iext(uri_owl_onProperty,X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_168]),
[final] ).
cnf(i_0_294,plain,
( icext(uri_owl_Restriction,X1)
| ~ iext(uri_owl_hasValue,X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_169]),
[final] ).
cnf(i_0_295,plain,
( icext(uri_owl_Restriction,X1)
| ~ iext(uri_owl_allValuesFrom,X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_170]),
[final] ).
cnf(i_0_296,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_297,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_298,plain,
( ip(X1)
| ~ iext(X1,X2,X3) ),
inference(split_conjunct,[status(thm)],[i_0_174]),
[final] ).
cnf(i_0_299,plain,
( ip(X1)
| ~ iext(uri_rdfs_subPropertyOf,X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_150]),
[final] ).
cnf(i_0_300,plain,
( ip(X1)
| ~ iext(uri_rdfs_subPropertyOf,X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_149]),
[final] ).
cnf(i_0_301,plain,
( ip(X1)
| ~ iext(uri_rdfs_subPropertyOf,X2,X1) ),
inference(split_conjunct,[status(thm)],[i_0_150]),
[final] ).
cnf(i_0_302,plain,
( ip(X1)
| ~ iext(uri_rdfs_subPropertyOf,X2,X1) ),
inference(split_conjunct,[status(thm)],[i_0_149]),
[final] ).
cnf(i_0_303,plain,
( ip(X1)
| ~ iext(uri_rdfs_range,X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_156]),
[final] ).
cnf(i_0_304,plain,
( ip(X1)
| ~ iext(uri_rdfs_range,X2,X1) ),
inference(split_conjunct,[status(thm)],[i_0_156]),
[final] ).
cnf(i_0_305,plain,
( ip(X1)
| ~ iext(uri_rdfs_domain,X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_155]),
[final] ).
cnf(i_0_306,plain,
( ip(X1)
| ~ iext(uri_owl_onProperty,X2,X1) ),
inference(split_conjunct,[status(thm)],[i_0_168]),
[final] ).
cnf(i_0_307,plain,
( ic(X1)
| ~ iext(uri_rdfs_subClassOf,X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_160]),
[final] ).
cnf(i_0_308,plain,
( ic(X1)
| ~ iext(uri_rdfs_subClassOf,X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_158]),
[final] ).
cnf(i_0_309,plain,
( ic(X1)
| ~ iext(uri_rdfs_subClassOf,X2,X1) ),
inference(split_conjunct,[status(thm)],[i_0_160]),
[final] ).
cnf(i_0_310,plain,
( ic(X1)
| ~ iext(uri_rdfs_subClassOf,X2,X1) ),
inference(split_conjunct,[status(thm)],[i_0_158]),
[final] ).
cnf(i_0_311,plain,
( ic(X1)
| ~ iext(uri_rdfs_domain,X2,X1) ),
inference(split_conjunct,[status(thm)],[i_0_155]),
[final] ).
cnf(i_0_312,plain,
( ic(X1)
| ~ iext(uri_owl_someValuesFrom,X2,X1) ),
inference(split_conjunct,[status(thm)],[i_0_167]),
[final] ).
cnf(i_0_313,plain,
( ic(X1)
| ~ iext(uri_owl_allValuesFrom,X2,X1) ),
inference(split_conjunct,[status(thm)],[i_0_170]),
[final] ).
cnf(i_0_314,plain,
( ic(X1)
| ~ iext(uri_owl_unionOf,X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_165]),
[final] ).
cnf(i_0_315,plain,
( ic(X1)
| ~ iext(uri_owl_intersectionOf,X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_166]),
[final] ).
cnf(i_0_316,plain,
( ic(X1)
| ~ iext(uri_owl_complementOf,X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_175]),
[final] ).
cnf(i_0_317,plain,
( ic(X1)
| ~ iext(uri_owl_complementOf,X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_159]),
[final] ).
cnf(i_0_318,plain,
( ic(X1)
| ~ iext(uri_owl_complementOf,X2,X1) ),
inference(split_conjunct,[status(thm)],[i_0_175]),
[final] ).
cnf(i_0_319,plain,
( ic(X1)
| ~ iext(uri_owl_complementOf,X2,X1) ),
inference(split_conjunct,[status(thm)],[i_0_159]),
[final] ).
cnf(i_0_320,plain,
( ix(X1)
| ~ iext(uri_rdf_type,X1,uri_owl_Ontology) ),
inference(split_conjunct,[status(thm)],[i_0_176]),
[final] ).
cnf(i_0_321,plain,
( ioxp(X1)
| ~ iext(uri_rdf_type,X1,uri_owl_OntologyProperty) ),
inference(split_conjunct,[status(thm)],[i_0_177]),
[final] ).
cnf(i_0_322,plain,
( iodp(X1)
| ~ iext(uri_rdf_type,X1,uri_owl_DatatypeProperty) ),
inference(split_conjunct,[status(thm)],[i_0_178]),
[final] ).
cnf(i_0_323,plain,
( ip(X1)
| ~ iext(uri_rdf_type,X1,uri_rdf_Property) ),
inference(split_conjunct,[status(thm)],[i_0_179]),
[final] ).
cnf(i_0_324,plain,
( ip(X1)
| ~ iext(uri_rdf_type,X1,uri_rdf_Property) ),
inference(split_conjunct,[status(thm)],[i_0_180]),
[final] ).
cnf(i_0_325,plain,
( ioap(X1)
| ~ iext(uri_rdf_type,X1,uri_owl_AnnotationProperty) ),
inference(split_conjunct,[status(thm)],[i_0_181]),
[final] ).
cnf(i_0_326,plain,
( lv(X1)
| ~ iext(uri_rdf_type,X1,uri_rdfs_Literal) ),
inference(split_conjunct,[status(thm)],[i_0_182]),
[final] ).
cnf(i_0_327,plain,
( idc(X1)
| ~ iext(uri_rdf_type,X1,uri_rdfs_Datatype) ),
inference(split_conjunct,[status(thm)],[i_0_183]),
[final] ).
cnf(i_0_328,plain,
( ic(X1)
| ~ iext(uri_rdf_type,X1,uri_rdfs_Class) ),
inference(split_conjunct,[status(thm)],[i_0_184]),
[final] ).
cnf(i_0_329,plain,
( ic(X1)
| ~ iext(uri_owl_unionOf,X1,uri_rdf_nil) ),
inference(split_conjunct,[status(thm)],[i_0_161]),
[final] ).
cnf(i_0_330,plain,
( ic(X1)
| ~ iext(uri_owl_intersectionOf,X1,uri_rdf_nil) ),
inference(split_conjunct,[status(thm)],[i_0_134]),
[final] ).
cnf(i_0_331,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_332,plain,
( iext(uri_rdf_type,X2,X1)
| ~ icext(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_162]),
[final] ).
cnf(i_0_333,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_334,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_335,plain,
( iext(uri_rdfs_subPropertyOf,X1,X1)
| ~ ip(X1) ),
inference(split_conjunct,[status(thm)],[i_0_187]),
[final] ).
cnf(i_0_336,plain,
( iext(uri_rdfs_subClassOf,X1,X1)
| ~ ic(X1) ),
inference(split_conjunct,[status(thm)],[i_0_188]),
[final] ).
cnf(i_0_337,plain,
( iext(uri_rdfs_subClassOf,X1,uri_rdfs_Resource)
| ~ ic(X1) ),
inference(split_conjunct,[status(thm)],[i_0_189]),
[final] ).
cnf(i_0_338,plain,
( iext(uri_rdf_type,X1,uri_rdfs_Literal)
| ~ lv(X1) ),
inference(split_conjunct,[status(thm)],[i_0_182]),
[final] ).
cnf(i_0_339,plain,
( iext(uri_rdf_type,X1,uri_owl_Ontology)
| ~ ix(X1) ),
inference(split_conjunct,[status(thm)],[i_0_176]),
[final] ).
cnf(i_0_340,plain,
( iext(uri_rdf_type,X1,uri_rdf_Property)
| ~ ip(X1) ),
inference(split_conjunct,[status(thm)],[i_0_179]),
[final] ).
cnf(i_0_341,plain,
( iext(uri_rdf_type,X1,uri_rdf_Property)
| ~ ip(X1) ),
inference(split_conjunct,[status(thm)],[i_0_180]),
[final] ).
cnf(i_0_342,plain,
( iext(uri_rdf_type,X1,uri_owl_OntologyProperty)
| ~ ioxp(X1) ),
inference(split_conjunct,[status(thm)],[i_0_177]),
[final] ).
cnf(i_0_343,plain,
( iext(uri_rdf_type,X1,uri_owl_DatatypeProperty)
| ~ iodp(X1) ),
inference(split_conjunct,[status(thm)],[i_0_178]),
[final] ).
cnf(i_0_344,plain,
( iext(uri_rdf_type,X1,uri_owl_AnnotationProperty)
| ~ ioap(X1) ),
inference(split_conjunct,[status(thm)],[i_0_181]),
[final] ).
cnf(i_0_345,plain,
( iext(uri_rdf_type,X1,uri_rdfs_Datatype)
| ~ idc(X1) ),
inference(split_conjunct,[status(thm)],[i_0_183]),
[final] ).
cnf(i_0_346,plain,
( iext(uri_rdf_type,X1,uri_rdfs_Class)
| ~ ic(X1) ),
inference(split_conjunct,[status(thm)],[i_0_184]),
[final] ).
cnf(i_0_347,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_348,plain,
iext(uri_ex_q,esk19_0,uri_ex_s),
inference(split_conjunct,[status(thm)],[i_0_191]),
[final] ).
cnf(i_0_349,plain,
iext(uri_ex_p,uri_ex_s,esk19_0),
inference(split_conjunct,[status(thm)],[i_0_191]),
[final] ).
cnf(i_0_350,plain,
iext(uri_rdfs_subPropertyOf,uri_rdfs_isDefinedBy,uri_rdfs_seeAlso),
inference(split_conjunct,[status(thm)],[rdfs_annotation_isdefinedby_sub]),
[final] ).
cnf(i_0_351,plain,
iext(uri_rdfs_subClassOf,uri_rdf_XMLLiteral,uri_rdfs_Literal),
inference(split_conjunct,[status(thm)],[rdfs_dat_xmlliteral_sub]),
[final] ).
cnf(i_0_352,plain,
iext(uri_rdfs_subClassOf,uri_rdfs_Seq,uri_rdfs_Container),
inference(split_conjunct,[status(thm)],[rdfs_container_seq_sub]),
[final] ).
cnf(i_0_353,plain,
iext(uri_rdfs_subClassOf,uri_rdfs_ContainerMembershipProperty,uri_rdf_Property),
inference(split_conjunct,[status(thm)],[rdfs_container_containermembershipproperty_sub]),
[final] ).
cnf(i_0_354,plain,
iext(uri_rdfs_subClassOf,uri_rdf_Bag,uri_rdfs_Container),
inference(split_conjunct,[status(thm)],[rdfs_container_bag_sub]),
[final] ).
cnf(i_0_355,plain,
iext(uri_rdfs_subClassOf,uri_rdf_Alt,uri_rdfs_Container),
inference(split_conjunct,[status(thm)],[rdfs_container_alt_sub]),
[final] ).
cnf(i_0_356,plain,
iext(uri_rdfs_subClassOf,uri_rdfs_Datatype,uri_rdfs_Class),
inference(split_conjunct,[status(thm)],[rdfs_datatype_sub]),
[final] ).
cnf(i_0_357,plain,
iext(uri_rdfs_range,uri_rdf_predicate,uri_rdfs_Resource),
inference(split_conjunct,[status(thm)],[rdfs_reification_predicate_range]),
[final] ).
cnf(i_0_358,plain,
iext(uri_rdfs_range,uri_rdf_predicate,uri_rdfs_Resource),
inference(split_conjunct,[status(thm)],[rdfs_reification_object_range]),
[final] ).
cnf(i_0_359,plain,
iext(uri_rdfs_range,uri_rdfs_member,uri_rdfs_Resource),
inference(split_conjunct,[status(thm)],[rdfs_container_member_range]),
[final] ).
cnf(i_0_360,plain,
iext(uri_rdfs_range,uri_rdfs_label,uri_rdfs_Literal),
inference(split_conjunct,[status(thm)],[rdfs_annotation_label_range]),
[final] ).
cnf(i_0_361,plain,
iext(uri_rdfs_range,uri_rdfs_seeAlso,uri_rdfs_Resource),
inference(split_conjunct,[status(thm)],[rdfs_annotation_seealso_range]),
[final] ).
cnf(i_0_362,plain,
iext(uri_rdfs_range,uri_rdfs_isDefinedBy,uri_rdfs_Resource),
inference(split_conjunct,[status(thm)],[rdfs_annotation_isdefinedby_range]),
[final] ).
cnf(i_0_363,plain,
iext(uri_rdfs_range,uri_rdfs_comment,uri_rdfs_Literal),
inference(split_conjunct,[status(thm)],[rdfs_annotation_comment_range]),
[final] ).
cnf(i_0_364,plain,
iext(uri_rdfs_range,uri_rdf_subject,uri_rdfs_Resource),
inference(split_conjunct,[status(thm)],[rdfs_reification_subject_range]),
[final] ).
cnf(i_0_365,plain,
iext(uri_rdfs_range,uri_rdf_value,uri_rdfs_Resource),
inference(split_conjunct,[status(thm)],[rdfs_value_range]),
[final] ).
cnf(i_0_366,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_367,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_368,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_369,plain,
iext(uri_rdfs_range,uri_rdfs_subPropertyOf,uri_rdf_Property),
inference(split_conjunct,[status(thm)],[rdfs_subpropertyof_range]),
[final] ).
cnf(i_0_370,plain,
iext(uri_rdfs_range,uri_rdfs_subClassOf,uri_rdfs_Class),
inference(split_conjunct,[status(thm)],[rdfs_subclassof_range]),
[final] ).
cnf(i_0_371,plain,
iext(uri_rdfs_range,uri_rdfs_range,uri_rdfs_Class),
inference(split_conjunct,[status(thm)],[rdfs_range_range]),
[final] ).
cnf(i_0_372,plain,
iext(uri_rdfs_range,uri_rdfs_domain,uri_rdfs_Class),
inference(split_conjunct,[status(thm)],[rdfs_domain_range]),
[final] ).
cnf(i_0_373,plain,
iext(uri_rdfs_range,uri_rdf_type,uri_rdfs_Class),
inference(split_conjunct,[status(thm)],[rdfs_type_range]),
[final] ).
cnf(i_0_374,plain,
iext(uri_rdfs_range,uri_rdf_rest,uri_rdf_List),
inference(split_conjunct,[status(thm)],[rdfs_collection_rest_range]),
[final] ).
cnf(i_0_375,plain,
iext(uri_rdfs_range,uri_rdf_first,uri_rdfs_Resource),
inference(split_conjunct,[status(thm)],[rdfs_collection_first_range]),
[final] ).
cnf(i_0_376,plain,
iext(uri_rdfs_domain,uri_rdf_predicate,uri_rdfs_Statement),
inference(split_conjunct,[status(thm)],[rdfs_reification_predicate_domain]),
[final] ).
cnf(i_0_377,plain,
iext(uri_rdfs_domain,uri_rdfs_member,uri_rdfs_Resource),
inference(split_conjunct,[status(thm)],[rdfs_container_member_domain]),
[final] ).
cnf(i_0_378,plain,
iext(uri_rdfs_domain,uri_rdfs_label,uri_rdfs_Resource),
inference(split_conjunct,[status(thm)],[rdfs_annotation_label_domain]),
[final] ).
cnf(i_0_379,plain,
iext(uri_rdfs_domain,uri_rdfs_seeAlso,uri_rdfs_Resource),
inference(split_conjunct,[status(thm)],[rdfs_annotation_seealso_domain]),
[final] ).
cnf(i_0_380,plain,
iext(uri_rdfs_domain,uri_rdfs_isDefinedBy,uri_rdfs_Resource),
inference(split_conjunct,[status(thm)],[rdfs_annotation_isdefinedby_domain]),
[final] ).
cnf(i_0_381,plain,
iext(uri_rdfs_domain,uri_rdfs_comment,uri_rdfs_Resource),
inference(split_conjunct,[status(thm)],[rdfs_annotation_comment_domain]),
[final] ).
cnf(i_0_382,plain,
iext(uri_rdfs_domain,uri_rdf_subject,uri_rdfs_Statement),
inference(split_conjunct,[status(thm)],[rdfs_reification_subject_domain]),
[final] ).
cnf(i_0_383,plain,
iext(uri_rdfs_domain,uri_rdf_value,uri_rdfs_Resource),
inference(split_conjunct,[status(thm)],[rdfs_value_domain]),
[final] ).
cnf(i_0_384,plain,
iext(uri_rdfs_domain,uri_rdf_object,uri_rdfs_Statement),
inference(split_conjunct,[status(thm)],[rdfs_reification_object_domain]),
[final] ).
cnf(i_0_385,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_386,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_387,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_388,plain,
iext(uri_rdfs_domain,uri_rdfs_subPropertyOf,uri_rdf_Property),
inference(split_conjunct,[status(thm)],[rdfs_subpropertyof_domain]),
[final] ).
cnf(i_0_389,plain,
iext(uri_rdfs_domain,uri_rdfs_subClassOf,uri_rdfs_Class),
inference(split_conjunct,[status(thm)],[rdfs_subclassof_domain]),
[final] ).
cnf(i_0_390,plain,
iext(uri_rdfs_domain,uri_rdfs_range,uri_rdf_Property),
inference(split_conjunct,[status(thm)],[rdfs_range_domain]),
[final] ).
cnf(i_0_391,plain,
iext(uri_rdfs_domain,uri_rdfs_domain,uri_rdf_Property),
inference(split_conjunct,[status(thm)],[rdfs_domain_domain]),
[final] ).
cnf(i_0_392,plain,
iext(uri_rdfs_domain,uri_rdf_type,uri_rdfs_Resource),
inference(split_conjunct,[status(thm)],[rdfs_type_domain]),
[final] ).
cnf(i_0_393,plain,
iext(uri_rdfs_domain,uri_rdf_rest,uri_rdf_List),
inference(split_conjunct,[status(thm)],[rdfs_collection_rest_domain]),
[final] ).
cnf(i_0_394,plain,
iext(uri_rdfs_domain,uri_rdf_first,uri_rdf_List),
inference(split_conjunct,[status(thm)],[rdfs_collection_first_domain]),
[final] ).
cnf(i_0_395,plain,
iext(uri_rdf_type,uri_rdf_XMLLiteral,uri_rdfs_Datatype),
inference(split_conjunct,[status(thm)],[rdfs_dat_xmlliteral_type]),
[final] ).
cnf(i_0_396,plain,
iext(uri_rdf_type,uri_rdf_subject,uri_rdf_Property),
inference(split_conjunct,[status(thm)],[rdf_reification_subject_type]),
[final] ).
cnf(i_0_397,plain,
iext(uri_rdf_type,uri_rdf_value,uri_rdf_Property),
inference(split_conjunct,[status(thm)],[rdf_reification_predicate_type]),
[final] ).
cnf(i_0_398,plain,
iext(uri_rdf_type,uri_rdf_object,uri_rdf_Property),
inference(split_conjunct,[status(thm)],[rdf_reification_object_type]),
[final] ).
cnf(i_0_399,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_400,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_401,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_402,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_403,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_404,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_405,plain,
iext(uri_rdf_type,uri_rdf_Property,uri_rdfs_Class),
inference(split_conjunct,[status(thm)],[rdfs_property_type]),
[final] ).
cnf(i_0_406,plain,
iext(uri_rdf_type,uri_rdf_type,uri_rdf_Property),
inference(split_conjunct,[status(thm)],[rdf_value_type]),
[final] ).
cnf(i_0_407,plain,
iext(uri_rdf_type,uri_rdf_type,uri_rdf_Property),
inference(split_conjunct,[status(thm)],[rdf_type_type]),
[final] ).
cnf(i_0_408,plain,
iext(uri_rdf_type,uri_rdf_rest,uri_rdf_Property),
inference(split_conjunct,[status(thm)],[rdf_collection_rest_type]),
[final] ).
cnf(i_0_409,plain,
iext(uri_rdf_type,uri_rdf_first,uri_rdf_Property),
inference(split_conjunct,[status(thm)],[rdf_collection_first_type]),
[final] ).
cnf(i_0_410,plain,
iext(uri_rdf_type,uri_rdf_nil,uri_rdf_List),
inference(split_conjunct,[status(thm)],[rdf_collection_nil_type]),
[final] ).
cnf(i_0_411,plain,
( lv(X2)
| ~ idc(X1)
| ~ icext(X1,X2) ),
inference(split_conjunct,[status(thm)],[i_0_192]),
[final] ).
cnf(i_0_412,plain,
( lv(X1)
| ~ icext(uri_rdfs_Literal,X1) ),
inference(split_conjunct,[status(thm)],[i_0_193]),
[final] ).
cnf(i_0_413,plain,
( ic(X1)
| ~ icext(uri_rdfs_Class,X1) ),
inference(split_conjunct,[status(thm)],[i_0_194]),
[final] ).
cnf(i_0_414,plain,
~ icext(uri_owl_Nothing,X1),
inference(split_conjunct,[status(thm)],[i_0_195]),
[final] ).
cnf(i_0_415,plain,
( icext(uri_rdfs_Literal,X1)
| ~ lv(X1) ),
inference(split_conjunct,[status(thm)],[i_0_193]),
[final] ).
cnf(i_0_416,plain,
( icext(uri_rdfs_Class,X1)
| ~ ic(X1) ),
inference(split_conjunct,[status(thm)],[i_0_194]),
[final] ).
cnf(i_0_417,plain,
icext(uri_rdfs_Resource,X1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[i_0_196,c_0_172])]),
[final] ).
cnf(i_0_418,plain,
icext(uri_owl_Thing,X1),
inference(cn,[status(thm)],[inference(rw,[status(thm)],[i_0_197,c_0_172])]),
[final] ).
cnf(i_0_419,plain,
( ip(X1)
| ~ ioxp(X1) ),
inference(split_conjunct,[status(thm)],[i_0_198]),
[final] ).
cnf(i_0_420,plain,
( ip(X1)
| ~ iodp(X1) ),
inference(split_conjunct,[status(thm)],[i_0_199]),
[final] ).
cnf(i_0_421,plain,
( ip(X1)
| ~ ioap(X1) ),
inference(split_conjunct,[status(thm)],[i_0_200]),
[final] ).
cnf(i_0_422,plain,
( ic(X1)
| ~ idc(X1) ),
inference(split_conjunct,[status(thm)],[i_0_201]),
[final] ).
cnf(i_0_423,plain,
ip(uri_owl_someValuesFrom),
inference(split_conjunct,[status(thm)],[owl_prop_somevaluesfrom_type]),
[final] ).
cnf(i_0_424,plain,
ip(uri_owl_onProperty),
inference(split_conjunct,[status(thm)],[owl_prop_onproperty_type]),
[final] ).
cnf(i_0_425,plain,
ip(uri_owl_hasValue),
inference(split_conjunct,[status(thm)],[owl_prop_hasvalue_type]),
[final] ).
cnf(i_0_426,plain,
ip(uri_owl_allValuesFrom),
inference(split_conjunct,[status(thm)],[owl_prop_allvaluesfrom_type]),
[final] ).
cnf(i_0_427,plain,
ip(uri_owl_unionOf),
inference(split_conjunct,[status(thm)],[owl_prop_unionof_type]),
[final] ).
cnf(i_0_428,plain,
ip(uri_owl_intersectionOf),
inference(split_conjunct,[status(thm)],[owl_prop_intersectionof_type]),
[final] ).
cnf(i_0_429,plain,
ip(uri_owl_complementOf),
inference(split_conjunct,[status(thm)],[owl_prop_complementof_type]),
[final] ).
cnf(i_0_430,plain,
ic(uri_owl_Thing),
inference(split_conjunct,[status(thm)],[owl_class_thing_type]),
[final] ).
cnf(i_0_431,plain,
ic(uri_owl_Nothing),
inference(split_conjunct,[status(thm)],[owl_class_nothing_type]),
[final] ).
cnf(i_0_432,plain,
$false,
inference(scs_inference,[],[i_0_349,i_0_348,i_0_276]),
[proof] ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.12 % Problem : SWB002+3 : TPTP v9.2.1. Released v5.2.0.
% 0.00/0.12 % Command : /export/starexec/sandbox/solver/bin/lemma_parallel_prover %s --lemma-prover /export/starexec/sandbox/solver/bin/cse --final-prover /export/starexec/sandbox/solver/bin/eprover --proof-time %d --global-time-limit %d
% 0.16/0.33 % Computer : n010.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:05:36 EDT 2026
% 0.16/0.34 % CPUTime :
% 0.16/0.35 % start to proof: theBenchmark
% 0.38/1.62 % Version : CSE_E---1.7
% 0.38/1.62 % Problem : theBenchmark.p
% 0.38/1.62 % SZS status Theorem for theBenchmark.p
% 0.38/1.62 % SZS output start CNFRefutation
% See solution above
% 0.38/1.64 % Total time : 1.274s
%------------------------------------------------------------------------------