(note TQG3)  ;; boolean version

(time 400)

(instance Number3-1 NonnegativeRealNumber)

(query (not (instance Number3-1 NegativeRealNumber)))

(answer yes)


;; Answer 1. [yes]

;; 1. 	(instance Number3-1 NonnegativeRealNumber)	[KB]	
;; 2. 	(instance Number3-1 NonnegativeRealNumber)	1 	
;; 3. 	(=>
;;     (instance ?X157 NonnegativeRealNumber)
;;     (<=>
;;         (and
;;             (equal
;;                 (AbsoluteValueFn ?X155) ?X157)
;;             (instance ?X155 RealNumber)
;;             (instance ?X157 RealNumber))
;;         (or
;;             (and
;;                 (instance ?X155 NonnegativeRealNumber)
;;                 (equal ?X155 ?X157))
;;             (and
;;                 (instance ?X155 NegativeRealNumber)
;;                 (equal ?X157
;;                     (SubtractionFn 0 ?X155))))))	[KB]	
;; 4. 	(or
;;     (instance ?X0 RealNumber)
;;     (not
;;         (equal ?X1 ?X0))
;;     (not
;;         (instance ?X1 NonnegativeRealNumber))
;;     (not
;;         (instance ?X0 NonnegativeRealNumber)))	3 	
;; 5. 	(=>
;;     (instance ?X119 RealNumber)
;;     (=>
;;         (instance ?X119 NonnegativeRealNumber)
;;         (or
;;             (equal
;;                 (SignumFn ?X119) 1)
;;             (equal
;;                 (SignumFn ?X119) 0))))	[KB]	
;; 6. 	(or
;;     (equal
;;         (SignumFn ?X0) 0)
;;     (equal
;;         (SignumFn ?X0) 1)
;;     (not
;;         (instance ?X0 NonnegativeRealNumber))
;;     (not
;;         (instance ?X0 RealNumber)))	5 	
;; 7. 	(or
;;     (not
;;         (instance ?X0 NonnegativeRealNumber))
;;     (equal
;;         (SignumFn ?X0) 0)
;;     (equal
;;         (SignumFn ?X0) 1))	4 6 	
;; 8. 	(or
;;     (equal
;;         (SignumFn Number3-1) 0)
;;     (equal
;;         (SignumFn Number3-1) 1))	2 7 	
;; 9. 	(not
;;     (not
;;         (instance Number3-1 NegativeRealNumber)))	[Negated Query]	
;; 10. 	(instance Number3-1 NegativeRealNumber)	9 	
;; 11. 	(=>
;;     (instance ?X119 RealNumber)
;;     (=>
;;         (instance ?X119 NegativeRealNumber)
;;         (equal
;;             (SignumFn ?X119) -1)))	[KB]	
;; 12. 	(or
;;     (equal
;;         (SignumFn ?X0) -1)
;;     (not
;;         (instance ?X0 NegativeRealNumber))
;;     (not
;;         (instance ?X0 RealNumber)))	11 	
;; 13. 	(subclass NegativeRealNumber RealNumber)	[KB]	
;; 14. 	(subclass NegativeRealNumber RealNumber)	13 	
;; 15. 	(=>
;;     (subclass ?X403 ?X404)
;;     (and
;;         (instance ?X403 SetOrClass)
;;         (instance ?X404 SetOrClass)))	[KB]	
;; 16. 	(or
;;     (instance ?X1 SetOrClass)
;;     (not
;;         (subclass ?X0 ?X1)))	15 	
;; 17. 	(or
;;     (instance ?X0 SetOrClass)
;;     (not
;;         (subclass ?X0 ?X1)))	15 	
;; 18. 	(=>
;;     (and
;;         (instance ?X403 SetOrClass)
;;         (instance ?X404 SetOrClass))
;;     (=>
;;         (and
;;             (subclass ?X403 ?X404)
;;             (instance ?X405 ?X403))
;;         (instance ?X405 ?X404)))	[KB]	
;; 19. 	(or
;;     (instance ?X2 ?X1)
;;     (not
;;         (instance ?X2 ?X0))
;;     (not
;;         (subclass ?X0 ?X1))
;;     (not
;;         (instance ?X1 SetOrClass))
;;     (not
;;         (instance ?X0 SetOrClass)))	18 	
;; 20. 	(or
;;     (not
;;         (subclass ?X0 ?X1))
;;     (not
;;         (instance ?X2 ?X0))
;;     (instance ?X2 ?X1))	16 17 19 	
;; 21. 	(or
;;     (instance ?X0 RealNumber)
;;     (not
;;         (instance ?X0 NegativeRealNumber)))	14 20 	
;; 22. 	(or
;;     (not
;;         (instance ?X0 NegativeRealNumber))
;;     (equal
;;         (SignumFn ?X0) -1))	12 21 	
;; 23. 	(equal
;;     (SignumFn Number3-1) -1)	10 22 	
;; 24. 	True	8 23