for all x: sat (counterexample is nan: True )   for x that is not nan: unsat
