;; The given facts.
(on red green)
(not (on green blue))
(or (on yellow green) (on yellow blue))
(above green blue)
;; Blue is on SOME block, but made specific to this world.
(or (on blue red) (on blue green) (on blue yellow) (on blue black))

;; On properties
;; Anti-reflexive
(all (?x) (not (on ?x ?x)))
;; Anti-symmetric
(all (?x ?y) (=> (on ?x ?y) (not (on ?y ?x))))
;; Only one block fits on top of another block
(all (?x ?y ?z) (=> (and (on ?x ?z) (block ?z) (not (= ?x ?y))) (not (on ?y ?z))))
;; A block is on only one block or table
(all (?x ?y ?z) (=> (and (on ?x ?y) (not (= ?y ?z))) (not (on ?x ?z))))
;; The table is special, it can't be on anything.
(all (?x) (not (on table ?x)))

;; Above properties
;; Base case in recursive definition
(all (?x ?y) (=> (on ?x ?y) (above ?x ?y)))
;; Recursive case (transitive)
(all (?x ?y ?z) (=> (and (above ?x ?y) (above ?y ?z)) (above ?x ?z)))
;; Anti-reflexive
(all (?x) (not (above ?x ?x)))
;; Anti-symmetric
(all (?x ?y) (=> (above ?x ?y) (not (above ?y ?x))))
;; This enables one of the key deductions in proving (on green yellow).
(all (?x ?y) (=> (and (above ?x ?y) (block ?y)) (not (on ?x table))))

;; Closed World version of every block is on something (and not
;; itself).  Note that the support for red, blue and yellow was
;; explicitely constrained in the input statements but green is only
;; indirectly constraints and black is not constrained at all.
(or (on green red) (on green blue) (on green yellow) (on green black)
    (on green table))
(or (on black red) (on black blue) (on black yellow) (on black green)
    (on black table))

;; These are here primarily to distinguish blocks from the table.
(block red)
(block green)
(block blue)
(block yellow)
(block black)
(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 yellow))
(not (= table blue))
(not (= table black))
(not (= red green))
(not (= red blue))
(not (= red yellow))
(not (= red black))
(not (= green blue))
(not (= green yellow))
(not (= green black))
(not (= blue yellow))
(not (= blue black))
(not (= yellow black))