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

(~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 w ~Connects(w,w))) ^

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