In reply to nnn314:
Yes exactly so seems like every evaluation point a new thread is spawn waiting for the fulfilling condition to be verified. That is the reason why by reducing the time you check the property then you experienced a profomance improvement compared to the first time. Probably if you run formal with just that property being checked i would guess you will see the resources kind of reaching the limit you set almost after fee cycles due to the amount of threads spawned waiting to be true.
Someone who knows formal tool more in depth then me could comment better on it.