So if you want to find a formula phi that does not satisfy some property (S3 in this example) you want to ensure that its negation does always hold, i.e. is valid. Thus, for a correct solution, our teaching tool should give you a "VALID" response when querying:

"phi -> !S3"

however querying "phi -> S3" and expecting a "NOT VALID" is not sufficient, as it it only states that there are cases where when having phi, S3 does not hold, while there may also still be cases where "phi -> S3" does in fact hold, which is not what you want to express as for those cases, your formula phi would actually satisfy the property S3. So again as a conclusion, if:

"phi -> !S3"

returns "VALID" as a result in our teaching tool, then you found a correct formula for the given requirements (at least if its not empty and also not equal to the other formula you need to find).