var2 W, Z, K, B;
var1 $;
pred Bl(var2 X, var1 t) = t in X <=> t+1 in X;
0 notin W & 0 notin Z & 0 notin K & 0 notin B;
$ in W & $ in Z & $ in K & $ in B;
all1 t:t<=$ =>
((t in W <=> t in Z) => (t in Z <=> t in B)) &
((t in K <=> t in Z) => (t in Z <=> t in B));
all1 t:t<$ =>
( Bl(W,t) & Bl(Z,t) & Bl(K,t) & Bl(B,t)) |
( Bl(W,t) & Bl(Z,t) & Bl(K,t) & ~Bl(B,t)) |
((t in W <=> t in B) &
~Bl(W,t) & Bl(Z,t) & Bl(K,t) & ~Bl(B,t)) |
((t in Z <=> t in B) &
Bl(W,t) & ~Bl(Z,t) & Bl(K,t) & ~Bl(B,t)) |
((t in K <=> t in B) &
Bl(W,t) & Bl(Z,t) & ~Bl(K,t) & ~Bl(B,t));