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