(in-package :cl-user)

(define-ontology inconsistent-finite-infinite ()
  (class !human :partial)
  (class !woman :partial)
  (class !man :partial)
  (sub-class-of !man !human)
  (sub-class-of !woman !human)
  (disjoint-classes !woman !man)
  (object-property !child)
  (object-property !father (inverse-of !child))
  (sub-class-of !human (restriction !father (all-values-from !man)))
  (sub-class-of !human (restriction !father (cardinality 1)))
  (sub-class-of !human (restriction !child (max-cardinality 1)))
  (object-property !ssn :inverse-functional (range (one-of !one !two)))
  (sub-class-of !human (restriction !ssn (cardinality 1)))
  (individual !mary (type !woman))
  (individual !one)
  (individual !two)
  )

(when (check inconsistent-finite-infinite)
  (warn "~a should be inconsistent but the reasoner thinks it is consistent" inconsistent-finite-infinite))


(define-ontology consistent-infinite-infinite ()
  (class !human :partial)
  (class !woman :partial)
  (class !man :partial)
  (sub-class-of !man !human)
  (sub-class-of !woman !human)
  (disjoint-classes !woman !man)
  (object-property !child)
  (object-property !father (inverse-of !child))
  (sub-class-of !human (restriction !father (all-values-from !man)))
  (sub-class-of !human (restriction !father (cardinality 1)))
  (sub-class-of !human (restriction !child (max-cardinality 1)))
  (object-property !ssn :inverse-functional)
  (sub-class-of !human (restriction !ssn (cardinality 1)))
  (individual !mary (type !woman))
  )

;; infinite loop
(when (not (check consistent-infinite-infinite))
  (warn "~a should be consistent but the reasoner thinks it is inconsistent" consistent-infinite-infinite))