(on red green)
(above green blue)

;; These are here primarily to distinguish blocks from the table.
(block red)
(block green)
(block blue)
(not (block table))

;; Equality axioms, some general, some specific.
(all (?x) (= ?x ?x))
(all (?x ?y) (=> (not (= ?x ?y)) (not (= ?y ?x))))
(not (= table green))
(not (= table red))
(not (= table blue))
(not (= red green))
(not (= red blue))
(not (= green blue))

(all (?x ?y) (=> (and (block ?x)(block ?y) (on ?x ?y)) (not (exi (?z) (and (block ?z) (on ?z ?y) (not(= ?z ?x)))))))

;;(all (?x ?y)
;;     (=> (and (or (block ?x) (= ?x table)) (block ?y) (on ?y ?x))
;;	 (not (exi (?z) (and (Block ?z) (on ?y ?z)(not(= ?z ?x)))))))

(all (?x ?y ?z) (=> (and (on ?x ?y) (on ?x ?z)) (= ?x ?z)))

(not (exi (?z) (on table ?z)))
(all (?x ?y) (<=> (above ?x ?y) (or (on ?x ?y) (exi (?z) (and (on ?x ?z) (above ?z ?y))))))
(all (?x ?y) (=> (and (Block ?x) (Block ?y) (above ?x ?y)) (not (on ?x table))))
(all (?x ?y) (=> (on ?x ?y) (above ?x ?y)))
(all (?x ?y) (=> (on ?x ?y) (not (above ?y ?x))))
(all (?x ?y) (=> (on ?x ?y) (not (on ?y ?x))))
(all (?x) (not (on ?x ?x)))
(all (?x) (not (above ?x ?x)))