@prefix log: . @prefix math: . @prefix owl: . @prefix xsd: . @prefix rdfs: . @prefix rdf: . @prefix : . ### Web Ontology Language OWL owl:AnnotationProperty rdfs:subClassOf rdf:Property. owl:Class rdfs:subClassOf rdfs:Class; rdfs:subClassOf rdfs:Class. owl:DataRange rdfs:subClassOf rdfs:Literal. owl:DatatypeProperty rdfs:subClassOf rdf:Property. owl:DeprecatedClass rdfs:subClassOf rdfs:Class. owl:DeprecatedProperty rdfs:subClassOf rdf:Property. owl:FunctionalProperty rdfs:subClassOf rdf:Property. owl:InverseFunctionalProperty rdfs:subClassOf owl:ObjectProperty. owl:Nothing owl:oneOf rdf:nil. owl:ObjectProperty rdfs:subClassOf rdf:Property. owl:OntologyProperty rdfs:subClassOf rdf:Property. owl:Restriction rdfs:subClassOf owl:Class. owl:SymmetricProperty rdfs:subClassOf owl:ObjectProperty. owl:Thing rdfs:subClassOf rdfs:Resource; rdfs:subClassOf rdfs:Resource. owl:TransitiveProperty rdfs:subClassOf owl:ObjectProperty. owl:allValuesFrom rdfs:domain owl:Restriction; rdfs:range rdfs:Class. owl:cardinality rdfs:domain owl:Restriction; rdfs:range xsd:nonNegativeInteger; rdfs:subPropertyOf owl:maxCardinality, owl:minCardinality. owl:complementOf rdfs:domain owl:Class; rdfs:range owl:Class; rdfs:subPropertyOf owl:disjointWith; a owl:SymmetricProperty. owl:differentFrom rdfs:domain owl:Thing; rdfs:range owl:Thing; a owl:SymmetricProperty. owl:disjointWith rdfs:domain owl:Class; rdfs:range owl:Class; a owl:SymmetricProperty. owl:distinctMembers rdfs:domain owl:AllDifferent; rdfs:range rdf:List. owl:hasValue rdfs:domain owl:Restriction; rdfs:range rdfs:Resource. owl:intersectionOf rdfs:domain owl:Class; rdfs:range rdf:List. owl:inverseOf rdfs:domain owl:ObjectProperty; rdfs:range owl:ObjectProperty; a owl:SymmetricProperty. owl:maxCardinality rdfs:domain owl:Restriction; rdfs:range xsd:nonNegativeInteger. owl:minCardinality rdfs:domain owl:Restriction; rdfs:range xsd:nonNegativeInteger. owl:onProperty rdfs:domain owl:Restriction; rdfs:range rdf:Property. owl:oneOf rdfs:domain rdfs:Class; rdfs:range rdf:List. owl:someValuesFrom rdfs:domain owl:Restriction; rdfs:range rdfs:Class. owl:unionOf rdfs:domain owl:Class; rdfs:range rdf:List. owl:backwardCompatibleWith rdfs:domain owl:Ontology; rdfs:range owl:Ontology; a owl:OntologyProperty. owl:imports rdfs:domain owl:Ontology; rdfs:range owl:Ontology; a owl:OntologyProperty. owl:incompatibleWith rdfs:domain owl:Ontology; rdfs:range owl:Ontology; a owl:OntologyProperty. owl:priorVersion rdfs:domain owl:Ontology; rdfs:range owl:Ontology; a owl:OntologyProperty. owl:versionInfo rdfs:domain rdfs:Resource; rdfs:range rdfs:Resource; a owl:AnnotationProperty. rdfs:comment a owl:AnnotationProperty. rdfs:isDefinedBy a owl:AnnotationProperty. rdfs:label a owl:AnnotationProperty. rdfs:seeAlso a owl:AnnotationProperty. ### inference rules for Web Ontology Language OWL {?P owl:inverseOf ?Q. ?S ?P ?O} => {?O ?Q ?S}. {?P rdf:type owl:SymmetricProperty. ?S ?P ?O} => {?O ?P ?S}. {?P rdf:type owl:TransitiveProperty. ?X ?P ?O. ?S ?P ?X} => {?S ?P ?O}. {?R owl:onProperty ?P; owl:hasValue ?Y. ?X a ?R} => {?X ?P ?Y}. {?P rdf:type owl:InverseFunctionalProperty. ?X ?P ?O. ?Y ?P ?O} => {?X owl:sameAs ?Y}. {?P rdf:type owl:FunctionalProperty. ?S ?P ?X. ?S ?P ?Y} => {?X owl:sameAs ?Y}. {?L rdf:first ?A; rdf:rest ?B. ?M rdf:first ?C; rdf:rest ?D. ?A owl:sameAs ?C. ?B owl:sameAs ?D} => {?L owl:sameAs ?M}. {?C1 owl:equivalentClass ?A. ?A owl:onProperty ?P1; owl:someValuesFrom ?C3. ?P1 rdfs:domain ?C1; rdfs:range ?C3; rdf:type owl:FunctionalProperty; owl:inverseOf ?P9. ?C1 owl:equivalentClass ?B. ?B owl:onProperty ?P3; owl:someValuesFrom ?C5. ?P3 rdfs:domain ?C1; rdfs:range ?C5; rdf:type owl:FunctionalProperty; owl:inverseOf ?P7. ?C5 owl:equivalentClass ?C. ?C owl:onProperty ?P2; owl:someValuesFrom ?C3. ?P2 rdfs:domain ?C5; rdfs:range ?C3; rdf:type owl:FunctionalProperty; owl:inverseOf ?P8. ?C5 owl:equivalentClass ?D. ?D owl:onProperty ?P7; owl:cardinality ?X1. ?X1 owl:sameAs ?Y1. ?C3 owl:equivalentClass ?F. ?F owl:onProperty ?P8; owl:cardinality ?X2. ?X2 owl:sameAs ?Y2. ?C3 owl:equivalentClass ?G. ?G owl:onProperty ?P9; owl:cardinality ?X3. ?C3 owl:oneOf ?E. ?E rdf:first ?Z; rdf:rest rdf:nil. (?Y1 ?Y2) math:product ?Z3. ?Z3 math:equalTo ?Y3} => {?X3 owl:sameAs ?Y3}. {?C1 owl:equivalentClass ?A. ?A owl:onProperty ?P1; owl:someValuesFrom ?C3. ?P1 rdfs:domain ?C1; rdfs:range ?C3; rdf:type owl:FunctionalProperty; owl:inverseOf ?P9. ?C1 owl:equivalentClass ?B. ?B owl:onProperty ?P3; owl:someValuesFrom ?C5. ?P3 rdfs:domain ?C1; rdfs:range ?C5; rdf:type owl:FunctionalProperty; owl:inverseOf ?P7. ?C5 owl:equivalentClass ?C. ?C owl:onProperty ?P2; owl:someValuesFrom ?C3. ?P2 rdfs:domain ?C5; rdfs:range ?C3; rdf:type owl:FunctionalProperty; owl:inverseOf ?P8. ?C5 owl:equivalentClass ?D. ?D owl:onProperty ?P7; owl:cardinality ?X1. ?C3 owl:equivalentClass ?F. ?F owl:onProperty ?P8; owl:cardinality ?X2. ?C3 owl:equivalentClass ?G. ?G owl:onProperty ?P9; owl:cardinality ?X3. ?X3 owl:sameAs ?Y3. ?C3 owl:oneOf ?E. ?E rdf:first ?Z; rdf:rest rdf:nil. ?O owl:oneOf ?L1. ?L1 :item ?X1, ?X2. ?O owl:oneOf ?L2. ?L2 :item ?Z1, ?Z2. (?Y3 ?Y2) math:integerQuotient ?Y1} => {?Z2 owl:sameAs ?Y2}. {?X log:notEqualTo ?Y. ?A owl:distinctMembers ?L. ?L :item ?X, ?Y} => {?X owl:differentFrom ?Y}. {?A owl:disjointWith ?B. ?X a ?A. ?Y a ?B } => {?X owl:differentFrom ?Y}. {?A rdfs:subPropertyOf ?B. ?B rdfs:subPropertyOf ?A} => {?A owl:equivalentProperty ?B}. {?A owl:inverseOf ?C. ?B owl:inverseOf ?C} => {?A rdfs:subPropertyOf ?B}. {?A owl:onProperty ?P, ?Q; owl:hasValue ?V. ?P rdfs:domain ?A; a owl:FunctionalProperty. ?Q rdfs:domain ?D; a owl:FunctionalProperty} => {?P rdfs:subPropertyOf ?Q}. {?A owl:onProperty ?P; owl:hasValue ?V. ?D owl:equivalentClass ?A. ?P rdfs:domain ?D; a owl:FunctionalProperty. ?B owl:onProperty ?Q; owl:hasValue ?V. ?D owl:equivalentClass ?B. ?Q rdfs:domain ?D; a owl:FunctionalProperty} => {?P rdfs:subPropertyOf ?Q}. {?B owl:onProperty ?P1; owl:someValuesFrom ?X. ?X owl:intersectionOf ?L. ?L :item ?I1. ?I1 owl:onProperty ?P2; owl:someValuesFrom owl:Thing. ?L :item ?I2. ?I2 owl:onProperty ?P3; owl:someValuesFrom owl:Thing. ?L :item ?I3. ?I3 owl:onProperty ?P2; owl:allValuesFrom ?C. ?L :item ?I4. ?I4 owl:onProperty ?P3; owl:allValuesFrom ?U. ?U2 owl:onProperty ?P2; owl:someValuesFrom owl:Thing. ?U owl:equivalentClass ?U2. ?L :item ?I5. ?I5 owl:onProperty ?P3; owl:allValuesFrom ?V. ?V2 owl:onProperty ?P3; owl:someValuesFrom owl:Thing. ?V owl:equivalentClass ?V2. ?L :item ?I6. ?I6 owl:onProperty ?P3; owl:allValuesFrom ?W. ?W2 owl:onProperty ?P2; owl:allValuesFrom ?C. ?W owl:equivalentClass ?W2. ?C owl:equivalentClass ?C1. ?C1 owl:onProperty ?P8; owl:allValuesFrom ?C2. ?P8 owl:inverseOf ?P2. ?D2 owl:onProperty ?P7; owl:allValuesFrom ?C3. ?P7 owl:inverseOf ?P3. ?C2 owl:equivalentClass ?D2. ?D3 owl:onProperty ?P9; owl:allValuesFrom ?C4. ?P9 owl:inverseOf ?P1. ?C3 owl:equivalentClass ?D3. ?C4 owl:complementOf ?A. ?P3 a owl:TransitiveProperty. ?D rdfs:subClassOf ?A, ?B} => {?D owl:equivalentClass owl:Nothing}. {?Z owl:equivalentClass ?J. ?J owl:onProperty ?P1; owl:someValuesFrom ?T. ?T owl:intersectionOf ?L. ?L :item ?I1, ?I2. ?I2 owl:onProperty ?P9; :someOrAll ?G. ?G2 owl:onProperty ?P1; owl:someValuesFrom ?U. ?G owl:equivalentClass ?G2. ?U owl:complementOf ?I1. ?P1 owl:inverseOf ?P9; a owl:FunctionalProperty} => {?Z owl:equivalentClass owl:Nothing}. {?J owl:intersectionOf ?L. ?L :item ?I1, ?I2. ?I1 rdfs:subClassOf ?J1. ?J1 owl:onProperty ?P; owl:someValuesFrom ?A1. ?I2 rdfs:subClassOf ?J2. ?J2 owl:onProperty ?P; owl:allValuesFrom ?A2. ?A1 rdfs:subClassOf ?C1. ?C1 owl:intersectionOf ?D1. ?D1 rdf:first ?E1; rdf:rest ?F1. ?F1 rdf:first ?G1; rdf:rest rdf:nil. ?E1 owl:unionOf ?H1. ?H1 :item ?X1. ?G1 owl:unionOf ?K1. ?K1 :item ?X1. ?A2 rdfs:subClassOf ?C2. ?C2 owl:intersectionOf ?D2. ?D2 rdf:first ?E2; rdf:rest ?F2. ?F2 rdf:first ?G2; rdf:rest rdf:nil. ?E2 owl:unionOf ?H2. ?H2 :item ?X2. ?G2 owl:unionOf ?K2. ?K2 :item ?X3. ?X1 owl:complementOf ?X2, ?X3. ?C rdfs:subClassOf ?J} => {?C owl:equivalentClass owl:Nothing}. {?J owl:intersectionOf ?L. ?L :item ?I1. ?I1 owl:onProperty ?P; owl:someValuesFrom ?S. ?L :item ?I2. ?I2 owl:onProperty ?Q; owl:someValuesFrom ?T. ?F owl:onProperty ?P; owl:someValuesFrom ?D. ?D owl:intersectionOf ?K. ?K :item ?S, ?T. ?L :item ?I3. ?G owl:complementOf ?I3. ?G owl:equivalentClass ?F. ?P rdf:type owl:FunctionalProperty; rdfs:subPropertyOf ?R. ?Q rdf:type owl:FunctionalProperty; rdfs:subPropertyOf ?R. ?R rdf:type owl:FunctionalProperty} => {?J owl:equivalentClass owl:Nothing}. {?J owl:intersectionOf ?L. ?L :item ?I1, ?I2. ?I2 owl:onProperty ?P; owl:someValuesFrom ?S. ?S owl:intersectionOf ?K. ?K :item ?U. ?U owl:onProperty ?Q; owl:someValuesFrom ?Y. ?Q owl:inverseOf ?P. ?K :item ?V. ?V owl:onProperty ?Q; owl:maxCardinality ?M. ?M math:equalTo 1. ?I1 owl:disjointWith ?Y} => {?J owl:equivalentClass owl:Nothing}. {?J owl:intersectionOf ?L. ?L :item ?I2. ?I2 owl:onProperty ?F; owl:someValuesFrom ?T. ?T owl:intersectionOf ?K. ?K :item ?G. ?G owl:onProperty ?Q; owl:allValuesFrom ?X. ?K :item ?H. ?H owl:onProperty ?P; owl:allValuesFrom ?U. ?V owl:onProperty ?S; owl:someValuesFrom ?X. ?U owl:equivalentClass ?V. ?L :item ?I1. ?X owl:complementOf ?I1. ?F rdf:type owl:FunctionalProperty; owl:inverseOf ?P. ?S rdf:type owl:FunctionalProperty; owl:inverseOf ?Q; rdfs:subPropertyOf ?F} => {?J owl:equivalentClass owl:Nothing}. {?J owl:intersectionOf ?L. ?L :item ?I2. ?I2 owl:onProperty ?P9; owl:someValuesFrom ?D. ?L :item ?I3. ?I3 owl:onProperty ?P8; owl:allValuesFrom ?E. ?E2 owl:onProperty ?P9; owl:someValuesFrom ?D. ?E owl:equivalentClass ?E2. ?X owl:intersectionOf ?K. ?D owl:equivalentClass ?X. ?K :item ?C, ?Y. ?Y owl:onProperty ?P1; owl:someValuesFrom ?Z. ?Z owl:complementOf ?C. ?L :item ?I1. ?I1 owl:complementOf ?C. ?P9 owl:inverseOf ?P1. ?P8 owl:inverseOf ?P2. ?P2 a owl:TransitiveProperty. ?P1 rdfs:subPropertyOf ?P2; a owl:FunctionalProperty} => {?J owl:equivalentClass owl:Nothing}. {?J owl:intersectionOf ?L. ?L :item ?I1, ?I2. ?I2 owl:onProperty ?P1; owl:someValuesFrom ?S. ?S2 owl:onProperty ?P1; owl:someValuesFrom ?T. ?S owl:equivalentClass ?S2. ?T owl:intersectionOf ?K. ?K :item ?I1, ?I3. ?I3 owl:onProperty ?P9; owl:allValuesFrom ?U. ?U owl:complementOf ?I1. ?P1 owl:inverseOf ?P9; a owl:TransitiveProperty} => {?J owl:equivalentClass owl:Nothing}. {?J owl:intersectionOf ?L. ?L :item ?I1. ?I1 owl:onProperty ?P; owl:someValuesFrom ?B. ?B owl:complementOf ?E. ?L :item ?I2. ?I2 owl:onProperty ?P; owl:allValuesFrom ?D. ?L :item ?I3. ?I3 owl:onProperty ?P; owl:allValuesFrom ?U. ?U owl:unionOf ?K. ?K :item ?E, ?Y. ?Y owl:complementOf ?D} => {?J owl:equivalentClass owl:Nothing}. {?J owl:intersectionOf ?L. ?L :item ?I1. ?I1 owl:onProperty ?P; owl:someValuesFrom ?B. ?B owl:complementOf ?E. ?L :item ?I2. ?I2 owl:onProperty ?P; owl:allValuesFrom ?D. ?L :item ?I3. ?I3 owl:onProperty ?P; owl:allValuesFrom ?U. ?U2 owl:intersectionOf ?K. ?U2 owl:complementOf ?U. ?K :item ?D, ?Y. ?Y owl:complementOf ?E} => {?J owl:equivalentClass owl:Nothing}. {?J owl:intersectionOf ?L. ?L :item ?I0. ?I0 owl:onProperty ?P; owl:maxCardinality ?M. ?M math:equalTo 0. ?L :item ?I1. ?I1 owl:onProperty ?P; owl:someValuesFrom ?C1} => {?J owl:equivalentClass owl:Nothing}. {?J owl:intersectionOf ?L. ?L :item ?I0. ?I0 owl:onProperty ?P; owl:maxCardinality ?M. ?M math:equalTo 1. ?L :item ?I1. ?I1 owl:onProperty ?P; owl:someValuesFrom ?C1. ?L :item ?I2. ?I2 owl:onProperty ?P; owl:someValuesFrom ?C2. ?C2 owl:disjointWith ?C1} => {?J owl:equivalentClass owl:Nothing}. {?J owl:intersectionOf ?L. ?L :item ?I0. ?I0 owl:onProperty ?P; owl:maxCardinality ?M. ?M math:equalTo 2. ?L :item ?I1. ?I1 owl:onProperty ?P; owl:someValuesFrom ?C1. ?L :item ?I2. ?I2 owl:onProperty ?P; owl:someValuesFrom ?C2. ?C2 owl:disjointWith ?C1. ?L :item ?I3. ?I3 owl:onProperty ?P; owl:someValuesFrom ?C3. ?C3 owl:disjointWith ?C1, ?C2} => {?J owl:equivalentClass owl:Nothing}. {?J owl:intersectionOf ?L. ?L :item ?I0. ?I0 owl:onProperty ?P; owl:maxCardinality ?M. ?M math:equalTo 3. ?L :item ?I1. ?I1 owl:onProperty ?P; owl:someValuesFrom ?C1. ?L :item ?I2. ?I2 owl:onProperty ?P; owl:someValuesFrom ?C2. ?C2 owl:disjointWith ?C1. ?L :item ?I3. ?I3 owl:onProperty ?P; owl:someValuesFrom ?C3. ?C3 owl:disjointWith ?C1, ?C2. ?L :item ?I4. ?I4 owl:onProperty ?P; owl:someValuesFrom ?C4. ?C4 owl:disjointWith ?C1, ?C2, ?C3} => {?J owl:equivalentClass owl:Nothing}. {?J owl:intersectionOf ?L. ?L :item ?I0. ?I0 owl:onProperty ?P; owl:maxCardinality ?M. ?M math:equalTo 4. ?L :item ?I1. ?I1 owl:onProperty ?P; owl:someValuesFrom ?C1. ?L :item ?I2. ?I2 owl:onProperty ?P; owl:someValuesFrom ?C2. ?C2 owl:disjointWith ?C1. ?L :item ?I3. ?I3 owl:onProperty ?P; owl:someValuesFrom ?C3. ?C3 owl:disjointWith ?C1, ?C2. ?L :item ?I4. ?I4 owl:onProperty ?P; owl:someValuesFrom ?C4. ?C4 owl:disjointWith ?C1, ?C2, ?C3. ?L :item ?I5. ?I5 owl:onProperty ?P; owl:someValuesFrom ?C5. ?C5 owl:disjointWith ?C1, ?C2, ?C3, ?C4} => {?J owl:equivalentClass owl:Nothing}. {?C owl:intersectionOf ?L. ?L :item ?I1. ?I1 owl:onProperty ?P1; owl:someValuesFrom ?C1. ?L :item ?I2. ?I2 owl:onProperty ?P2; owl:someValuesFrom ?C2. ?C2 owl:disjointWith ?C1. ?L :item ?I3. ?I3 owl:onProperty ?P3; owl:someValuesFrom ?C3. ?P1 a owl:FunctionalProperty. ?P2 a owl:FunctionalProperty. ?P3 rdfs:subPropertyOf ?P1, ?P2} => {?C owl:equivalentClass owl:Nothing}. {?J owl:intersectionOf ?L. ?L :item ?I1. ?I1 owl:onProperty ?P; owl:allValuesFrom ?S. ?S owl:complementOf ?G. ?L :item ?I2. ?I2 owl:onProperty ?P; owl:someValuesFrom ?T. ?T owl:intersectionOf ?K. ?K :item ?F. ?F owl:onProperty ?Q; owl:someValuesFrom ?G. ?K :item ?G. ?P rdf:type owl:FunctionalProperty. ?Q owl:inverseOf ?P} => {?J owl:equivalentClass owl:Nothing}. {?J owl:intersectionOf ?L. ?L :item ?I1. ?I1 owl:onProperty ?P1; owl:someValuesFrom ?C1. ?L :item ?I2. ?I2 owl:onProperty ?P2; owl:someValuesFrom ?T. ?T owl:intersectionOf ?K. ?K :item ?X. ?X owl:complementOf ?C1. ?K :item ?H. ?H owl:onProperty ?P8; owl:allValuesFrom ?V. ?U owl:onProperty ?P3; owl:someValuesFrom owl:Thing. ?V owl:equivalentClass ?U. ?P1 a owl:FunctionalProperty. ?P2 a owl:FunctionalProperty; owl:inverseOf ?P8. ?P3 a owl:FunctionalProperty; rdfs:subPropertyOf ?P1, ?P2} => {?J owl:equivalentClass owl:Nothing}. {?J owl:intersectionOf ?L. ?L :item ?I2. ?I2 owl:onProperty ?F; owl:maxCardinality ?M. ?M math:equalTo 1. ?L :item ?I3. ?I3 owl:onProperty ?F; owl:someValuesFrom ?T. ?U owl:onProperty ?Q; owl:allValuesFrom ?X. ?T owl:equivalentClass ?U. ?L :item ?I4. ?I4 owl:onProperty ?P; owl:someValuesFrom ?X. ?L :item ?I1. ?I1 owl:complementOf ?X. ?Q owl:inverseOf ?P. ?P rdfs:subPropertyOf ?F} => {?J owl:equivalentClass owl:Nothing}. {?J owl:intersectionOf ?L. ?L :item ?I1. ?I1 owl:onProperty ?P1; owl:someValuesFrom ?S. ?S owl:intersectionOf ?K. ?K :item ?U. ?U owl:complementOf ?C1. ?K :item ?V. ?V owl:complementOf ?C2. ?L :item ?I2. ?I2 owl:onProperty ?P2; owl:someValuesFrom ?T. ?T owl:intersectionOf ?O. ?O :item ?G. ?G owl:onProperty ?P8; owl:maxCardinality ?M. ?M math:equalTo 1. ?O :item ?H. ?H owl:onProperty ?P8; owl:someValuesFrom ?W. ?X owl:onProperty ?P1; owl:allValuesFrom ?C1. ?W owl:equivalentClass ?X. ?P2 owl:inverseOf ?P8} => {?J owl:equivalentClass owl:Nothing}. {?A owl:onProperty ?X; owl:minCardinality ?N. ?N math:greaterThan 2. owl:Thing rdfs:subClassOf ?B. ?B owl:onProperty ?P; owl:someValuesFrom ?O. ?O owl:oneOf ?L. ?L rdf:first ?S; rdf:rest rdf:nil. ?S rdf:type ?D. ?D owl:onProperty ?Q; owl:maxCardinality ?M. ?M math:equalTo 2. ?Q owl:inverseOf ?P. ?C rdfs:subClassOf ?A} => {?C owl:equivalentClass owl:Nothing}. {?Z owl:equivalentClass ?J. ?J owl:intersectionOf ?L. ?L :item ?I0. ?I0 owl:onProperty ?P; owl:maxCardinality ?M. ?M math:equalTo 1. ?L :item ?I1. ?I1 owl:onProperty ?P1; owl:someValuesFrom ?C1. ?C1 owl:intersectionOf ?K1. ?K1 :item ?X1. ?X1 owl:onProperty ?T; owl:maxCardinality ?M1. ?M1 math:equalTo 1. ?K1 :item ?X2. ?X2 owl:onProperty ?T1; owl:someValuesFrom ?D1. ?L :item ?I2. ?I2 owl:onProperty ?P2; owl:someValuesFrom ?C2. ?C2 owl:intersectionOf ?K2. ?K2 :item ?Y1. ?Y1 owl:onProperty ?T; owl:maxCardinality ?M2. ?M2 math:equalTo 1. ?K2 :item ?Y2. ?Y2 owl:onProperty ?T2; owl:someValuesFrom ?D2. ?D2 owl:disjointWith ?D1. ?P1 rdfs:subPropertyOf ?P. ?P2 rdfs:subPropertyOf ?P. ?T1 rdfs:subPropertyOf ?T. ?T2 rdfs:subPropertyOf ?T} => {?Z owl:equivalentClass owl:Nothing}. {?J owl:intersectionOf ?L. ?L :item ?I1. ?I1 owl:onProperty ?P; owl:someValuesFrom ?S. ?S owl:onProperty ?Q; owl:minCardinality ?N. ?N math:equalTo 2. ?L :item ?I2. ?I2 owl:onProperty ?P; owl:allValuesFrom ?A. ?A owl:unionOf ?K. ?K :item ?C, ?V. ?V owl:onProperty ?Q; owl:maxCardinality ?M. ?M math:equalTo 1. ?L :item ?I3. ?I3 owl:onProperty ?P; owl:allValuesFrom ?D. ?C owl:disjointWith ?D} => {?J owl:equivalentClass owl:Nothing}. {?C1 owl:equivalentClass ?A. ?A owl:onProperty ?P1; owl:someValuesFrom ?C6. ?P1 rdfs:domain ?C1; rdfs:range ?C6; rdf:type owl:FunctionalProperty. ?C1 owl:equivalentClass ?B. ?B owl:onProperty ?P3; owl:someValuesFrom ?C5. ?P3 rdfs:domain ?C1; rdfs:range ?C5; rdf:type owl:FunctionalProperty. ?C5 owl:equivalentClass ?C. ?C owl:onProperty ?P2; owl:someValuesFrom ?C6. ?P2 rdfs:domain ?C5; rdfs:range ?C6; rdf:type owl:FunctionalProperty. ?C5 owl:equivalentClass ?D. ?D owl:onProperty ?P7; owl:cardinality ?X1. ?P7 owl:inverseOf ?P3. ?C6 owl:equivalentClass ?F. ?F owl:onProperty ?P8; owl:cardinality ?X2. ?P8 owl:inverseOf ?P2. ?C6 owl:equivalentClass ?H. ?H owl:onProperty ?P9; owl:cardinality ?X3. ?P9 owl:inverseOf ?P1. ?H owl:equivalentClass ?I. ?I owl:onProperty ?P4; owl:someValuesFrom ?C3. ?P4 rdfs:domain ?C6; rdfs:range ?C3; rdf:type owl:FunctionalProperty. ?C3 owl:equivalentClass ?G. ?G owl:onProperty ?P6; owl:maxCardinality ?X4. ?P6 owl:inverseOf ?P4. (?X1 ?X2) math:product ?X. ?X math:notEqualTo ?X3} => {?C3 owl:equivalentClass owl:Nothing}. {?C1 owl:equivalentClass ?A. ?A owl:onProperty ?P1; owl:someValuesFrom ?C3. ?P1 rdfs:domain ?C1; rdfs:range ?C3; rdf:type owl:FunctionalProperty. ?C1 owl:equivalentClass ?B. ?B owl:onProperty ?P3; owl:someValuesFrom ?C5. ?P3 rdfs:domain ?C1; rdfs:range ?C5; rdf:type owl:FunctionalProperty. ?C5 owl:equivalentClass ?C. ?C owl:onProperty ?P2; owl:someValuesFrom ?C3. ?P2 rdfs:domain ?C5; rdfs:range ?C3; rdf:type owl:FunctionalProperty. ?C5 owl:equivalentClass ?D. ?D owl:onProperty ?P7; owl:cardinality ?X1. ?P7 owl:inverseOf ?P3. ?C3 owl:equivalentClass ?F. ?F owl:onProperty ?P8; owl:cardinality ?X2. ?P8 owl:inverseOf ?P2. ?C3 owl:equivalentClass ?G. ?G owl:onProperty ?P9; owl:cardinality ?X3. ?P9 owl:inverseOf ?P1. (?X1 ?X2) math:product ?X. ?X math:notEqualTo ?X3} => {?C3 owl:equivalentClass owl:Nothing}. {?D owl:equivalentClass ?C. ?C owl:unionOf ?L. ?L :allClasses owl:Nothing} => {?D owl:equivalentClass owl:Nothing}. {?D owl:complementOf ?C. ?C owl:intersectionOf ?L. ?L :allClasses owl:Thing} => {?D owl:equivalentClass owl:Nothing}. {?C owl:intersectionOf ?L. ?L :item ?A, ?B. ?A owl:disjointWith ?B} => {?C owl:equivalentClass owl:Nothing}. {?C owl:intersectionOf ?L. ?L :item owl:Nothing} => {?C owl:equivalentClass owl:Nothing}. {?A owl:onProperty ?P; owl:maxCardinality ?M. ?B owl:onProperty ?P; owl:minCardinality ?N. ?M math:lessThan ?N. ?C rdfs:subClassOf ?A, ?B} => {?C owl:equivalentClass owl:Nothing}. {?D owl:complementOf ?C. ?D owl:equivalentClass owl:Nothing} => {?C owl:equivalentClass owl:Thing}. {?C owl:unionOf ?L. ?L :item owl:Thing} => {?C owl:equivalentClass owl:Thing}. {?D owl:intersectionOf ?L3. ?L3 rdf:first ?X; rdf:rest ?L4. ?L4 rdf:first ?Y; rdf:rest rdf:nil. ?X owl:complementOf ?A. ?Y owl:complementOf ?B. ?Z owl:complementOf ?C. ?C owl:unionOf ?L1. ?L1 rdf:first ?A; rdf:rest ?L2. ?L2 rdf:first ?B; rdf:rest rdf:nil} => {?D owl:equivalentClass ?Z}. {?D owl:unionOf ?L3. ?L3 rdf:first ?X; rdf:rest ?L4. ?L4 rdf:first ?Y; rdf:rest rdf:nil. ?X owl:complementOf ?A. ?Y owl:complementOf ?B. ?Z owl:complementOf ?C. ?C owl:intersectionOf ?L1. ?L1 rdf:first ?A; rdf:rest ?L2. ?L2 rdf:first ?B; rdf:rest rdf:nil} => {?D owl:equivalentClass ?Z}. {?A rdfs:subClassOf ?B. ?B rdfs:subClassOf ?A} => {?A owl:equivalentClass ?B}. {?B owl:intersectionOf ?L. ?L rdf:first ?A; rdf:rest rdf:nil} => {?A rdfs:subClassOf ?B}. {?A owl:intersectionOf ?X. ?X :item ?B} => {?A rdfs:subClassOf ?B}. {?B owl:intersectionOf ?Y. ?A owl:intersectionOf ?X. ?X :includes ?Y} => {?A rdfs:subClassOf ?B}. {?B owl:unionOf ?Y. ?A owl:unionOf ?X. ?Y :includes ?X} => {?A rdfs:subClassOf ?B}. {?B owl:oneOf ?Y. ?A owl:oneOf ?X. ?Y :includes ?X} => {?A rdfs:subClassOf ?B}. {?R owl:onProperty ?P; owl:allValuesFrom ?A. ?S owl:onProperty ?P; owl:allValuesFrom ?A} => {?R rdfs:subClassOf ?S}. {?A owl:onProperty rdf:type; owl:hasValue ?B} => {?A rdfs:subClassOf ?B}. {?R owl:onProperty ?P; owl:minCardinality ?M. ?S owl:onProperty ?P; owl:maxCardinality ?M. ?T owl:onProperty ?P; owl:cardinality ?M. ?C rdfs:subClassOf ?R, ?S} => {?C rdfs:subClassOf ?T}. {?X owl:intersectionOf ?L. ?L :item ?U. ?U owl:onProperty ?P; owl:minCardinality ?I. ?L :item ?V. ?V owl:onProperty ?Q; owl:minCardinality ?J. ?Y owl:onProperty ?R; owl:minCardinality ?K. (?I ?J) math:sum ?G. ?G math:equalTo ?K. ?P rdfs:subPropertyOf ?R; rdfs:range ?A. ?Q rdfs:subPropertyOf ?R; rdfs:range ?B. ?A owl:disjointWith ?B} => {?X rdfs:subClassOf ?Y}. {?R owl:onProperty ?P; owl:allValuesFrom ?A. ?P rdfs:range ?A} => {owl:Thing rdfs:subClassOf ?R}. {rdf:type rdfs:domain ?Y. ?X a rdfs:Class} => {?X rdfs:subClassOf ?Y}. {owl:Thing rdfs:subClassOf ?U. ?U owl:onProperty ?P; owl:maxCardinality ?M. ?M math:equalTo 1} => {?P a owl:FunctionalProperty}. {?P owl:inverseOf ?Q. ?Q a owl:FunctionalProperty} => {?P a owl:InverseFunctionalProperty}. {?C owl:oneOf ?L. ?L rdf:first ?X; rdf:rest rdf:nil. ?P rdfs:range ?C} => {?P a owl:FunctionalProperty}. {?P owl:inverseOf ?Q. ?Q a owl:InverseFunctionalProperty} => {?P a owl:FunctionalProperty}. {?C owl:oneOf ?L. ?L rdf:first ?X; rdf:rest rdf:nil. ?P rdfs:domain ?C} => {?P a owl:InverseFunctionalProperty}. {?P rdfs:subPropertyOf ?Q; owl:inverseOf ?Q} => {?P a owl:SymmetricProperty}. {?P rdfs:range ?R. ?R owl:oneOf ?B. ?P :reflexive ?B. ?D owl:oneOf ?A. ?A :includes ?B. ?P rdf:type owl:InverseFunctionalProperty} => {?P a owl:SymmetricProperty}. {?P rdfs:range ?R. ?R owl:oneOf ?B. ?P :reflexive ?B. ?P rdf:type owl:SymmetricProperty} => {?P a owl:TransitiveProperty}. {?C owl:equivalentClass ?R. ?R owl:onProperty ?P; owl:someValuesFrom ?A. ?X ?P ?Y. ?Y a ?A} => {?X a ?C}. {?C owl:oneOf ?L. ?L :item ?X} => {?X a ?C}. {?C owl:intersectionOf ?L. ?X :inAllOf ?L} => {?X a ?C}. {?C owl:equivalentClass ?D. ?D owl:intersectionOf ?L. ?X :inAllOf ?L} => {?X a ?C}. {?C owl:unionOf ?L. ?X :inSomeOf ?L} => {?X a ?C}. {?C owl:unionOf ?L. ?L :item ?A, ?B. ?A owl:complementOf ?B} => {?X a ?C}. {?C owl:unionOf ?L. ?L :item ?A, ?B. ?A owl:onProperty ?P; owl:someValuesFrom owl:Thing. ?B owl:onProperty ?P; owl:maxCardinality ?M. ?M math:equalTo 0} => {?X a ?C}. {?R owl:onProperty ?P; owl:allValuesFrom ?A. ?S owl:onProperty ?P; owl:allValuesFrom ?A. ?X rdf:type ?R} => {?X a ?S}. {?C owl:complementOf ?A. ?B owl:complementOf ?A. ?X rdf:type ?C} => {?X a ?B}. {?R owl:onProperty ?P; owl:allValuesFrom ?A. ?X ?P ?Y; a ?R} => {?Y a ?A}. {?R owl:onProperty ?P; owl:hasValue ?Y. ?X ?P ?Y} => {?X a ?R}. {?R owl:onProperty ?P; owl:someValuesFrom owl:Thing. ?P owl:inverseOf ?Q; rdfs:range ?O. ?Y ?Q ?X; a ?O} => {?X a ?R}. {?R owl:onProperty ?P; owl:someValuesFrom ?A. ?X ?P ?Y. ?Y a ?A} => {?X a ?R}. {?R owl:onProperty ?P; owl:maxCardinality ?M. ?M math:equalTo 1. ?P a owl:FunctionalProperty} => {?X a ?R}. {?R owl:onProperty ?P; owl:minCardinality ?M. ?M math:equalTo 1. ?P rdfs:range ?A. ?A owl:oneOf ?B. ?P :reflexive ?B. ?P rdf:type owl:SymmetricProperty} => {?X a ?R}. {?L rdf:rest ?M. ?A owl:distinctMembers ?L} => {?A owl:distinctMembers ?M}. {?R owl:onProperty ?P; owl:minCardinality ?M. ?P rdfs:range ?X. ?X owl:oneOf ?L. ?L :memberCount ?N. ?M math:notLessThan ?N} => {?X owl:distinctMembers ?L}. {?A rdfs:subClassOf ?C. ?B owl:complementOf ?C} => {?B owl:disjointWith ?A}. {?A rdfs:subClassOf ?C. ?C owl:intersectionOf ?L. ?L :item ?I. ?B owl:complementOf ?I} => {?A owl:disjointWith ?B}. {?A rdfs:subClassOf ?C. ?C owl:complementOf ?D. ?D owl:unionOf ?L. ?L :item ?B} => {?A owl:disjointWith ?B}. {?T owl:onProperty ?P; owl:cardinality ?M. ?M math:equalTo 1. ?C rdfs:subClassOf ?T. ?A rdfs:subClassOf ?C; rdfs:subClassOf ?R. ?R owl:onProperty ?P; owl:hasValue ?V. ?B rdfs:subClassOf ?C; rdfs:subClassOf ?S. ?S owl:onProperty ?P; owl:hasValue ?W} => {?A owl:disjointWith ?B}. {?R owl:onProperty ?P; owl:someValuesFrom owl:Thing. ?S owl:onProperty ?P; owl:allValuesFrom ?D. ?D owl:equivalentClass owl:Nothing. ?E rdfs:subClassOf ?R, ?S} => {?R owl:disjointWith ?S}. {?P rdfs:domain ?C. ?C rdfs:subClassOf ?D} => {?P rdfs:domain ?D}. {?P owl:inverseOf ?Q. ?P rdfs:range ?C} => {?Q rdfs:domain ?C}. {?P rdfs:range ?R. ?R owl:oneOf ?B. ?P :reflexive ?B. ?D owl:oneOf ?A. ?A :includes ?B. ?P rdf:type owl:InverseFunctionalProperty} => {?P rdfs:domain ?D}. {?P rdfs:range ?C. ?C rdfs:subClassOf ?D} => {?P rdfs:range ?D}. {?P owl:inverseOf ?Q. ?P rdfs:domain ?C} => {?Q rdfs:range ?C}. {?R owl:onProperty ?P; owl:allValuesFrom ?A. owl:Thing rdfs:subClassOf ?R} => {?P rdfs:range ?A}. {?P rdfs:range ?C; rdfs:range ?D. ?E owl:intersectionOf ?L. ?L :item ?C, ?D} => {?P rdfs:range ?E}. {?A owl:equivalentClass ?R. ?R owl:onProperty ?P; owl:someValuesFrom ?C. ?C owl:equivalentClass owl:Thing. ?B owl:equivalentClass ?S. ?S owl:onProperty ?P; owl:allValuesFrom ?D. ?D owl:equivalentClass owl:Nothing} => {?A owl:complementOf ?B}. {?A owl:equivalentClass ?R. ?R owl:onProperty ?P; owl:minCardinality ?N. ?B owl:equivalentClass ?S. ?S owl:onProperty ?P; owl:maxCardinality ?M. ?M math:lessThan ?N} => {?A owl:complementOf ?B}. {?U owl:complementOf ?V. ?V owl:intersectionOf ?K. ?K rdf:first ?X; rdf:rest ?K1. ?K1 rdf:first ?Y; rdf:rest rdf:nil. ?A owl:complementOf ?X. ?L rdf:first ?A; rdf:rest ?L1. ?L1 rdf:first ?B; rdf:rest rdf:nil. ?B owl:complementOf ?Y} => {?U owl:unionOf ?L}. {?U owl:complementOf ?V. ?V owl:intersectionOf ?K. ?K rdf:first ?X; rdf:rest ?K1. ?K1 rdf:first ?Y; rdf:rest rdf:nil. ?A owl:complementOf ?Y. ?L rdf:first ?A; rdf:rest ?L1. ?L1 rdf:first ?B; rdf:rest rdf:nil. ?B owl:complementOf ?X} => {?U owl:unionOf ?L}. {?U owl:oneOf ?K. ?L :ones ?K} => {?U owl:unionOf ?L}. {?I owl:complementOf ?V. ?V owl:unionOf ?K. ?K :item ?X, ?Y. ?A owl:complementOf ?X. ?L :item ?A, ?B. ?B owl:complementOf ?Y} => {?I owl:intersectionOf ?L}. {?I owl:intersectionOf ?K. ?K :item ?R. ?R owl:onProperty ?P; owl:maxCardinality ?M. ?K :item ?S. ?S owl:onProperty ?P; owl:minCardinality ?N. ?N math:equalTo ?M. ?L rdf:first ?T; rdf:rest rdf:nil. ?T owl:onProperty ?P; owl:cardinality ?O. ?O math:equalTo ?M} => {?I owl:intersectionOf ?L}. {?L :item ?R. ?R owl:onProperty ?P; owl:maxCardinality ?M. ?L :item ?S. ?S owl:onProperty ?P; owl:minCardinality ?N. ?N math:equalTo ?M. ?C owl:onProperty ?P; owl:cardinality ?O. ?O math:equalTo ?M} => {?C owl:intersectionOf ?L}. {?U owl:unionOf ?L. ?K :unions ?L} => {?U owl:oneOf ?K}. {?C owl:complementOf ?R. ?R owl:onProperty ?P; owl:minCardinality ?N. (?N 1) math:difference ?M} => {?C owl:onProperty ?P; owl:maxCardinality ?M}. {?C owl:complementOf ?R. ?R owl:onProperty ?P; owl:maxCardinality ?M. (?M 1) math:sum ?N} => {?C owl:onProperty ?P; owl:minCardinality ?N}. {?R owl:onProperty ?P; owl:minCardinality ?M. ?M math:equalTo 1. ?P rdfs:range ?A. ?A owl:oneOf ?L. ?L :item ?O. ?P rdfs:range ?B. ?B owl:oneOf ?K. ?K :item ?O. ?S a ?R} => {?S ?P ?O}. {?R owl:onProperty ?P; owl:someValuesFrom ?C. ?A rdfs:subClassOf ?R. ?S a ?A} => {?S ?P _:O. _:O a ?C}. ### inconsistency detections @@ {?A owl:equivalentClass owl:Nothing. ?X a ?A} => false. {rdf:nil rdf:first ?X} => false. {rdf:nil rdf:rest ?X} => false. {?Y owl:disjointWith ?Z. ?X a ?Y, ?Z} => false. {?Y owl:disjointWith ?X; owl:equivalentClass ?X} => false. {?P a owl:FunctionalProperty. ?S ?P ?X, ?Y. ?X owl:differentFrom ?Y} => false. {?P a owl:InverseFunctionalProperty. ?X ?P ?O. ?Y ?P ?O. ?X owl:differentFrom ?Y} => false. {?A owl:differentFrom ?A} => false. {?R owl:onProperty ?P; owl:maxCardinality ?M. ?M math:equalTo 0. ?X ?P ?Y; a ?R} => false. {?R owl:onProperty ?P; owl:maxCardinality ?M. ?M math:equalTo 1. ?X ?P ?Y1, ?Y2; a ?R. ?Y2 owl:differentFrom ?Y1} => false. {?R owl:onProperty ?P; owl:maxCardinality ?M. ?M math:equalTo 2. ?X ?P ?Y1, ?Y2, ?Y3; a ?R. ?Y2 owl:differentFrom ?Y1. ?Y3 owl:differentFrom ?Y1, ?Y2} => false. {?R owl:onProperty ?P; owl:minCardinality ?M. ?P rdfs:range ?X. ?X owl:oneOf ?L. ?L :memberCount ?N. ?M math:greaterThan ?N} => false. {?R owl:onProperty ?P; owl:hasValue ?V. ?X ?P ?Y; a ?R. ?V owl:differentFrom ?Y} => false. {?R owl:onProperty ?P; owl:someValuesFrom ?S. ?S owl:equivalentClass owl:Nothing. ?X a ?R} => false. {owl:Thing owl:oneOf ?L} => false. {?C owl:oneOf ?L. ?P rdfs:domain ?C. ?X ?P ?O. ?L :notItem ?X} => false. {?C owl:oneOf ?L. ?P rdfs:range ?C. ?S ?P ?X. ?L :notItem ?X} => false. {?C owl:oneOf ?L. ?X a ?C. ?L :notItem ?X} => false. ### support @@ {?S rdf:first ?X} => {?S :item ?X}. {?S rdf:rest ?B. ?B :item ?X} => {?S :item ?X}. {} => {rdf:nil :notItem ?X}. {?S rdf:first ?A. ?A owl:differentFrom ?X. ?S rdf:rest ?B. ?B :notItem ?X} => {?S :notItem ?X}. {} => {?X :includes rdf:nil}. {?S rdf:first ?A. ?X :item ?E. ?E owl:equivalentClass ?A. ?S rdf:rest ?B. ?X :includes ?B} => {?X :includes ?S}. {} => {?X :inAllOf rdf:nil}. {?S rdf:first ?A. ?X a ?A. ?S rdf:rest ?B. ?X :inAllOf ?B} => {?X :inAllOf ?S}. {?S rdf:first ?A. ?X a ?A} => {?X :inSomeOf ?S}. {?S rdf:rest ?B. ?X :inSomeOf ?B} => {?X :inSomeOf ?S}. {} => {rdf:nil :memberCount 0}. {?A rdf:rest ?B. ?B :memberCount ?M. (?M 1) math:sum ?N} => {?A :memberCount ?N}. {} => {rdf:nil :allClasses ?C}. {?L rdf:first ?A; rdf:rest ?B. ?A owl:equivalentClass ?C. ?B :allClasses ?C} => {?L :allClasses ?C}. {?L rdf:first ?A. ?A owl:equivalentClass ?C} => {?L :someClasses ?C}. {?L rdf:rest ?B. ?B :someClasses ?C} => {?L :someClasses ?C}. {} => {?P :reflexive rdf:nil}. {?S rdf:first ?A. ?A ?P ?A. ?S rdf:rest ?B. ?P :reflexive ?B} => {?P :reflexive ?S}. {?L rdf:first ?O. ?O owl:oneOf ?J. ?J :item ?A} => {?L :oneItem ?A}. {?L rdf:rest ?B. ?B :oneItem ?A} => {?L :oneItem ?A}. {?L :oneItem ?A} => {?L :ones rdf:nil}. {?K rdf:first ?A. ?L :oneItem ?A. ?K rdf:rest ?B. ?L :ones ?B} => {?L :ones ?K}. {?K :item ?A} => {?K :unions rdf:nil}. {?L rdf:first ?O. ?O owl:oneOf ?J. ?J :item ?A. ?K :item ?A. ?L rdf:rest ?B. ?K :unions ?B} => {?K :unions ?L}. {?R owl:someValuesFrom ?C} => {?R :someOrAll ?C}. {?R owl:allValuesFrom ?C} => {?R :someOrAll ?C}.