%------------------------------------------------------------------------------
% File : LEO-II---2.3.1
% Problem : SWB015+1 : TPTP v9.3.1. Released v5.2.0.
% Transfm : none
% Format : tptp:raw
% Command : leo --cores 7 --timeout 300 --proofoutput 1 --foatp e --atp e=/export/starexec/sandbox2/solver/bin/eprover /export/starexec/sandbox2/benchmark/theBenchmark.p
% Computer : n010.cluster.edu
% Model : x86_64 x86_64
% CPU : Intel(R) Xeon(R) CPU E5-2620 v4 2.10GHz
% Memory : 8046.5625MB
% OS : Linux 6.8.0-71-generic
% CPULimit : 300s
% WCLimit : 300s
% DateTime : Wed Oct 7 10:50:42 AM UTC 2026
% Result : Theorem 3.01s 0.74s
% Output : CNFRefutation 3.01s
% Verified :
% SZS Type : Refutation
% Derivation depth : 14
% Number of leaves : 10
% Syntax : Number of formulae : 103 ( 66 unt; 0 typ; 0 def)
% Number of atoms : 492 ( 169 equ; 0 cnn)
% Maximal formula atoms : 3 ( 4 avg)
% Number of connectives : 808 ( 169 ~; 104 |; 9 &; 508 @)
% ( 6 <=>; 12 =>; 0 <=; 0 <~>)
% Maximal formula depth : 9 ( 3 avg)
% Number of types : 2 ( 0 usr)
% Number of type conns : 0 ( 0 >; 0 *; 0 +; 0 <<)
% Number of symbols : 172 ( 169 usr; 159 con; 0-3 aty)
% Number of variables : 219 ( 0 ^; 219 !; 0 ?; 219 :)
% Comments :
%------------------------------------------------------------------------------
thf(tp_dat_str_0,type,
dat_str_0: $i ).
thf(tp_dat_str_1,type,
dat_str_1: $i ).
thf(tp_dat_str_2,type,
dat_str_2: $i ).
thf(tp_dat_str_3,type,
dat_str_3: $i ).
thf(tp_ic,type,
ic: $i > $o ).
thf(tp_icext,type,
icext: $i > $i > $o ).
thf(tp_idc,type,
idc: $i > $o ).
thf(tp_iext,type,
iext: $i > $i > $i > $o ).
thf(tp_ioap,type,
ioap: $i > $o ).
thf(tp_iodp,type,
iodp: $i > $o ).
thf(tp_ioxp,type,
ioxp: $i > $o ).
thf(tp_ip,type,
ip: $i > $o ).
thf(tp_ir,type,
ir: $i > $o ).
thf(tp_ix,type,
ix: $i > $o ).
thf(tp_literal_typed,type,
literal_typed: $i > $i > $i ).
thf(tp_lv,type,
lv: $i > $o ).
thf(tp_tautology,type,
tautology: $o ).
thf(tp_uri_owl_AllDifferent,type,
uri_owl_AllDifferent: $i ).
thf(tp_uri_owl_AllDisjointClasses,type,
uri_owl_AllDisjointClasses: $i ).
thf(tp_uri_owl_AllDisjointProperties,type,
uri_owl_AllDisjointProperties: $i ).
thf(tp_uri_owl_Annotation,type,
uri_owl_Annotation: $i ).
thf(tp_uri_owl_AnnotationProperty,type,
uri_owl_AnnotationProperty: $i ).
thf(tp_uri_owl_AsymmetricProperty,type,
uri_owl_AsymmetricProperty: $i ).
thf(tp_uri_owl_Axiom,type,
uri_owl_Axiom: $i ).
thf(tp_uri_owl_Class,type,
uri_owl_Class: $i ).
thf(tp_uri_owl_DataRange,type,
uri_owl_DataRange: $i ).
thf(tp_uri_owl_DatatypeProperty,type,
uri_owl_DatatypeProperty: $i ).
thf(tp_uri_owl_DeprecatedClass,type,
uri_owl_DeprecatedClass: $i ).
thf(tp_uri_owl_DeprecatedProperty,type,
uri_owl_DeprecatedProperty: $i ).
thf(tp_uri_owl_FunctionalProperty,type,
uri_owl_FunctionalProperty: $i ).
thf(tp_uri_owl_InverseFunctionalProperty,type,
uri_owl_InverseFunctionalProperty: $i ).
thf(tp_uri_owl_IrreflexiveProperty,type,
uri_owl_IrreflexiveProperty: $i ).
thf(tp_uri_owl_IrreflexiveReflexiveProperty,type,
uri_owl_IrreflexiveReflexiveProperty: $i ).
thf(tp_uri_owl_NamedIndividual,type,
uri_owl_NamedIndividual: $i ).
thf(tp_uri_owl_NegativePropertyAssertion,type,
uri_owl_NegativePropertyAssertion: $i ).
thf(tp_uri_owl_Nothing,type,
uri_owl_Nothing: $i ).
thf(tp_uri_owl_ObjectProperty,type,
uri_owl_ObjectProperty: $i ).
thf(tp_uri_owl_Ontology,type,
uri_owl_Ontology: $i ).
thf(tp_uri_owl_OntologyProperty,type,
uri_owl_OntologyProperty: $i ).
thf(tp_uri_owl_ReflexiveProperty,type,
uri_owl_ReflexiveProperty: $i ).
thf(tp_uri_owl_Restriction,type,
uri_owl_Restriction: $i ).
thf(tp_uri_owl_SymmetricProperty,type,
uri_owl_SymmetricProperty: $i ).
thf(tp_uri_owl_Thing,type,
uri_owl_Thing: $i ).
thf(tp_uri_owl_TransitiveProperty,type,
uri_owl_TransitiveProperty: $i ).
thf(tp_uri_owl_allValuesFrom,type,
uri_owl_allValuesFrom: $i ).
thf(tp_uri_owl_annotatedProperty,type,
uri_owl_annotatedProperty: $i ).
thf(tp_uri_owl_annotatedSource,type,
uri_owl_annotatedSource: $i ).
thf(tp_uri_owl_annotatedTarget,type,
uri_owl_annotatedTarget: $i ).
thf(tp_uri_owl_assertionProperty,type,
uri_owl_assertionProperty: $i ).
thf(tp_uri_owl_backwardCompatibleWith,type,
uri_owl_backwardCompatibleWith: $i ).
thf(tp_uri_owl_bottomDataProperty,type,
uri_owl_bottomDataProperty: $i ).
thf(tp_uri_owl_bottomObjectProperty,type,
uri_owl_bottomObjectProperty: $i ).
thf(tp_uri_owl_cardinality,type,
uri_owl_cardinality: $i ).
thf(tp_uri_owl_complementOf,type,
uri_owl_complementOf: $i ).
thf(tp_uri_owl_datatypeComplementOf,type,
uri_owl_datatypeComplementOf: $i ).
thf(tp_uri_owl_deprecated,type,
uri_owl_deprecated: $i ).
thf(tp_uri_owl_differentFrom,type,
uri_owl_differentFrom: $i ).
thf(tp_uri_owl_disjointUnionOf,type,
uri_owl_disjointUnionOf: $i ).
thf(tp_uri_owl_disjointWith,type,
uri_owl_disjointWith: $i ).
thf(tp_uri_owl_distinctMembers,type,
uri_owl_distinctMembers: $i ).
thf(tp_uri_owl_equivalentClass,type,
uri_owl_equivalentClass: $i ).
thf(tp_uri_owl_equivalentProperty,type,
uri_owl_equivalentProperty: $i ).
thf(tp_uri_owl_hasKey,type,
uri_owl_hasKey: $i ).
thf(tp_uri_owl_hasSelf,type,
uri_owl_hasSelf: $i ).
thf(tp_uri_owl_hasValue,type,
uri_owl_hasValue: $i ).
thf(tp_uri_owl_imports,type,
uri_owl_imports: $i ).
thf(tp_uri_owl_incompatibleWith,type,
uri_owl_incompatibleWith: $i ).
thf(tp_uri_owl_intersectionOf,type,
uri_owl_intersectionOf: $i ).
thf(tp_uri_owl_inverseOf,type,
uri_owl_inverseOf: $i ).
thf(tp_uri_owl_maxCardinality,type,
uri_owl_maxCardinality: $i ).
thf(tp_uri_owl_maxQualifiedCardinality,type,
uri_owl_maxQualifiedCardinality: $i ).
thf(tp_uri_owl_members,type,
uri_owl_members: $i ).
thf(tp_uri_owl_minCardinality,type,
uri_owl_minCardinality: $i ).
thf(tp_uri_owl_minQualifiedCardinality,type,
uri_owl_minQualifiedCardinality: $i ).
thf(tp_uri_owl_onClass,type,
uri_owl_onClass: $i ).
thf(tp_uri_owl_onDataRange,type,
uri_owl_onDataRange: $i ).
thf(tp_uri_owl_onDatatype,type,
uri_owl_onDatatype: $i ).
thf(tp_uri_owl_onProperty,type,
uri_owl_onProperty: $i ).
thf(tp_uri_owl_oneOf,type,
uri_owl_oneOf: $i ).
thf(tp_uri_owl_priorVersion,type,
uri_owl_priorVersion: $i ).
thf(tp_uri_owl_propertyChainAxiom,type,
uri_owl_propertyChainAxiom: $i ).
thf(tp_uri_owl_propertyDisjointWith,type,
uri_owl_propertyDisjointWith: $i ).
thf(tp_uri_owl_qualifiedCardinality,type,
uri_owl_qualifiedCardinality: $i ).
thf(tp_uri_owl_rational,type,
uri_owl_rational: $i ).
thf(tp_uri_owl_real,type,
uri_owl_real: $i ).
thf(tp_uri_owl_sameAs,type,
uri_owl_sameAs: $i ).
thf(tp_uri_owl_someValuesFrom,type,
uri_owl_someValuesFrom: $i ).
thf(tp_uri_owl_sourceIndividual,type,
uri_owl_sourceIndividual: $i ).
thf(tp_uri_owl_targetIndividual,type,
uri_owl_targetIndividual: $i ).
thf(tp_uri_owl_targetValue,type,
uri_owl_targetValue: $i ).
thf(tp_uri_owl_topDataProperty,type,
uri_owl_topDataProperty: $i ).
thf(tp_uri_owl_topObjectProperty,type,
uri_owl_topObjectProperty: $i ).
thf(tp_uri_owl_unionOf,type,
uri_owl_unionOf: $i ).
thf(tp_uri_owl_versionIRI,type,
uri_owl_versionIRI: $i ).
thf(tp_uri_owl_versionInfo,type,
uri_owl_versionInfo: $i ).
thf(tp_uri_owl_withRestrictions,type,
uri_owl_withRestrictions: $i ).
thf(tp_uri_rdf_Alt,type,
uri_rdf_Alt: $i ).
thf(tp_uri_rdf_Bag,type,
uri_rdf_Bag: $i ).
thf(tp_uri_rdf_List,type,
uri_rdf_List: $i ).
thf(tp_uri_rdf_PlainLiteral,type,
uri_rdf_PlainLiteral: $i ).
thf(tp_uri_rdf_Property,type,
uri_rdf_Property: $i ).
thf(tp_uri_rdf_XMLLiteral,type,
uri_rdf_XMLLiteral: $i ).
thf(tp_uri_rdf__1,type,
uri_rdf__1: $i ).
thf(tp_uri_rdf__2,type,
uri_rdf__2: $i ).
thf(tp_uri_rdf__3,type,
uri_rdf__3: $i ).
thf(tp_uri_rdf_first,type,
uri_rdf_first: $i ).
thf(tp_uri_rdf_langRange,type,
uri_rdf_langRange: $i ).
thf(tp_uri_rdf_nil,type,
uri_rdf_nil: $i ).
thf(tp_uri_rdf_object,type,
uri_rdf_object: $i ).
thf(tp_uri_rdf_predicate,type,
uri_rdf_predicate: $i ).
thf(tp_uri_rdf_rest,type,
uri_rdf_rest: $i ).
thf(tp_uri_rdf_subject,type,
uri_rdf_subject: $i ).
thf(tp_uri_rdf_type,type,
uri_rdf_type: $i ).
thf(tp_uri_rdf_value,type,
uri_rdf_value: $i ).
thf(tp_uri_rdfs_Class,type,
uri_rdfs_Class: $i ).
thf(tp_uri_rdfs_Container,type,
uri_rdfs_Container: $i ).
thf(tp_uri_rdfs_ContainerMembershipProperty,type,
uri_rdfs_ContainerMembershipProperty: $i ).
thf(tp_uri_rdfs_Datatype,type,
uri_rdfs_Datatype: $i ).
thf(tp_uri_rdfs_Literal,type,
uri_rdfs_Literal: $i ).
thf(tp_uri_rdfs_Resource,type,
uri_rdfs_Resource: $i ).
thf(tp_uri_rdfs_Seq,type,
uri_rdfs_Seq: $i ).
thf(tp_uri_rdfs_Statement,type,
uri_rdfs_Statement: $i ).
thf(tp_uri_rdfs_comment,type,
uri_rdfs_comment: $i ).
thf(tp_uri_rdfs_domain,type,
uri_rdfs_domain: $i ).
thf(tp_uri_rdfs_isDefinedBy,type,
uri_rdfs_isDefinedBy: $i ).
thf(tp_uri_rdfs_label,type,
uri_rdfs_label: $i ).
thf(tp_uri_rdfs_member,type,
uri_rdfs_member: $i ).
thf(tp_uri_rdfs_range,type,
uri_rdfs_range: $i ).
thf(tp_uri_rdfs_seeAlso,type,
uri_rdfs_seeAlso: $i ).
thf(tp_uri_rdfs_subClassOf,type,
uri_rdfs_subClassOf: $i ).
thf(tp_uri_rdfs_subPropertyOf,type,
uri_rdfs_subPropertyOf: $i ).
thf(tp_uri_xml_nonNegativeInteger,type,
uri_xml_nonNegativeInteger: $i ).
thf(tp_uri_xsd_NCName,type,
uri_xsd_NCName: $i ).
thf(tp_uri_xsd_NMTOKEN,type,
uri_xsd_NMTOKEN: $i ).
thf(tp_uri_xsd_Name,type,
uri_xsd_Name: $i ).
thf(tp_uri_xsd_anyURI,type,
uri_xsd_anyURI: $i ).
thf(tp_uri_xsd_base64Binary,type,
uri_xsd_base64Binary: $i ).
thf(tp_uri_xsd_boolean,type,
uri_xsd_boolean: $i ).
thf(tp_uri_xsd_byte,type,
uri_xsd_byte: $i ).
thf(tp_uri_xsd_dateTime,type,
uri_xsd_dateTime: $i ).
thf(tp_uri_xsd_dateTimeStamp,type,
uri_xsd_dateTimeStamp: $i ).
thf(tp_uri_xsd_decimal,type,
uri_xsd_decimal: $i ).
thf(tp_uri_xsd_double,type,
uri_xsd_double: $i ).
thf(tp_uri_xsd_float,type,
uri_xsd_float: $i ).
thf(tp_uri_xsd_hexBinary,type,
uri_xsd_hexBinary: $i ).
thf(tp_uri_xsd_int,type,
uri_xsd_int: $i ).
thf(tp_uri_xsd_integer,type,
uri_xsd_integer: $i ).
thf(tp_uri_xsd_language,type,
uri_xsd_language: $i ).
thf(tp_uri_xsd_length,type,
uri_xsd_length: $i ).
thf(tp_uri_xsd_long,type,
uri_xsd_long: $i ).
thf(tp_uri_xsd_maxExclusive,type,
uri_xsd_maxExclusive: $i ).
thf(tp_uri_xsd_maxInclusive,type,
uri_xsd_maxInclusive: $i ).
thf(tp_uri_xsd_maxLength,type,
uri_xsd_maxLength: $i ).
thf(tp_uri_xsd_minExclusive,type,
uri_xsd_minExclusive: $i ).
thf(tp_uri_xsd_minInclusive,type,
uri_xsd_minInclusive: $i ).
thf(tp_uri_xsd_minLength,type,
uri_xsd_minLength: $i ).
thf(tp_uri_xsd_negativeInteger,type,
uri_xsd_negativeInteger: $i ).
thf(tp_uri_xsd_nonNegativeInteger,type,
uri_xsd_nonNegativeInteger: $i ).
thf(tp_uri_xsd_nonPositiveInteger,type,
uri_xsd_nonPositiveInteger: $i ).
thf(tp_uri_xsd_normalizedString,type,
uri_xsd_normalizedString: $i ).
thf(tp_uri_xsd_pattern,type,
uri_xsd_pattern: $i ).
thf(tp_uri_xsd_positiveInteger,type,
uri_xsd_positiveInteger: $i ).
thf(tp_uri_xsd_short,type,
uri_xsd_short: $i ).
thf(tp_uri_xsd_string,type,
uri_xsd_string: $i ).
thf(tp_uri_xsd_token,type,
uri_xsd_token: $i ).
thf(tp_uri_xsd_unsignedByte,type,
uri_xsd_unsignedByte: $i ).
thf(tp_uri_xsd_unsignedInt,type,
uri_xsd_unsignedInt: $i ).
thf(tp_uri_xsd_unsignedLong,type,
uri_xsd_unsignedLong: $i ).
thf(tp_uri_xsd_unsignedShort,type,
uri_xsd_unsignedShort: $i ).
thf(205,axiom,
! [X: $i,Y: $i] :
( ( iext @ uri_owl_sameAs @ X @ Y )
<=> ( X = Y ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',owl_eqdis_sameas) ).
thf(214,axiom,
! [X: $i,Y: $i] :
( ( iext @ uri_owl_differentFrom @ X @ Y )
<=> ( X != Y ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',owl_eqdis_differentfrom) ).
thf(304,axiom,
ip @ uri_owl_sameAs,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',owl_prop_sameas_type) ).
thf(305,axiom,
! [X: $i,Y: $i] :
( ( iext @ uri_owl_sameAs @ X @ Y )
=> ( ( ir @ X )
& ( ir @ Y ) ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',owl_prop_sameas_ext) ).
thf(377,axiom,
! [X: $i,Y: $i] :
~ ( iext @ uri_owl_bottomObjectProperty @ X @ Y ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',owl_prop_bottomobjectproperty_ext) ).
thf(379,axiom,
! [X: $i,Y: $i] :
~ ( iext @ uri_owl_bottomDataProperty @ X @ Y ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',owl_prop_bottomdataproperty_ext) ).
thf(483,axiom,
! [P: $i,Q: $i,R: $i] :
( ( ( iext @ uri_rdfs_subPropertyOf @ P @ Q )
& ( iext @ uri_rdfs_subPropertyOf @ Q @ R ) )
=> ( iext @ uri_rdfs_subPropertyOf @ P @ R ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rdfs_subpropertyof_trans) ).
thf(488,axiom,
! [C: $i,D: $i,E: $i] :
( ( ( iext @ uri_rdfs_subClassOf @ C @ D )
& ( iext @ uri_rdfs_subClassOf @ D @ E ) )
=> ( iext @ uri_rdfs_subClassOf @ C @ E ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',rdfs_subclassof_trans) ).
thf(558,axiom,
! [S: $i,P: $i,O: $i] :
( ( iext @ P @ S @ O )
=> ( ip @ P ) ),
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',simple_iext_property) ).
thf(559,conjecture,
iext @ uri_owl_sameAs @ uri_owl_sameAs @ uri_owl_sameAs,
file('/export/starexec/sandbox2/benchmark/theBenchmark.p',testcase_conclusion_fullish_015_Reflective_Tautologies_I) ).
thf(560,negated_conjecture,
( ( iext @ uri_owl_sameAs @ uri_owl_sameAs @ uri_owl_sameAs )
= $false ),
inference(negate_conjecture,[status(cth)],[559]) ).
thf(561,plain,
( ( iext @ uri_owl_sameAs @ uri_owl_sameAs @ uri_owl_sameAs )
= $false ),
inference(unfold_def,[status(thm)],[560]) ).
thf(562,plain,
( ( ! [X: $i,Y: $i] :
( ( iext @ uri_owl_sameAs @ X @ Y )
<=> ( X = Y ) ) )
= $true ),
inference(unfold_def,[status(thm)],[205]) ).
thf(563,plain,
( ( ! [X: $i,Y: $i] :
( ( iext @ uri_owl_differentFrom @ X @ Y )
<=> ( X != Y ) ) )
= $true ),
inference(unfold_def,[status(thm)],[214]) ).
thf(564,plain,
( ( ip @ uri_owl_sameAs )
= $true ),
inference(unfold_def,[status(thm)],[304]) ).
thf(565,plain,
( ( ! [X: $i,Y: $i] :
( ( iext @ uri_owl_sameAs @ X @ Y )
=> ( ( ir @ X )
& ( ir @ Y ) ) ) )
= $true ),
inference(unfold_def,[status(thm)],[305]) ).
thf(566,plain,
( ( ! [X: $i,Y: $i] :
~ ( iext @ uri_owl_bottomObjectProperty @ X @ Y ) )
= $true ),
inference(unfold_def,[status(thm)],[377]) ).
thf(567,plain,
( ( ! [X: $i,Y: $i] :
~ ( iext @ uri_owl_bottomDataProperty @ X @ Y ) )
= $true ),
inference(unfold_def,[status(thm)],[379]) ).
thf(568,plain,
( ( ! [P: $i,Q: $i,R: $i] :
( ( ( iext @ uri_rdfs_subPropertyOf @ P @ Q )
& ( iext @ uri_rdfs_subPropertyOf @ Q @ R ) )
=> ( iext @ uri_rdfs_subPropertyOf @ P @ R ) ) )
= $true ),
inference(unfold_def,[status(thm)],[483]) ).
thf(569,plain,
( ( ! [C: $i,D: $i,E: $i] :
( ( ( iext @ uri_rdfs_subClassOf @ C @ D )
& ( iext @ uri_rdfs_subClassOf @ D @ E ) )
=> ( iext @ uri_rdfs_subClassOf @ C @ E ) ) )
= $true ),
inference(unfold_def,[status(thm)],[488]) ).
thf(570,plain,
( ( ! [S: $i,P: $i,O: $i] :
( ( iext @ P @ S @ O )
=> ( ip @ P ) ) )
= $true ),
inference(unfold_def,[status(thm)],[558]) ).
thf(571,plain,
( ( ~ ( iext @ uri_owl_sameAs @ uri_owl_sameAs @ uri_owl_sameAs ) )
= $true ),
inference(polarity_switch,[status(thm)],[561]) ).
thf(572,plain,
( ( ! [S: $i,P: $i,O: $i] :
( ( iext @ P @ S @ O )
=> ( ip @ P ) ) )
= $true ),
inference(copy,[status(thm)],[570]) ).
thf(573,plain,
( ( ! [C: $i,D: $i,E: $i] :
( ( ( iext @ uri_rdfs_subClassOf @ C @ D )
& ( iext @ uri_rdfs_subClassOf @ D @ E ) )
=> ( iext @ uri_rdfs_subClassOf @ C @ E ) ) )
= $true ),
inference(copy,[status(thm)],[569]) ).
thf(574,plain,
( ( ! [P: $i,Q: $i,R: $i] :
( ( ( iext @ uri_rdfs_subPropertyOf @ P @ Q )
& ( iext @ uri_rdfs_subPropertyOf @ Q @ R ) )
=> ( iext @ uri_rdfs_subPropertyOf @ P @ R ) ) )
= $true ),
inference(copy,[status(thm)],[568]) ).
thf(575,plain,
( ( ! [X: $i,Y: $i] :
~ ( iext @ uri_owl_bottomDataProperty @ X @ Y ) )
= $true ),
inference(copy,[status(thm)],[567]) ).
thf(576,plain,
( ( ! [X: $i,Y: $i] :
~ ( iext @ uri_owl_bottomObjectProperty @ X @ Y ) )
= $true ),
inference(copy,[status(thm)],[566]) ).
thf(577,plain,
( ( ! [X: $i,Y: $i] :
( ( iext @ uri_owl_sameAs @ X @ Y )
=> ( ( ir @ X )
& ( ir @ Y ) ) ) )
= $true ),
inference(copy,[status(thm)],[565]) ).
thf(578,plain,
( ( ip @ uri_owl_sameAs )
= $true ),
inference(copy,[status(thm)],[564]) ).
thf(579,plain,
( ( ! [X: $i,Y: $i] :
( ( iext @ uri_owl_differentFrom @ X @ Y )
<=> ( X != Y ) ) )
= $true ),
inference(copy,[status(thm)],[563]) ).
thf(580,plain,
( ( ! [X: $i,Y: $i] :
( ( iext @ uri_owl_sameAs @ X @ Y )
<=> ( X = Y ) ) )
= $true ),
inference(copy,[status(thm)],[562]) ).
thf(581,plain,
( ( ~ ( iext @ uri_owl_sameAs @ uri_owl_sameAs @ uri_owl_sameAs ) )
= $true ),
inference(copy,[status(thm)],[571]) ).
thf(582,plain,
( ( ! [SX0: $i,SX1: $i,SX2: $i] :
( ~ ( iext @ SX1 @ SX0 @ SX2 )
| ( ip @ SX1 ) ) )
= $true ),
inference(unfold_def,[status(thm)],[572]) ).
thf(583,plain,
( ( ! [SX0: $i,SX1: $i,SX2: $i] :
( ~ ~ ( ~ ( iext @ uri_rdfs_subClassOf @ SX0 @ SX1 )
| ~ ( iext @ uri_rdfs_subClassOf @ SX1 @ SX2 ) )
| ( iext @ uri_rdfs_subClassOf @ SX0 @ SX2 ) ) )
= $true ),
inference(unfold_def,[status(thm)],[573]) ).
thf(584,plain,
( ( ! [SX0: $i,SX1: $i] :
( ~ ( iext @ uri_owl_sameAs @ SX0 @ SX1 )
| ~ ( ~ ( ir @ SX0 )
| ~ ( ir @ SX1 ) ) ) )
= $true ),
inference(unfold_def,[status(thm)],[577]) ).
thf(585,plain,
( ( ! [SX0: $i,SX1: $i] :
~ ( ~ ( ~ ( iext @ uri_owl_differentFrom @ SX0 @ SX1 )
| ( SX0 != SX1 ) )
| ~ ( ~ ( ( SX0 != SX1 ) )
| ( iext @ uri_owl_differentFrom @ SX0 @ SX1 ) ) ) )
= $true ),
inference(unfold_def,[status(thm)],[579]) ).
thf(586,plain,
( ( ! [SX0: $i,SX1: $i,SX2: $i] :
( ~ ~ ( ~ ( iext @ uri_rdfs_subPropertyOf @ SX0 @ SX1 )
| ~ ( iext @ uri_rdfs_subPropertyOf @ SX1 @ SX2 ) )
| ( iext @ uri_rdfs_subPropertyOf @ SX0 @ SX2 ) ) )
= $true ),
inference(unfold_def,[status(thm)],[574]) ).
thf(587,plain,
( ( ! [SX0: $i,SX1: $i] :
~ ( ~ ( ~ ( iext @ uri_owl_sameAs @ SX0 @ SX1 )
| ( SX0 = SX1 ) )
| ~ ( ( SX0 != SX1 )
| ( iext @ uri_owl_sameAs @ SX0 @ SX1 ) ) ) )
= $true ),
inference(unfold_def,[status(thm)],[580]) ).
thf(588,plain,
! [SV1: $i] :
( ( ! [SY19: $i] :
~ ( iext @ uri_owl_bottomDataProperty @ SV1 @ SY19 ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[575]) ).
thf(589,plain,
! [SV2: $i] :
( ( ! [SY20: $i] :
~ ( iext @ uri_owl_bottomObjectProperty @ SV2 @ SY20 ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[576]) ).
thf(590,plain,
( ( iext @ uri_owl_sameAs @ uri_owl_sameAs @ uri_owl_sameAs )
= $false ),
inference(extcnf_not_pos,[status(thm)],[581]) ).
thf(591,plain,
! [SV3: $i] :
( ( ! [SY21: $i,SY22: $i] :
( ~ ( iext @ SY21 @ SV3 @ SY22 )
| ( ip @ SY21 ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[582]) ).
thf(592,plain,
! [SV4: $i] :
( ( ! [SY23: $i,SY24: $i] :
( ~ ~ ( ~ ( iext @ uri_rdfs_subClassOf @ SV4 @ SY23 )
| ~ ( iext @ uri_rdfs_subClassOf @ SY23 @ SY24 ) )
| ( iext @ uri_rdfs_subClassOf @ SV4 @ SY24 ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[583]) ).
thf(593,plain,
! [SV5: $i] :
( ( ! [SY25: $i] :
( ~ ( iext @ uri_owl_sameAs @ SV5 @ SY25 )
| ~ ( ~ ( ir @ SV5 )
| ~ ( ir @ SY25 ) ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[584]) ).
thf(594,plain,
! [SV6: $i] :
( ( ! [SY26: $i] :
~ ( ~ ( ~ ( iext @ uri_owl_differentFrom @ SV6 @ SY26 )
| ( SV6 != SY26 ) )
| ~ ( ~ ( ( SV6 != SY26 ) )
| ( iext @ uri_owl_differentFrom @ SV6 @ SY26 ) ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[585]) ).
thf(595,plain,
! [SV7: $i] :
( ( ! [SY27: $i,SY28: $i] :
( ~ ~ ( ~ ( iext @ uri_rdfs_subPropertyOf @ SV7 @ SY27 )
| ~ ( iext @ uri_rdfs_subPropertyOf @ SY27 @ SY28 ) )
| ( iext @ uri_rdfs_subPropertyOf @ SV7 @ SY28 ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[586]) ).
thf(596,plain,
! [SV8: $i] :
( ( ! [SY29: $i] :
~ ( ~ ( ~ ( iext @ uri_owl_sameAs @ SV8 @ SY29 )
| ( SV8 = SY29 ) )
| ~ ( ( SV8 != SY29 )
| ( iext @ uri_owl_sameAs @ SV8 @ SY29 ) ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[587]) ).
thf(597,plain,
! [SV9: $i,SV1: $i] :
( ( ~ ( iext @ uri_owl_bottomDataProperty @ SV1 @ SV9 ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[588]) ).
thf(598,plain,
! [SV10: $i,SV2: $i] :
( ( ~ ( iext @ uri_owl_bottomObjectProperty @ SV2 @ SV10 ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[589]) ).
thf(599,plain,
! [SV3: $i,SV11: $i] :
( ( ! [SY30: $i] :
( ~ ( iext @ SV11 @ SV3 @ SY30 )
| ( ip @ SV11 ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[591]) ).
thf(600,plain,
! [SV12: $i,SV4: $i] :
( ( ! [SY31: $i] :
( ~ ~ ( ~ ( iext @ uri_rdfs_subClassOf @ SV4 @ SV12 )
| ~ ( iext @ uri_rdfs_subClassOf @ SV12 @ SY31 ) )
| ( iext @ uri_rdfs_subClassOf @ SV4 @ SY31 ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[592]) ).
thf(601,plain,
! [SV13: $i,SV5: $i] :
( ( ~ ( iext @ uri_owl_sameAs @ SV5 @ SV13 )
| ~ ( ~ ( ir @ SV5 )
| ~ ( ir @ SV13 ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[593]) ).
thf(602,plain,
! [SV14: $i,SV6: $i] :
( ( ~ ( ~ ( ~ ( iext @ uri_owl_differentFrom @ SV6 @ SV14 )
| ( SV6 != SV14 ) )
| ~ ( ~ ( ( SV6 != SV14 ) )
| ( iext @ uri_owl_differentFrom @ SV6 @ SV14 ) ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[594]) ).
thf(603,plain,
! [SV15: $i,SV7: $i] :
( ( ! [SY32: $i] :
( ~ ~ ( ~ ( iext @ uri_rdfs_subPropertyOf @ SV7 @ SV15 )
| ~ ( iext @ uri_rdfs_subPropertyOf @ SV15 @ SY32 ) )
| ( iext @ uri_rdfs_subPropertyOf @ SV7 @ SY32 ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[595]) ).
thf(604,plain,
! [SV16: $i,SV8: $i] :
( ( ~ ( ~ ( ~ ( iext @ uri_owl_sameAs @ SV8 @ SV16 )
| ( SV8 = SV16 ) )
| ~ ( ( SV8 != SV16 )
| ( iext @ uri_owl_sameAs @ SV8 @ SV16 ) ) ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[596]) ).
thf(605,plain,
! [SV9: $i,SV1: $i] :
( ( iext @ uri_owl_bottomDataProperty @ SV1 @ SV9 )
= $false ),
inference(extcnf_not_pos,[status(thm)],[597]) ).
thf(606,plain,
! [SV10: $i,SV2: $i] :
( ( iext @ uri_owl_bottomObjectProperty @ SV2 @ SV10 )
= $false ),
inference(extcnf_not_pos,[status(thm)],[598]) ).
thf(607,plain,
! [SV17: $i,SV3: $i,SV11: $i] :
( ( ~ ( iext @ SV11 @ SV3 @ SV17 )
| ( ip @ SV11 ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[599]) ).
thf(608,plain,
! [SV18: $i,SV12: $i,SV4: $i] :
( ( ~ ~ ( ~ ( iext @ uri_rdfs_subClassOf @ SV4 @ SV12 )
| ~ ( iext @ uri_rdfs_subClassOf @ SV12 @ SV18 ) )
| ( iext @ uri_rdfs_subClassOf @ SV4 @ SV18 ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[600]) ).
thf(609,plain,
! [SV13: $i,SV5: $i] :
( ( ( ~ ( iext @ uri_owl_sameAs @ SV5 @ SV13 ) )
= $true )
| ( ( ~ ( ~ ( ir @ SV5 )
| ~ ( ir @ SV13 ) ) )
= $true ) ),
inference(extcnf_or_pos,[status(thm)],[601]) ).
thf(610,plain,
! [SV14: $i,SV6: $i] :
( ( ~ ( ~ ( iext @ uri_owl_differentFrom @ SV6 @ SV14 )
| ( SV6 != SV14 ) )
| ~ ( ~ ( ( SV6 != SV14 ) )
| ( iext @ uri_owl_differentFrom @ SV6 @ SV14 ) ) )
= $false ),
inference(extcnf_not_pos,[status(thm)],[602]) ).
thf(611,plain,
! [SV19: $i,SV15: $i,SV7: $i] :
( ( ~ ~ ( ~ ( iext @ uri_rdfs_subPropertyOf @ SV7 @ SV15 )
| ~ ( iext @ uri_rdfs_subPropertyOf @ SV15 @ SV19 ) )
| ( iext @ uri_rdfs_subPropertyOf @ SV7 @ SV19 ) )
= $true ),
inference(extcnf_forall_pos,[status(thm)],[603]) ).
thf(612,plain,
! [SV16: $i,SV8: $i] :
( ( ~ ( ~ ( iext @ uri_owl_sameAs @ SV8 @ SV16 )
| ( SV8 = SV16 ) )
| ~ ( ( SV8 != SV16 )
| ( iext @ uri_owl_sameAs @ SV8 @ SV16 ) ) )
= $false ),
inference(extcnf_not_pos,[status(thm)],[604]) ).
thf(613,plain,
! [SV17: $i,SV3: $i,SV11: $i] :
( ( ( ~ ( iext @ SV11 @ SV3 @ SV17 ) )
= $true )
| ( ( ip @ SV11 )
= $true ) ),
inference(extcnf_or_pos,[status(thm)],[607]) ).
thf(614,plain,
! [SV18: $i,SV12: $i,SV4: $i] :
( ( ( ~ ~ ( ~ ( iext @ uri_rdfs_subClassOf @ SV4 @ SV12 )
| ~ ( iext @ uri_rdfs_subClassOf @ SV12 @ SV18 ) ) )
= $true )
| ( ( iext @ uri_rdfs_subClassOf @ SV4 @ SV18 )
= $true ) ),
inference(extcnf_or_pos,[status(thm)],[608]) ).
thf(615,plain,
! [SV13: $i,SV5: $i] :
( ( ( iext @ uri_owl_sameAs @ SV5 @ SV13 )
= $false )
| ( ( ~ ( ~ ( ir @ SV5 )
| ~ ( ir @ SV13 ) ) )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[609]) ).
thf(616,plain,
! [SV14: $i,SV6: $i] :
( ( ~ ( ~ ( iext @ uri_owl_differentFrom @ SV6 @ SV14 )
| ( SV6 != SV14 ) ) )
= $false ),
inference(extcnf_or_neg,[status(thm)],[610]) ).
thf(617,plain,
! [SV14: $i,SV6: $i] :
( ( ~ ( ~ ( ( SV6 != SV14 ) )
| ( iext @ uri_owl_differentFrom @ SV6 @ SV14 ) ) )
= $false ),
inference(extcnf_or_neg,[status(thm)],[610]) ).
thf(618,plain,
! [SV19: $i,SV15: $i,SV7: $i] :
( ( ( ~ ~ ( ~ ( iext @ uri_rdfs_subPropertyOf @ SV7 @ SV15 )
| ~ ( iext @ uri_rdfs_subPropertyOf @ SV15 @ SV19 ) ) )
= $true )
| ( ( iext @ uri_rdfs_subPropertyOf @ SV7 @ SV19 )
= $true ) ),
inference(extcnf_or_pos,[status(thm)],[611]) ).
thf(619,plain,
! [SV16: $i,SV8: $i] :
( ( ~ ( ~ ( iext @ uri_owl_sameAs @ SV8 @ SV16 )
| ( SV8 = SV16 ) ) )
= $false ),
inference(extcnf_or_neg,[status(thm)],[612]) ).
thf(620,plain,
! [SV16: $i,SV8: $i] :
( ( ~ ( ( SV8 != SV16 )
| ( iext @ uri_owl_sameAs @ SV8 @ SV16 ) ) )
= $false ),
inference(extcnf_or_neg,[status(thm)],[612]) ).
thf(621,plain,
! [SV17: $i,SV3: $i,SV11: $i] :
( ( ( iext @ SV11 @ SV3 @ SV17 )
= $false )
| ( ( ip @ SV11 )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[613]) ).
thf(622,plain,
! [SV18: $i,SV12: $i,SV4: $i] :
( ( ( ~ ( ~ ( iext @ uri_rdfs_subClassOf @ SV4 @ SV12 )
| ~ ( iext @ uri_rdfs_subClassOf @ SV12 @ SV18 ) ) )
= $false )
| ( ( iext @ uri_rdfs_subClassOf @ SV4 @ SV18 )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[614]) ).
thf(623,plain,
! [SV13: $i,SV5: $i] :
( ( ( ~ ( ir @ SV5 )
| ~ ( ir @ SV13 ) )
= $false )
| ( ( iext @ uri_owl_sameAs @ SV5 @ SV13 )
= $false ) ),
inference(extcnf_not_pos,[status(thm)],[615]) ).
thf(624,plain,
! [SV14: $i,SV6: $i] :
( ( ~ ( iext @ uri_owl_differentFrom @ SV6 @ SV14 )
| ( SV6 != SV14 ) )
= $true ),
inference(extcnf_not_neg,[status(thm)],[616]) ).
thf(625,plain,
! [SV14: $i,SV6: $i] :
( ( ~ ( ( SV6 != SV14 ) )
| ( iext @ uri_owl_differentFrom @ SV6 @ SV14 ) )
= $true ),
inference(extcnf_not_neg,[status(thm)],[617]) ).
thf(626,plain,
! [SV19: $i,SV15: $i,SV7: $i] :
( ( ( ~ ( ~ ( iext @ uri_rdfs_subPropertyOf @ SV7 @ SV15 )
| ~ ( iext @ uri_rdfs_subPropertyOf @ SV15 @ SV19 ) ) )
= $false )
| ( ( iext @ uri_rdfs_subPropertyOf @ SV7 @ SV19 )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[618]) ).
thf(627,plain,
! [SV16: $i,SV8: $i] :
( ( ~ ( iext @ uri_owl_sameAs @ SV8 @ SV16 )
| ( SV8 = SV16 ) )
= $true ),
inference(extcnf_not_neg,[status(thm)],[619]) ).
thf(628,plain,
! [SV16: $i,SV8: $i] :
( ( ( SV8 != SV16 )
| ( iext @ uri_owl_sameAs @ SV8 @ SV16 ) )
= $true ),
inference(extcnf_not_neg,[status(thm)],[620]) ).
thf(629,plain,
! [SV18: $i,SV12: $i,SV4: $i] :
( ( ( ~ ( iext @ uri_rdfs_subClassOf @ SV4 @ SV12 )
| ~ ( iext @ uri_rdfs_subClassOf @ SV12 @ SV18 ) )
= $true )
| ( ( iext @ uri_rdfs_subClassOf @ SV4 @ SV18 )
= $true ) ),
inference(extcnf_not_neg,[status(thm)],[622]) ).
thf(630,plain,
! [SV13: $i,SV5: $i] :
( ( ( ~ ( ir @ SV5 ) )
= $false )
| ( ( iext @ uri_owl_sameAs @ SV5 @ SV13 )
= $false ) ),
inference(extcnf_or_neg,[status(thm)],[623]) ).
thf(631,plain,
! [SV5: $i,SV13: $i] :
( ( ( ~ ( ir @ SV13 ) )
= $false )
| ( ( iext @ uri_owl_sameAs @ SV5 @ SV13 )
= $false ) ),
inference(extcnf_or_neg,[status(thm)],[623]) ).
thf(632,plain,
! [SV14: $i,SV6: $i] :
( ( ( ~ ( iext @ uri_owl_differentFrom @ SV6 @ SV14 ) )
= $true )
| ( ( SV6 != SV14 )
= $true ) ),
inference(extcnf_or_pos,[status(thm)],[624]) ).
thf(633,plain,
! [SV14: $i,SV6: $i] :
( ( ( ~ ( ( SV6 != SV14 ) ) )
= $true )
| ( ( iext @ uri_owl_differentFrom @ SV6 @ SV14 )
= $true ) ),
inference(extcnf_or_pos,[status(thm)],[625]) ).
thf(634,plain,
! [SV19: $i,SV15: $i,SV7: $i] :
( ( ( ~ ( iext @ uri_rdfs_subPropertyOf @ SV7 @ SV15 )
| ~ ( iext @ uri_rdfs_subPropertyOf @ SV15 @ SV19 ) )
= $true )
| ( ( iext @ uri_rdfs_subPropertyOf @ SV7 @ SV19 )
= $true ) ),
inference(extcnf_not_neg,[status(thm)],[626]) ).
thf(635,plain,
! [SV16: $i,SV8: $i] :
( ( ( ~ ( iext @ uri_owl_sameAs @ SV8 @ SV16 ) )
= $true )
| ( ( SV8 = SV16 )
= $true ) ),
inference(extcnf_or_pos,[status(thm)],[627]) ).
thf(636,plain,
! [SV16: $i,SV8: $i] :
( ( ( SV8 != SV16 )
= $true )
| ( ( iext @ uri_owl_sameAs @ SV8 @ SV16 )
= $true ) ),
inference(extcnf_or_pos,[status(thm)],[628]) ).
thf(637,plain,
! [SV18: $i,SV12: $i,SV4: $i] :
( ( ( ~ ( iext @ uri_rdfs_subClassOf @ SV4 @ SV12 ) )
= $true )
| ( ( ~ ( iext @ uri_rdfs_subClassOf @ SV12 @ SV18 ) )
= $true )
| ( ( iext @ uri_rdfs_subClassOf @ SV4 @ SV18 )
= $true ) ),
inference(extcnf_or_pos,[status(thm)],[629]) ).
thf(638,plain,
! [SV13: $i,SV5: $i] :
( ( ( ir @ SV5 )
= $true )
| ( ( iext @ uri_owl_sameAs @ SV5 @ SV13 )
= $false ) ),
inference(extcnf_not_neg,[status(thm)],[630]) ).
thf(639,plain,
! [SV5: $i,SV13: $i] :
( ( ( ir @ SV13 )
= $true )
| ( ( iext @ uri_owl_sameAs @ SV5 @ SV13 )
= $false ) ),
inference(extcnf_not_neg,[status(thm)],[631]) ).
thf(640,plain,
! [SV14: $i,SV6: $i] :
( ( ( iext @ uri_owl_differentFrom @ SV6 @ SV14 )
= $false )
| ( ( SV6 != SV14 )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[632]) ).
thf(641,plain,
! [SV14: $i,SV6: $i] :
( ( ( SV6 != SV14 )
= $false )
| ( ( iext @ uri_owl_differentFrom @ SV6 @ SV14 )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[633]) ).
thf(642,plain,
! [SV19: $i,SV15: $i,SV7: $i] :
( ( ( ~ ( iext @ uri_rdfs_subPropertyOf @ SV7 @ SV15 ) )
= $true )
| ( ( ~ ( iext @ uri_rdfs_subPropertyOf @ SV15 @ SV19 ) )
= $true )
| ( ( iext @ uri_rdfs_subPropertyOf @ SV7 @ SV19 )
= $true ) ),
inference(extcnf_or_pos,[status(thm)],[634]) ).
thf(643,plain,
! [SV16: $i,SV8: $i] :
( ( ( iext @ uri_owl_sameAs @ SV8 @ SV16 )
= $false )
| ( ( SV8 = SV16 )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[635]) ).
thf(644,plain,
! [SV16: $i,SV8: $i] :
( ( ( SV8 = SV16 )
= $false )
| ( ( iext @ uri_owl_sameAs @ SV8 @ SV16 )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[636]) ).
thf(645,plain,
! [SV18: $i,SV12: $i,SV4: $i] :
( ( ( iext @ uri_rdfs_subClassOf @ SV4 @ SV12 )
= $false )
| ( ( ~ ( iext @ uri_rdfs_subClassOf @ SV12 @ SV18 ) )
= $true )
| ( ( iext @ uri_rdfs_subClassOf @ SV4 @ SV18 )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[637]) ).
thf(646,plain,
! [SV14: $i,SV6: $i] :
( ( ( SV6 = SV14 )
= $false )
| ( ( iext @ uri_owl_differentFrom @ SV6 @ SV14 )
= $false ) ),
inference(extcnf_not_pos,[status(thm)],[640]) ).
thf(647,plain,
! [SV14: $i,SV6: $i] :
( ( ( SV6 = SV14 )
= $true )
| ( ( iext @ uri_owl_differentFrom @ SV6 @ SV14 )
= $true ) ),
inference(extcnf_not_neg,[status(thm)],[641]) ).
thf(648,plain,
! [SV19: $i,SV15: $i,SV7: $i] :
( ( ( iext @ uri_rdfs_subPropertyOf @ SV7 @ SV15 )
= $false )
| ( ( ~ ( iext @ uri_rdfs_subPropertyOf @ SV15 @ SV19 ) )
= $true )
| ( ( iext @ uri_rdfs_subPropertyOf @ SV7 @ SV19 )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[642]) ).
thf(649,plain,
! [SV4: $i,SV18: $i,SV12: $i] :
( ( ( iext @ uri_rdfs_subClassOf @ SV12 @ SV18 )
= $false )
| ( ( iext @ uri_rdfs_subClassOf @ SV4 @ SV12 )
= $false )
| ( ( iext @ uri_rdfs_subClassOf @ SV4 @ SV18 )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[645]) ).
thf(650,plain,
! [SV7: $i,SV19: $i,SV15: $i] :
( ( ( iext @ uri_rdfs_subPropertyOf @ SV15 @ SV19 )
= $false )
| ( ( iext @ uri_rdfs_subPropertyOf @ SV7 @ SV15 )
= $false )
| ( ( iext @ uri_rdfs_subPropertyOf @ SV7 @ SV19 )
= $true ) ),
inference(extcnf_not_pos,[status(thm)],[648]) ).
thf(651,plain,
$false = $true,
inference(fo_atp_e,[status(thm)],[578,650,649,647,646,644,643,639,638,621,606,605,590]) ).
thf(652,plain,
$false,
inference(solved_all_splits,[solved_all_splits(join,[])],[651]) ).
%------------------------------------------------------------------------------
%----ORIGINAL SYSTEM OUTPUT
% 0.00/0.04 % Problem : SWB015+1 : TPTP v9.3.1. Released v5.2.0.
% 0.00/0.05 % Command : leo --cores 7 --timeout 300 --proofoutput 1 --foatp e --atp e=/export/starexec/sandbox2/solver/bin/eprover /export/starexec/sandbox2/benchmark/theBenchmark.p
% 0.09/0.20 % Computer : n010.cluster.edu
% 0.09/0.20 % Model : x86_64 x86_64
% 0.09/0.20 % CPU : Intel(R) Xeon(R) CPU E5-2620 v4 @ 2.10GHz
% 0.09/0.20 % Memory : 8046.5625MB
% 0.09/0.20 % OS : Linux 6.8.0-71-generic
% 0.09/0.20 % CPULimit : 300
% 0.09/0.20 % WCLimit : 300
% 0.09/0.20 % DateTime : Tue Oct 6 15:52:25 UTC 2026
% 0.09/0.20 % CPUTime :
% 0.09/0.21 Running leo --cores 7 --timeout 300 --proofoutput 1 --foatp e --atp e=/export/starexec/sandbox2/solver/bin/eprover /export/starexec/sandbox2/benchmark/theBenchmark.p
% 3.01/0.74 ...
% 3.01/0.74
% 3.01/0.74 No.of.Axioms: 9
% 3.01/0.74
% 3.01/0.74 Length.of.Defs: 0
% 3.01/0.74
% 3.01/0.74 Contains.Choice.Funs: false
% 3.01/0.74 ......
% 3.01/0.74
% 3.01/0.74 ********************************
% 3.01/0.74 * All subproblems solved! *
% 3.01/0.74 ********************************
% 3.01/0.74 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p : (rf:1,axioms:9,ps:0,u:6,ude:true,rLeibEQ:true,rAndEQ:true,use_choice:true,use_extuni:true,use_extcnf_combined:false,expand_extuni:false,foatp:e,atp_timeout:299,atp_calls_frequency:5,ordering:none,proof_output:1,protocol_output:false,clause_count:651,loop_count:0,foatp_calls:1,translation:fof_full)
% 3.01/0.74
% 3.01/0.74 %**** Beginning of derivation protocol ****
% 3.01/0.74 % SZS output start CNFRefutation
% See solution above
% 3.01/0.74
% 3.01/0.74 %**** End of derivation protocol ****
% 3.01/0.74 %**** no. of clauses in derivation: 103 ****
% 3.01/0.74 %**** clause counter: 651 ****
% 3.01/0.74
% 3.01/0.74 % SZS status Theorem for /export/starexec/sandbox2/benchmark/theBenchmark.p : (rf:1,axioms:9,ps:0,u:6,ude:true,rLeibEQ:true,rAndEQ:true,use_choice:true,use_extuni:true,use_extcnf_combined:false,expand_extuni:false,foatp:e,atp_timeout:299,atp_calls_frequency:5,ordering:none,proof_output:1,protocol_output:false,clause_count:651,loop_count:0,foatp_calls:1,translation:fof_full)
%------------------------------------------------------------------------------