(define (domain daml+oil) 
        (:types 
                Thing - object
                        ;The most general (object) class in DAML.
                        ;This is equal to the union of any class and its complement.

                Property - @rdf:Property
                ObjectProperty - @rdf:Property
                        ;if P is an ObjectProperty, and P(x, y), then y is an object.

                Literal - String
                Nothing - object
                        ;the class with no things in it.

                UnambiguousProperty - ObjectProperty
                        ;if P is an UnambiguousProperty, then if P(x, y) and P(z, y) then x=z.
                        ;aka injective. e.g. if firstBorne(m, Susan)
                        ;and firstBorne(n, Susan) then m and n are the same.

                Class - @rdfs:Class
                        ;The class of all "object" classes

                List - @rdf:Seq
                Restriction - Class
                        ;something is in the class R if it satisfies the attached restrictions,
                        ;and vice versa.

                Ontology - object
                        ;An Ontology is a document that describes
                        ;a vocabulary of terms for communication between
                        ;(human and) automated agents.

                UniqueProperty - @rdf:Property
                        ;compare with maxCardinality=1; e.g. integer successor:
                        ;if P is a UniqueProperty, then if P(x, y) and P(x, z) then y=z.
                        ;cf OIL FunctionalProperty.

                DatatypeProperty - @rdf:Property
                        ;if P is a DatatypeProperty, and P(x, y), then y is a data value.

                TransitiveProperty - ObjectProperty
                        ;if P is a TransitiveProperty, then if P(x, y) and P(y, z) then P(x, z).
                        ;cf OIL TransitiveProperty.

                Datatype - @rdfs:Class
                        ;The class of all datatype classes

        )
 
        (:objects 
                nil - List
                        ;the empty list; this used to be called Empty.

        )
 
        (:predicates
                (subPropertyOf ob1 - object ob2 - object)
                (equivalentTo ob1 - object ob2 - object 
                        ;for equivalentTo(X, Y), read X is an equivalent term to Y.
)
                (sameClassAs cl1 - Class cl2 - Class 
                        ;for sameClassAs(X, Y), read X is an equivalent class to Y.
                        ;cf OIL Equivalent
)
                (label ob1 - object ob2 - object)
                (maxCardinality re1 - Restriction in2 - Integer 
                        ;for onProperty(R, P) and maxCardinality(R, n), read:
                        ;i is in class R if and only if there are at most n distinct j with P(i, j).
                        ;cf OIL MaxCardinality
)
                (imports ob1 - object ob2 - object 
                        ;for imports(X, Y) read: X imports Y;
                        ;i.e. X asserts the* contents of Y by reference;
                        ;i.e. if imports(X, Y) and you believe X and Y says something,
                        ;then you should believe it.
                        ;Note: "the contents" is, in the general case,
                        ;an il-formed definite description. Different
                        ;interactions with a resource may expose contents
                        ;that vary with time, data format, preferred language,
                        ;requestor credentials, etc. So for "the contents",
                        ;read "any contents".
)
                (type ob1 - object ob2 - object)
                (hasClass re1 - Restriction cl2 - @rdfs:Class 
                        ;for onProperty(R, P) and hasClass(R, X), read:
                        ;i is in class R if and only if for some j, P(i, j) and type(j, X).
                        ;cf OIL HasValue
)
                (versionInfo ob1 - object ob2 - object 

                        ;generally, a string giving information about this
                        ;version; e.g. RCS/CVS keywords
)
                (samePropertyAs ob1 - object ob2 - object 
                        ;for samePropertyAs(P, R), read P is an equivalent property to R.
)
                (value ob1 - object ob2 - object)
                (hasClassQ re1 - Restriction cl2 - @rdfs:Class 
                        ;property for specifying class restriction with cardinalityQ constraints
)
                (disjointWith cl1 - Class cl2 - Class 
                        ;for disjointWith(X, Y) read: X and Y have no members in common.
                        ;cf OIL Disjoint
)
                (cardinalityQ re1 - Restriction in2 - Integer 
                        ;for onProperty(R, P), cardinalityQ(R, n) and hasClassQ(R, X), read:
                        ;i is in class R if and only if there are exactly n distinct j with P(i, j)
                        ;and type(j, X).
                        ;cf OIL Cardinality
)
                (onProperty re1 - Restriction pr2 - @rdf:Property 
                        ;for onProperty(R, P), read:
                        ;R is a restricted with respect to property P.
)
                (inverseOf ob1 - ObjectProperty ob2 - ObjectProperty 
                        ;for inverseOf(R, S) read: R is the inverse of S; i.e.
                        ;if R(x, y) then S(y, x) and vice versa.
                        ;cf OIL inverseRelationOf
)
                (cardinality re1 - Restriction in2 - Integer 
                        ;for onProperty(R, P) and cardinality(R, n), read:
                        ;i is in class R if and only if there are exactly n distinct j with P(i, j).
                        ;cf OIL Cardinality
)
                (first li1 - List ob2 - object)
                (subClassOf ob1 - object ob2 - object)
                (intersectionOf cl1 - Class li2 - List 
                        ;for intersectionOf(X, Y) read: X is the intersection of the classes in the list Y;
                        ;i.e. if something is in all the classes in Y, then it's in X, and vice versa.
                        ;cf OIL AND
)
                (range ob1 - object ob2 - object)
                (disjointUnionOf cl1 - Class li2 - List 
                        ;for disjointUnionOf(X, Y) read: X is the disjoint union of the classes in
                        ;the list Y: (a) for any c1 and c2 in Y, disjointWith(c1, c2),
                        ;and (b) unionOf(X, Y). i.e. if something is in any of the classes in Y, it's
                        ;in X, and vice versa.
                        ;cf OIL disjoint-covered
)
                (minCardinality re1 - Restriction in2 - Integer 
                        ;for onProperty(R, P) and minCardinality(R, n), read:
                        ;i is in class R if and only if there are at least n distinct j with P(i, j).
                        ;cf OIL MinCardinality
)
                (minCardinalityQ re1 - Restriction in2 - Integer 
                        ;for onProperty(R, P), minCardinalityQ(R, n) and hasClassQ(R, X), read:
                        ;i is in class R if and only if there are at least n distinct j with P(i, j)
                        ;and type(j, X).
                        ;cf OIL MinCardinality
)
                (sameIndividualAs th1 - Thing th2 - Thing 
                        ;for sameIndividualAs(a, b), read a is the same individual as b.
)
                (seeAlso ob1 - object ob2 - object)
                (complementOf cl1 - Class cl2 - Class 
                        ;for complementOf(X, Y) read: X is the complement of Y; if something is in Y,
                        ;then it's not in X, and vice versa.
                        ;cf OIL NOT
)
                (unionOf cl1 - Class li2 - List 
                        ;for unionOf(X, Y) read: X is the union of the classes in the list Y;
                        ;i.e. if something is in any of the classes in Y, it's in X, and vice versa.
                        ;cf OIL OR
)
                (isDefinedBy ob1 - ob2 - object)
                (maxCardinalityQ re1 - Restriction in2 - Integer 
                        ;for onProperty(R, P), maxCardinalityQ(R, n) and hasClassQ(R, X), read:
                        ;i is in class R if and only if there are at most n distinct j with P(i, j)
                        ;and type(j, X).
                        ;cf OIL MaxCardinality
)
                (hasValue re1 - Restriction ob2 - object 
                        ;for onProperty(R, P) and hasValue(R, V), read:
                        ;i is in class R if and only if P(i, V).
                        ;cf OIL HasFiller
)
                (oneOf cl1 - Class li2 - List 
                        ;for oneOf(C, L) read everything in C is one of the
                        ;things in L;
                        ;This lets us define classes by enumerating the members.
                        ;cf OIL OneOf
)
                (domain ob1 - object ob2 - object)
                (differentIndividualFrom th1 - Thing th2 - Thing 
                        ;for differentIndividualFrom(a, b), read a is not the same individual as b.
)
                (toClass re1 - Restriction cl2 - @rdfs:Class 
                        ;for onProperty(R, P) and toClass(R, X), read:
                        ;i is in class R if and only if for all j, P(i, j) implies type(j, X).
                        ;cf OIL ValueType
)
                (comment ob1 - object ob2 - object)
                (item li1 - List ob2 - object 
                        ;for item(L, I) read: I is an item in L; either first(L, I)
                        ;or item(R, I) where rest(L, R).
)
                (rest li1 - List li2 - List)
        )


        (:facts
                (forall (ob1 - object ob2 - object) (if (subPropertyOf ob1 ob2) (@rdfs:subPropertyOf ob1 ob2)))
                (forall (ob1 - object ob2 - object) (if (sameClassAs ob1 ob2) (equivalentTo ob1 ob2)))
                (forall (ob1 - object ob2 - object) (if (sameClassAs ob1 ob2) (@rdfs:subClassOf ob1 ob2)))
                (forall (ob1 - object ob2 - object) (if (label ob1 ob2) (@rdfs:label ob1 ob2)))
                (forall (ob1 - object ob2 - object) (if (type ob1 ob2) (@rdf:type ob1 ob2)))
                (forall (ob1 - object ob2 - object) (if (samePropertyAs ob1 ob2) (equivalentTo ob1 ob2)))
                (forall (ob1 - object ob2 - object) (if (samePropertyAs ob1 ob2) (@rdfs:subPropertyOf ob1 ob2)))
                (forall (ob1 - object ob2 - object) (if (value ob1 ob2) (@rdf:value ob1 ob2)))
                (forall (ob1 - object ob2 - object) (if (subClassOf ob1 ob2) (@rdfs:subClassOf ob1 ob2)))
                (forall (ob1 - object ob2 - object) (if (range ob1 ob2) (@rdfs:range ob1 ob2)))
                (forall (ob1 - object ob2 - object) (if (sameIndividualAs ob1 ob2) (equivalentTo ob1 ob2)))
                (forall (ob1 - object ob2 - object) (if (seeAlso ob1 ob2) (@rdfs:seeAlso ob1 ob2)))
                (forall (ob1 - object ob2 - object) (if (isDefinedBy ob1 ob2) (@rdfs:isDefinedBy ob1 ob2)))
                (forall (ob1 - object ob2 - object) (if (isDefinedBy ob1 ob2) (seeAlso ob1 ob2)))
                (forall (ob1 - object ob2 - object) (if (domain ob1 ob2) (@rdfs:domain ob1 ob2)))
                (forall (ob1 - object ob2 - object) (if (comment ob1 ob2) (@rdfs:comment ob1 ob2)))
                (forall (x - object) (if (is Thing x) (or (is Nothing x) (not (is Nothing x)))))
                (forall (x - object) (if (or (is Nothing x) (not (is Nothing x))) (is Thing x)))
                (forall (x - object) (if (not (is Thing x)) (is Nothing x)))
                (forall (x - object) (if (is Nothing x) (not (is Thing x))))
                (forall (ob1 - object ob2 - object) (if (@rdfs:subPropertyOf ob1 ob2) (subPropertyOf ob1 ob2)))
                (forall (x - object) (if (is String x) (is Literal x)))
                (forall (x - object) (if (is @rdf:Property x) (is Property x)))
                (forall (ob1 - object ob2 - object) (if (@rdf:type ob1 ob2) (type ob1 ob2)))
                (forall (ob1 - object ob2 - object) (if (@rdf:value ob1 ob2) (value ob1 ob2)))
                (forall (ob1 - object ob2 - object) (if (@rdfs:subClassOf ob1 ob2) (subClassOf ob1 ob2)))
                (forall (ob1 - object ob2 - object) (if (@rdfs:domain ob1 ob2) (domain ob1 ob2)))
                (forall (ob1 - object ob2 - object) (if (@rdfs:range ob1 ob2) (range ob1 ob2)))
                (forall (ob1 - object ob2 - object) (if (@rdfs:label ob1 ob2) (label ob1 ob2)))
                (forall (ob1 - object ob2 - object) (if (@rdfs:comment ob1 ob2) (comment ob1 ob2)))
                (forall (ob1 - object ob2 - object) (if (@rdfs:seeAlso ob1 ob2) (seeAlso ob1 ob2)))
                (forall (ob1 - object ob2 - object) (if (@rdfs:isDefinedBy ob1 ob2) (isDefinedBy ob1 ob2)))
        )
)