source: CGBLisp/examples/klee.result@ 1

Last change on this file since 1 was 1, checked in by Marek Rychlik, 15 years ago

First import of a version circa 1997.
File size: 38.6 KB
Line 
1------------------- CASE 1 -------------------
2Condition:
3 Green list: [ U * A^2 - U + 2 ]
4 Red list: [ U - 4, U, A ]
5 Basis: [ ( - 1) * X1^2 + ( - 1) * Y1^2 + (1) * R2^2 + ( - 2) * R2 + (1), (1) * R1 + (1) * R2 + ( - 1), ( - 1) * X2^2 + ( - 1) * Y2^2 + (1) * S2^2 + ( - 2) * S2 + (1), (1) * S1 + (1) * S2 + ( - 1), ( - 1) * Y1 * X2 + (1) * X1 * Y2, ( - 2) * Y2 * A + (1) * A^2 + ( - 2) * S2 + (1), ( - 2) * Y1 * A + (1) * A^2 + ( - 2) * R2 + (1), (U) * R2 * S2 * V + ( - U + 1) * R2 * V + ( - U + 1) * S2 * V + (U - 2) * V + (1), ( - 4) * Y2 * R2 + (2) * A * R2 + (4) * Y1 * S2 + ( - 2) * A * S2 + ( - 2) * Y1 + (2) * Y2, (1) * X1 * A^2 + ( - 1) * X2 * A^2 + (2) * X2 * R2 + ( - 2) * X1 * S2 + (1) * X1 + ( - 1) * X2, ( - 1) * X1 * X2 * Y2 + ( - 1) * Y1 * Y2^2 + (1) * Y1 * S2^2 + ( - 2) * Y1 * S2 + (1) * Y1, ( - 4 * U) * Y1 * S2^2 * V + (2 * U) * A * S2^2 * V + (6 * U - 4) * Y1 * S2 * V + (2 * U - 4) * Y2 * S2 * V + ( - 4 * U + 4) * A * S2 * V + ( - 2 * U + 2) * Y1 * V + ( - 2 * U + 6) * Y2 * V + (2 * U - 4) * A * V + ( - 4) * Y2 + (2) * A, (4) * A^2 * R2^2 + ( - 4) * A^2 * S2^2 + ( - 8) * A^2 * R2 + (16) * Y1^2 * S2 + ( - 16) * Y1 * Y2 * S2 + (8) * A^2 * S2 + ( - 16) * R2^2 * S2 + (16) * R2 * S2^2 + ( - 12) * Y1^2 + (8) * Y1 * Y2 + (4) * Y2^2 + (8) * R2^2 + (8) * R2 * S2 + ( - 16) * S2^2 + ( - 8) * R2 + (8) * S2, ( - 8) * X1 * X2 * R2 + ( - 2) * A^2 * R2 + (8) * Y1^2 * S2 + (8) * X1 * X2 * S2 + ( - 8) * Y1 * Y2 * S2 + (2) * A^2 * S2 + ( - 8) * R2^2 * S2 + (8) * R2 * S2^2 + ( - 8) * Y1^2 + (4) * Y1 * Y2 + (4) * Y2^2 + (8) * R2^2 + (4) * R2 * S2 + ( - 12) * S2^2 + ( - 10) * R2 + (10) * S2, ( - 32) * Y1^2 * Y2 * S2 + (32) * Y1 * Y2^2 * S2 + (8) * A * R2^2 * S2 + (32) * Y1 * R2 * S2^2 + ( - 16) * A * R2 * S2^2 + ( - 32) * Y1 * S2^3 + (8) * A * S2^3 + (24) * Y1^2 * Y2 + ( - 16) * Y1 * Y2^2 + ( - 8) * Y2^3 + ( - 4) * A * R2^2 + ( - 48) * Y1 * R2 * S2 + (32) * Y1 * S2^2 + (16) * Y2 * S2^2 + (4) * A * S2^2 + (20) * Y1 * R2 + (6) * A * R2 + ( - 20) * Y2 * S2 + ( - 6) * A * S2 + ( - 6) * Y1 + (6) * Y2, (16) * X1 * Y1 * Y2 * S2 + ( - 16) * X1 * Y2^2 * S2 + ( - 8) * X2 * R2^2 * S2 + ( - 8) * X1 * R2 * S2^2 + (8) * X2 * R2 * S2^2 + (8) * X1 * S2^3 + ( - 12) * X1 * Y1 * Y2 + (8) * X1 * Y2^2 + (4) * X2 * Y2^2 + (4) * X2 * R2^2 + (16) * X1 * R2 * S2 + (8) * X2 * R2 * S2 + ( - 16) * X1 * S2^2 + ( - 12) * X2 * S2^2 + ( - 8) * X1 * R2 + ( - 8) * X2 * R2 + (8) * X1 * S2 + (8) * X2 * S2, (8) * A * R2^3 + ( - 32) * Y1^3 * S2 + (32) * Y1 * Y2^2 * S2 + (32) * Y1 * R2^2 * S2 + ( - 8) * A * R2^2 * S2 + ( - 8) * A * R2 * S2^2 + ( - 32) * Y1 * S2^3 + (8) * A * S2^3 + (24) * Y1^3 + (8) * Y1^2 * Y2 + ( - 24) * Y1 * Y2^2 + ( - 8) * Y2^3 + ( - 16) * Y1 * R2^2 + ( - 16) * A * R2^2 + ( - 80) * Y1 * R2 * S2 + (24) * A * R2 * S2 + (80) * Y1 * S2^2 + (16) * Y2 * S2^2 + ( - 8) * A * S2^2 + (48) * Y1 * R2 + (8) * A * R2 + ( - 24) * Y1 * S2 + ( - 24) * Y2 * S2 + ( - 8) * A * S2 + ( - 8) * Y1 + (8) * Y2, ( - 8) * X2 * R2^3 + (16) * X1 * Y1^2 * S2 + ( - 16) * X1 * Y2^2 * S2 + ( - 8) * X1 * R2^2 * S2 + (8) * X2 * R2 * S2^2 + (8) * X1 * S2^3 + ( - 12) * X1 * Y1^2 + ( - 4) * X1 * Y1 * Y2 + (12) * X1 * Y2^2 + (4) * X2 * Y2^2 + (4) * X1 * R2^2 + (20) * X2 * R2^2 + (24) * X1 * R2 * S2 + ( - 8) * X2 * R2 * S2 + ( - 28) * X1 * S2^2 + ( - 12) * X2 * S2^2 + ( - 16) * X1 * R2 + ( - 16) * X2 * R2 + (16) * X1 * S2 + (16) * X2 * S2, (4) * X2 * A * R2^2 + (4) * X1 * A * R2 * S2 + ( - 4) * X2 * A * R2 * S2 + ( - 4) * X1 * A * S2^2 + ( - 2) * X1 * A * R2 + ( - 6) * X2 * A * R2 + (8) * X1 * Y1 * S2 + ( - 8) * X1 * Y2 * S2 + (2) * X1 * A * S2 + (6) * X2 * A * S2 + ( - 6) * X1 * Y1 + (4) * X1 * Y2 + (2) * X2 * Y2, (4 * U) * X1 * Y2 * S2^2 * V + ( - 2 * U) * X2 * A * S2^2 * V + ( - 6 * U + 4) * X1 * Y2 * S2 * V + ( - 2 * U + 4) * X2 * Y2 * S2 * V + (4 * U - 4) * X2 * A * S2 * V + (2 * U - 2) * X1 * Y2 * V + (2 * U - 6) * X2 * Y2 * V + ( - 2 * U + 4) * X2 * A * V + (4) * X2 * Y2 + ( - 2) * X2 * A, ( - 8 * U^3) * X1 * X2 * S2^2 * V + ( - 2 * U^3) * A^2 * S2^2 * V + (4 * U^3) * Y1^2 * S2 * V + (16 * U^3 - 16 * U^2) * X1 * X2 * S2 * V + ( - 4 * U^3 + 8 * U^2) * Y1 * Y2 * S2 * V + ( - 8 * U^2) * Y2^2 * S2 * V + (4 * U^3 - 4 * U^2) * A^2 * S2 * V + (8 * U^2) * S2^3 * V + ( - 4 * U^3 + 4 * U^2) * Y1^2 * V + ( - 8 * U^3 + 16 * U^2) * X1 * X2 * V + (4 * U^3 - 12 * U^2) * Y1 * Y2 * V + (8 * U^2) * Y2^2 * V + ( - 2 * U^3 + 4 * U^2) * A^2 * V + (2 * U^3 - 28 * U^2 + 8 * U) * S2^2 * V + ( - 8 * U^2) * X1 * X2 + (8 * U^2) * Y1 * Y2 + ( - 8 * U^2) * Y2^2 + ( - 2 * U^2) * A^2 + ( - 8 * U^2) * R2 * S2 + (8 * U^2) * S2^2 + ( - 4 * U - 8) * R2 * V + ( - 4 * U^3 + 36 * U^2 - 20 * U - 8) * S2 * V + (12 * U^2) * R2 + ( - 12 * U^2 + 8 * U) * S2 + (2 * U^3 - 16 * U^2 + 16 * U + 16) * V + (2 * U^2 - 12 * U - 8), (64) * Y1^4 * S2 + ( - 64) * Y1 * Y2^3 * S2 + ( - 64) * Y1^2 * R2^2 * S2 + (64) * Y1 * Y2 * S2^3 + ( - 48) * Y1^4 + ( - 16) * Y1^3 * Y2 + (48) * Y1 * Y2^3 + (16) * Y2^4 + (32) * Y1^2 * R2^2 + (16) * R2^4 + (192) * Y1^2 * R2 * S2 + (8) * A^2 * R2 * S2 + ( - 48) * R2^3 * S2 + ( - 64) * Y1^2 * S2^2 + ( - 128) * Y1 * Y2 * S2^2 + ( - 32) * Y2^2 * S2^2 + ( - 8) * A^2 * S2^2 + (64) * R2^2 * S2^2 + ( - 48) * R2 * S2^3 + (16) * S2^4 + ( - 120) * Y1^2 * R2 + ( - 10) * A^2 * R2 + ( - 24) * R2^3 + ( - 24) * Y1^2 * S2 + (104) * Y1 * Y2 * S2 + (40) * Y2^2 * S2 + (10) * A^2 * S2 + (40) * R2^2 * S2 + ( - 24) * R2 * S2^2 + (8) * S2^3 + (40) * Y1^2 + ( - 28) * Y1 * Y2 + ( - 12) * Y2^2 + (24) * R2^2 + ( - 20) * R2 * S2 + ( - 4) * S2^2 + ( - 10) * R2 + (10) * S2, ( - 32 * U^3) * A * S2^4 * V + ( - 32 * U^3 + 128 * U^2) * Y1 * Y2^2 * S2 * V + (32 * U^3 - 128 * U^2) * Y2^3 * S2 * V + ( - 64 * U^3 + 128 * U^2) * Y2 * S2^3 * V + (136 * U^3 - 96 * U^2) * A * S2^3 * V + ( - 8 * U^3 + 32 * U^2) * Y1^2 * Y2 * V + (48 * U^3 - 192 * U^2) * Y1 * Y2^2 * V + ( - 40 * U^3 + 160 * U^2) * Y2^3 * V + (4 * U^3 - 8 * U^2) * A * R2^2 * V + (208 * U^3 - 544 * U^2 + 128 * U) * Y2 * S2^2 * V + ( - 220 * U^3 + 320 * U^2 - 32 * U) * A * S2^2 * V + (128 * U^2) * Y1 * Y2^2 + ( - 128 * U^2) * Y2^3 + ( - 32 * U^2) * A * R2 * S2 + ( - 128 * U^2) * Y1 * S2^2 + (128 * U^2) * Y2 * S2^2 + (4 * U^3 - 16 * U^2 + 32 * U) * Y1 * R2 * V + ( - 10 * U^3 + 32 * U^2 - 24 * U - 32) * A * R2 * V + ( - 32 * U - 128) * Y1 * S2 * V + ( - 228 * U^3 + 752 * U^2 - 320 * U - 128) * Y2 * S2 * V + (162 * U^3 - 368 * U^2 + 104 * U + 96) * A * S2 * V + (40 * U^2) * A * R2 + (224 * U^2) * Y1 * S2 + ( - 288 * U^2 + 128 * U) * Y2 * S2 + (32 * U^2 - 32 * U) * A * S2 + ( - 6 * U^3 + 32 * U^2 - 32 * U + 64) * Y1 * V + (86 * U^3 - 352 * U^2 + 224 * U + 192) * Y2 * V + ( - 40 * U^3 + 120 * U^2 - 48 * U - 64) * A * V + ( - 96 * U^2 + 32 * U) * Y1 + (176 * U^2 - 192 * U - 128) * Y2 + ( - 40 * U^2 + 40 * U + 32) * A, (32 * U^3) * X1 * S2^4 * V + (16 * U^3 - 64 * U^2) * X1 * Y2^2 * S2 * V + ( - 16 * U^3 + 64 * U^2) * X2 * Y2^2 * S2 * V + ( - 120 * U^3 + 64 * U^2) * X1 * S2^3 * V + (16 * U^3 - 32 * U^2) * X2 * S2^3 * V + (4 * U^3 - 16 * U^2) * X1 * Y1 * Y2 * V + ( - 24 * U^3 + 96 * U^2) * X1 * Y2^2 * V + (20 * U^3 - 80 * U^2) * X2 * Y2^2 * V + ( - 4 * U^3 + 8 * U^2) * X2 * R2^2 * V + (168 * U^3 - 184 * U^2) * X1 * S2^2 * V + ( - 52 * U^3 + 136 * U^2 - 32 * U) * X2 * S2^2 * V + ( - 64 * U^2) * X1 * Y2^2 + (64 * U^2) * X2 * Y2^2 + (32 * U^2) * X2 * R2 * S2 + (32 * U^2) * X1 * S2^2 + ( - 32 * U^2) * X2 * S2^2 + ( - 8 * U) * X1 * R2 * V + (8 * U^3 - 24 * U^2 + 16 * U + 32) * X2 * R2 * V + ( - 104 * U^3 + 176 * U^2 - 8 * U) * X1 * S2 * V + (56 * U^3 - 184 * U^2 + 80 * U + 32) * X2 * S2 * V + ( - 40 * U^2) * X2 * R2 + ( - 56 * U^2) * X1 * S2 + (56 * U^2 - 32 * U) * X2 * S2 + (24 * U^3 - 56 * U^2 + 16 * U) * X1 * V + ( - 24 * U^3 + 96 * U^2 - 64 * U - 64) * X2 * V + (24 * U^2 - 8 * U) * X1 + ( - 24 * U^2 + 48 * U + 32) * X2, (16 * U^3) * Y1^3 * S2 * V + ( - 16 * U^3) * Y1 * Y2^2 * S2 * V + ( - 16 * U^3 + 16 * U^2) * Y1^3 * V + (8 * U^3 - 48 * U^2) * Y1^2 * Y2 * V + (48 * U^2) * Y1 * Y2^2 * V + (8 * U^3 - 16 * U^2) * Y2^3 * V + ( - 4 * U^3 + 16 * U^2) * A * R2^2 * V + ( - 8 * U^3) * Y2 * S2^2 * V + ( - 16 * U^2) * A * S2^2 * V + (64 * U^2) * Y1^2 * Y2 + ( - 64 * U^2) * Y1 * Y2^2 + ( - 16 * U^2) * A * R2^2 + ( - 64 * U^2) * Y1 * R2 * S2 + (32 * U^2) * A * R2 * S2 + (64 * U^2) * Y1 * S2^2 + ( - 16 * U^2) * A * S2^2 + ( - 4 * U^3 + 24 * U^2 - 64 * U) * Y1 * R2 * V + (10 * U^3 - 52 * U^2 + 32 * U) * A * R2 * V + (4 * U^3 - 8 * U^2) * Y1 * S2 * V + (16 * U^3 - 32 * U^2 + 64 * U) * Y2 * S2 * V + ( - 2 * U^3 + 44 * U^2 - 32 * U) * A * S2 * V + (64 * U^2) * Y1 * R2 + (16 * U^2) * A * R2 + ( - 32 * U^2) * Y1 * S2 + ( - 32 * U^2) * Y2 * S2 + ( - 16 * U^2) * A * S2 + (2 * U^3 - 32 * U^2 + 96 * U) * Y1 * V + ( - 10 * U^3 + 48 * U^2 - 96 * U) * Y2 * V + ( - 4 * U^3 + 8 * U^2) * A * V + ( - 8 * U^2 - 64 * U) * Y1 + (64 * U) * Y2 + ( - 4 * U^2) * A, ( - 8 * U^3) * X1 * Y1^2 * S2 * V + (8 * U^3) * X1 * Y2^2 * S2 * V + (8 * U^3 - 8 * U^2) * X1 * Y1^2 * V + ( - 4 * U^3 + 24 * U^2) * X1 * Y1 * Y2 * V + ( - 24 * U^2) * X1 * Y2^2 * V + ( - 4 * U^3 + 8 * U^2) * X2 * Y2^2 * V + (4 * U^3 - 16 * U^2) * X2 * R2^2 * V + (16 * U^2) * X1 * S2^2 * V + (4 * U^3) * X2 * S2^2 * V + ( - 32 * U^2) * X1 * Y1 * Y2 + (32 * U^2) * X1 * Y2^2 + (16 * U^2) * X2 * R2^2 + (16 * U^2) * X1 * R2 * S2 + ( - 16 * U^2) * X2 * R2 * S2 + ( - 16 * U^2) * X1 * S2^2 + (16 * U) * X1 * R2 * V + ( - 8 * U^3 + 40 * U^2 - 16 * U) * X2 * R2 * V + ( - 32 * U^2 + 16 * U) * X1 * S2 * V + ( - 8 * U^3 + 8 * U^2 - 16 * U) * X2 * S2 * V + ( - 24 * U^2) * X1 * R2 + ( - 24 * U^2) * X2 * R2 + (24 * U^2) * X1 * S2 + (24 * U^2) * X2 * S2 + (16 * U^2 - 32 * U) * X1 * V + (8 * U^3 - 32 * U^2 + 32 * U) * X2 * V + (16 * U) * X1 + (8 * U^2 - 16 * U) * X2, (4 * U^3) * A^2 * S2^3 * V + ( - 12 * U^3 + 4 * U^2) * A^2 * S2^2 * V + ( - 4 * U) * A^2 * R2 * V + (4 * U^3) * Y1^2 * S2 * V + ( - 8 * U^3 + 16 * U^2) * Y1 * Y2 * S2 * V + (4 * U^3 - 16 * U^2) * Y2^2 * S2 * V + (12 * U^3 - 8 * U^2 - 4 * U) * A^2 * S2 * V + ( - 8 * U^3 + 16 * U^2) * S2^3 * V + (4 * U^2) * A^2 * R2 + ( - 4 * U^3 + 4 * U^2) * Y1^2 * V + (8 * U^3 - 24 * U^2) * Y1 * Y2 * V + ( - 4 * U^3 + 20 * U^2) * Y2^2 * V + ( - 4 * U^3 + 4 * U^2 + 8 * U) * A^2 * V + (24 * U^3 - 64 * U^2 + 16 * U) * S2^2 * V + (16 * U^2) * Y1 * Y2 + ( - 16 * U^2) * Y2^2 + ( - 4 * U^2 - 4 * U) * A^2 + ( - 16 * U^2) * R2 * S2 + (16 * U^2) * S2^2 + ( - 16) * R2 * V + ( - 24 * U^3 + 80 * U^2 - 32 * U - 16) * S2 * V + (16 * U^2) * R2 + ( - 24 * U^2 + 16 * U) * S2 + (8 * U^3 - 32 * U^2 + 16 * U + 32) * V + (8 * U^2 - 16 * U - 16), (4 * U^2) * X1 * A * S2^3 * V + ( - 14 * U^2 + 8 * U) * X1 * A * S2^2 * V + (2 * U^2 - 4 * U) * X2 * A * S2^2 * V + ( - 4) * X2 * A * R2 * V + (2 * U^2) * X1 * Y1 * S2 * V + ( - 4 * U^2 + 8 * U) * X1 * Y2 * S2 * V + (2 * U^2 - 8 * U) * X2 * Y2 * S2 * V + (16 * U^2 - 20 * U) * X1 * A * S2 * V + ( - 4 * U^2 + 12 * U - 4) * X2 * A * S2 * V + (4 * U) * X2 * A * R2 + (4 * U) * X1 * A * S2 + ( - 4 * U) * X2 * A * S2 + ( - 2 * U^2 + 2 * U) * X1 * Y1 * V + (4 * U^2 - 12 * U) * X1 * Y2 * V + ( - 2 * U^2 + 10 * U) * X2 * Y2 * V + ( - 6 * U^2 + 12 * U) * X1 * A * V + (2 * U^2 - 8 * U + 8) * X2 * A * V + (8 * U) * X1 * Y2 + ( - 8 * U) * X2 * Y2 + ( - 6 * U) * X1 * A + (2 * U - 4) * X2 * A, ( - 8 * U^3 + 32 * U^2) * Y1^3 * Y2 * V + (24 * U^3 - 96 * U^2) * Y1^2 * Y2^2 * V + ( - 24 * U^3 + 96 * U^2) * Y1 * Y2^3 * V + (8 * U^3 - 32 * U^2) * Y2^4 * V + ( - 16 * U^3 + 32 * U^2) * Y2^2 * S2^2 * V + (4 * U^3 - 8 * U^2) * A^2 * S2^2 * V + (8 * U^3) * S2^4 * V + (128 * U^2) * Y1^2 * Y2^2 + ( - 128 * U^2) * Y1 * Y2^3 + ( - 128 * U^2) * Y1^2 * S2^2 + (128 * U^2) * Y1 * Y2 * S2^2 + (4 * U^3 - 16 * U^2 + 32 * U) * Y1^2 * R2 * V + ( - U^3 + 4 * U^2 - 8 * U) * A^2 * R2 * V + ( - 4 * U^3 + 8 * U^2) * R2^3 * V + ( - 4 * U^3 + 16 * U^2 - 64 * U) * Y1^2 * S2 * V + ( - 12 * U^3 + 48 * U^2) * Y1 * Y2 * S2 * V + (44 * U^3 - 144 * U^2 + 96 * U) * Y2^2 * S2 * V + ( - 7 * U^3 + 20 * U^2 - 8 * U) * A^2 * S2 * V + ( - 44 * U^3 + 56 * U^2) * S2^3 * V + (16 * U^2) * A^2 * R2 + (224 * U^2) * Y1^2 * S2 + ( - 192 * U^2) * Y1 * Y2 * S2 + ( - 32 * U^2) * Y2^2 * S2 + ( - 16 * U^2) * A^2 * S2 + (32 * U^2) * R2^2 * S2 + ( - 64 * U^2) * R2 * S2^2 + (32 * U^2) * S2^3 + ( - 4 * U^3 + 24 * U^2 - 16 * U) * Y1^2 * V + (18 * U^3 - 96 * U^2 + 96 * U) * Y1 * Y2 * V + ( - 30 * U^3 + 136 * U^2 - 144 * U) * Y2^2 * V + (4 * U^3 - 16 * U^2 + 16 * U) * A^2 * V + (16 * U^3 - 52 * U^2 + 48 * U) * R2^2 * V + (82 * U^3 - 196 * U^2 + 96 * U) * S2^2 * V + ( - 96 * U^2 + 32 * U) * Y1^2 + (112 * U^2 - 96 * U) * Y1 * Y2 + ( - 32 * U^2 + 96 * U) * Y2^2 + (4 * U^2 - 8 * U) * A^2 + ( - 40 * U^2) * R2^2 + (40 * U^2) * R2 * S2 + (8 * U^2) * S2^2 + ( - 19 * U^3 + 82 * U^2 - 120 * U + 48) * R2 * V + ( - 65 * U^3 + 226 * U^2 - 216 * U + 48) * S2 * V + (20 * U^2) * R2 + ( - 52 * U^2 + 48 * U) * S2 + (26 * U^3 - 124 * U^2 + 192 * U - 96) * V + (26 * U^2 - 72 * U + 48), (64 * U^4 - 256 * U^3) * Y1 * Y2^3 * S2 * V + ( - 64 * U^4 + 256 * U^3) * Y2^4 * S2 * V + (128 * U^4 - 256 * U^3) * Y2^2 * S2^3 * V + ( - 64 * U^4) * S2^5 * V + (16 * U^4 - 64 * U^3) * Y1^2 * Y2^2 * V + ( - 96 * U^4 + 384 * U^3) * Y1 * Y2^3 * V + (80 * U^4 - 320 * U^3) * Y2^4 * V + ( - 448 * U^4 + 1216 * U^3 - 256 * U^2) * Y2^2 * S2^2 * V + (8 * U^4 - 48 * U^3) * A^2 * S2^2 * V + (368 * U^4 - 320 * U^3) * S2^4 * V + ( - 256 * U^3) * Y1 * Y2^3 + (256 * U^3) * Y2^4 + (256 * U^3) * Y1 * Y2 * S2^2 + ( - 256 * U^3) * Y2^2 * S2^2 + ( - 8 * U^3 + 64 * U) * A^2 * R2 * V + (32 * U^4 - 64 * U^3 - 64 * U^2) * Y1^2 * S2 * V + ( - 80 * U^4 + 288 * U^3 - 64 * U^2 + 256 * U) * Y1 * Y2 * S2 * V + (560 * U^4 - 2016 * U^3 + 1024 * U^2 + 256 * U) * Y2^2 * S2 * V + ( - 16 * U^4 + 120 * U^3 - 96 * U^2 - 64 * U) * A^2 * S2 * V + ( - 880 * U^4 + 1600 * U^3 - 448 * U^2) * S2^3 * V + ( - 64 * U^2) * A^2 * R2 + ( - 576 * U^3) * Y1 * Y2 * S2 + (704 * U^3 - 256 * U^2) * Y2^2 * S2 + (64 * U^2) * A^2 * S2 + (64 * U^3) * R2 * S2^2 + ( - 128 * U^3) * S2^3 + ( - 32 * U^4 + 96 * U^3 - 32 * U^2) * Y1^2 * V + (80 * U^4 - 384 * U^3 + 352 * U^2 - 128 * U) * Y1 * Y2 * V + ( - 240 * U^4 + 1120 * U^3 - 960 * U^2 - 384 * U) * Y2^2 * V + (8 * U^4 - 64 * U^3 + 96 * U^2) * A^2 * V + (16 * U^2) * R2^2 * V + (1064 * U^4 - 2976 * U^3 + 1840 * U^2 + 64 * U) * S2^2 * V + (384 * U^3 - 320 * U^2) * Y1 * Y2 + ( - 576 * U^3 + 768 * U^2 + 256 * U) * Y2^2 + (8 * U^3 - 48 * U^2) * A^2 + ( - 176 * U^3 + 256 * U^2) * R2 * S2 + (416 * U^3 - 448 * U^2) * S2^2 + (8 * U^3 - 80 * U^2 + 192) * R2 * V + ( - 640 * U^4 + 2408 * U^3 - 2288 * U^2 + 192) * S2 * V + (144 * U^3 - 272 * U^2) * R2 + ( - 480 * U^3 + 880 * U^2 - 64 * U) * S2 + (152 * U^4 - 720 * U^3 + 960 * U^2 - 64 * U - 384) * V + (152 * U^3 - 416 * U^2 + 128 * U + 192), (8 * U^3) * X2 * A * S2^3 * V + (8 * U^3 - 32 * U^2) * X1 * Y1^2 * Y2 * V + ( - 24 * U^3 + 96 * U^2) * X1 * Y1 * Y2^2 * V + (24 * U^3 - 96 * U^2) * X1 * Y2^3 * V + ( - 8 * U^3 + 32 * U^2) * X2 * Y2^3 * V + ( - 4 * U^3 + 8 * U^2) * X1 * A * R2^2 * V + (16 * U^3 - 32 * U^2) * X2 * Y2 * S2^2 * V + (4 * U^3 - 24 * U^2) * X1 * A * S2^2 * V + ( - 32 * U^3 + 40 * U^2) * X2 * A * S2^2 * V + ( - 128 * U^2) * X1 * Y1 * Y2^2 + (128 * U^2) * X1 * Y2^3 + (32 * U^2) * X1 * A * R2 * S2 + ( - 32 * U^2) * X2 * A * R2 * S2 + (128 * U^2) * X1 * Y1 * S2^2 + ( - 128 * U^2) * X1 * Y2 * S2^2 + ( - 32 * U^2) * X1 * A * S2^2 + (32 * U^2) * X2 * A * S2^2 + ( - 4 * U^3 + 16 * U^2 - 32 * U) * X1 * Y1 * R2 * V + (10 * U^3 - 32 * U^2 + 32 * U) * X1 * A * R2 * V + (8 * U^2 - 24 * U) * X2 * A * R2 * V + (64 * U) * X1 * Y1 * S2 * V + (12 * U^3 - 48 * U^2) * X1 * Y2 * S2 * V + ( - 40 * U^3 + 128 * U^2 - 96 * U) * X2 * Y2 * S2 * V + ( - 10 * U^3 + 64 * U^2 - 64 * U) * X1 * A * S2 * V + (40 * U^3 - 104 * U^2 + 72 * U) * X2 * A * S2 * V + ( - 40 * U^2) * X1 * A * R2 + (16 * U^2) * X2 * A * R2 + ( - 224 * U^2) * X1 * Y1 * S2 + (192 * U^2) * X1 * Y2 * S2 + (32 * U^2) * X2 * Y2 * S2 + (40 * U^2) * X1 * A * S2 + ( - 8 * U^2) * X2 * A * S2 + (6 * U^3 - 32 * U^2 + 16 * U) * X1 * Y1 * V + ( - 14 * U^3 + 80 * U^2 - 96 * U) * X1 * Y2 * V + (24 * U^3 - 112 * U^2 + 144 * U) * X2 * Y2 * V + ( - 16 * U^2 + 32 * U) * X1 * A * V + ( - 16 * U^3 + 56 * U^2 - 48 * U) * X2 * A * V + (96 * U^2 - 32 * U) * X1 * Y1 + ( - 96 * U^2 + 96 * U) * X1 * Y2 + (16 * U^2 - 96 * U) * X2 * Y2 + ( - 16 * U) * X1 * A + ( - 16 * U^2 + 24 * U) * X2 * A, (16 * U^3 - 64 * U^2) * Y1^4 * V + ( - 96 * U^3 + 384 * U^2) * Y1^2 * Y2^2 * V + (128 * U^3 - 512 * U^2) * Y1 * Y2^3 * V + ( - 48 * U^3 + 192 * U^2) * Y2^4 * V + ( - 32 * U^3 + 64 * U^2) * Y1^2 * R2^2 * V + (16 * U^3) * R2^4 * V + (96 * U^3 - 192 * U^2) * Y2^2 * S2^2 * V + ( - 16 * U^3 + 32 * U^2) * A^2 * S2^2 * V + ( - 48 * U^3) * S2^4 * V + ( - 256 * U^2) * Y1^3 * Y2 + ( - 512 * U^2) * Y1^2 * Y2^2 + (768 * U^2) * Y1 * Y2^3 + (256 * U^2) * Y1^2 * R2 * S2 + ( - 64 * U^2) * A^2 * R2 * S2 + (512 * U^2) * Y1^2 * S2^2 + ( - 768 * U^2) * Y1 * Y2 * S2^2 + (64 * U^2) * A^2 * S2^2 + (64 * U^3 - 192 * U^2) * Y1^2 * R2 * V + (16 * U^2) * A^2 * R2 * V + ( - 64 * U^3 + 64 * U^2) * R2^3 * V + ( - 32 * U^3 + 64 * U^2 + 384 * U) * Y1^2 * S2 * V + (96 * U^3 - 320 * U^2 - 128 * U) * Y1 * Y2 * S2 * V + ( - 256 * U^3 + 832 * U^2 - 512 * U) * Y2^2 * S2 * V + (32 * U^3 - 112 * U^2 + 64 * U) * A^2 * S2 * V + (256 * U^3 - 320 * U^2) * S2^3 * V + ( - 192 * U^2) * Y1^2 * R2 + ( - 80 * U^2) * A^2 * R2 + ( - 64 * U^2) * R2^3 + ( - 1344 * U^2) * Y1^2 * S2 + (1344 * U^2) * Y1 * Y2 * S2 + (192 * U^2) * Y2^2 * S2 + (80 * U^2) * A^2 * S2 + (64 * U^2) * R2^2 * S2 + (192 * U^2) * R2 * S2^2 + ( - 192 * U^2) * S2^3 + (32 * U^2 - 192 * U) * Y1^2 * V + ( - 96 * U^3 + 448 * U^2 - 320 * U) * Y1 * Y2 * V + (160 * U^3 - 736 * U^2 + 768 * U) * Y2^2 * V + ( - 16 * U^3 + 64 * U^2 - 64 * U) * A^2 * V + (96 * U^3 - 192 * U^2 - 32 * U) * R2^2 * V + ( - 464 * U^3 + 1120 * U^2 - 608 * U) * S2^2 * V + (576 * U^2) * Y1^2 + ( - 672 * U^2 + 384 * U) * Y1 * Y2 + (160 * U^2 - 512 * U) * Y2^2 + ( - 16 * U^2 + 32 * U) * A^2 + (320 * U^2) * R2^2 + ( - 448 * U^2) * R2 * S2 + (96 * U^2) * S2^2 + ( - 64 * U^3 + 176 * U^2 + 128 * U - 256) * R2 * V + (352 * U^3 - 1232 * U^2 + 1216 * U - 256) * S2 * V + ( - 208 * U^2 + 160 * U) * R2 + (336 * U^2 - 352 * U) * S2 + ( - 80 * U^3 + 384 * U^2 - 704 * U + 512) * V + ( - 80 * U^2 + 224 * U - 256), ( - 32 * U^5 + 128 * U^4) * X1 * Y1^2 * Y2^2 * V + (96 * U^5 - 384 * U^4) * X1 * Y1 * Y2^3 * V + ( - 96 * U^5 + 384 * U^4) * X1 * Y2^4 * V + (32 * U^5 - 128 * U^4) * X2 * Y2^4 * V + ( - 64 * U^5 + 128 * U^4) * X2 * Y2^2 * S2^2 * V + (16 * U^5 - 32 * U^4) * X2 * A^2 * S2^2 * V + (32 * U^5) * X2 * S2^4 * V + (512 * U^4) * X1 * Y1 * Y2^3 + ( - 512 * U^4) * X1 * Y2^4 + ( - 256 * U^4) * X2 * R2^2 * S2^2 + ( - 256 * U^4) * X1 * R2 * S2^3 + (256 * U^4) * X2 * R2 * S2^3 + (256 * U^4) * X1 * S2^4 + ( - 48 * U^5 + 192 * U^4 - 128 * U^3) * X1 * Y2^2 * S2 * V + (176 * U^5 - 576 * U^4 + 384 * U^3) * X2 * Y2^2 * S2 * V + ( - 32 * U^5 + 96 * U^4 - 64 * U^3) * X2 * A^2 * S2 * V + ( - 8 * U^5 + 128 * U^3) * X1 * S2^3 * V + ( - 176 * U^5 + 224 * U^4) * X2 * S2^3 * V + (64 * U^4) * X2 * A^2 * R2 + ( - 64 * U^4) * X2 * A^2 * S2 + (512 * U^4) * X2 * R2^2 * S2 + (768 * U^4) * X1 * R2 * S2^2 + ( - 256 * U^4) * X2 * R2 * S2^2 + ( - 768 * U^4) * X1 * S2^3 + ( - 256 * U^4) * X2 * S2^3 + (64 * U^3 - 128 * U^2) * X1 * Y1^2 * V + ( - 4 * U^5 + 48 * U^4 - 256 * U^3 + 384 * U^2) * X1 * Y1 * Y2 * V + (56 * U^5 - 320 * U^4 + 512 * U^3 - 384 * U^2) * X1 * Y2^2 * V + ( - 116 * U^5 + 528 * U^4 - 576 * U^3 + 128 * U^2) * X2 * Y2^2 * V + (16 * U^5 - 64 * U^4 + 64 * U^3) * X2 * A^2 * V + ( - 32 * U^3) * X1 * R2^2 * V + (4 * U^5 - 40 * U^4 + 96 * U^3 - 128 * U^2) * X2 * R2^2 * V + (24 * U^5 - 8 * U^4 - 480 * U^3 + 384 * U^2) * X1 * S2^2 * V + (324 * U^5 - 776 * U^4 + 384 * U^3 - 128 * U^2) * X2 * S2^2 * V + (64 * U^4 + 128 * U^3 - 512 * U^2) * X1 * Y1 * Y2 + (128 * U^4 - 384 * U^3 + 512 * U^2) * X1 * Y2^2 + ( - 256 * U^4 + 384 * U^3) * X2 * Y2^2 + (16 * U^4 - 32 * U^3) * X2 * A^2 + ( - 320 * U^4 + 256 * U^2) * X2 * R2^2 + ( - 800 * U^4 + 256 * U^2) * X1 * R2 * S2 + ( - 320 * U^4 - 256 * U^2) * X2 * R2 * S2 + (800 * U^4 - 256 * U^2) * X1 * S2^2 + (672 * U^4) * X2 * S2^2 + (72 * U^3 - 128 * U^2 + 128 * U) * X1 * R2 * V + ( - 8 * U^5 + 88 * U^4 - 272 * U^3 + 416 * U^2 - 256 * U) * X2 * R2 * V + ( - 24 * U^5 + 16 * U^4 + 584 * U^3 - 896 * U^2 + 128 * U) * X1 * S2 * V + ( - 248 * U^5 + 856 * U^4 - 784 * U^3 + 416 * U^2 - 256 * U) * X2 * S2 * V + (288 * U^4 + 32 * U^3 - 384 * U^2) * X1 * R2 + (392 * U^4 - 32 * U^3 - 256 * U^2) * X2 * R2 + ( - 296 * U^4 - 32 * U^3 + 512 * U^2) * X1 * S2 + ( - 504 * U^4 + 192 * U^3 + 256 * U^2) * X2 * S2 + (8 * U^5 - 8 * U^4 - 272 * U^3 + 640 * U^2 - 256 * U) * X1 * V + (72 * U^5 - 352 * U^4 + 576 * U^3 - 576 * U^2 + 512 * U) * X2 * V + (8 * U^4 + 8 * U^3 - 256 * U^2 + 128 * U) * X1 + (72 * U^4 - 208 * U^3 + 160 * U^2 - 256 * U) * X2, (256 * U^5 - 1024 * U^4) * Y2^4 * S2^2 * V + ( - 16 * U^5 + 64 * U^4) * A^4 * S2^2 * V + ( - 512 * U^5 + 1024 * U^4) * Y2^2 * S2^4 * V + (256 * U^5) * S2^6 * V + ( - 512 * U^5 + 2560 * U^4 - 2048 * U^3) * Y2^4 * S2 * V + (32 * U^5 - 160 * U^4 + 128 * U^3) * A^4 * S2 * V + (2048 * U^5 - 6144 * U^4 + 2048 * U^3) * Y2^2 * S2^3 * V + ( - 1536 * U^5 + 1536 * U^4) * S2^5 * V + (1024 * U^4) * Y1 * Y2^3 * S2 + ( - 1024 * U^4) * Y2^4 * S2 + ( - 1024 * U^4) * Y1 * Y2 * S2^3 + (1024 * U^4) * Y2^2 * S2^3 + ( - 32 * U^5 + 64 * U^4 + 256 * U^3) * Y1^2 * Y2^2 * V + (64 * U^5 - 1024 * U^3) * Y1 * Y2^3 * V + (224 * U^5 - 1600 * U^4 + 2816 * U^3) * Y2^4 * V + ( - 16 * U^5 + 96 * U^4 - 128 * U^3) * A^4 * V + ( - 3008 * U^5 + 12544 * U^4 - 9984 * U^3) * Y2^2 * S2^2 * V + (48 * U^5 - 192 * U^4 + 192 * U^3) * A^2 * S2^2 * V + (3808 * U^5 - 7872 * U^4 + 3072 * U^3) * S2^4 * V + ( - 256 * U^4 + 1024 * U^3) * Y1 * Y2^3 + (512 * U^4 - 2048 * U^3) * Y2^4 + ( - 16 * U^4 + 64 * U^3) * A^4 + (256 * U^3) * A^2 * R2 * S2 + (2560 * U^4 - 1024 * U^3) * Y1 * Y2 * S2^2 + ( - 3072 * U^4 + 2048 * U^3) * Y2^2 * S2^2 + ( - 256 * U^3) * A^2 * S2^2 + ( - 256 * U^4) * R2 * S2^3 + (512 * U^4) * S2^4 + (16 * U^4 + 64 * U^3 - 256 * U^2) * A^2 * R2 * V + ( - 64 * U^5 + 384 * U^3 + 256 * U^2) * Y1^2 * S2 * V + (96 * U^5 - 896 * U^3 - 768 * U^2) * Y1 * Y2 * S2 * V + (1888 * U^5 - 10624 * U^4 + 14848 * U^3 - 3072 * U^2) * Y2^2 * S2 * V + ( - 96 * U^5 + 464 * U^4 - 832 * U^3 + 640 * U^2) * A^2 * S2 * V + ( - 4960 * U^5 + 16064 * U^4 - 13312 * U^3 + 2048 * U^2) * S2^3 * V + ( - 32 * U^4 + 256 * U^2) * A^2 * R2 + ( - 2048 * U^4 + 3328 * U^3) * Y1 * Y2 * S2 + (3072 * U^4 - 6400 * U^3) * Y2^2 * S2 + (32 * U^4 - 256 * U^2) * A^2 * S2 + (768 * U^4 - 1280 * U^3) * R2 * S2^2 + ( - 1792 * U^4 + 2304 * U^3) * S2^3 + (64 * U^5 - 64 * U^4 - 320 * U^3 + 128 * U^2) * Y1^2 * V + ( - 96 * U^5 + 128 * U^4 + 1024 * U^3 - 896 * U^2) * Y1 * Y2 * V + ( - 416 * U^5 + 3136 * U^4 - 7104 * U^3 + 4352 * U^2) * Y2^2 * V + (48 * U^5 - 288 * U^4 + 576 * U^3 - 384 * U^2) * A^2 * V + ( - 32 * U^3 - 64 * U^2) * R2^2 * V + (3520 * U^5 - 16032 * U^4 + 21472 * U^3 - 8384 * U^2) * S2^2 * V + (320 * U^4 - 1664 * U^3 + 1280 * U^2) * Y1 * Y2 + ( - 768 * U^4 + 3968 * U^3 - 3072 * U^2) * Y2^2 + (48 * U^4 - 192 * U^3 + 192 * U^2) * A^2 + ( - 608 * U^4 + 1728 * U^3 - 1024 * U^2) * R2 * S2 + (2112 * U^4 - 4992 * U^3 + 2048 * U^2) * S2^2 + ( - 16 * U^4 + 96 * U^3 + 512 * U^2 - 1024 * U) * R2 * V + ( - 1248 * U^5 + 7632 * U^4 - 14880 * U^3 + 10112 * U^2 - 1024 * U) * S2 * V + (64 * U^4 - 672 * U^3 + 1088 * U^2) * R2 + ( - 992 * U^4 + 4128 * U^3 - 3776 * U^2) * S2 + (160 * U^5 - 1312 * U^4 + 3584 * U^3 - 4224 * U^2 + 2048 * U) * V + (160 * U^4 - 992 * U^3 + 1600 * U^2 - 1024 * U), (64 * U^4 - 256 * U^3) * X1 * Y2^4 * S2 * V + ( - 64 * U^4 + 256 * U^3) * X2 * Y2^4 * S2 * V + (128 * U^4 - 256 * U^3) * X2 * Y2^2 * S2^3 * V + ( - 64 * U^4) * X2 * S2^5 * V + (16 * U^4 - 64 * U^3) * X1 * Y1 * Y2^3 * V + ( - 96 * U^4 + 384 * U^3) * X1 * Y2^4 * V + (80 * U^4 - 320 * U^3) * X2 * Y2^4 * V + ( - 448 * U^4 + 1216 * U^3 - 256 * U^2) * X2 * Y2^2 * S2^2 * V + (8 * U^4 - 48 * U^3) * X2 * A^2 * S2^2 * V + (368 * U^4 - 320 * U^3) * X2 * S2^4 * V + ( - 256 * U^3) * X1 * Y2^4 + (256 * U^3) * X2 * Y2^4 + (256 * U^3) * X1 * Y2^2 * S2^2 + ( - 256 * U^3) * X2 * Y2^2 * S2^2 + ( - 8 * U^3 + 64 * U) * X2 * A^2 * R2 * V + ( - 48 * U^4 + 224 * U^3 - 128 * U^2 + 256 * U) * X1 * Y2^2 * S2 * V + (560 * U^4 - 2016 * U^3 + 1024 * U^2 + 256 * U) * X2 * Y2^2 * S2 * V + ( - 16 * U^4 + 120 * U^3 - 96 * U^2 - 64 * U) * X2 * A^2 * S2 * V + ( - 16 * U^4 + 32 * U^3 + 32 * U^2) * X1 * S2^3 * V + ( - 880 * U^4 + 1600 * U^3 - 448 * U^2) * X2 * S2^3 * V + ( - 64 * U^2) * X2 * A^2 * R2 + ( - 576 * U^3) * X1 * Y2^2 * S2 + (704 * U^3 - 256 * U^2) * X2 * Y2^2 * S2 + (64 * U^2) * X2 * A^2 * S2 + (64 * U^3) * X2 * R2 * S2^2 + ( - 128 * U^3) * X2 * S2^3 + ( - 8 * U^4 + 48 * U^3 - 80 * U^2) * X1 * Y1 * Y2 * V + (64 * U^4 - 352 * U^3 + 384 * U^2 - 128 * U) * X1 * Y2^2 * V + ( - 248 * U^4 + 1136 * U^3 - 944 * U^2 - 384 * U) * X2 * Y2^2 * V + (8 * U^4 - 64 * U^3 + 96 * U^2) * X2 * A^2 * V + (8 * U^4 - 32 * U^3 + 32 * U^2 + 32 * U) * X2 * R2^2 * V + (48 * U^4 - 112 * U^3 - 64 * U^2 + 32 * U) * X1 * S2^2 * V + (1072 * U^4 - 2976 * U^3 + 1792 * U^2 + 32 * U) * X2 * S2^2 * V + (384 * U^3 - 320 * U^2) * X1 * Y2^2 + ( - 576 * U^3 + 768 * U^2 + 256 * U) * X2 * Y2^2 + (8 * U^3 - 48 * U^2) * X2 * A^2 + ( - 176 * U^3 + 256 * U^2) * X2 * R2 * S2 + (416 * U^3 - 448 * U^2) * X2 * S2^2 + (16 * U^2 - 32 * U - 32) * X1 * R2 * V + ( - 16 * U^4 + 88 * U^3 - 144 * U^2 - 96 * U + 192) * X2 * R2 * V + ( - 48 * U^4 + 128 * U^3 + 48 * U^2 - 96 * U - 32) * X1 * S2 * V + ( - 656 * U^4 + 2424 * U^3 - 2224 * U^2 + 32 * U + 192) * X2 * S2 * V + (128 * U^3 - 240 * U^2 + 32 * U) * X2 * R2 + ( - 16 * U^3 + 32 * U^2 + 32 * U) * X1 * S2 + ( - 464 * U^3 + 848 * U^2 - 96 * U) * X2 * S2 + (16 * U^4 - 48 * U^3 - 32 * U^2 + 96 * U + 64) * X1 * V + (168 * U^4 - 784 * U^3 + 992 * U^2 - 384) * X2 * V + (16 * U^3 - 16 * U^2 - 64 * U - 32) * X1 + (168 * U^3 - 448 * U^2 + 96 * U + 192) * X2 ]
6------------------- CASE 2 -------------------
7Condition:
8 Green list: [ U - 4, 2 * A^2 - 1 ]
9 Red list: [ A ]
10 Basis: [ ( - 1) * X1^2 + ( - 1) * Y1^2 + (1) * R2^2 + ( - 2) * R2 + (1), (1) * R1 + (1) * R2 + ( - 1), ( - 1) * X2^2 + ( - 1) * Y2^2 + (1) * S2^2 + ( - 2) * S2 + (1), (1) * S1 + (1) * S2 + ( - 1), ( - 1) * Y1 * X2 + (1) * X1 * Y2, ( - 2) * Y2 * A + (1) * A^2 + ( - 2) * S2 + (1), ( - 2) * Y1 * A + (1) * A^2 + ( - 2) * R2 + (1), (4) * R2 * S2 * V + ( - 3) * R2 * V + ( - 3) * S2 * V + (2) * V + (1), ( - 4) * Y2 * R2 + (2) * A * R2 + (4) * Y1 * S2 + ( - 2) * A * S2 + ( - 2) * Y1 + (2) * Y2, (1) * X1 * A^2 + ( - 1) * X2 * A^2 + (2) * X2 * R2 + ( - 2) * X1 * S2 + (1) * X1 + ( - 1) * X2, ( - 1) * X1 * X2 * Y2 + ( - 1) * Y1 * Y2^2 + (1) * Y1 * S2^2 + ( - 2) * Y1 * S2 + (1) * Y1, ( - 16) * Y1 * S2^2 * V + (8) * A * S2^2 * V + (20) * Y1 * S2 * V + (4) * Y2 * S2 * V + ( - 12) * A * S2 * V + ( - 6) * Y1 * V + ( - 2) * Y2 * V + (4) * A * V + ( - 4) * Y2 + (2) * A, (4) * A^2 * R2^2 + ( - 4) * A^2 * S2^2 + ( - 8) * A^2 * R2 + (16) * Y1^2 * S2 + ( - 16) * Y1 * Y2 * S2 + (8) * A^2 * S2 + ( - 16) * R2^2 * S2 + (16) * R2 * S2^2 + ( - 12) * Y1^2 + (8) * Y1 * Y2 + (4) * Y2^2 + (8) * R2^2 + (8) * R2 * S2 + ( - 16) * S2^2 + ( - 8) * R2 + (8) * S2, ( - 8) * X1 * X2 * R2 + ( - 2) * A^2 * R2 + (8) * Y1^2 * S2 + (8) * X1 * X2 * S2 + ( - 8) * Y1 * Y2 * S2 + (2) * A^2 * S2 + ( - 8) * R2^2 * S2 + (8) * R2 * S2^2 + ( - 8) * Y1^2 + (4) * Y1 * Y2 + (4) * Y2^2 + (8) * R2^2 + (4) * R2 * S2 + ( - 12) * S2^2 + ( - 10) * R2 + (10) * S2, ( - 32) * Y1^2 * Y2 * S2 + (32) * Y1 * Y2^2 * S2 + (8) * A * R2^2 * S2 + (32) * Y1 * R2 * S2^2 + ( - 16) * A * R2 * S2^2 + ( - 32) * Y1 * S2^3 + (8) * A * S2^3 + (24) * Y1^2 * Y2 + ( - 16) * Y1 * Y2^2 + ( - 8) * Y2^3 + ( - 4) * A * R2^2 + ( - 48) * Y1 * R2 * S2 + (32) * Y1 * S2^2 + (16) * Y2 * S2^2 + (4) * A * S2^2 + (20) * Y1 * R2 + (6) * A * R2 + ( - 20) * Y2 * S2 + ( - 6) * A * S2 + ( - 6) * Y1 + (6) * Y2, (16) * X1 * Y1 * Y2 * S2 + ( - 16) * X1 * Y2^2 * S2 + ( - 8) * X2 * R2^2 * S2 + ( - 8) * X1 * R2 * S2^2 + (8) * X2 * R2 * S2^2 + (8) * X1 * S2^3 + ( - 12) * X1 * Y1 * Y2 + (8) * X1 * Y2^2 + (4) * X2 * Y2^2 + (4) * X2 * R2^2 + (16) * X1 * R2 * S2 + (8) * X2 * R2 * S2 + ( - 16) * X1 * S2^2 + ( - 12) * X2 * S2^2 + ( - 8) * X1 * R2 + ( - 8) * X2 * R2 + (8) * X1 * S2 + (8) * X2 * S2, (8) * A * R2^3 + ( - 32) * Y1^3 * S2 + (32) * Y1 * Y2^2 * S2 + (32) * Y1 * R2^2 * S2 + ( - 8) * A * R2^2 * S2 + ( - 8) * A * R2 * S2^2 + ( - 32) * Y1 * S2^3 + (8) * A * S2^3 + (24) * Y1^3 + (8) * Y1^2 * Y2 + ( - 24) * Y1 * Y2^2 + ( - 8) * Y2^3 + ( - 16) * Y1 * R2^2 + ( - 16) * A * R2^2 + ( - 80) * Y1 * R2 * S2 + (24) * A * R2 * S2 + (80) * Y1 * S2^2 + (16) * Y2 * S2^2 + ( - 8) * A * S2^2 + (48) * Y1 * R2 + (8) * A * R2 + ( - 24) * Y1 * S2 + ( - 24) * Y2 * S2 + ( - 8) * A * S2 + ( - 8) * Y1 + (8) * Y2, ( - 8) * X2 * R2^3 + (16) * X1 * Y1^2 * S2 + ( - 16) * X1 * Y2^2 * S2 + ( - 8) * X1 * R2^2 * S2 + (8) * X2 * R2 * S2^2 + (8) * X1 * S2^3 + ( - 12) * X1 * Y1^2 + ( - 4) * X1 * Y1 * Y2 + (12) * X1 * Y2^2 + (4) * X2 * Y2^2 + (4) * X1 * R2^2 + (20) * X2 * R2^2 + (24) * X1 * R2 * S2 + ( - 8) * X2 * R2 * S2 + ( - 28) * X1 * S2^2 + ( - 12) * X2 * S2^2 + ( - 16) * X1 * R2 + ( - 16) * X2 * R2 + (16) * X1 * S2 + (16) * X2 * S2, (4) * X2 * A * R2^2 + (4) * X1 * A * R2 * S2 + ( - 4) * X2 * A * R2 * S2 + ( - 4) * X1 * A * S2^2 + ( - 2) * X1 * A * R2 + ( - 6) * X2 * A * R2 + (8) * X1 * Y1 * S2 + ( - 8) * X1 * Y2 * S2 + (2) * X1 * A * S2 + (6) * X2 * A * S2 + ( - 6) * X1 * Y1 + (4) * X1 * Y2 + (2) * X2 * Y2, (16) * X1 * Y2 * S2^2 * V + ( - 8) * X2 * A * S2^2 * V + ( - 20) * X1 * Y2 * S2 * V + ( - 4) * X2 * Y2 * S2 * V + (12) * X2 * A * S2 * V + (6) * X1 * Y2 * V + (2) * X2 * Y2 * V + ( - 4) * X2 * A * V + (4) * X2 * Y2 + ( - 2) * X2 * A, ( - 512) * X1 * X2 * S2^2 * V + ( - 128) * A^2 * S2^2 * V + (256) * Y1^2 * S2 * V + (768) * X1 * X2 * S2 * V + ( - 128) * Y1 * Y2 * S2 * V + ( - 128) * Y2^2 * S2 * V + (192) * A^2 * S2 * V + (128) * S2^3 * V + ( - 192) * Y1^2 * V + ( - 256) * X1 * X2 * V + (64) * Y1 * Y2 * V + (128) * Y2^2 * V + ( - 64) * A^2 * V + ( - 288) * S2^2 * V + ( - 128) * X1 * X2 + (128) * Y1 * Y2 + ( - 128) * Y2^2 + ( - 32) * A^2 + ( - 128) * R2 * S2 + (128) * S2^2 + ( - 24) * R2 * V + (232) * S2 * V + (192) * R2 + ( - 160) * S2 + ( - 48) * V + ( - 24), (64) * Y1^4 * S2 + ( - 64) * Y1 * Y2^3 * S2 + ( - 64) * Y1^2 * R2^2 * S2 + (64) * Y1 * Y2 * S2^3 + ( - 48) * Y1^4 + ( - 16) * Y1^3 * Y2 + (48) * Y1 * Y2^3 + (16) * Y2^4 + (32) * Y1^2 * R2^2 + (16) * R2^4 + (192) * Y1^2 * R2 * S2 + (8) * A^2 * R2 * S2 + ( - 48) * R2^3 * S2 + ( - 64) * Y1^2 * S2^2 + ( - 128) * Y1 * Y2 * S2^2 + ( - 32) * Y2^2 * S2^2 + ( - 8) * A^2 * S2^2 + (64) * R2^2 * S2^2 + ( - 48) * R2 * S2^3 + (16) * S2^4 + ( - 120) * Y1^2 * R2 + ( - 10) * A^2 * R2 + ( - 24) * R2^3 + ( - 24) * Y1^2 * S2 + (104) * Y1 * Y2 * S2 + (40) * Y2^2 * S2 + (10) * A^2 * S2 + (40) * R2^2 * S2 + ( - 24) * R2 * S2^2 + (8) * S2^3 + (40) * Y1^2 + ( - 28) * Y1 * Y2 + ( - 12) * Y2^2 + (24) * R2^2 + ( - 20) * R2 * S2 + ( - 4) * S2^2 + ( - 10) * R2 + (10) * S2, ( - 2048) * A * S2^4 * V + ( - 2048) * Y2 * S2^3 * V + (7168) * A * S2^3 * V + (128) * A * R2^2 * V + (5120) * Y2 * S2^2 * V + ( - 9088) * A * S2^2 * V + (2048) * Y1 * Y2^2 + ( - 2048) * Y2^3 + ( - 512) * A * R2 * S2 + ( - 2048) * Y1 * S2^2 + (2048) * Y2 * S2^2 + (128) * Y1 * R2 * V + ( - 256) * A * R2 * V + ( - 256) * Y1 * S2 * V + ( - 3968) * Y2 * S2 * V + (4992) * A * S2 * V + (640) * A * R2 + (3584) * Y1 * S2 + ( - 4096) * Y2 * S2 + (384) * A * S2 + (64) * Y1 * V + (960) * Y2 * V + ( - 896) * A * V + ( - 1408) * Y1 + (1920) * Y2 + ( - 448) * A, (2048) * X1 * S2^4 * V + ( - 6656) * X1 * S2^3 * V + (512) * X2 * S2^3 * V + ( - 128) * X2 * R2^2 * V + (7808) * X1 * S2^2 * V + ( - 1280) * X2 * S2^2 * V + ( - 1024) * X1 * Y2^2 + (1024) * X2 * Y2^2 + (512) * X2 * R2 * S2 + (512) * X1 * S2^2 + ( - 512) * X2 * S2^2 + ( - 32) * X1 * R2 * V + (224) * X2 * R2 * V + ( - 3872) * X1 * S2 * V + (992) * X2 * S2 * V + ( - 640) * X2 * R2 + ( - 896) * X1 * S2 + (768) * X2 * S2 + (704) * X1 * V + ( - 320) * X2 * V + (352) * X1 + ( - 160) * X2, (1024) * Y1^3 * S2 * V + ( - 1024) * Y1 * Y2^2 * S2 * V + ( - 768) * Y1^3 * V + ( - 256) * Y1^2 * Y2 * V + (768) * Y1 * Y2^2 * V + (256) * Y2^3 * V + ( - 512) * Y2 * S2^2 * V + ( - 256) * A * S2^2 * V + (1024) * Y1^2 * Y2 + ( - 1024) * Y1 * Y2^2 + ( - 256) * A * R2^2 + ( - 1024) * Y1 * R2 * S2 + (512) * A * R2 * S2 + (1024) * Y1 * S2^2 + ( - 256) * A * S2^2 + ( - 128) * Y1 * R2 * V + ( - 64) * A * R2 * V + (128) * Y1 * S2 * V + (768) * Y2 * S2 * V + (448) * A * S2 * V + (1024) * Y1 * R2 + (256) * A * R2 + ( - 512) * Y1 * S2 + ( - 512) * Y2 * S2 + ( - 256) * A * S2 + ( - 256) * Y2 * V + ( - 128) * A * V + ( - 384) * Y1 + (256) * Y2 + ( - 64) * A, ( - 512) * X1 * Y1^2 * S2 * V + (512) * X1 * Y2^2 * S2 * V + (384) * X1 * Y1^2 * V + (128) * X1 * Y1 * Y2 * V + ( - 384) * X1 * Y2^2 * V + ( - 128) * X2 * Y2^2 * V + (256) * X1 * S2^2 * V + (256) * X2 * S2^2 * V + ( - 512) * X1 * Y1 * Y2 + (512) * X1 * Y2^2 + (256) * X2 * R2^2 + (256) * X1 * R2 * S2 + ( - 256) * X2 * R2 * S2 + ( - 256) * X1 * S2^2 + (64) * X1 * R2 * V + (64) * X2 * R2 * V + ( - 448) * X1 * S2 * V + ( - 448) * X2 * S2 * V + ( - 384) * X1 * R2 + ( - 384) * X2 * R2 + (384) * X1 * S2 + (384) * X2 * S2 + (128) * X1 * V + (128) * X2 * V + (64) * X1 + (64) * X2, (256) * A^2 * S2^3 * V + ( - 704) * A^2 * S2^2 * V + ( - 16) * A^2 * R2 * V + (256) * Y1^2 * S2 * V + ( - 256) * Y1 * Y2 * S2 * V + (624) * A^2 * S2 * V + ( - 256) * S2^3 * V + (64) * A^2 * R2 + ( - 192) * Y1^2 * V + (128) * Y1 * Y2 * V + (64) * Y2^2 * V + ( - 160) * A^2 * V + (576) * S2^2 * V + (256) * Y1 * Y2 + ( - 256) * Y2^2 + ( - 80) * A^2 + ( - 256) * R2 * S2 + (256) * S2^2 + ( - 16) * R2 * V + ( - 400) * S2 * V + (256) * R2 + ( - 320) * S2 + (96) * V + (48), (64) * X1 * A * S2^3 * V + ( - 192) * X1 * A * S2^2 * V + (16) * X2 * A * S2^2 * V + ( - 4) * X2 * A * R2 * V + (32) * X1 * Y1 * S2 * V + ( - 32) * X1 * Y2 * S2 * V + (176) * X1 * A * S2 * V + ( - 20) * X2 * A * S2 * V + (16) * X2 * A * R2 + (16) * X1 * A * S2 + ( - 16) * X2 * A * S2 + ( - 24) * X1 * Y1 * V + (16) * X1 * Y2 * V + (8) * X2 * Y2 * V + ( - 48) * X1 * A * V + (8) * X2 * A * V + (32) * X1 * Y2 + ( - 32) * X2 * Y2 + ( - 24) * X1 * A + (4) * X2 * A, ( - 512) * Y2^2 * S2^2 * V + (128) * A^2 * S2^2 * V + (512) * S2^4 * V + (2048) * Y1^2 * Y2^2 + ( - 2048) * Y1 * Y2^3 + ( - 2048) * Y1^2 * S2^2 + (2048) * Y1 * Y2 * S2^2 + (128) * Y1^2 * R2 * V + ( - 32) * A^2 * R2 * V + ( - 128) * R2^3 * V + ( - 256) * Y1^2 * S2 * V + (896) * Y2^2 * S2 * V + ( - 160) * A^2 * S2 * V + ( - 1920) * S2^3 * V + (256) * A^2 * R2 + (3584) * Y1^2 * S2 + ( - 3072) * Y1 * Y2 * S2 + ( - 512) * Y2^2 * S2 + ( - 256) * A^2 * S2 + (512) * R2^2 * S2 + ( - 1024) * R2 * S2^2 + (512) * S2^3 + (64) * Y1^2 * V + ( - 320) * Y2^2 * V + (64) * A^2 * V + (384) * R2^2 * V + (2496) * S2^2 * V + ( - 1408) * Y1^2 + (1408) * Y1 * Y2 + ( - 128) * Y2^2 + (32) * A^2 + ( - 640) * R2^2 + (640) * R2 * S2 + (128) * S2^2 + ( - 336) * R2 * V + ( - 1360) * S2 * V + (320) * R2 + ( - 640) * S2 + (352) * V + (176), ( - 2048) * Y1^2 * R2^2 * V + (2048) * R2^4 * V + (512) * A^2 * S2^2 * V + ( - 8192) * Y1^3 * Y2 + (8192) * Y1^2 * Y2^2 + (8192) * Y1^2 * R2 * S2 + ( - 2048) * A^2 * R2 * S2 + ( - 8192) * Y1^2 * S2^2 + (2048) * A^2 * S2^2 + (3584) * Y1^2 * R2 * V + (128) * A^2 * R2 * V + ( - 7680) * R2^3 * V + ( - 2048) * Y1^2 * S2 * V + (1024) * Y1 * Y2 * S2 * V + (512) * Y2^2 * S2 * V + ( - 896) * A^2 * S2 * V + ( - 512) * S2^3 * V + ( - 6144) * Y1^2 * R2 + (512) * A^2 * R2 + ( - 2048) * R2^3 + (6144) * Y1 * Y2 * S2 + ( - 512) * A^2 * S2 + (8192) * R2^2 * S2 + ( - 6144) * R2 * S2^2 + (256) * Y1^2 * V + ( - 512) * Y1 * Y2 * V + ( - 768) * Y2^2 * V + (256) * A^2 * V + (10496) * R2^2 * V + (1536) * S2^2 * V + (1536) * Y1^2 + ( - 1536) * Y1 * Y2 + ( - 512) * Y2^2 + (128) * A^2 + (2560) * R2^2 + ( - 6656) * R2 * S2 + (4608) * S2^2 + ( - 6080) * R2 * V + ( - 1472) * S2 * V + ( - 1536) * R2 + (256) * S2 + (1664) * V + (832), ( - 262144) * Y1^3 * Y2^2 + (262144) * Y1^2 * Y2^3 + (262144) * Y1^3 * S2^2 + ( - 262144) * Y1 * Y2^2 * S2^2 + ( - 65536) * A * R2^2 * S2^2 + ( - 262144) * Y1 * R2 * S2^3 + (131072) * A * R2 * S2^3 + (262144) * Y1 * S2^4 + ( - 65536) * A * S2^4 + ( - 16384) * Y1^3 * R2 * V + (2048) * A^3 * R2 * V + (16384) * Y1 * R2^3 * V + (16384) * Y2^3 * S2 * V + ( - 2048) * A^3 * S2 * V + ( - 16384) * Y2 * S2^3 * V + ( - 16384) * A^3 * R2 + ( - 458752) * Y1^3 * S2 + (393216) * Y1 * Y2^2 * S2 + (65536) * Y2^3 * S2 + (16384) * A^3 * S2 + ( - 65536) * Y1 * R2^2 * S2 + (81920) * A * R2^2 * S2 + (720896) * Y1 * R2 * S2^2 + ( - 98304) * A * R2 * S2^2 + ( - 524288) * Y1 * S2^3 + ( - 131072) * Y2 * S2^3 + (16384) * A * S2^3 + (16384) * Y1^3 * V + (8192) * Y1^2 * Y2 * V + ( - 8192) * Y1 * Y2^2 * V + ( - 16384) * Y2^3 * V + ( - 49152) * Y1 * R2^2 * V + ( - 6144) * A * R2^2 * V + (49152) * Y2 * S2^2 * V + (6144) * A * S2^2 * V + (180224) * Y1^3 + ( - 65536) * Y1^2 * Y2 + ( - 81920) * Y1 * Y2^2 + ( - 32768) * Y2^3 + (81920) * Y1 * R2^2 + (16384) * A * R2^2 + ( - 507904) * Y1 * R2 * S2 + ( - 90112) * A * R2 * S2 + (180224) * Y1 * S2^2 + (245760) * Y2 * S2^2 + (73728) * A * S2^2 + (45056) * Y1 * R2 * V + (10240) * A * R2 * V + ( - 45056) * Y2 * S2 * V + ( - 10240) * A * S2 * V + (49152) * Y1 * R2 + (6144) * A * R2 + (90112) * Y1 * S2 + ( - 139264) * Y2 * S2 + ( - 6144) * A * S2 + ( - 12288) * Y1 * V + (12288) * Y2 * V + ( - 24576) * Y1 + (24576) * Y2, (131072) * X1 * Y1^2 * Y2^2 + ( - 131072) * X1 * Y1 * Y2^3 + ( - 131072) * X1 * Y1^2 * S2^2 + (131072) * X1 * Y2^2 * S2^2 + (65536) * X2 * R2^2 * S2^2 + (65536) * X1 * R2 * S2^3 + ( - 65536) * X2 * R2 * S2^3 + ( - 65536) * X1 * S2^4 + (8192) * X1 * Y1^2 * R2 * V + ( - 2048) * X2 * A^2 * R2 * V + ( - 8192) * X1 * R2^3 * V + ( - 8192) * X2 * Y2^2 * S2 * V + (2048) * X2 * A^2 * S2 * V + (8192) * X2 * S2^3 * V + (16384) * X2 * A^2 * R2 + (229376) * X1 * Y1^2 * S2 + ( - 196608) * X1 * Y2^2 * S2 + ( - 32768) * X2 * Y2^2 * S2 + ( - 16384) * X2 * A^2 * S2 + (32768) * X1 * R2^2 * S2 + ( - 81920) * X2 * R2^2 * S2 + ( - 245760) * X1 * R2 * S2^2 + ( - 16384) * X2 * R2 * S2^2 + (212992) * X1 * S2^3 + (98304) * X2 * S2^3 + ( - 8192) * X1 * Y1^2 * V + ( - 4096) * X1 * Y1 * Y2 * V + (4096) * X1 * Y2^2 * V + (8192) * X2 * Y2^2 * V + (24576) * X1 * R2^2 * V + (6144) * X2 * R2^2 * V + ( - 2048) * X1 * S2^2 * V + ( - 24576) * X2 * S2^2 * V + ( - 90112) * X1 * Y1^2 + (32768) * X1 * Y1 * Y2 + (40960) * X1 * Y2^2 + (16384) * X2 * Y2^2 + ( - 40960) * X1 * R2^2 + ( - 16384) * X2 * R2^2 + (229376) * X1 * R2 * S2 + (147456) * X2 * R2 * S2 + ( - 188416) * X1 * S2^2 + ( - 131072) * X2 * S2^2 + ( - 24064) * X1 * R2 * V + ( - 9728) * X2 * R2 * V + (4608) * X1 * S2 * V + (23040) * X2 * S2 * V + ( - 32768) * X1 * R2 + ( - 14336) * X2 * R2 + (30720) * X1 * S2 + (16384) * X2 * S2 + (5120) * X1 * V + ( - 3072) * X2 * V + (2560) * X1 + ( - 1536) * X2, (512) * X2 * A * S2^3 * V + ( - 128) * X1 * A * R2^2 * V + (512) * X2 * Y2 * S2^2 * V + ( - 128) * X1 * A * S2^2 * V + ( - 1408) * X2 * A * S2^2 * V + ( - 2048) * X1 * Y1 * Y2^2 + (2048) * X1 * Y2^3 + (512) * X1 * A * R2 * S2 + ( - 512) * X2 * A * R2 * S2 + (2048) * X1 * Y1 * S2^2 + ( - 2048) * X1 * Y2 * S2^2 + ( - 512) * X1 * A * S2^2 + (512) * X2 * A * S2^2 + ( - 128) * X1 * Y1 * R2 * V + (256) * X1 * A * R2 * V + (32) * X2 * A * R2 * V + (256) * X1 * Y1 * S2 * V + ( - 896) * X2 * Y2 * S2 * V + (128) * X1 * A * S2 * V + (1184) * X2 * A * S2 * V + ( - 640) * X1 * A * R2 + (256) * X2 * A * R2 + ( - 3584) * X1 * Y1 * S2 + (3072) * X1 * Y2 * S2 + (512) * X2 * Y2 * S2 + (640) * X1 * A * S2 + ( - 128) * X2 * A * S2 + ( - 64) * X1 * Y1 * V + (320) * X2 * Y2 * V + ( - 128) * X1 * A * V + ( - 320) * X2 * A * V + (1408) * X1 * Y1 + ( - 1152) * X1 * Y2 + ( - 128) * X2 * Y2 + ( - 64) * X1 * A + ( - 160) * X2 * A ]
Note: See TracBrowser for help on using the repository browser.