Very tricky. For your formulas phi1 and phi2, we can check that they are satisfiable, they are not equivalent and both imply !S1&S2. So, what is wrong here?

Read carefully the exercise problem. The formulas should satisfy

phi[i] -> !S1&S2

but that should be strict, i.e., the formulas should **not** satisfy

phi[i] <-> !S1&S2

However, this is the case with your formula phi2.