(: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 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))