A1: ~Equals(CA, CB)
A2: ~Equals(CA, CC)
A3: ~Equals(CB, CA)
A4: ~Equals(CB, CC)
A5: ~Equals(CC, CA)
A6: ~Equals(CC, CB)
A7: ~Equals(CA, CTable)
A8: ~Equals(CB, CTable)
A9: ~Equals(CC, CTable)
A10: Block(CA)
A11: Block(CB)
A12: Block(CC)
A13: ~Block(CTable)
A14: ~On(x7, y6, s5) v ~On(x7, z8, s5) v Equals(y6, z8)
A15: ~On(x15, z14, s13) v ~On(y16, z14, s13) v Equals(x15, y16) v Equals(z14, CTable)
A16: ~Clear(x22, s21) v ~Block(y23) v ~On(y23, x22, s21) v Equals(x22, CTable)
A17: Block(F_1(y26, x25, s24)) v Clear(x25, s24)
A18: On(F_1(y19, x28, s27), x28, s27) v Clear(x28, s27)
A19: ~Equals(x29, CTable) v Clear(x29, s30)
A20: ~Clear(x36, s35) v ~Clear(y37, s35) v ~On(x36, z38, s35) v On(x36, y37, result(move(x36, y37), s35))
A21: ~Clear(x40, s39) v ~Clear(y41, s39) v ~On(x40, z42, s39) v Clear(z42, result(move(x40, y41), s39))
A22: ~On(x50, y49, s48) v Equals(x50, z51) v On(x50, y49, result(move(z51, w47), s48))
A23: ~Clear(x57, s56) v Equals(x57, z58) v Clear(x57, result(move(y59, z58), s56))
A24: On(CA, CTable, CS0)
A25: On(CC, CB, CS0)
A26: On(CB, CTable, CS0)
A27: Clear(CC, CS0)
A28: Clear(CA, CS0)
A29: Clear(CTable, s61)
A30: ~On(CA, CB, s63) v Answer(s63)
S31: ~Clear(y67, CS0) v ~On(CC, z68, CS0) v Clear(z68, result(move(CC, y67), CS0))      Res(21,27) {s39/CS0, x40/CC}
S32: ~On(CC, z69, CS0) v Clear(z69, result(move(CC, CTable), CS0))      Res(31,29) {s61/CS0, y67/CTable}
S33: Clear(CB, result(move(CC, CTable), CS0))      Res(32,25) {z69/CB}
S34: ~Clear(x70, result(move(CC, CTable), CS0)) v ~On(x70, z71, result(move(CC, CTable), CS0)) v On(x70, CB, result(move(x70, CB), result(move(CC, CTable), CS0)))      Res(33,20) {y37/CB, s35/result(move(CC, CTable), CS0)}
S35: ~Clear(CA, result(move(CC, CTable), CS0)) v ~On(CA, z72, result(move(CC, CTable), CS0)) v Answer(result(move(CA, CB), result(move(CC, CTable), CS0)))      Res(34,30) {s63/result(move(x70, CB), result(move(CC, CTable), CS0)), x70/CA}
S36: ~Clear(CA, s73) v Clear(CA, result(move(y74, CTable), s73))      Res(7,23) {z58/CTable, x57/CA}
S37: ~On(CA, z75, result(move(CC, CTable), CS0)) v Answer(result(move(CA, CB), result(move(CC, CTable), CS0))) v ~Clear(CA, CS0)      Res(35,36) {y74/CC, s73/CS0}
S38: ~On(CA, z76, result(move(CC, CTable), CS0)) v Answer(result(move(CA, CB), result(move(CC, CTable), CS0)))      Res(37,28) {}
S39: ~On(CA, y78, s77) v On(CA, y78, result(move(CC, w79), s77))      Res(2,22) {x50/CA, z51/CC}
S40: On(CA, CTable, result(move(CC, w80), CS0))      Res(39,24) {s77/CS0, y78/CTable}
S41: Answer(result(move(CA, CB), result(move(CC, CTable), CS0)))      Res(38,40) {w80/CTable, z76/CTable}