Extension by rule #1, Skolem constant sk_0 introduced. Next applicable rule #2 (with binding X=sk_0) will produce a 3-way split.
