{ unsatisfiable }

(down x []<>x & -(<>[]p -> p))