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

(Priority(A1, A2) ^ ~Priority(A2, A1) ^ (all a ~Priority(a, a))) ^

(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
  Blocked(a1, w1) <->
   (exists a2 exists w2
          (~Equals(a2, a1) ^ Priority(a2, a1) ^
           On(a2, w2, S1) ^ Connects(w2, w1)))) ^
           
(all a1 all w1 all w2 
   Allowed(a1,w1,w2) <-> 
      ((Equals(w1, w2)  ^ (all w3 (Connects(w1, w3) -> Blocked(a1, w3)))) v
       (~Equals(w1, w2) ^ ~(Blocked(a1, 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)))))) ^

(On(A1, W2, S1) ^ (On(A2, W3, S1)))