(defstep bflt3 (k &optional (a 1) (b 1) (c 1))
  (let ((casestr (format nil "a=~a AND b=~a AND c=~a" a b c)))
    (spread (case casestr)
	    ((then (flatten)(replaces (-1 -2 -3))(eval-formula -4))
	     (if (< c 3) ;; <---- NEED TO CHANGE SOMETHING HERE
		 (let ((nc (+ c 1)))
		   (bflt3 a b nc)) ;; <---- NEED TO CHANGE SOMETHING HERE
	       (if (< b 3) ;; <---- NEED TO CHANGE SOMETHING HERE
		   (let ((nb (+ b 1)))
		     (bflt3 a nb)) ;; <---- NEED TO CHANGE SOMETHING HERE
		 (if (< a 3) ;; <---- NEED TO CHANGE SOMETHING HERE
		     (let ((na (+ a 1)))
		       (bflt3 na)) ;; <---- NEED TO CHANGE SOMETHING HERE
		   (grind)))))))
  "Checks a^3+b^3 /= c^3 for 0 < a,b,c <= k"
  "Checking a^3+b^3 /= c^3 for 0 < a,b,c <= k")

 (defstep bfltn ()
   (then
    ;; ...
    )
   "Checks a^n+b^n /= c^n for 0 < a,b,c <= k"
   "Checking a^n+b^n /= c^n for 0 < a,b,c <= k")

(defstep quadratic ()
  (then
   ;; ...
   )
  "Checks if a quadratic polynomial has zeros"
  "Checking if a quadratic polynomial has zeros")