A1: Workoutstation(CW1)
A2: Workoutstation(CW2)
A3: Workoutstation(CW3)
A4: Workoutstation(CW4)
A5: ~Workoutstation(w245) v Equals(w245, CW1) v Equals(w245, CW2) v Equals(w245, CW3) v Equals(w245, 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(a247) v Equals(a247, CA1) v Equals(a247, 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(a254, w1253, s252) v ~On(a254, w2255, s252) v Equals(w1253, w2255)
A44: Workoutstation(F_20(a260, s259))
A45: On(a262, F_20(a262, s261), s261)
A46: ~Unconflicted(s270) v ~On(a1272, w271, s270) v ~On(a2273, w271, s270) v Equals(a1272, a2273)
A47: On(F_22(a2266, a1265, w264, s274), F_21(a2266, a1265, w264, s274), s274) v Unconflicted(s274)
A48: On(F_23(a2266, a1265, w264, s275), F_21(a2266, a1265, w264, s275), s275) v Unconflicted(s275)
A49: ~Equals(F_22(a2279, a1278, w277, s276), F_23(a2279, a1278, w277, s276)) v Unconflicted(s276)
A50: ~On(a285, w2284, CS2) v On(a285, F_24(w2284, a285), CS1)
A51: ~On(a287, w2286, CS2) v Connects(F_24(w2286, a287), w2286)
A52: ~On(a289, w2288, CS2) v Allowed(a289, F_24(w2288, a289), w2288)
A53: ~On(a291, w1290, CS1) v ~Connects(w1290, w2292) v ~Allowed(a291, w1290, w2292) v On(a291, w2292, CS2)
A54: ~Allowed(a1300, w1299, w2298) v Equals(w1299, w2298) v ~Athlete(a2301) v ~On(a2301, w2298, CS1)
A55: ~Equals(w1303, w2302) v Allowed(a1304, w1303, w2302)
A56: Athlete(F_25(a2308, w2307, w1306, a1305)) v Allowed(a1305, w1306, w2307)
A57: On(F_25(a2296, w2309, w1310, a1311), w2309, CS1) v Allowed(a1311, w1310, w2309)
A58: Unconflicted(CS1)
A59: On(CA1, CW2, CS1)
A60: On(CA2, CW3, CS1)
A61: Unconflicted(CS2)
S62: ~Connects(CW2, w2312) v ~Allowed(CA1, CW2, w2312) v On(CA1, w2312, CS2)      Res(53,59) {w1290/CW2, a291/CA1}
S63: ~Allowed(CA1, CW2, CW4) v On(CA1, CW4, CS2)      Res(62,32) {w2312/CW4}
S64: ~Connects(CW3, w2313) v ~Allowed(CA2, CW3, w2313) v On(CA2, w2313, CS2)      Res(53,60) {w1290/CW3, a291/CA2}
S65: ~Allowed(CA2, CW3, CW4) v On(CA2, CW4, CS2)      Res(64,30) {w2313/CW4}
S66: ~Allowed(a1353, CW2, CW4) v ~Athlete(a2354) v ~On(a2354, CW4, CS1)      Res(11,54) {w2298/CW4, w1299/CW2}
S67: ~Allowed(a1355, CW2, CW4) v ~On(CA1, CW4, CS1)      Res(66,22) {a2354/CA1}
S68: ~On(CA1, w2357, CS1) v Equals(CW2, w2357)      Res(43,59) {s252/CS1, a254/CA1, w1253/CW2}
S69: ~On(CA1, CW4, CS1) v ~Allowed(a1359, CW2, CW2) v ~On(CA1, CW2, CS1)      Para(67,68) {w2357/CW4}
S70: ~On(CA1, CW4, CS1) v ~Allowed(a1360, CW2, CW2)      Res(69,59) {}
S71: ~On(CA1, CW4, CS1)      Res(70,55) {a1360/a1304, w1303/CW2, w2302/CW2}
S72: ~Allowed(a1364, CW3, CW4) v ~Athlete(a2365) v ~On(a2365, CW4, CS1)      Res(14,54) {w2298/CW4, w1299/CW3}
S73: ~Allowed(a1366, CW3, CW4) v ~On(CA2, CW4, CS1)      Res(72,23) {a2365/CA2}
S74: ~On(CA2, w2367, CS1) v Equals(CW3, w2367)      Res(43,60) {s252/CS1, a254/CA2, w1253/CW3}
S75: ~On(CA2, CW4, CS1) v ~Allowed(a1368, CW3, CW3) v ~On(CA2, CW3, CS1)      Para(73,74) {w2367/CW4}
S76: ~On(CA2, CW4, CS1) v ~Allowed(a1369, CW3, CW3)      Res(75,60) {}
S77: ~On(CA2, CW4, CS1)      Res(76,55) {w1303/CW3, a1369/a1304, w2302/CW3}
S78: On(CA1, CW4, CS2) v Athlete(F_25(a2372, CW4, CW2, CA1))      Res(63,56) {w2307/CW4, a1305/CA1, w1306/CW2}
S79: On(CA1, CW4, CS2) v Equals(F_25(a2373, CW4, CW2, CA1), CA1) v Equals(F_25(a2373, CW4, CW2, CA1), CA2)      Res(78,26) {a247/F_25(a2372, CW4, CW2, CA1)}
S80: On(CA1, CW4, CS2) v On(F_25(a2374, CW4, CW2, CA1), CW4, CS1)      Res(63,57) {w1310/CW2, w2309/CW4, a1311/CA1}
S81: On(CA1, CW4, CS2) v Equals(F_25(a2379, CW4, CW2, CA1), CA2) v On(CA1, CW4, CS2) v On(CA1, CW4, CS1)      Para(79,80) {a2373/a2374}
S82: On(CA1, CW4, CS2) v Equals(F_25(a2380, CW4, CW2, CA1), CA2) v On(CA1, CW4, CS2)      Res(71,81) {}
S83: Equals(F_25(a21, CW4, CW2, CA1), CA2) v On(CA1, CW4, CS2)      Fact(82) {}
S84: On(CA1, CW4, CS2) v On(CA2, CW4, CS1) v Allowed(CA1, CW2, CW4)      Para(83,57) {w1310/CW2, a21/a2296, a1311/CA1, w2309/CW4}
S85: On(CA1, CW4, CS2) v Allowed(CA1, CW2, CW4)      Res(77,84) {}
S86: On(CA1, CW4, CS2) v On(CA1, CW4, CS2)      Res(63,85) {}
S87: On(CA1, CW4, CS2)      Fact(86) {}
S88: On(CA2, CW4, CS2) v Athlete(F_25(a22, CW4, CW3, CA2))      Res(65,56) {a1305/CA2, w2307/CW4, w1306/CW3}
S89: On(CA2, CW4, CS2) v Equals(F_25(a23, CW4, CW3, CA2), CA1) v Equals(F_25(a23, CW4, CW3, CA2), CA2)      Res(88,26) {a247/F_25(a22, CW4, CW3, CA2)}
S90: On(CA2, CW4, CS2) v On(F_25(a24, CW4, CW3, CA2), CW4, CS1)      Res(65,57) {w1310/CW3, a1311/CA2, w2309/CW4}
S91: On(CA2, CW4, CS2) v Equals(F_25(a25, CW4, CW3, CA2), CA2) v On(CA2, CW4, CS2) v On(CA1, CW4, CS1)      Para(89,90) {a23/a24}
S92: Equals(F_25(a26, CW4, CW3, CA2), CA2) v On(CA2, CW4, CS2) v On(CA1, CW4, CS1)      Fact(91) {}
S93: Equals(F_25(a27, CW4, CW3, CA2), CA2) v On(CA2, CW4, CS2)      Res(71,92) {}
S94: On(CA2, CW4, CS2) v On(CA2, CW4, CS1) v Allowed(CA2, CW3, CW4)      Para(93,57) {a27/a2296, w1310/CW3, a1311/CA2, w2309/CW4}
S95: On(CA2, CW4, CS2) v Allowed(CA2, CW3, CW4)      Res(77,94) {}
S96: On(CA2, CW4, CS2) v On(CA2, CW4, CS2)      Res(65,95) {}
S97: On(CA2, CW4, CS2)      Fact(96) {}
S98: ~Unconflicted(CS2) v ~On(a28, CW4, CS2) v Equals(CA1, a28)      Res(87,46) {w271/CW4, s270/CS2, a1272/CA1}
S99: ~Unconflicted(CS2) v Equals(CA1, CA2)      Res(97,98) {a28/CA2}
S100: ~Unconflicted(CS2)      Res(99,24) {}
S101: F      Res(100,61) {}