First of all: The message you got does not mean that you are wrong, it just means that you have not submitted the solution the teaching tool has computed, and therefore it may or may not be correct (a tutor has to check this manually to decide whether to give you the points).

So, let me check that here: The initial checks are not conclusive as you found out and that is true. From here, many ways are possible, and our student portal does currently not check all possible correct results.

So, you started with with the initial states ψ[0] (where you added the clauses of Phi) and the safety property ψ[1]=Phi:

ψ[0] = {s1,s5} = a & !b = CNF{!b; a; a|b|!c}
ψ[1] = {s0,s1,s2,s3,s5,s6,s7} = a|b|!c = CNF{a|b|!c}

That is okay (the teaching tool starts differently). Now you check for CTIs, by checking whether ψ[1]->[]Phi is valid, but it is not valid and you get the counterexample s6->s4 since s6 is in ψ[1] but has as successor s4 which is not in Phi.

So, you need to check reachability of s6 within one step, and you therefore check ψ[0] & !ψ[s6] -> []!ψ[s6] which is true since the initial states ψ[0] cannot reach s6. So, we can remove s6 from ψ[1] which could be done by adding the clause !ψ[s6] = !(!a&b&c) = a|!b|!c.

Maybe we can add a generalized clause, i.e., a subset of {a,!b,!c}? To find out, we have to check for all subsets C of {a,!b,!c} whether (1) ψ[0]&C->[]C and (2) Init->C holds.

Here I don't understand your solution, since you could have generalized the clause, but at the end, you did not (which is also correct, since clause generalization is a matter of optimization).

Hence, you added the clause {a,!b,!c} of !ψ[s6] to the assertions and got now

ψ[0] = {s1,s5} = CNF{a|b|!c; a|!b|!c; !b; a; }
ψ[1] = {s0,s1,s2,s3,s5,s7} = CNF{a|b|!c; a|!b|!c}

which is what you can do. As there is not yet a fixpoint, you continue by checking for CTIs again, and check whether ψ[1]->[]Phi is valid. This time, it is valid, so we have to extend the sequence of assertions, and you add ψ[1] = Phi and got

ψ[0] = {s1,s5} = CNF{!b; a; a|b|!c; a|!b|!c}
ψ[1] = {s0,s1,s2,s3,s5,s7} = CNF{a|b|!c; a|!b|!c}
ψ[2] = {s0,s1,s2,s3,s5,s6,s7} = CNF{a|b|!c}

Next, you try to propagate clauses, and you find that our added clause a|!b|!c can be propagated from ψ[1] to ψ[2] which yields a fixpoint.

Yeap, that is a valid PDR computation, I would say. Write your tutor that you should get your points. I just don't understand why you tried the clause generalization and dropped it, but still it is correct.