%------------------------------------------------------------------------------
% File : SRASS---0.1
% Problem : SWB067+1 : TPTP v5.2.0. Released v5.2.0.
% Transfm : none
% Format : tptp
% Command : SRASS -q2 -a 0 10 10 10 -i3 -n60 %s
% Computer : art07.cs.miami.edu
% Model : i686 i686
% CPU : Intel(R) Pentium(R) 4 CPU 2.80GHz @ 2793MHz
% Memory : 2018MB
% OS : Linux 2.6.26.8-57.fc8
% CPULimit : 300s
% DateTime : Fri Mar 4 03:45:35 EST 2011
% Result : Theorem 145.59s
% Output : Solution 145.94s
% Verified :
% SZS Type : None (Parsing solution fails)
% Syntax : Number of formulae : 0
% Comments :
%------------------------------------------------------------------------------
%----ERROR: Could not form TPTP format derivation
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% Reading problem from /tmp/SystemOnTPTP10750/SWB067+1.tptp
% Adding relevance values
% Extracting the conjecture
% Sorting axioms by relevance
% Looking for THM ...
% WARNING: TreeLimitedRun lost 0.73s, total lost is 0.73s
% not found
% Adding ~C to TBU ... ~conclusion_rdfbased_sem_inv_trans:
% ---- Iteration 1 (0 axioms selected)
% Looking for TBU SAT ...
% yes
% Looking for TBU model ...
% not found
% Looking for CSA axiom ... owl_prop_equivalentproperty_ext:
% CSA axiom owl_prop_equivalentproperty_ext found
% Looking for CSA axiom ... owl_eqdis_equivalentproperty:
% CSA axiom owl_eqdis_equivalentproperty found
% Looking for CSA axiom ... premise_rdfbased_sem_inv_trans:
% WARNING: TreeLimitedRun lost 0.16s, total lost is 0.89s
% CSA axiom premise_rdfbased_sem_inv_trans found
% ---- Iteration 2 (3 axioms selected)
% Looking for TBU SAT ...
% yes
% Looking for TBU model ...
% not found
% Looking for CSA axiom ... owl_prop_equivalentproperty_type:
% CSA axiom owl_prop_equivalentproperty_type found
% Looking for CSA axiom ... simple_iext_property:
% CSA axiom simple_iext_property found
% Looking for CSA axiom ... rdfs_subclassof_trans:
% WARNING: TreeLimitedRun lost 0.20s, total lost is 1.09s
% CSA axiom rdfs_subclassof_trans found
% ---- Iteration 3 (6 axioms selected)
% Looking for TBU SAT ...
% WARNING: TreeLimitedRun lost 0.18s, total lost is 1.27s
% yes
% Looking for TBU model ...
% not found
% Looking for CSA axiom ... rdfs_subpropertyof_trans:
% WARNING: TreeLimitedRun lost 0.16s, total lost is 1.43s
% CSA axiom rdfs_subpropertyof_trans found
% Looking for CSA axiom ... owl_prop_bottomdataproperty_ext:
% CSA axiom owl_prop_bottomdataproperty_ext found
% Looking for CSA axiom ... owl_prop_bottomobjectproperty_ext:
% WARNING: TreeLimitedRun lost 0.02s, total lost is 1.45s
% CSA axiom owl_prop_bottomobjectproperty_ext found
% ---- Iteration 4 (9 axioms selected)
% Looking for TBU SAT ...
% WARNING: TreeLimitedRun lost 0.18s, total lost is 1.63s
% yes
% Looking for TBU model ...
% not found
% Looking for CSA axiom ... simple_ir:
% CSA axiom simple_ir found
% Looking for CSA axiom ... owl_parts_ir_cond_set:
% CSA axiom owl_parts_ir_cond_set found
% Looking for CSA axiom ... rdfs_subclassof_reflex:
% WARNING: TreeLimitedRun lost 0.17s, total lost is 1.80s
% CSA axiom rdfs_subclassof_reflex found
% ---- Iteration 5 (12 axioms selected)
% Looking for TBU SAT ...
% yes
% Looking for TBU model ...
% WARNING: TreeLimitedRun lost 0.18s, total lost is 1.98s
% not found
% Looking for CSA axiom ... owl_parts_ip_cond_inst:
% rdfs_subpropertyof_main:
% WARNING: TreeLimitedRun lost 0.22s, total lost is 2.20s
% CSA axiom rdfs_subpropertyof_main found
% Looking for CSA axiom ... rdfs_subpropertyof_reflex:
% WARNING: TreeLimitedRun lost 0.18s, total lost is 2.38s
% CSA axiom rdfs_subpropertyof_reflex found
% Looking for CSA axiom ... owl_prop_inverseof_ext:
% CSA axiom owl_prop_inverseof_ext found
% ---- Iteration 6 (15 axioms selected)
% Looking for TBU SAT ...
% WARNING: TreeLimitedRun lost 0.17s, total lost is 2.55s
% yes
% Looking for TBU model ...
% not found
% Looking for CSA axiom ... owl_parts_ip_cond_inst:
% WARNING: TreeLimitedRun lost 0.26s, total lost is 2.81s
% owl_prop_propertydisjointwith_ext:
% CSA axiom owl_prop_propertydisjointwith_ext found
% Looking for CSA axiom ... owl_rdfsext_subpropertyof:
% CSA axiom owl_rdfsext_subpropertyof found
% Looking for CSA axiom ... owl_eqdis_propertydisjointwith:
% WARNING: TreeLimitedRun lost 0.17s, total lost is 2.98s
% CSA axiom owl_eqdis_propertydisjointwith found
% ---- Iteration 7 (18 axioms selected)
% Looking for TBU SAT ...
% yes
% Looking for TBU model ...
% not found
% Looking for CSA axiom ... owl_parts_ip_cond_inst:
% WARNING: TreeLimitedRun lost 0.10s, total lost is 3.08s
% owl_inv:
% WARNING: TreeLimitedRun lost 0.18s, total lost is 3.26s
% CSA axiom owl_inv found
% Looking for CSA axiom ... owl_prop_inverseof_type:
% WARNING: TreeLimitedRun lost 0.18s, total lost is 3.44s
% rdfs_cext_def:
% CSA axiom rdfs_cext_def found
% Looking for CSA axiom ... rdfs_domain_main:
% WARNING: TreeLimitedRun lost 0.08s, total lost is 3.52s
% rdfs_range_main:
% WARNING: TreeLimitedRun lost 0.11s, total lost is 3.63s
% rdfs_subclassof_main:
% CSA axiom rdfs_subclassof_main found
% ---- Iteration 8 (21 axioms selected)
% Looking for TBU SAT ...
% WARNING: TreeLimitedRun lost 0.13s, total lost is 3.76s
% no
% Looking for TBU UNS ...
% yes - theorem proved
% ---- Selection completed
% Selected axioms are ... :rdfs_subclassof_main:rdfs_cext_def:owl_inv:owl_eqdis_propertydisjointwith:owl_rdfsext_subpropertyof:owl_prop_propertydisjointwith_ext:owl_prop_inverseof_ext:rdfs_subpropertyof_reflex:rdfs_subpropertyof_main:rdfs_subclassof_reflex:owl_parts_ir_cond_set:simple_ir:owl_prop_bottomobjectproperty_ext:owl_prop_bottomdataproperty_ext:rdfs_subpropertyof_trans:rdfs_subclassof_trans:simple_iext_property:owl_prop_equivalentproperty_type:premise_rdfbased_sem_inv_trans:owl_eqdis_equivalentproperty:owl_prop_equivalentproperty_ext (21)
% Unselected axioms are ... :owl_parts_ip_cond_inst:owl_prop_inverseof_type:rdfs_domain_main:rdfs_range_main:owl_rdfsext_subclassof:owl_npa_object_if:rdf_collection_first_type:rdf_collection_rest_type:rdf_container_n_type_001:rdf_container_n_type_002:rdf_container_n_type_003:rdf_reification_object_type:rdf_reification_predicate_type:rdf_reification_subject_type:rdfs_property_type:owl_parts_iodp_cond_set:owl_parts_ip_cond_set:owl_prop_onproperty_type:owl_rdfsext_range:owl_char_asymmetric:owl_char_irreflexive:owl_char_reflexive:owl_char_symmetric:owl_char_transitive:rdfs_class_instsub_resource:owl_parts_ioap_cond_set:owl_parts_ioxp_cond_set:owl_prop_allvaluesfrom_type:owl_prop_annotatedproperty_type:owl_prop_annotatedsource_type:owl_prop_annotatedtarget_type:owl_prop_assertionproperty_type:owl_prop_bottomobjectproperty_type:owl_prop_cardinality_type:owl_prop_complementof_type:owl_prop_datatypecomplementof_type:owl_prop_differentfrom_type:owl_prop_disjointunionof_type:owl_prop_disjointwith_type:owl_prop_distinctmembers_type:owl_prop_equivalentclass_type:owl_prop_haskey_type:owl_prop_hasself_type:owl_prop_hasvalue_type:owl_prop_intersectionof_type:owl_prop_maxcardinality_type:owl_prop_maxqualifiedcardinality_type:owl_prop_members_type:owl_prop_mincardinality_type:owl_prop_minqualifiedcardinality_type:owl_prop_onclass_type:owl_prop_ondatarange_type:owl_prop_ondatatype_type:owl_prop_oneof_type:owl_prop_propertychainaxiom_type:owl_prop_propertydisjointwith_type:owl_prop_qualifiedcardinality_type:owl_prop_sameas_type:owl_prop_somevaluesfrom_type:owl_prop_sourceindividual_type:owl_prop_targetindividual_type:owl_prop_targetvalue_type:owl_prop_topobjectproperty_type:owl_prop_unionof_type:owl_prop_withrestrictions_type:rdfs_annotation_isdefinedby_sub:rdfs_container_containermembershipproperty_sub:rdfs_dat_xmlliteral_sub:rdfs_datatype_sub:rdfs_subclassof_domain:rdfs_subclassof_range:rdfs_subpropertyof_domain:rdfs_subpropertyof_range:owl_prop_complementof_ext:owl_prop_disjointwith_ext:owl_prop_equivalentclass_ext:owl_bool_complementof_class:owl_restrict_allvaluesfrom:owl_restrict_hasself:owl_restrict_hasvalue:owl_restrict_somevaluesfrom:owl_eqdis_disjointwith:owl_eqdis_equivalentclass:rdf_type_ip:rdf_type_type:rdf_value_type:rdfs_container_alt_sub:rdfs_container_bag_sub:rdfs_container_seq_sub:rdfs_domain_domain:rdfs_lv_def:owl_parts_ioxp_cond_inst:owl_parts_ip_def:owl_class_literal_ext:owl_prop_backwardcompatiblewith_ext:owl_prop_datatypecomplementof_ext:owl_prop_imports_ext:owl_prop_incompatiblewith_ext:owl_prop_ondatatype_ext:owl_prop_priorversion_ext:owl_prop_versioniri_ext:owl_chain_000:owl_chain_001:owl_chain_002:owl_chain_003:rdfs_ic_def:rdfs_range_range:owl_parts_ioap_cond_inst:owl_class_classrdfs_ext:owl_class_ontology_ext:owl_class_restriction_ext:owl_prop_annotatedproperty_ext:owl_prop_annotatedsource_ext:owl_prop_annotatedtarget_ext:owl_prop_deprecated_ext:owl_prop_differentfrom_ext:owl_prop_isdefinedby_ext:owl_prop_sameas_ext:owl_prop_seealso_ext:owl_prop_topobjectproperty_ext:owl_prop_versioninfo_ext:rdfs_container_containermembershipproperty_instsub_member:rdfs_datatype_instsub_literal:owl_parts_ic_cond_inst:owl_class_asymmetricproperty_ext:owl_class_classowl_ext:owl_class_deprecatedclass_ext:owl_class_deprecatedproperty_ext:owl_class_functionalproperty_ext:owl_class_inversefunctionalproperty_ext:owl_class_irreflexiveproperty_ext:owl_class_objectproperty_ext:owl_class_reflexiveproperty_ext:owl_class_symmetricproperty_ext:owl_class_transitiveproperty_ext:owl_class_asymmetricproperty_type:owl_class_property_ext:owl_class_property_type:owl_class_reflexiveproperty_type:owl_class_symmetricproperty_type:owl_class_transitiveproperty_type:owl_prop_onproperty_ext:owl_rdfsext_domain:simple_lv:owl_parts_ic_cond_set:owl_parts_lv_cond_set:owl_class_literal_type:owl_class_nothing_ext:owl_prop_backwardcompatiblewith_type_annot:owl_prop_backwardcompatiblewith_type_onto:owl_prop_cardinality_ext:owl_prop_comment_type:owl_prop_deprecated_type:owl_prop_imports_type:owl_prop_incompatiblewith_type_annot:owl_prop_incompatiblewith_type_onto:owl_prop_isdefinedby_type:owl_prop_label_type:owl_prop_maxcardinality_ext:owl_prop_maxqualifiedcardinality_ext:owl_prop_mincardinality_ext:owl_prop_minqualifiedcardinality_ext:owl_prop_ondatarange_ext:owl_prop_priorversion_type_annot:owl_prop_priorversion_type_onto:owl_prop_qualifiedcardinality_ext:owl_prop_seealso_type:owl_prop_versioninfo_type:owl_prop_versioniri_type:owl_dat_dtype_xmlliteral_type:owl_parts_ix_cond_set:owl_class_negativepropertyassertion_ext:owl_prop_allvaluesfrom_ext:owl_prop_assertionproperty_ext:owl_prop_bottomdataproperty_type:owl_prop_onclass_ext:owl_prop_propertychainaxiom_ext:owl_prop_somevaluesfrom_ext:owl_prop_topdataproperty_type:owl_bool_intersectionof_dtype_001:owl_bool_intersectionof_dtype_002:owl_bool_intersectionof_dtype_003:owl_bool_unionof_dtype_001:owl_bool_unionof_dtype_002:owl_bool_unionof_dtype_003:owl_restrict_exactqcr_object_001:owl_restrict_maxqcr_object_001:owl_eqdis_differentfrom:owl_eqdis_sameas:owl_char_functional:owl_char_inversefunctional:owl_dat_facet_langrange_type:owl_dat_facet_length_type:owl_dat_facet_maxexclusive_type:owl_dat_facet_maxinclusive_type:owl_dat_facet_maxlength_type:owl_dat_facet_minexclusive_type:owl_dat_facet_mininclusive_type:owl_dat_facet_minlength_type:owl_dat_facet_pattern_type:rdfs_collection_first_domain:rdfs_collection_first_range:rdfs_collection_rest_domain:rdfs_collection_rest_range:owl_parts_ic_def:owl_parts_iodp_cond_inst:owl_parts_lv_def:rdf_collection_nil_type:rdfs_annotation_comment_domain:rdfs_annotation_comment_range:rdfs_annotation_isdefinedby_domain:rdfs_annotation_isdefinedby_range:rdfs_annotation_label_domain:rdfs_annotation_label_range:rdfs_annotation_seealso_domain:rdfs_annotation_seealso_range:rdfs_container_member_domain:rdfs_container_member_range:rdfs_container_n_domain_001:rdfs_container_n_domain_002:rdfs_container_n_domain_003:rdfs_container_n_range_001:rdfs_container_n_range_002:rdfs_container_n_range_003:rdfs_container_n_type_001:rdfs_container_n_type_002:rdfs_container_n_type_003:rdfs_dat_xmlliteral_type:rdfs_domain_range:rdfs_range_domain:rdfs_reification_object_domain:rdfs_reification_object_range:rdfs_reification_predicate_domain:rdfs_reification_predicate_range:rdfs_reification_subject_domain:rdfs_reification_subject_range:rdfs_type_domain:rdfs_type_range:rdfs_value_domain:rdfs_value_range:owl_parts_idc_def:owl_parts_ioap_def:owl_parts_iodp_def:owl_parts_ioxp_def:owl_parts_ir_def:owl_parts_ix_def:owl_class_datatype_ext:owl_prop_comment_ext:owl_prop_label_ext:owl_prop_topdataproperty_ext:owl_restrict_minqcr_data_001:owl_ndis_alldifferent_distinctmembers_fi_001:owl_ndis_alldifferent_members_fi_001:owl_ndis_alldisjointclasses_fi_001:owl_ndis_alldisjointclasses_fi_002:owl_ndis_alldisjointclasses_fi_003:owl_ndis_alldisjointclasses_if_002:owl_ndis_alldisjointclasses_if_003:owl_ndis_alldisjointproperties_fi_001:owl_ndis_alldisjointproperties_fi_002:owl_ndis_alldisjointproperties_fi_003:owl_ndis_alldisjointproperties_if_002:owl_ndis_alldisjointproperties_if_003:owl_npa_data_if:owl_npa_object_fi:owl_dat_dtype_xmlliteral_ext:owl_dat_facet_langrange_ext:owl_dat_facet_length_ext:owl_dat_facet_maxexclusive_ext:owl_dat_facet_maxinclusive_ext:owl_dat_facet_maxlength_ext:owl_dat_facet_minexclusive_ext:owl_dat_facet_mininclusive_ext:owl_dat_facet_minlength_ext:owl_dat_facet_pattern_ext:rdfs_ir_def:owl_class_alldifferent_ext:owl_class_alldisjointclasses_ext:owl_class_alldisjointproperties_ext:owl_class_annotationproperty_ext:owl_class_classrdfs_type:owl_class_datatypeproperty_ext:owl_class_deprecatedproperty_type:owl_class_functionalproperty_type:owl_class_inversefunctionalproperty_type:owl_class_irreflexiveproperty_type:owl_class_negativepropertyassertion_type:owl_class_objectproperty_type:owl_class_ontologyproperty_ext:owl_class_resource_ext:owl_prop_disjointunionof_ext:owl_prop_distinctmembers_ext:owl_prop_haskey_ext:owl_prop_intersectionof_ext:owl_prop_members_ext:owl_prop_oneof_ext:owl_prop_sourceindividual_ext:owl_prop_targetindividual_ext:owl_prop_targetvalue_ext:owl_prop_unionof_ext:owl_prop_withrestrictions_ext:owl_bool_intersectionof_class_000:owl_enum_dtype_001:owl_enum_dtype_002:owl_enum_dtype_003:owl_restrict_exactqcr_data_001:owl_restrict_maxqcr_data_001:owl_key_000:owl_npa_data_fi:owl_dat_dtype_relation_disjoint_anyuri_xmlliteral:owl_dat_dtype_relation_disjoint_base64binary_xmlliteral:owl_dat_dtype_relation_disjoint_boolean_xmlliteral:owl_dat_dtype_relation_disjoint_datetime_xmlliteral:owl_dat_dtype_relation_disjoint_double_xmlliteral:owl_dat_dtype_relation_disjoint_float_xmlliteral:owl_dat_dtype_relation_disjoint_hexbinary_xmlliteral:owl_dat_dtype_relation_disjoint_plainliteral_xmlliteral:owl_dat_dtype_relation_disjoint_real_xmlliteral:owl_parts_idc_cond_inst:owl_parts_idc_cond_set:owl_class_alldifferent_type:owl_class_alldisjointclasses_type:owl_class_alldisjointproperties_type:owl_class_annotation_ext:owl_class_annotation_type:owl_class_annotationproperty_type:owl_class_axiom_ext:owl_class_axiom_type:owl_class_classowl_type:owl_class_datarange_ext:owl_class_datarange_type:owl_class_datatype_type:owl_class_datatypeproperty_type:owl_class_deprecatedclass_type:owl_class_namedindividual_ext:owl_class_namedindividual_type:owl_class_nothing_type:owl_class_ontology_type:owl_class_ontologyproperty_type:owl_class_resource_type:owl_class_restriction_type:owl_class_thing_ext:owl_class_thing_type:owl_prop_hasself_ext:owl_prop_hasvalue_ext:owl_bool_datatypecomplementof:owl_bool_unionof_class_000:owl_enum_class_000:owl_enum_class_001:owl_enum_class_002:owl_enum_class_003:owl_restrict_exactqcr_object_002:owl_restrict_exactqcr_object_003:owl_restrict_maxqcr_object_002:owl_restrict_maxqcr_object_003:owl_restrict_minqcr_data_000:owl_restrict_minqcr_object_002:owl_restrict_minqcr_object_003:owl_eqdis_disjointunionof_000:owl_ndis_alldifferent_distinctmembers_fi_000:owl_ndis_alldifferent_distinctmembers_fi_002:owl_ndis_alldifferent_distinctmembers_fi_003:owl_ndis_alldifferent_distinctmembers_if_002:owl_ndis_alldifferent_distinctmembers_if_003:owl_ndis_alldifferent_members_fi_000:owl_ndis_alldifferent_members_fi_002:owl_ndis_alldifferent_members_fi_003:owl_ndis_alldifferent_members_if_002:owl_ndis_alldifferent_members_if_003:owl_ndis_alldisjointclasses_fi_000:owl_ndis_alldisjointproperties_fi_000:owl_key_001:owl_key_002:owl_key_003:owl_dat_dtype_anyuri_ext:owl_dat_dtype_anyuri_type:owl_dat_dtype_base64binary_ext:owl_dat_dtype_base64binary_type:owl_dat_dtype_boolean_ext:owl_dat_dtype_boolean_type:owl_dat_dtype_byte_ext:owl_dat_dtype_byte_type:owl_dat_dtype_datetime_ext:owl_dat_dtype_datetime_type:owl_dat_dtype_datetimestamp_ext:owl_dat_dtype_datetimestamp_type:owl_dat_dtype_decimal_ext:owl_dat_dtype_decimal_type:owl_dat_dtype_double_ext:owl_dat_dtype_double_type:owl_dat_dtype_float_ext:owl_dat_dtype_float_type:owl_dat_dtype_hexbinary_ext:owl_dat_dtype_hexbinary_type:owl_dat_dtype_int_ext:owl_dat_dtype_int_type:owl_dat_dtype_integer_ext:owl_dat_dtype_integer_type:owl_dat_dtype_language_ext:owl_dat_dtype_language_type:owl_dat_dtype_long_ext:owl_dat_dtype_long_type:owl_dat_dtype_name_ext:owl_dat_dtype_name_type:owl_dat_dtype_ncname_ext:owl_dat_dtype_ncname_type:owl_dat_dtype_negativeinteger_ext:owl_dat_dtype_negativeinteger_type:owl_dat_dtype_nmtoken_ext:owl_dat_dtype_nmtoken_type:owl_dat_dtype_nonnegativeinteger_ext:owl_dat_dtype_nonnegativeinteger_type:owl_dat_dtype_nonpositiveinteger_ext:owl_dat_dtype_nonpositiveinteger_type:owl_dat_dtype_normalizedstring_ext:owl_dat_dtype_normalizedstring_type:owl_dat_dtype_plainliteral_ext:owl_dat_dtype_plainliteral_type:owl_dat_dtype_positiveinteger_ext:owl_dat_dtype_positiveinteger_type:owl_dat_dtype_rational_ext:owl_dat_dtype_rational_type:owl_dat_dtype_real_ext:owl_dat_dtype_real_type:owl_dat_dtype_short_ext:owl_dat_dtype_short_type:owl_dat_dtype_string_ext:owl_dat_dtype_string_type:owl_dat_dtype_token_ext:owl_dat_dtype_token_type:owl_dat_dtype_unsignedbyte_ext:owl_dat_dtype_unsignedbyte_type:owl_dat_dtype_unsignedint_ext:owl_dat_dtype_unsignedint_type:owl_dat_dtype_unsignedlong_ext:owl_dat_dtype_unsignedlong_type:owl_dat_dtype_unsignedshort_ext:owl_dat_dtype_unsignedshort_type:owl_bool_intersectionof_class_001:owl_bool_intersectionof_class_002:owl_bool_intersectionof_class_003:owl_bool_unionof_class_001:owl_bool_unionof_class_002:owl_bool_unionof_class_003:owl_restrict_exactcard_000:owl_restrict_exactqcr_data_000:owl_restrict_maxcard_000:owl_restrict_maxqcr_data_000:owl_restrict_mincard_000:owl_restrict_mincard_001:owl_eqdis_disjointunionof_001:owl_eqdis_disjointunionof_002:owl_eqdis_disjointunionof_003:owl_dat_dtype_relation_disjoint_anyuri_base64binary:owl_dat_dtype_relation_disjoint_anyuri_boolean:owl_dat_dtype_relation_disjoint_anyuri_datetime:owl_dat_dtype_relation_disjoint_anyuri_double:owl_dat_dtype_relation_disjoint_anyuri_float:owl_dat_dtype_relation_disjoint_anyuri_hexbinary:owl_dat_dtype_relation_disjoint_anyuri_plainliteral:owl_dat_dtype_relation_disjoint_anyuri_real:owl_dat_dtype_relation_disjoint_base64binary_boolean:owl_dat_dtype_relation_disjoint_base64binary_datetime:owl_dat_dtype_relation_disjoint_base64binary_double:owl_dat_dtype_relation_disjoint_base64binary_float:owl_dat_dtype_relation_disjoint_base64binary_hexbinary:owl_dat_dtype_relation_disjoint_base64binary_plainliteral:owl_dat_dtype_relation_disjoint_base64binary_real:owl_dat_dtype_relation_disjoint_boolean_datetime:owl_dat_dtype_relation_disjoint_boolean_double:owl_dat_dtype_relation_disjoint_boolean_float:owl_dat_dtype_relation_disjoint_boolean_hexbinary:owl_dat_dtype_relation_disjoint_boolean_plainliteral:owl_dat_dtype_relation_disjoint_boolean_real:owl_dat_dtype_relation_disjoint_datetime_double:owl_dat_dtype_relation_disjoint_datetime_float:owl_dat_dtype_relation_disjoint_datetime_hexbinary:owl_dat_dtype_relation_disjoint_datetime_plainliteral:owl_dat_dtype_relation_disjoint_datetime_real:owl_dat_dtype_relation_disjoint_double_float:owl_dat_dtype_relation_disjoint_double_hexbinary:owl_dat_dtype_relation_disjoint_double_plainliteral:owl_dat_dtype_relation_disjoint_double_real:owl_dat_dtype_relation_disjoint_float_hexbinary:owl_dat_dtype_relation_disjoint_float_plainliteral:owl_dat_dtype_relation_disjoint_float_real:owl_dat_dtype_relation_disjoint_hexbinary_plainliteral:owl_dat_dtype_relation_disjoint_hexbinary_real:owl_dat_dtype_relation_disjoint_plainliteral_real:owl_dat_dtype_relation_subtype_nonnegativeinteger_integer:owl_dat_dtype_relation_subtype_positiveinteger_nonnegativeinteger:owl_dat_dtype_relation_subtype_unsignedlong_nonnegativeinteger:owl_restrict_exactcard_001:owl_restrict_exactcard_002:owl_restrict_exactcard_003:owl_restrict_exactqcr_data_002:owl_restrict_exactqcr_data_003:owl_restrict_exactqcr_object_000:owl_restrict_maxcard_001:owl_restrict_maxcard_002:owl_restrict_maxcard_003:owl_restrict_maxqcr_data_002:owl_restrict_maxqcr_data_003:owl_restrict_maxqcr_object_000:owl_restrict_mincard_002:owl_restrict_mincard_003:owl_restrict_minqcr_data_002:owl_restrict_minqcr_data_003:owl_restrict_minqcr_object_000:owl_restrict_minqcr_object_001:owl_dat_dtype_relation_subtype_byte_short:owl_dat_dtype_relation_subtype_datetimestamp_datetime:owl_dat_dtype_relation_subtype_decimal_rational:owl_dat_dtype_relation_subtype_int_long:owl_dat_dtype_relation_subtype_integer_decimal:owl_dat_dtype_relation_subtype_language_token:owl_dat_dtype_relation_subtype_long_integer:owl_dat_dtype_relation_subtype_name_token:owl_dat_dtype_relation_subtype_ncname_name:owl_dat_dtype_relation_subtype_negativeinteger_nonpositiveinteger:owl_dat_dtype_relation_subtype_nmtoken_token:owl_dat_dtype_relation_subtype_nonpositiveinteger_integer:owl_dat_dtype_relation_subtype_normalizedstring_string:owl_dat_dtype_relation_subtype_rational_real:owl_dat_dtype_relation_subtype_short_int:owl_dat_dtype_relation_subtype_string_plainliteral:owl_dat_dtype_relation_subtype_token_normalizedstring:owl_dat_dtype_relation_subtype_unsignedbyte_unsignedshort:owl_dat_dtype_relation_subtype_unsignedint_unsignedlong:owl_dat_dtype_relation_subtype_unsignedshort_unsignedint:owl_ndis_alldifferent_distinctmembers_if_000:owl_ndis_alldifferent_distinctmembers_if_001:owl_ndis_alldifferent_members_if_000:owl_ndis_alldifferent_members_if_001:owl_ndis_alldisjointclasses_if_000:owl_ndis_alldisjointclasses_if_001:owl_ndis_alldisjointproperties_if_000:owl_ndis_alldisjointproperties_if_001 (538)
% SZS status THM for /tmp/SystemOnTPTP10750/SWB067+1.tptp
% Looking for THM ...
% found
% SZS output start Solution for /tmp/SystemOnTPTP10750/SWB067+1.tptp
% TreeLimitedRun: ----------------------------------------------------------
% TreeLimitedRun: /home/graph/tptp/Systems/EP---1.2/eproof --print-statistics -xAuto -tAuto --cpu-limit=600 --proof-time-unlimited --memory-limit=Auto --tstp-in --tstp-out /tmp/SRASS.s.p
% TreeLimitedRun: CPU time limit is 600s
% TreeLimitedRun: WC time limit is 1200s
% TreeLimitedRun: PID is 14756
% TreeLimitedRun: ----------------------------------------------------------
% PrfWatch: 0.00 CPU 0.01 WC
% # Preprocessing time : 0.014 s
% # Problem is unsatisfiable (or provable), constructing proof object
% # SZS status Theorem
% # SZS output start CNFRefutation.
% fof(3, axiom,![X4]:![X5]:(iext(uri_owl_inverseOf,X4,X5)<=>((ip(X4)&ip(X5))&![X3]:![X6]:(iext(X4,X3,X6)<=>iext(X5,X6,X3)))),file('/tmp/SRASS.s.p', owl_inv)).
% fof(5, axiom,![X4]:![X5]:(iext(uri_rdfs_subPropertyOf,X4,X5)<=>((ip(X4)&ip(X5))&![X3]:![X6]:(iext(X4,X3,X6)=>iext(X5,X3,X6)))),file('/tmp/SRASS.s.p', owl_rdfsext_subpropertyof)).
% fof(17, axiom,![X11]:![X7]:![X12]:(iext(X7,X11,X12)=>ip(X7)),file('/tmp/SRASS.s.p', simple_iext_property)).
% fof(19, axiom,(iext(uri_owl_inverseOf,uri_ex_p3,uri_ex_p2)&iext(uri_owl_inverseOf,uri_ex_p2,uri_ex_p1)),file('/tmp/SRASS.s.p', premise_rdfbased_sem_inv_trans)).
% fof(20, axiom,![X4]:![X5]:(iext(uri_owl_equivalentProperty,X4,X5)<=>((ip(X4)&ip(X5))&![X3]:![X6]:(iext(X4,X3,X6)<=>iext(X5,X3,X6)))),file('/tmp/SRASS.s.p', owl_eqdis_equivalentproperty)).
% fof(22, conjecture,iext(uri_owl_equivalentProperty,uri_ex_p3,uri_ex_p1),file('/tmp/SRASS.s.p', conclusion_rdfbased_sem_inv_trans)).
% fof(23, negated_conjecture,~(iext(uri_owl_equivalentProperty,uri_ex_p3,uri_ex_p1)),inference(assume_negation,[status(cth)],[22])).
% fof(26, negated_conjecture,~(iext(uri_owl_equivalentProperty,uri_ex_p3,uri_ex_p1)),inference(fof_simplification,[status(thm)],[23,theory(equality)])).
% fof(38, plain,![X4]:![X5]:((~(iext(uri_owl_inverseOf,X4,X5))|((ip(X4)&ip(X5))&![X3]:![X6]:((~(iext(X4,X3,X6))|iext(X5,X6,X3))&(~(iext(X5,X6,X3))|iext(X4,X3,X6)))))&(((~(ip(X4))|~(ip(X5)))|?[X3]:?[X6]:((~(iext(X4,X3,X6))|~(iext(X5,X6,X3)))&(iext(X4,X3,X6)|iext(X5,X6,X3))))|iext(uri_owl_inverseOf,X4,X5))),inference(fof_nnf,[status(thm)],[3])).
% fof(39, plain,![X7]:![X8]:((~(iext(uri_owl_inverseOf,X7,X8))|((ip(X7)&ip(X8))&![X9]:![X10]:((~(iext(X7,X9,X10))|iext(X8,X10,X9))&(~(iext(X8,X10,X9))|iext(X7,X9,X10)))))&(((~(ip(X7))|~(ip(X8)))|?[X11]:?[X12]:((~(iext(X7,X11,X12))|~(iext(X8,X12,X11)))&(iext(X7,X11,X12)|iext(X8,X12,X11))))|iext(uri_owl_inverseOf,X7,X8))),inference(variable_rename,[status(thm)],[38])).
% fof(40, plain,![X7]:![X8]:((~(iext(uri_owl_inverseOf,X7,X8))|((ip(X7)&ip(X8))&![X9]:![X10]:((~(iext(X7,X9,X10))|iext(X8,X10,X9))&(~(iext(X8,X10,X9))|iext(X7,X9,X10)))))&(((~(ip(X7))|~(ip(X8)))|((~(iext(X7,esk1_2(X7,X8),esk2_2(X7,X8)))|~(iext(X8,esk2_2(X7,X8),esk1_2(X7,X8))))&(iext(X7,esk1_2(X7,X8),esk2_2(X7,X8))|iext(X8,esk2_2(X7,X8),esk1_2(X7,X8)))))|iext(uri_owl_inverseOf,X7,X8))),inference(skolemize,[status(esa)],[39])).
% fof(41, plain,![X7]:![X8]:![X9]:![X10]:(((((~(iext(X7,X9,X10))|iext(X8,X10,X9))&(~(iext(X8,X10,X9))|iext(X7,X9,X10)))&(ip(X7)&ip(X8)))|~(iext(uri_owl_inverseOf,X7,X8)))&(((~(ip(X7))|~(ip(X8)))|((~(iext(X7,esk1_2(X7,X8),esk2_2(X7,X8)))|~(iext(X8,esk2_2(X7,X8),esk1_2(X7,X8))))&(iext(X7,esk1_2(X7,X8),esk2_2(X7,X8))|iext(X8,esk2_2(X7,X8),esk1_2(X7,X8)))))|iext(uri_owl_inverseOf,X7,X8))),inference(shift_quantors,[status(thm)],[40])).
% fof(42, plain,![X7]:![X8]:![X9]:![X10]:(((((~(iext(X7,X9,X10))|iext(X8,X10,X9))|~(iext(uri_owl_inverseOf,X7,X8)))&((~(iext(X8,X10,X9))|iext(X7,X9,X10))|~(iext(uri_owl_inverseOf,X7,X8))))&((ip(X7)|~(iext(uri_owl_inverseOf,X7,X8)))&(ip(X8)|~(iext(uri_owl_inverseOf,X7,X8)))))&((((~(iext(X7,esk1_2(X7,X8),esk2_2(X7,X8)))|~(iext(X8,esk2_2(X7,X8),esk1_2(X7,X8))))|(~(ip(X7))|~(ip(X8))))|iext(uri_owl_inverseOf,X7,X8))&(((iext(X7,esk1_2(X7,X8),esk2_2(X7,X8))|iext(X8,esk2_2(X7,X8),esk1_2(X7,X8)))|(~(ip(X7))|~(ip(X8))))|iext(uri_owl_inverseOf,X7,X8)))),inference(distribute,[status(thm)],[41])).
% cnf(45,plain,(ip(X2)|~iext(uri_owl_inverseOf,X1,X2)),inference(split_conjunct,[status(thm)],[42])).
% cnf(46,plain,(ip(X1)|~iext(uri_owl_inverseOf,X1,X2)),inference(split_conjunct,[status(thm)],[42])).
% cnf(47,plain,(iext(X1,X3,X4)|~iext(uri_owl_inverseOf,X1,X2)|~iext(X2,X4,X3)),inference(split_conjunct,[status(thm)],[42])).
% cnf(48,plain,(iext(X2,X3,X4)|~iext(uri_owl_inverseOf,X1,X2)|~iext(X1,X4,X3)),inference(split_conjunct,[status(thm)],[42])).
% fof(59, plain,![X4]:![X5]:((~(iext(uri_rdfs_subPropertyOf,X4,X5))|((ip(X4)&ip(X5))&![X3]:![X6]:(~(iext(X4,X3,X6))|iext(X5,X3,X6))))&(((~(ip(X4))|~(ip(X5)))|?[X3]:?[X6]:(iext(X4,X3,X6)&~(iext(X5,X3,X6))))|iext(uri_rdfs_subPropertyOf,X4,X5))),inference(fof_nnf,[status(thm)],[5])).
% fof(60, plain,![X7]:![X8]:((~(iext(uri_rdfs_subPropertyOf,X7,X8))|((ip(X7)&ip(X8))&![X9]:![X10]:(~(iext(X7,X9,X10))|iext(X8,X9,X10))))&(((~(ip(X7))|~(ip(X8)))|?[X11]:?[X12]:(iext(X7,X11,X12)&~(iext(X8,X11,X12))))|iext(uri_rdfs_subPropertyOf,X7,X8))),inference(variable_rename,[status(thm)],[59])).
% fof(61, plain,![X7]:![X8]:((~(iext(uri_rdfs_subPropertyOf,X7,X8))|((ip(X7)&ip(X8))&![X9]:![X10]:(~(iext(X7,X9,X10))|iext(X8,X9,X10))))&(((~(ip(X7))|~(ip(X8)))|(iext(X7,esk5_2(X7,X8),esk6_2(X7,X8))&~(iext(X8,esk5_2(X7,X8),esk6_2(X7,X8)))))|iext(uri_rdfs_subPropertyOf,X7,X8))),inference(skolemize,[status(esa)],[60])).
% fof(62, plain,![X7]:![X8]:![X9]:![X10]:((((~(iext(X7,X9,X10))|iext(X8,X9,X10))&(ip(X7)&ip(X8)))|~(iext(uri_rdfs_subPropertyOf,X7,X8)))&(((~(ip(X7))|~(ip(X8)))|(iext(X7,esk5_2(X7,X8),esk6_2(X7,X8))&~(iext(X8,esk5_2(X7,X8),esk6_2(X7,X8)))))|iext(uri_rdfs_subPropertyOf,X7,X8))),inference(shift_quantors,[status(thm)],[61])).
% fof(63, plain,![X7]:![X8]:![X9]:![X10]:((((~(iext(X7,X9,X10))|iext(X8,X9,X10))|~(iext(uri_rdfs_subPropertyOf,X7,X8)))&((ip(X7)|~(iext(uri_rdfs_subPropertyOf,X7,X8)))&(ip(X8)|~(iext(uri_rdfs_subPropertyOf,X7,X8)))))&(((iext(X7,esk5_2(X7,X8),esk6_2(X7,X8))|(~(ip(X7))|~(ip(X8))))|iext(uri_rdfs_subPropertyOf,X7,X8))&((~(iext(X8,esk5_2(X7,X8),esk6_2(X7,X8)))|(~(ip(X7))|~(ip(X8))))|iext(uri_rdfs_subPropertyOf,X7,X8)))),inference(distribute,[status(thm)],[62])).
% cnf(64,plain,(iext(uri_rdfs_subPropertyOf,X1,X2)|~ip(X2)|~ip(X1)|~iext(X2,esk5_2(X1,X2),esk6_2(X1,X2))),inference(split_conjunct,[status(thm)],[63])).
% cnf(65,plain,(iext(uri_rdfs_subPropertyOf,X1,X2)|iext(X1,esk5_2(X1,X2),esk6_2(X1,X2))|~ip(X2)|~ip(X1)),inference(split_conjunct,[status(thm)],[63])).
% cnf(68,plain,(iext(X2,X3,X4)|~iext(uri_rdfs_subPropertyOf,X1,X2)|~iext(X1,X3,X4)),inference(split_conjunct,[status(thm)],[63])).
% fof(107, plain,![X11]:![X7]:![X12]:(~(iext(X7,X11,X12))|ip(X7)),inference(fof_nnf,[status(thm)],[17])).
% fof(108, plain,![X13]:![X14]:![X15]:(~(iext(X14,X13,X15))|ip(X14)),inference(variable_rename,[status(thm)],[107])).
% cnf(109,plain,(ip(X1)|~iext(X1,X2,X3)),inference(split_conjunct,[status(thm)],[108])).
% cnf(111,plain,(iext(uri_owl_inverseOf,uri_ex_p2,uri_ex_p1)),inference(split_conjunct,[status(thm)],[19])).
% cnf(112,plain,(iext(uri_owl_inverseOf,uri_ex_p3,uri_ex_p2)),inference(split_conjunct,[status(thm)],[19])).
% fof(113, plain,![X4]:![X5]:((~(iext(uri_owl_equivalentProperty,X4,X5))|((ip(X4)&ip(X5))&![X3]:![X6]:((~(iext(X4,X3,X6))|iext(X5,X3,X6))&(~(iext(X5,X3,X6))|iext(X4,X3,X6)))))&(((~(ip(X4))|~(ip(X5)))|?[X3]:?[X6]:((~(iext(X4,X3,X6))|~(iext(X5,X3,X6)))&(iext(X4,X3,X6)|iext(X5,X3,X6))))|iext(uri_owl_equivalentProperty,X4,X5))),inference(fof_nnf,[status(thm)],[20])).
% fof(114, plain,![X7]:![X8]:((~(iext(uri_owl_equivalentProperty,X7,X8))|((ip(X7)&ip(X8))&![X9]:![X10]:((~(iext(X7,X9,X10))|iext(X8,X9,X10))&(~(iext(X8,X9,X10))|iext(X7,X9,X10)))))&(((~(ip(X7))|~(ip(X8)))|?[X11]:?[X12]:((~(iext(X7,X11,X12))|~(iext(X8,X11,X12)))&(iext(X7,X11,X12)|iext(X8,X11,X12))))|iext(uri_owl_equivalentProperty,X7,X8))),inference(variable_rename,[status(thm)],[113])).
% fof(115, plain,![X7]:![X8]:((~(iext(uri_owl_equivalentProperty,X7,X8))|((ip(X7)&ip(X8))&![X9]:![X10]:((~(iext(X7,X9,X10))|iext(X8,X9,X10))&(~(iext(X8,X9,X10))|iext(X7,X9,X10)))))&(((~(ip(X7))|~(ip(X8)))|((~(iext(X7,esk8_2(X7,X8),esk9_2(X7,X8)))|~(iext(X8,esk8_2(X7,X8),esk9_2(X7,X8))))&(iext(X7,esk8_2(X7,X8),esk9_2(X7,X8))|iext(X8,esk8_2(X7,X8),esk9_2(X7,X8)))))|iext(uri_owl_equivalentProperty,X7,X8))),inference(skolemize,[status(esa)],[114])).
% fof(116, plain,![X7]:![X8]:![X9]:![X10]:(((((~(iext(X7,X9,X10))|iext(X8,X9,X10))&(~(iext(X8,X9,X10))|iext(X7,X9,X10)))&(ip(X7)&ip(X8)))|~(iext(uri_owl_equivalentProperty,X7,X8)))&(((~(ip(X7))|~(ip(X8)))|((~(iext(X7,esk8_2(X7,X8),esk9_2(X7,X8)))|~(iext(X8,esk8_2(X7,X8),esk9_2(X7,X8))))&(iext(X7,esk8_2(X7,X8),esk9_2(X7,X8))|iext(X8,esk8_2(X7,X8),esk9_2(X7,X8)))))|iext(uri_owl_equivalentProperty,X7,X8))),inference(shift_quantors,[status(thm)],[115])).
% fof(117, plain,![X7]:![X8]:![X9]:![X10]:(((((~(iext(X7,X9,X10))|iext(X8,X9,X10))|~(iext(uri_owl_equivalentProperty,X7,X8)))&((~(iext(X8,X9,X10))|iext(X7,X9,X10))|~(iext(uri_owl_equivalentProperty,X7,X8))))&((ip(X7)|~(iext(uri_owl_equivalentProperty,X7,X8)))&(ip(X8)|~(iext(uri_owl_equivalentProperty,X7,X8)))))&((((~(iext(X7,esk8_2(X7,X8),esk9_2(X7,X8)))|~(iext(X8,esk8_2(X7,X8),esk9_2(X7,X8))))|(~(ip(X7))|~(ip(X8))))|iext(uri_owl_equivalentProperty,X7,X8))&(((iext(X7,esk8_2(X7,X8),esk9_2(X7,X8))|iext(X8,esk8_2(X7,X8),esk9_2(X7,X8)))|(~(ip(X7))|~(ip(X8))))|iext(uri_owl_equivalentProperty,X7,X8)))),inference(distribute,[status(thm)],[116])).
% cnf(118,plain,(iext(uri_owl_equivalentProperty,X1,X2)|iext(X2,esk8_2(X1,X2),esk9_2(X1,X2))|iext(X1,esk8_2(X1,X2),esk9_2(X1,X2))|~ip(X2)|~ip(X1)),inference(split_conjunct,[status(thm)],[117])).
% cnf(119,plain,(iext(uri_owl_equivalentProperty,X1,X2)|~ip(X2)|~ip(X1)|~iext(X2,esk8_2(X1,X2),esk9_2(X1,X2))|~iext(X1,esk8_2(X1,X2),esk9_2(X1,X2))),inference(split_conjunct,[status(thm)],[117])).
% cnf(129,negated_conjecture,(~iext(uri_owl_equivalentProperty,uri_ex_p3,uri_ex_p1)),inference(split_conjunct,[status(thm)],[26])).
% cnf(134,plain,(ip(uri_ex_p1)),inference(spm,[status(thm)],[45,111,theory(equality)])).
% cnf(138,plain,(ip(uri_ex_p3)),inference(spm,[status(thm)],[46,112,theory(equality)])).
% cnf(142,plain,(iext(uri_ex_p1,X1,X2)|~iext(uri_ex_p2,X2,X1)),inference(spm,[status(thm)],[48,111,theory(equality)])).
% cnf(143,plain,(iext(uri_ex_p2,X1,X2)|~iext(uri_ex_p3,X2,X1)),inference(spm,[status(thm)],[48,112,theory(equality)])).
% cnf(174,plain,(iext(uri_ex_p2,X1,X2)|~iext(uri_ex_p1,X2,X1)),inference(spm,[status(thm)],[47,111,theory(equality)])).
% cnf(175,plain,(iext(uri_ex_p3,X1,X2)|~iext(uri_ex_p2,X2,X1)),inference(spm,[status(thm)],[47,112,theory(equality)])).
% cnf(237,plain,(iext(uri_rdfs_subPropertyOf,X1,X2)|~ip(X1)|~iext(X2,esk5_2(X1,X2),esk6_2(X1,X2))),inference(csr,[status(thm)],[64,109])).
% cnf(241,plain,(iext(uri_owl_equivalentProperty,X1,X2)|~ip(X2)|~iext(X2,esk8_2(X1,X2),esk9_2(X1,X2))|~iext(X1,esk8_2(X1,X2),esk9_2(X1,X2))),inference(csr,[status(thm)],[119,109])).
% cnf(242,plain,(iext(uri_owl_equivalentProperty,X1,X2)|~iext(X2,esk8_2(X1,X2),esk9_2(X1,X2))|~iext(X1,esk8_2(X1,X2),esk9_2(X1,X2))),inference(csr,[status(thm)],[241,109])).
% cnf(250,plain,(iext(X1,esk8_2(X1,uri_ex_p1),esk9_2(X1,uri_ex_p1))|iext(uri_ex_p1,esk8_2(X1,uri_ex_p1),esk9_2(X1,uri_ex_p1))|iext(uri_owl_equivalentProperty,X1,uri_ex_p1)|~ip(X1)),inference(spm,[status(thm)],[118,134,theory(equality)])).
% cnf(276,plain,(iext(uri_rdfs_subPropertyOf,X1,uri_ex_p1)|~ip(X1)|~iext(uri_ex_p2,esk6_2(X1,uri_ex_p1),esk5_2(X1,uri_ex_p1))),inference(spm,[status(thm)],[237,142,theory(equality)])).
% cnf(325,plain,(iext(uri_ex_p2,esk6_2(uri_ex_p1,X1),esk5_2(uri_ex_p1,X1))|iext(uri_rdfs_subPropertyOf,uri_ex_p1,X1)|~ip(X1)|~ip(uri_ex_p1)),inference(spm,[status(thm)],[174,65,theory(equality)])).
% cnf(329,plain,(iext(uri_ex_p2,esk6_2(uri_ex_p1,X1),esk5_2(uri_ex_p1,X1))|iext(uri_rdfs_subPropertyOf,uri_ex_p1,X1)|~ip(X1)|$false),inference(rw,[status(thm)],[325,134,theory(equality)])).
% cnf(330,plain,(iext(uri_ex_p2,esk6_2(uri_ex_p1,X1),esk5_2(uri_ex_p1,X1))|iext(uri_rdfs_subPropertyOf,uri_ex_p1,X1)|~ip(X1)),inference(cn,[status(thm)],[329,theory(equality)])).
% cnf(525,plain,(iext(uri_rdfs_subPropertyOf,X1,uri_ex_p1)|~ip(X1)|~iext(uri_ex_p3,esk5_2(X1,uri_ex_p1),esk6_2(X1,uri_ex_p1))),inference(spm,[status(thm)],[276,143,theory(equality)])).
% cnf(541,plain,(iext(uri_rdfs_subPropertyOf,uri_ex_p3,uri_ex_p1)|~ip(uri_ex_p3)|~ip(uri_ex_p1)),inference(spm,[status(thm)],[525,65,theory(equality)])).
% cnf(542,plain,(iext(uri_rdfs_subPropertyOf,uri_ex_p3,uri_ex_p1)|$false|~ip(uri_ex_p1)),inference(rw,[status(thm)],[541,138,theory(equality)])).
% cnf(543,plain,(iext(uri_rdfs_subPropertyOf,uri_ex_p3,uri_ex_p1)|$false|$false),inference(rw,[status(thm)],[542,134,theory(equality)])).
% cnf(544,plain,(iext(uri_rdfs_subPropertyOf,uri_ex_p3,uri_ex_p1)),inference(cn,[status(thm)],[543,theory(equality)])).
% cnf(549,plain,(iext(uri_ex_p1,X1,X2)|~iext(uri_ex_p3,X1,X2)),inference(spm,[status(thm)],[68,544,theory(equality)])).
% cnf(678,plain,(iext(uri_ex_p3,esk5_2(uri_ex_p1,X1),esk6_2(uri_ex_p1,X1))|iext(uri_rdfs_subPropertyOf,uri_ex_p1,X1)|~ip(X1)),inference(spm,[status(thm)],[175,330,theory(equality)])).
% cnf(733,plain,(iext(uri_rdfs_subPropertyOf,uri_ex_p1,uri_ex_p3)|~ip(uri_ex_p1)|~ip(uri_ex_p3)),inference(spm,[status(thm)],[237,678,theory(equality)])).
% cnf(736,plain,(iext(uri_rdfs_subPropertyOf,uri_ex_p1,uri_ex_p3)|$false|~ip(uri_ex_p3)),inference(rw,[status(thm)],[733,134,theory(equality)])).
% cnf(737,plain,(iext(uri_rdfs_subPropertyOf,uri_ex_p1,uri_ex_p3)|$false|$false),inference(rw,[status(thm)],[736,138,theory(equality)])).
% cnf(738,plain,(iext(uri_rdfs_subPropertyOf,uri_ex_p1,uri_ex_p3)),inference(cn,[status(thm)],[737,theory(equality)])).
% cnf(746,plain,(iext(uri_ex_p3,X1,X2)|~iext(uri_ex_p1,X1,X2)),inference(spm,[status(thm)],[68,738,theory(equality)])).
% cnf(1296,plain,(iext(uri_ex_p1,esk8_2(uri_ex_p3,uri_ex_p1),esk9_2(uri_ex_p3,uri_ex_p1))|iext(uri_ex_p3,esk8_2(uri_ex_p3,uri_ex_p1),esk9_2(uri_ex_p3,uri_ex_p1))|iext(uri_owl_equivalentProperty,uri_ex_p3,uri_ex_p1)),inference(spm,[status(thm)],[250,138,theory(equality)])).
% cnf(1300,plain,(iext(uri_ex_p1,esk8_2(uri_ex_p3,uri_ex_p1),esk9_2(uri_ex_p3,uri_ex_p1))|iext(uri_ex_p3,esk8_2(uri_ex_p3,uri_ex_p1),esk9_2(uri_ex_p3,uri_ex_p1))),inference(sr,[status(thm)],[1296,129,theory(equality)])).
% cnf(1301,plain,(iext(uri_ex_p1,esk8_2(uri_ex_p3,uri_ex_p1),esk9_2(uri_ex_p3,uri_ex_p1))),inference(csr,[status(thm)],[1300,549])).
% cnf(1303,plain,(iext(uri_owl_equivalentProperty,uri_ex_p3,uri_ex_p1)|~iext(uri_ex_p3,esk8_2(uri_ex_p3,uri_ex_p1),esk9_2(uri_ex_p3,uri_ex_p1))),inference(spm,[status(thm)],[242,1301,theory(equality)])).
% cnf(1304,plain,(iext(uri_ex_p3,esk8_2(uri_ex_p3,uri_ex_p1),esk9_2(uri_ex_p3,uri_ex_p1))),inference(spm,[status(thm)],[746,1301,theory(equality)])).
% cnf(1307,plain,(~iext(uri_ex_p3,esk8_2(uri_ex_p3,uri_ex_p1),esk9_2(uri_ex_p3,uri_ex_p1))),inference(sr,[status(thm)],[1303,129,theory(equality)])).
% cnf(1314,plain,($false),inference(rw,[status(thm)],[1307,1304,theory(equality)])).
% cnf(1315,plain,($false),inference(cn,[status(thm)],[1314,theory(equality)])).
% cnf(1316,plain,($false),1315,['proof']).
% # SZS output end CNFRefutation
% # Processed clauses : 319
% # ...of these trivial : 2
% # ...subsumed : 123
% # ...remaining for further processing: 194
% # Other redundant clauses eliminated : 0
% # Clauses deleted for lack of memory : 0
% # Backward-subsumed : 5
% # Backward-rewritten : 6
% # Generated clauses : 785
% # ...of the previous two non-trivial : 637
% # Contextual simplify-reflections : 114
% # Paramodulations : 785
% # Factorizations : 0
% # Equation resolutions : 0
% # Current number of processed clauses: 182
% # Positive orientable unit clauses: 18
% # Positive unorientable unit clauses: 0
% # Negative unit clauses : 3
% # Non-unit-clauses : 161
% # Current number of unprocessed clauses: 341
% # ...number of literals in the above : 1715
% # Clause-clause subsumption calls (NU) : 2049
% # Rec. Clause-clause subsumption calls : 1238
% # Unit Clause-clause subsumption calls : 15
% # Rewrite failures with RHS unbound : 0
% # Indexed BW rewrite attempts : 10
% # Indexed BW rewrite successes : 3
% # Backwards rewriting index: 245 leaves, 1.47+/-1.837 terms/leaf
% # Paramod-from index: 89 leaves, 1.24+/-0.687 terms/leaf
% # Paramod-into index: 189 leaves, 1.32+/-1.291 terms/leaf
% # -------------------------------------------------
% # User time : 0.060 s
% # System time : 0.003 s
% # Total time : 0.063 s
% # Maximum resident set size: 0 pages
% PrfWatch: 0.17 CPU 0.26 WC
% FINAL PrfWatch: 0.17 CPU 0.26 WC
% SZS output end Solution for /tmp/SystemOnTPTP10750/SWB067+1.tptp
%
%------------------------------------------------------------------------------