------------------- CASE 1 -------------------
Condition:
  Green list: [ 2 * Y1 * Y2 * S2 + 2 * R2 * S2^2 + 2 * S2 * A^2 - 3 * Y1 * Y2 - Y2^2 - 8 * R2 * S2 - 4 * S2^2 - 4 * A^2 + 8 * R2 + 14 * S2 - 12, 2 * Y1^2 * S2 - 2 * R2^2 * S2 + 2 * S2 * A^2 - 3 * Y1^2 - Y1 * Y2 + 4 * R2^2 + 4 * R2 * S2 - 4 * A^2 - 8 * R2 - 2 * S2 + 4, 2 * X2 * R2 - R2 * A - S2 * A - X1 - 3 * X2 + 4 * A, Y1 * A^2 - Y2 * A^2 - 2 * Y1 * S2 + 3 * Y1 + Y2, X2^2 + Y2^2 - S2^2 + A^2 + 2 * S2 - 2, X1^2 + Y1^2 - R2^2 + A^2 + 2 * R2 - 2, R1 + R2 - 2, S1 + S2 - 2, Y1 * X2 - X1 * Y2 - Y1 * A + Y2 * A, A^2 * U - U + 2, X2 * A - S2 + 1, X1 * A - R2 + 1, Y2^2 * A - S2^2 * A + A^3 + X2 * S2 + 2 * S2 * A - X2 - 2 * A, Y1^2 * A - R2^2 * A + A^3 + X1 * R2 + 2 * R2 * A - X1 - 2 * A, S2 * A * U - X2 * U - A * U + 2 * X2, R2 * A * U - X1 * U - A * U + 2 * X1, Y2^2 * U - 2 * Y2^2 + 2 * S2^2 - 2 * A^2 - 4 * S2 + 2, Y1^2 * U - 2 * Y1^2 + 2 * R2^2 - 2 * A^2 - 4 * R2 + 2, R2 * A^2 + S2 * A^2 - 2 * R2 * S2 - 4 * A^2 + 3 * R2 + 3 * S2 - 4, R2 * S2 * U - 2 * R2 * U - 2 * S2 * U + R2 + S2 + 4 * U - 4, 2 * X1 * S2 - R2 * A - S2 * A - 3 * X1 - X2 + 4 * A, Y2 * R2 + Y1 * S2 - 2 * Y1 - 2 * Y2, Y1 * S2 * U - 2 * Y1 * U + Y1 - Y2, X1 * Y2 * U - Y2 * A * U - 2 * X1 * Y2 - Y1 * A + Y2 * A, X1 * X2 + Y1 * Y2 + R2 * S2 + A^2 - 3 * R2 - 3 * S2 + 6, Y1 * Y2 * U - 2 * Y1 * Y2 - 2 * R2 * S2 - 2 * A^2 + 4 * R2 + 4 * S2 - 6, 2 * Y1 * Y2 * A + 2 * R2 * S2 * A + 2 * A^3 - 5 * R2 * A - 5 * S2 * A + X1 + X2 + 8 * A ]
  Red list: [ A, X1 - X2 ]
 Basis: [ ]
Finished loading klee3.lisp
T