(note TQG32)  ;; boolean version
(time 300)

;; Intensional query requiring circular subclass reasoning.

(instance Class32-1 Class)
(instance Class32-2 Class)
(instance Class32-3 Class)

(subclass Class32-1 Animal)
(subclass Class32-2 Animal)
(subclass Class32-3 Animal)

(subclass Class32-1 Class32-2)
(subclass Class32-2 Class32-3)
(subclass Class32-3 Class32-1)

(query (forall (?X) (=> (instance ?X Class32-2) (instance ?X Class32-1))))

(answer yes)


;; Answer 1. [yes]

;; 1. 	(not
;;     (forall (?X0)
;;         (=>
;;             (instance ?X0 Class32-2)
;;             (instance ?X0 Class32-1))))	[Negated Query]	
;; 2. 	(not
;;     (instance sk508 Class32-1))	1 	
;; 3. 	(subclass Class32-3 Class32-1)	[KB]	
;; 4. 	(subclass Class32-3 Class32-1)	3 	
;; 5. 	(=>
;;     (subclass ?X403 ?X404)
;;     (and
;;         (instance ?X403 SetOrClass)
;;         (instance ?X404 SetOrClass)))	[KB]	
;; 6. 	(or
;;     (instance ?X1 SetOrClass)
;;     (not
;;         (subclass ?X0 ?X1)))	5 	
;; 7. 	(or
;;     (instance ?X0 SetOrClass)
;;     (not
;;         (subclass ?X0 ?X1)))	5 	
;; 8. 	(=>
;;     (and
;;         (instance ?X403 SetOrClass)
;;         (instance ?X404 SetOrClass))
;;     (=>
;;         (and
;;             (subclass ?X403 ?X404)
;;             (instance ?X405 ?X403))
;;         (instance ?X405 ?X404)))	[KB]	
;; 9. 	(or
;;     (instance ?X2 ?X1)
;;     (not
;;         (instance ?X2 ?X0))
;;     (not
;;         (subclass ?X0 ?X1))
;;     (not
;;         (instance ?X1 SetOrClass))
;;     (not
;;         (instance ?X0 SetOrClass)))	8 	
;; 10. 	(or
;;     (not
;;         (subclass ?X0 ?X1))
;;     (not
;;         (instance ?X2 ?X0))
;;     (instance ?X2 ?X1))	6 7 9 	
;; 11. 	(or
;;     (instance ?X0 Class32-1)
;;     (not
;;         (instance ?X0 Class32-3)))	4 10 	
;; 12. 	(not
;;     (instance sk508 Class32-3))	2 11 	
;; 13. 	(instance sk508 Class32-2)	1 	
;; 14. 	(subclass Class32-2 Class32-3)	[KB]	
;; 15. 	(subclass Class32-2 Class32-3)	14 	
;; 16. 	(or
;;     (not
;;         (instance ?X0 Class32-2))
;;     (instance ?X0 Class32-3))	15 10 	
;; 17. 	True	12 13 16