A1: Workoutstation(CW1)
A2: Workoutstation(CW2)
A3: Workoutstation(CW3)
A4: Workoutstation(CW4)
A5: ~Workoutstation(w82) v Equals(w82, CW1) v Equals(w82, CW2) v Equals(w82, CW3) v Equals(w82, CW4)
A6: ~Equals(CW1, CW2)
A7: ~Equals(CW1, CW3)
A8: ~Equals(CW1, CW4)
A9: ~Equals(CW2, CW1)
A10: ~Equals(CW2, CW3)
A11: ~Equals(CW2, CW4)
A12: ~Equals(CW3, CW1)
A13: ~Equals(CW3, CW2)
A14: ~Equals(CW3, CW4)
A15: ~Equals(CW4, CW1)
A16: ~Equals(CW4, CW2)
A17: ~Equals(CW4, CW3)
A18: Situation(CS1)
A19: Situation(CS2)
A20: ~Equals(CS1, CS2)
A21: ~Equals(CS2, CS1)
A22: Athlete(CA1)
A23: Athlete(CA2)
A24: ~Equals(CA1, CA2)
A25: ~Equals(CA2, CA1)
A26: ~Athlete(a84) v Equals(a84, CA1) v Equals(a84, CA2)
A27: Connects(CW1, CW2)
A28: Connects(CW3, CW2)
A29: Connects(CW1, CW3)
A30: Connects(CW3, CW4)
A31: Connects(CW2, CW3)
A32: Connects(CW2, CW4)
A33: Connects(CW1, CW1)
A34: Connects(CW2, CW2)
A35: Connects(CW3, CW3)
A36: Connects(CW4, CW4)
A37: ~Connects(CW2, CW1)
A38: ~Connects(CW4, CW2)
A39: ~Connects(CW3, CW1)
A40: ~Connects(CW1, CW4)
A41: ~Connects(CW4, CW3)
A42: ~Connects(CW4, CW1)
A43: ~On(a91, w190, s89) v ~On(a91, w292, s89) v Equals(w190, w292)
A44: Workoutstation(F_2(a97, s96))
A45: On(a99, F_2(a99, s98), s98)
A46: ~Unconflicted(s107) v ~On(a1109, w108, s107) v ~On(a2110, w108, s107) v Equals(a1109, a2110)
A47: On(F_4(a2103, a1102, w101, s111), F_3(a2103, a1102, w101, s111), s111) v Unconflicted(s111)
A48: On(F_5(a2103, a1102, w101, s112), F_3(a2103, a1102, w101, s112), s112) v Unconflicted(s112)
A49: ~Equals(F_4(a2116, a1115, w114, s113), F_5(a2116, a1115, w114, s113)) v Unconflicted(s113)
A50: ~On(a121, w2120, CS2) v On(a121, F_6(w2120, a121), CS1)
A51: ~On(a123, w2122, CS2) v Connects(F_6(w2122, a123), w2122)
A52: ~On(a125, w2124, CS2) v Allowed(a125, F_6(w2124, a125), w2124)
A53: ~Allowed(a1133, w1132, w2131) v Equals(w1132, w2131) v ~Athlete(a2134) v ~On(a2134, w2131, CS1)
A54: ~Equals(w1136, w2135) v Allowed(a1137, w1136, w2135)
A55: Athlete(F_7(a2141, w2140, w1139, a1138)) v Allowed(a1138, w1139, w2140)
A56: On(F_7(a2129, w2142, w1143, a1144), w2142, CS1) v Allowed(a1144, w1143, w2142)
A57: Unconflicted(CS1)
A58: On(CA1, CW2, CS1)
A59: On(CA2, CW3, CS1)
A60: ~Allowed(CA1, CW2, CW4)
S61: ~On(CA1, w1145, CS1) v Equals(w1145, CW2)      Res(43,58) {s89/CS1, w292/CW2, a91/CA1}
S62: ~On(CA2, w1146, CS1) v Equals(w1146, CW3)      Res(43,59) {s89/CS1, w292/CW3, a91/CA2}
S63: ~On(CA1, CW4, CS1)      Res(61,16) {w1145/CW4}
S64: ~On(CA2, CW4, CS1)      Res(62,17) {w1146/CW4}
S65: On(F_7(a2147, CW4, CW2, CA1), CW4, CS1)      Res(56,60) {w2142/CW4, a1144/CA1, w1143/CW2}
S66: Athlete(F_7(a2148, CW4, CW2, CA1))      Res(55,60) {w2140/CW4, w1139/CW2, a1138/CA1}
S67: Equals(F_7(a2149, CW4, CW2, CA1), CA1) v Equals(F_7(a2149, CW4, CW2, CA1), CA2)      Res(66,26) {a84/F_7(a2148, CW4, CW2, CA1)}
S68: Equals(F_7(a2151, CW4, CW2, CA1), CA2) v On(CA1, CW4, CS1)      Para(65,67) {a2149/a2147}
S69: On(CA1, CW4, CS1) v On(CA2, CW4, CS1)      Para(65,68) {a2151/a2147}
S70: On(CA2, CW4, CS1)      Res(63,69) {}
S71: F      Res(64,70) {}