With this change, the tableau rules for simplifying formula are applied iteratively until a fixpoint is reached.