on(red,green)

!on(green, blue)

on(yellow,green) v on(yellow,blue)

above(green, blue)

on(blue,red) v on(blue, green) v on(blue,yellow) v on(blue,black)

all x ~on(x,x)

all x all y on(x,y) -> ~on(y,x)

all x all y all z on(x,z) ^ block(z) ^ ~Equals(x,y) -> ~on(y,z)

(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))