The translation of G [b SW a] yields the following LO1 formula:

∀t1. (t0≤t1 → (∃t0. t1≤t0 ∧ (∀t2. (t1≤t2 ∧ t2<t0 → ¬a[t2])) ∧ b[t0] ∧ a[t0]))

We may use fresh variables for all quantified variables:

∀t1. (t0≤t1 → (∃t3. t1≤t3 ∧ (∀t2. (t1≤t2 ∧ t2<t3 → ¬a[t2])) ∧ b[t3] ∧ a[t3]))

replace t0 with 0

∀t1. (0≤t1 → (∃t3. t1≤t3 ∧ (∀t2. (t1≤t2 ∧ t2<t3 → ¬a[t2])) ∧ b[t3] ∧ a[t3]))

replace t1 with t0

∀t0. (0≤t0 → (∃t3. t0≤t3 ∧ (∀t2. (t0≤t2 ∧ t2<t3 → ¬a[t2])) ∧ b[t3] ∧ a[t3]))

replace t3 with t1

∀t0. (0≤t0 → (∃t1. t0≤t1 ∧ (∀t2. (t0≤t2 ∧ t2<t1 → ¬a[t2])) ∧ b[t1] ∧ a[t1]))