(note TQG50)  ;; boolean version

;; Skolemization of a deep class hierarchy, with subsumption.

(time 300)

(instance Creature50-1 Animal)

(=>
  (subclass Reptile Animal)
  (exists (?C1 ?C2 ?C3 ?C4 ?C5 ?C6 ?C7 ?C8 ?C9 ?C10)
    (and
      (subclass ?C1 ?C2)
      (subclass ?C2 ?C3)
      (subclass ?C3 ?C4)
      (subclass ?C4 ?C5)
      (subclass ?C5 ?C6)
      (subclass ?C6 ?C7)
      (subclass ?C7 ?C8)
      (subclass ?C8 ?C9)
      (subclass ?C9 ?C10)
      (subclass ?C10 Reptile)
      (instance Creature50-1 ?C1))))

(query (instance Creature50-1 Reptile))

(answer yes)


;; Answer 1. [yes]

;; 1. 	(=>
;;     (subclass Reptile Animal)
;;     (exists (?X0 ?X1 ?X2 ?X3 ?X4 ?X5 ?X6 ?X7 ?X8 ?X9)
;;         (and
;;             (subclass ?X0 ?X1)
;;             (subclass ?X1 ?X2)
;;             (subclass ?X2 ?X3)
;;             (subclass ?X3 ?X4)
;;             (subclass ?X4 ?X5)
;;             (subclass ?X5 ?X6)
;;             (subclass ?X6 ?X7)
;;             (subclass ?X7 ?X8)
;;             (subclass ?X8 ?X9)
;;             (subclass ?X9 Reptile)
;;             (instance Creature50-1 ?X0))))	[KB]	
;; 2. 	(or
;;     (instance Creature50-1 sk523)
;;     (not
;;         (subclass Reptile Animal)))	1 	
;; 3. 	(subclass Reptile Animal)	[KB]	
;; 4. 	(subclass Reptile Animal)	3 	
;; 5. 	(instance Creature50-1 sk523)	2 4 	
;; 6. 	(=>
;;     (subclass ?X403 ?X404)
;;     (and
;;         (instance ?X403 SetOrClass)
;;         (instance ?X404 SetOrClass)))	[KB]	
;; 7. 	(or
;;     (instance ?X1 SetOrClass)
;;     (not
;;         (subclass ?X0 ?X1)))	6 	
;; 8. 	(or
;;     (instance ?X0 SetOrClass)
;;     (not
;;         (subclass ?X0 ?X1)))	6 	
;; 9. 	(=>
;;     (and
;;         (instance ?X403 SetOrClass)
;;         (instance ?X404 SetOrClass))
;;     (=>
;;         (and
;;             (subclass ?X403 ?X404)
;;             (instance ?X405 ?X403))
;;         (instance ?X405 ?X404)))	[KB]	
;; 10. 	(or
;;     (instance ?X2 ?X1)
;;     (not
;;         (instance ?X2 ?X0))
;;     (not
;;         (subclass ?X0 ?X1))
;;     (not
;;         (instance ?X1 SetOrClass))
;;     (not
;;         (instance ?X0 SetOrClass)))	9 	
;; 11. 	(or
;;     (not
;;         (subclass ?X0 ?X1))
;;     (not
;;         (instance ?X2 ?X0))
;;     (instance ?X2 ?X1))	7 8 10 	
;; 12. 	(or
;;     (subclass sk523 sk524)
;;     (not
;;         (subclass Reptile Animal)))	1 	
;; 13. 	(subclass sk523 sk524)	12 4 	
;; 14. 	(or
;;     (not
;;         (instance ?X0 sk523))
;;     (instance ?X0 sk524))	11 13 	
;; 15. 	(instance Creature50-1 sk524)	5 14 	
;; 16. 	(or
;;     (subclass sk524 sk525)
;;     (not
;;         (subclass Reptile Animal)))	1 	
;; 17. 	(subclass sk524 sk525)	16 4 	
;; 18. 	(or
;;     (not
;;         (instance ?X0 sk524))
;;     (instance ?X0 sk525))	11 17 	
;; 19. 	(instance Creature50-1 sk525)	15 18 	
;; 20. 	(or
;;     (subclass sk525 sk526)
;;     (not
;;         (subclass Reptile Animal)))	1 	
;; 21. 	(subclass sk525 sk526)	20 4 	
;; 22. 	(or
;;     (not
;;         (instance ?X0 sk525))
;;     (instance ?X0 sk526))	11 21 	
;; 23. 	(instance Creature50-1 sk526)	19 22 	
;; 24. 	(or
;;     (subclass sk526 sk527)
;;     (not
;;         (subclass Reptile Animal)))	1 	
;; 25. 	(subclass sk526 sk527)	24 4 	
;; 26. 	(or
;;     (not
;;         (instance ?X0 sk526))
;;     (instance ?X0 sk527))	11 25 	
;; 27. 	(instance Creature50-1 sk527)	23 26 	
;; 28. 	(or
;;     (subclass sk527 sk528)
;;     (not
;;         (subclass Reptile Animal)))	1 	
;; 29. 	(subclass sk527 sk528)	28 4 	
;; 30. 	(or
;;     (not
;;         (instance ?X0 sk527))
;;     (instance ?X0 sk528))	11 29 	
;; 31. 	(instance Creature50-1 sk528)	27 30 	
;; 32. 	(or
;;     (subclass sk528 sk529)
;;     (not
;;         (subclass Reptile Animal)))	1 	
;; 33. 	(subclass sk528 sk529)	32 4 	
;; 34. 	(or
;;     (not
;;         (instance ?X0 sk528))
;;     (instance ?X0 sk529))	11 33 	
;; 35. 	(instance Creature50-1 sk529)	31 34 	
;; 36. 	(or
;;     (subclass sk529 sk530)
;;     (not
;;         (subclass Reptile Animal)))	1 	
;; 37. 	(subclass sk529 sk530)	36 4 	
;; 38. 	(or
;;     (not
;;         (instance ?X0 sk529))
;;     (instance ?X0 sk530))	11 37 	
;; 39. 	(instance Creature50-1 sk530)	35 38 	
;; 40. 	(or
;;     (subclass sk530 sk531)
;;     (not
;;         (subclass Reptile Animal)))	1 	
;; 41. 	(subclass sk530 sk531)	40 4 	
;; 42. 	(or
;;     (not
;;         (instance ?X0 sk530))
;;     (instance ?X0 sk531))	11 41 	
;; 43. 	(instance Creature50-1 sk531)	39 42 	
;; 44. 	(or
;;     (subclass sk531 sk532)
;;     (not
;;         (subclass Reptile Animal)))	1 	
;; 45. 	(subclass sk531 sk532)	44 4 	
;; 46. 	(or
;;     (not
;;         (instance ?X0 sk531))
;;     (instance ?X0 sk532))	11 45 	
;; 47. 	(instance Creature50-1 sk532)	43 46 	
;; 48. 	(not
;;     (instance Creature50-1 Reptile))	[Negated Query]	
;; 49. 	(not
;;     (instance Creature50-1 Reptile))	48 	
;; 50. 	(or
;;     (subclass sk532 Reptile)
;;     (not
;;         (subclass Reptile Animal)))	1 	
;; 51. 	(subclass sk532 Reptile)	50 4 	
;; 52. 	(or
;;     (instance ?X0 Reptile)
;;     (not
;;         (instance ?X0 sk532)))	11 51 	
;; 53. 	True	47 49 52