( 
  (GIVEN w x y z) 
    (= w2 (sqr w))
    (= x2 (sqr x))
    (= y2 (sqr y))
    (= z2 (sqr z))
    (= t (sqr (- (- (- (- (* 6 (* w y)) (* 12 w2)) x2) y2) z2)))
    (= r (- (* (* 16 w2) (+ x2 y2)) t))
  (RETURN r)
)