Workoutstation(W1) ^ Workoutstation(W2) ^ Workoutstation(W3) ^ Workoutstation(W4) 
all w Workoutstation(w) -> Equals(w,W1) v Equals(w,W2) v Equals(w,W3) v Equals(w,W4)

~Equals(W1,W2)
~Equals(W1,W3)
~Equals(W1,W4)
~Equals(W2,W1)
~Equals(W2,W3)
~Equals(W2,W4)
~Equals(W3,W1)
~Equals(W3,W2)
~Equals(W3,W4)
~Equals(W4,W1)
~Equals(W4,W2)
~Equals(W4,W3)

Situation(S1) ^ Situation(S2) 
~Equals(S1,S2) ^ ~Equals(S2, S1)

Athlete(A1) ^ Athlete(A2)
~Equals(A1,A2) ^ ~Equals(A2, A1)
all a Athlete(a) -> Equals(a,A1) v Equals(a,A2)

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

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

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

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

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

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

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

Unconflicted(S1)

~(On(A1,W2,S1) ^ On(A2,W3,S1) -> ~Unconflicted(S2))