(Connects(W1, W2) ^ 
 Connects(W1, W3) ^
 Connects(W2, W3) ^
 Connects(W3, W2) ^
 Connects(W2, W4) ^
 Connects(W3, W4) ^
 (all w Connects(w,w))) ^

(~Connects(W1, W4) ^ ~Connects(W2, W1) ^ ~Connects(W3, W1) ^
 ~Connects(W4, W2)  ^ ~Connects(W4, W3) ^ ~Connects(W4, W1)) ^

(all s 
  (Unconflicted(s) <-> 
    (all w all a1 all a2 (On(a1,w,s) ^ 
                          On(a2,w,s) -> Equals(a1,a2))))) ^

(Unconflicted(S1)) ^

(all a all w2 
  (On(a,w2, S2) -> 
    (exists w1 
      (On(a,w1,S1) ^ Connects(w1,w2) ^ Allowed(a,w1,w2))))) ^

(all a1 all w1 all w2 
   Allowed(a1,w1,w2) <-> 
      (Equals(w1, w2) v ~(exists a2 On(a2,w2,S1)))) ^

(all a all s exists w
   On(a, w, s)) ^

(all s all a all w1 all w2
  ((On(a, w1, s) ^ On(a, w2, s)) -> Equals(w1, w2)))