@prefix : <http://infomesh.net/2001/05/rdflint/vars#> .
@prefix rdf: <http://www.w3.org/1999/02/22-rdf-syntax-ns#> .
@prefix rdfs: <http://www.w3.org/2000/01/rdf-schema#> .
@prefix daml: <http://www.daml.org/2001/03/daml+oil#> .
@prefix log: <http://www.w3.org/2000/10/swap/log#> .

this log:forAll :a , :b , :c , :p , :q , :r , :s , :x , :y , :z .

daml:Class rdfs:subClassOf rdfs:Class .
daml:Datatype rdfs:subClassOf rdfs:Class .
daml:Thing 
   daml:unionOf (daml:Nothing [ daml:complementOf daml:Nothing ]) .
daml:Nothing daml:complementOf daml:Thing .
daml:equivalentTo a rdf:Property .
daml:sameClassAs a rdf:Property; 
   rdfs:subPropertyOf daml:equivalentTo, rdfs:subClassOf .
daml:samePropertyAs a rdf:Property; 
   rdfs:subPropertyOf daml:equivalentTo, rdfs:subPropertyOf .
daml:sameIndividualAs a rdf:Property; rdfs:subPropertyOf daml:equivalentTo; 
   rdfs:domain daml:Thing; rdfs:range daml:Thing .
daml:disjointWith a rdf:Property; 
   rdfs:domain rdfs:Class; rdfs:range rdfs:Class .
daml:differentIndividualFrom a rdf:Property; 
   rdfs:domain rdfs:Thing; rdfs:range rdfs:Thing .
daml:unionOf a rdf:Property; rdfs:domain rdfs:Class; rdfs:range daml:List .
daml:disjointUnionOf a rdf:Property; 
   rdfs:domain rdfs:Class; rdfs:range daml:List .
daml:intersectionOf a rdf:Property; 
   rdfs:domain rdfs:Class; rdfs:range daml:List .
daml:complementOf a rdf:Property; 
   rdfs:domain rdfs:Class; rdfs:range daml:Class .
daml:oneOf a rdf:Property; 
   rdfs:domain rdfs:Class; rdfs:range daml:List .
daml:Restriction a rdfs:Class; 
   rdfs:subClassOf daml:Class .
daml:onProperty a rdf:Property; 
   rdfs:domain daml:Restriction; 
   rdfs:range rdf:Property .
daml:toClass a rdf:Property; 
   rdfs:domain daml:Restriction; rdfs:range rdfs:Class .
daml:hasValue a rdf:Property; rdfs:domain daml:Restriction .
daml:hasClass a rdf:Property;
   rdfs:domain daml:Restriction; rdfs:range rdfs:Class .

# Equivalencies and inverses

{ :p = :q } log:implies { :q = :p } .
{ :a :b :c . :d = :a } log:implies { :d :b :c } .
{ :a :b :c . :d = :b } log:implies { :a :d :c } .
{ :a :b :c . :d = :c } log:implies { :a :b :d } .

{ :p daml:inverseOf :q } log:implies { :q daml:inverseOf :p } .
{ :p daml:inverseOf :q . :a :p :b } log:implies { :b :q :a } .

{ :x daml:inverseOf :x . :y :p :x . :p a daml:TransitiveProperty }
  log:implies { :y daml:inverseOf :y } .

{ :p a daml:TransitiveProperty . :x :p :y . :y :p :z } 
  log:implies { :x :p :z } .

rdfs:subPropertyOf a daml:TransitiveProperty .
rdfs:subClassOf a daml:TransitiveProperty .

{ :p a daml:UniqueProperty . :x :p :y . :x :p :z } 
   log:implies { :y = :z } .

{ :p a daml:UnambiguousProperty . :y :p :x . :z :p :x } 
   log:implies { :y = :z } .

{ :a a :b . :b rdfs:subClassOf :c } log:implies { :a a :c } .

{ :p rdfs:domain :r . :q rdfs:subPropertyOf :p } 
   log:implies { :q rdfs:domain :r } .
{ :p rdfs:range :r . :q rdfs:subPropertyOf :p } 
   log:implies { :q rdfs:range :r } .

{ :x daml:oneOf (:y) } log:implies { :x a rdfs:Class . :y a :x } .