Local Model Checking -calrification

Question

2021.08 paper Problem 4.a

Here in Node #4,5 and 6, I did not understand how we arrived at this solution on left side of Node 3.

I think it is supposed to be like below, please correct me if I am wrong.

in Node 3, s1 |- (c|b)->[]x

Node 4: s1 |- !(c | b)         (since !(c|b)-| []x causes a split in Node 3)

Node 5: s1 ⊬ !c & !b 

Node 5 should cause a split because of AND  operator? Node 6 will have s1 |-!c (Here s1 contains c so this will violate) and another Node will have s1 |-!b (Here s1 contains b so this will violate)? Although the final answer on satisfiability may be the same because of "OR" operator on Node 3, this will change however the solution on left side as compared to the solution shown in the answer sheet as Node 6 in answer sheet as s1 |- c.

Answer 1

I think your explanation is not right.

The tool can handle implications directly, but you may need to convert them first to the basic operations. If so, node 3: s1 ⊬ c|b -> []x1 will first become  s1 ⊬ !(c|b) | []x1 and will then split into 4: s1 ⊬!c|b and 7: s1 ⊬ []x1. To disprove the disjunctive goal in node 3, we have to disprove both goals 4 and 7. To disprove goal 4, we have to prove goal 5, and that is proved since c holds in s1.

Comments

I got your point, I just wanted to split and solve the "->" operator which at the end gives same answer as s1 ⊬ !c & !b. Thank you for you clarification