(:name type-theorem-1
 :body (=> (Type ?p rdf\:Property) (Type ?p rdfs\:Resource)))


(:name type-theorem-2
 :body (=> (Type ?c rdfs\:Class) (Type ?c rdfs\:Resource)))


(:name type-theorem-3
 :body (=> (Type ?s rdf\:Statement) (Type ?s rdfs\:Resource)))


(:name type-theorem-4
 :body (=> (Type ?c rdf\:Container) (Type ?c rdfs\:Resource)))


(:name type-theorem-5
 :body (Type rdf\:Property rdfs\:Class))


(:name subClassOf-theorem-1
 :body (PropertyValue subClassOf rdf\:Property rdfs\:Resource))


(:name subClassOf-theorem-2
 :body (PropertyValue subClassOf rdfs\:Class rdfs\:Resource))


(:name subClassOf-theorem-3
 :body (PropertyValue subClassOf rdf\:Statement rdfs\:Resource))


(:name subClassOf-theorem-4
 :body (PropertyValue subClassOf rdf\:Bag rdf\:Container))


(:name subClassOf-theorem-5
 :body (PropertyValue subClassOf rdf\:Seq rdf\:Container))


(:name subClassOf-theorem-6
 :body (PropertyValue subClassOf rdf\:Alt rdf\:Container))


(:name subClassOf-theorem-7
 :body (PropertyValue subClassOf rdf\:ContainerMembershipProperty
        rdf\:Property))


(:name subClassOf-theorem-8
 :body (=>
        (and (PropertyValue subClassOf ?csub ?csuper) (Type ?x ?csub))
        (Type ?x ?csuper)))


(:name subPropertyOf-theorem-1
 :body (=>
        (and (PropertyValue subPropertyOf ?subP ?superP)
         (PropertyValue ?subP ?o ?v))
        (PropertyValue ?superP ?o ?v)))


(:name range-theorem-1
 :body (PropertyValue rdfs\:range subClassOf rdfs\:Class))


(:name range-theorem-2
 :body (PropertyValue rdfs\:range rdfs\:range rdfs\:Class))


(:name range-theorem-3
 :body (PropertyValue rdfs\:range rdf\:type rdfs\:Class))


(:name range-theorem-4
 :body (PropertyValue rdfs\:range rdf\:subject rdfs\:Resource))


(:name range-theorem-5
 :body (PropertyValue rdfs\:range rdf\:predicate rdf\:Property))


(:name range-theorem-6
 :body (PropertyValue rdfs\:range rdf\:object rdfs\:Resource))


(:name range-theorem-7
 :body (PropertyValue rdfs\:range subPropertyOf rdf\:Property))


(:name range-theorem-8
 :body (=>
        (and (PropertyValue rdfs\:range ?p ?r)
         (PropertyValue ?p ?x ?y))
        (Type ?y ?r)))


(:name domain-theorem-1
 :body (PropertyValue rdfs\:domain rdfs\:domain rdf\:Property))


(:name domain-theorem-2
 :body (PropertyValue rdfs\:range rdfs\:domain rdfs\:Class))


(:name domain-theorem-3
 :body (PropertyValue rdfs\:domain rdf\:type rdfs\:Resource))


(:name domain-theorem-4
 :body (PropertyValue rdfs\:domain rdf\:subject rdf\:Statement))


(:name domain-theorem-5
 :body (PropertyValue rdfs\:domain rdf\:predicate rdf\:Statement))


(:name domain-theorem-6
 :body (PropertyValue rdfs\:domain rdf\:object rdf\:Statement))


(:name domain-theorem-7
 :body (PropertyValue rdfs\:domain subClassOf rdfs\:Class))


(:name domain-theorem-8
 :body (PropertyValue rdfs\:domain rdfs\:range rdf\:Property))


(:name domain-theorem-9
 :body (PropertyValue rdfs\:domain subPropertyOf rdf\:Property))


(:name domain-theorem-10
 :body (=>
        (and (PropertyValue rdfs\:domain ?p ?d)
         (PropertyValue ?p ?x ?y))
        (Type ?x ?d)))


(:name domain-theorem-11
 :body (PropertyValue rdfs\:domain rdf\:value rdfs\:Resource))


(:name domain-theorem-11+i
 :body (PropertyValue rdfs\:domain rdf\:_i rdf\:Container))


(:name Thing-theorem-1
 :body (=> (Type rdfs\:Class ?c)
        (PropertyValue subClassOf ?c daml\:Thing)))


(:name Nothing-theorem-1
 :body (=> (Type ?x daml\:Nothing) FALSE))


(:name TransitiveProperty-theorem-1
 :body (PropertyValue subClassOf daml\:TransitiveProperty
        daml\:AbstractProperty))


(:name TransitiveProperty-theorem-2
 :body (Type subClassOf daml\:TransitiveProperty))


(:name TransitiveProperty-theorem-3
 :body (Type subPropertyOf daml\:TransitiveProperty))


(:name TransitiveProperty-theorem-4
 :body (=>
        (and (Type ?p daml\:TransitiveProperty)
         (PropertyValue ?p ?x ?y) (PropertyValue ?p ?y ?z))
        (PropertyValue ?p ?x ?z)))


(:name UniqueProperty-theorem-1
 :body (PropertyValue subClassOf daml\:UniqueProperty rdf\:Property))


(:name UniqueProperty-theorem-1
 :body (Type rdf\:predicate daml\:UniqueProperty))


(:name UniqueProperty-theorem-2
 :body (Type rdf\:subject daml\:UniqueProperty))


(:name UniqueProperty-theorem-3
 :body (Type rdf\:object daml\:UniqueProperty))


(:name UniqueProperty-theorem-4
 :body (Type rdfs\:range daml\:UniqueProperty))


(:name UniqueProperty-theorem-6
 :body (Type rdf\:_i daml\:UniqueProperty))


(:name UnambiguousProperty-theorem-1
 :body (PropertyValue subClassOf daml\:UnambiguousProperty
        daml\:AbstractProperty))


(:name equivalentTo-theorem-1
 :body (PropertyValue daml\:inverseOf daml\:equivalentTo
        daml\:equivalentTo))


(:name equivalentTo-theorem-2
 :body (Type daml\:TransitiveProperty daml\:equivalentTo))


(:name equivalentTo-theorem-3
 :body (=> (Type ?x daml\:Thing)
        (PropertyValue daml\:equivalentTo ?x ?x)))


(:name equivalentTo-theorem-4
 :body (=> (and (PropertyValue daml\:equivalentTo ?x ?y) (Type ?x ?c))
        (Type ?y ?c)))


(:name equivalentTo-theorem-5
 :body (=>
        (and (Type ?p daml\:UniqueProperty) (PropertyValue ?p ?x ?y)
         (PropertyValue ?p ?x ?z))
        (PropertyValue daml\:equivalentTo ?y ?z)))


(:name equivalentTo-theorem-6
 :body (=>
        (and (Type ?p daml\:UnambiguousProperty)
         (PropertyValue ?p ?x ?v) (PropertyValue ?p ?y ?v))
        (PropertyValue daml\:equivalentTo ?x ?y)))


(:name sameClassAs-theorem-1
 :body (PropertyValue subPropertyOf daml\:sameClassAs subClassOf))


(:name sameClassAs-theorem-2
 :body (=>
        (and (PropertyValue subClassOf ?c1 ?c2)
         (PropertyValue subClassOf ?c2 ?c1))
        (PropertyValue daml\:sameClassAs ?c1 ?c2)))


(:name sameClassAs-theorem-3
 :body (=>
        (and (PropertyValue daml\:equivalentTo ?c1 ?c2)
         (Type ?c1 rdfs\:Class))
        (PropertyValue daml\:sameClassAs ?c1 ?c2)))


(:name samePropertyAs-theorem-1
 :body (PropertyValue subPropertyOf daml\:samePropertyAs subPropertyOf))


(:name samePropertyAs-theorem-2
 :body (PropertyValue daml\:inverseOf daml\:samePropertyAs
        daml\:samePropertyAs))


(:name samePropertyAs-theorem-3
 :body (=>
        (and (PropertyValue subPropertyOf ?p1 ?p2)
         (PropertyValue subPropertyOf ?p2 ?p1))
        (PropertyValue daml\:samePropertyAs ?p1 ?p2)))


(:name samePropertyAs-theorem-4
 :body (=>
        (and (PropertyValue daml\:equivalentTo ?p1 ?p2)
         (Type ?p1 rdf\:Property))
        (PropertyValue daml\:samePropertyAs ?p1 ?p2)))


(:name disjointWith-theorem-1
 :body (PropertyValue rdfs\:domain daml\:disjointWith rdfs\:Class))


(:name disjointWith-theorem-2
 :body (PropertyValue daml\:inverseOf daml\:disjointWith
        daml\:disjointWith))


(:name disjointWith-theorem-3
 :body (PropertyValue daml\:disjointWith rdf\:Property rdfs\:Class))


(:name disjointWith-theorem-4
 :body (=>
        (and (PropertyValue daml\:disjointWith ?c1 ?c2) (Type ?x ?c1)
         (Type ?x ?c2))
        FALSE))


(:name disjointWith-theorem-5
 :body (=>
        (and (PropertyValue daml\:disjointWith ?c1 ?c2)
         (PropertyValue subClassOf ?c ?c1))
        (PropertyValue daml\:disjointWith ?c ?c2)))


(:name disjointWith-theorem-6
 :body (=>
        (and (PropertyValue daml\:disjointWith ?c1 ?c2)
         (PropertyValue subClassOf ?c ?c1)
         (PropertyValue subClassOf ?c ?c2))
        (PropertyValue daml\:sameClassAs ?c daml\:Nothing)))


(:name unionOf-theorem-1
 :body (PropertyValue rdfs\:domain daml\:unionOf rdfs\:Class))


(:name unionOf-theorem-2
 :body (PropertyValue rdfs\:range daml\:unionOf daml\:List))


(:name unionOf-theorem-3
 :body (=>
        (and (PropertyValue daml\:unionOf ?c1 ?l)
         (PropertyValue daml\:unionOf ?c2 ?l))
        (PropertyValue daml\:sameClassAs ?c1 ?c2)))


(:name disjointUnionOf-theorem-1
 :body (PropertyValue subPropertyOf daml\:disjointUnionOf
        daml\:unionOf))


(:name intersectionOf-theorem-1
 :body (PropertyValue rdfs\:domain daml\:intersectionOf rdfs\:Class))


(:name intersectionOf-theorem-2
 :body (PropertyValue rdfs\:range daml\:intersectionOf daml\:List))


(:name complementOf-theorem-1
 :body (PropertyValue subPropertyOf daml\:complementOf
        daml\:disjointWith))


(:name complementOf-theorem-2
 :body (PropertyValue daml\:inverseOf daml\:complementOf
        daml\:complementOf))


(:name complementOf-theorem-3
 :body (=>
        (and (PropertyValue daml\:complementOf ?c1 ?c2)
         (PropertyValue daml\:disjointWith ?c1 ?c3))
        (PropertyValue subClassOf ?c3 ?c2)))


(:name complementOf-theorem-4
 :body (=>
        (and (PropertyValue daml\:complementOf ?c1 ?c2)
         (PropertyValue daml\:complementOf ?c3 ?c4)
         (PropertyValue subClassOf ?c1 ?c3))
        (PropertyValue subClassOf ?c4 ?c2)))


(:name oneOf-theorem-1
 :body (PropertyValue rdfs\:domain daml\:oneOf rdfs\:Class))


(:name oneOf-theorem-2
 :body (PropertyValue rdfs\:range daml\:oneOf daml\:List))


(:name oneOf-theorem-3
 :body (=>
        (and (PropertyValue daml\:oneOf ?c1 ?l)
         (PropertyValue daml\:oneOf ?c2 ?l))
        (PropertyValue daml\:sameClassAs ?c1 ?c2)))


(:name toClass-theorem-1
 :body (=>
        (and (PropertyValue daml\:onProperty ?r ?p)
         (PropertyValue daml\:toClass ?r ?c) (Type ?x ?r)
         (PropertyValue ?p ?x ?v))
        (Type ?v ?c)))


(:name toClass-theorem-2
 :body (=>
        (and (PropertyValue daml\:onProperty ?r1 ?p)
         (PropertyValue daml\:toClass ?r1 ?c1)
         (PropertyValue daml\:onProperty ?r2 ?p)
         (PropertyValue daml\:toClass ?r2 ?c2)
         (PropertyValue subClassOf ?c1 ?c2))
        (PropertyValue subClassOf ?r1 ?r2)))


(:name toClass-theorem-3
 :body (=>
        (and (PropertyValue daml\:onProperty ?r1 ?p)
         (PropertyValue daml\:toClass ?r1 ?c1)
         (PropertyValue daml\:onProperty ?r2 ?p)
         (PropertyValue daml\:toClass ?r2 ?c2)
         (PropertyValue daml\:disjointWith ?c1 ?c2))
        (PropertyValue daml\:disjointWith ?r1 ?r2)))


(:name hasValue-theorem-1
 :body (=>
        (and (PropertyValue daml\:onProperty ?r ?p)
         (PropertyValue daml\:hasValue ?r ?v) (Type ?i ?r))
        (PropertyValue ?p ?i ?v)))


(:name hasValue-theorem-2
 :body (=>
        (and (PropertyValue daml\:onProperty ?r ?p)
         (PropertyValue daml\:hasValue ?r ?v) (PropertyValue ?p ?i ?v))
        (Type ?i ?r)))


(:name hasClass-theorem-1
 :body (=>
        (and (PropertyValue daml\:hasClass ?r ?c)
         (PropertyValue daml\:onProperty ?r ?p)
         (PropertyValue ?p ?x ?v) (Type ?v ?c))
        (Type ?x ?r)))


(:name minCardinalityQ-theorem-1
 :body (=>
        (and (PropertyValue daml\:minCardinality ?r1 ?n)
         (PropertyValue daml\:onProperty ?r1 ?p)
         (PropertyValue daml\:minCardinalityQ ?r2 ?n)
         (PropertyValue daml\:onProperty ?r2 ?p)
         (PropertyValue daml\:hasClassQ ?r2 daml\:Thing))
        (PropertyValue daml\:sameClassAs ?r1 ?r2)))


(:name minCardinalityQ-theorem-2
 :body (=>
        (and (PropertyValue daml\:hasValue ?r1 ?v)
         (PropertyValue daml\:onProperty ?r1 ?p) (Type ?v ?c)
         (PropertyValue daml\:hasClassQ ?r2 ?c)
         (PropertyValue daml\:minCardinalityQ ?r2 1.)
         (PropertyValue daml\:onProperty ?r1 ?p))
        (PropertyValue subClassOf ?r1 ?r2)))


(:name minCardinalityQ-theorem-3
 :body (=>
        (and (PropertyValue daml\:hasClass ?r1 ?c)
         (PropertyValue daml\:onProperty ?r1 ?p)
         (PropertyValue daml\:hasClassQ ?r2 ?c)
         (PropertyValue daml\:minCardinalityQ ?r2 1.))
        (PropertyValue daml\:sameClassAs ?r2 ?r1)))


(:name minCardinalityQ-theorem-4
 :body (=>
        (and (PropertyValue daml\:minCardinalityQ ?r1 ?n1)
         (PropertyValue daml\:onProperty ?r1 ?p)
         (PropertyValue daml\:hasClassQ ?r1 ?c1)
         (PropertyValue daml\:minCardinalityQ ?r2 ?n2)
         (PropertyValue daml\:onProperty ?r2 ?p)
         (PropertyValue daml\:hasClassQ ?r2 ?c2)
         (PropertyValue subClassOf ?c1 ?c2) (>= ?n1 ?n2))
        (PropertyValue subClassOf ?r1 ?r2)))


(:name maxCardinalityQ-theorem-1
 :body (=>
        (and (PropertyValue daml\:maxCardinality ?r1 ?n)
         (PropertyValue daml\:onProperty ?r1 ?p)
         (PropertyValue daml\:maxCardinalityQ ?r2 ?n)
         (PropertyValue daml\:onProperty ?r2 ?p)
         (PropertyValue daml\:hasClassQ ?r2 daml\:Thing))
        (PropertyValue daml\:sameClassAs ?r1 ?r2)))


(:name maxCardinalityQ-theorem-2
 :body (=>
        (and (PropertyValue daml\:minCardinalityQ ?r1 ?n1)
         (PropertyValue daml\:onProperty ?r1 ?p)
         (PropertyValue daml\:hasClassQ ?r1 ?c1)
         (PropertyValue daml\:maxCardinalityQ ?r2 ?n2)
         (PropertyValue daml\:onProperty ?r2 ?p)
         (PropertyValue daml\:hasClassQ ?r2 ?c2)
         (PropertyValue subClassOf ?c1 ?c2) (> ?n1 ?n2))
        (PropertyValue daml\:disjointWith ?r1 ?r2)))


(:name maxCardinalityQ-theorem-3
 :body (=>
        (and (PropertyValue daml\:maxCardinalityQ ?r 0.)
         (PropertyValue daml\:onProperty ?r ?p)
         (PropertyValue daml\:hasClassQ ?r ?c) (Type ?x ?r)
         (PropertyValue ?p ?x ?v) (Type ?v ?c))
        FALSE))


(:name maxCardinalityQ-theorem-4
 :body (=>
        (and (PropertyValue daml\:maxCardinalityQ ?r 1.)
         (PropertyValue daml\:onProperty ?r ?p)
         (PropertyValue daml\:hasClassQ ?r ?c) (Type ?x ?r)
         (PropertyValue ?p ?x ?v1) (Type ?v1 ?c)
         (PropertyValue ?p ?x ?v2) (Type ?v2 ?c))
        (PropertyValue daml\:equivalentTo ?v1 ?v2)))


(:name maxCardinalityQ-theorem-5
 :body (=>
        (and (PropertyValue daml\:maxCardinalityQ ?r1 ?n1)
         (PropertyValue daml\:onProperty ?r1 ?p)
         (PropertyValue daml\:hasClassQ ?r1 ?c1)
         (PropertyValue daml\:maxCardinalityQ ?r2 ?n2)
         (PropertyValue daml\:onProperty ?r2 ?p)
         (PropertyValue daml\:hasClassQ ?r2 ?c2)
         (PropertyValue subClassOf ?c2 ?c1) (< ?n1 ?n2))
        (PropertyValue subClassOf ?r1 ?r2)))


(:name cardinalityQ-theorem-1
 :body (=>
        (and (PropertyValue daml\:cardinality ?r1 ?n)
         (PropertyValue daml\:onProperty ?r1 ?p)
         (PropertyValue daml\:cardinalityQ ?r2 ?n)
         (PropertyValue daml\:onProperty ?r2 ?p)
         (PropertyValue daml\:hasClassQ ?r2 daml\:Thing))
        (PropertyValue daml\:sameClassAs ?r1 ?r2)))


(:name cardinalityQ-theorem-2
 :body (=>
        (and (PropertyValue daml\:cardinalityQ ?r1 ?n)
         (PropertyValue daml\:onProperty ?r1 ?p)
         (PropertyValue daml\:hasClassQ ?r1 ?c)
         (PropertyValue daml\:minCardinalityQ ?r2 ?n)
         (PropertyValue daml\:onProperty ?r2 ?p)
         (PropertyValue daml\:hasClassQ ?r2 ?c)
         (PropertyValue daml\:maxCardinalityQ ?r3 ?n)
         (PropertyValue daml\:onProperty ?r3 ?p)
         (PropertyValue daml\:hasClassQ ?r3 ?c)
         (PropertyValue daml\:first ?l1 ?r2)
         (PropertyValue daml\:rest ?l1 ?l2)
         (PropertyValue daml\:first ?l2 ?r3)
         (PropertyValue daml\:rest ?l2 daml\:nil))
        (PropertyValue daml\:intersectionOf ?r1 ?l1)))


(:name inverseOf-theorem-1
 :body (PropertyValue rdfs\:domain daml\:inverseOf
        daml\:AbstractProperty))


(:name inverseOf-theorem-2
 :body (PropertyValue rdfs\:range daml\:inverseOf
        daml\:AbstractProperty))


(:name inverseOf-theorem-3
 :body (=>
        (and (PropertyValue daml\:inverseOf ?p1 ?p2)
         (PropertyValue ?p1 ?x1 ?x2))
        (PropertyValue ?p2 ?x2 ?x1)))


(:name first-theorem-1
 :body (PropertyValue rdfs\:domain daml\:first daml\:List))


(:name first-theorem-2
 :body (PropertyValue subPropertyOf daml\:first rdf\:_1))


(:name first-theorem-3
 :body (=> (and (Type ?l daml\:List) (PropertyValue rdf\:_1 ?l ?x))
        (PropertyValue daml\:first ?l ?x)))


(:name rest-theorem-1
 :body (PropertyValue rdfs\:domain daml\:rest daml\:List))


(:name rest-theorem-2
 :body (PropertyValue rdfs\:range daml\:rest daml\:List))


(:name rest-theorem-3
 :body (Type daml\:rest uniqueProperty))


(:name rest-theorem-3+N
 :body (=>
        (and (PropertyValue daml\:rest ?l ?r) (PropertyValue _N ?r ?x))
        (PropertyValue _N+1 ?l ?x)))


(:name item-theorem-1
 :body (PropertyValue rdfs\:domain daml\:item daml\:List))


(:name item-theorem-2
 :body (=>
        (and (PropertyValue daml\:unionOf ?c ?l)
         (PropertyValue daml\:item ?l ?c1))
        (PropertyValue subClassOf ?c1 ?c)))


(:name item-theorem-3
 :body (=>
        (and (PropertyValue daml\:intersectionOf ?c ?l)
         (PropertyValue daml\:item ?l ?c1))
        (PropertyValue subClassOf ?c ?c1)))


(:name item-theorem-4
 :body (=> (and (PropertyValue daml\:oneOf ?c ?l) (Type ?x ?c))
        (PropertyValue daml\:item ?l ?x)))


(:name item-theorem-5
 :body (=>
        (and (PropertyValue daml\:oneOf ?c ?l)
         (PropertyValue daml\:item ?l ?x))
        (Type ?x ?c)))


(:name item-theorem-6
 :body (=>
        (and (PropertyValue daml\:rest ?l ?r)
         (PropertyValue daml\:item ?r ?x))
        (PropertyValue daml\:item ?l ?x)))


(:name item-theorem-7
 :body (PropertyValue subPropertyOf daml\:first daml\:item))


(:name item-theorem-7+N
 :body (=> (and (Type ?l daml\:List) (PropertyValue _N ?l ?x))
        (PropertyValue daml\:item ?l ?x)))


(:name nil-theorem-1
 :body (=> (PropertyValue daml\:first daml\:nil ?x) FALSE))


(:name nil-theorem-2
 :body (=> (PropertyValue daml\:rest daml\:nil ?x) FALSE))