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

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

(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 exists w3
          (~Equals(a2, a1) ^ On(a2, w3, S1) ^ Connects(w3, w2))))) ^

(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))) ^

(Deadlocked(S1) <->
  (all a exists w1
    (On(a, w1, S1) ^
     (all w2 ((Connects(w1, w2) ^
              Allowed(a, w1, w2)) -> Equals(w1, w2)))))) ^

(Deadlocked(S1))