The vertical column is the time, each line described the signal on a different variable or formula. So first step, we have b, second a, third a,c, and then repetitively b, followed by a, followed by a,c …

Somebody claims that two formulas are different. We call them q1 and q3, which q0, q2 being their subformulas.

[a SU b] means that we need to have be after finitely many steps. The way to there shall be covered by a in every step. The path starting from the first, fourth, (n*3+1)th position already starts in b, so [a SU b] is statisfied here. Steps 3,6,(n*3) satisfy a but not but b. Also that satisfies [a SU b] already as their successor satisfies b. Step 2, 5, (n*3)+2 satisfy a but not b. As their successor's successor satisfies b, and the step in between satisfies a, they satisfy [a SU b] as well.

That's why we write 111 111 … in the line of [a SU b]. Same thing for [q0 SU c]. We satisfy c at most after two steps. So from every step on [q0 SU c] is satisfied.

The signal traces in the line of q1 and q3 were obtained from the same input traces. As q1 and q3 differ, we know that the formulas are not equivalent.