UNB/ CS/ David Bremner/ research/ sparks lp/ PM4-gmpl
set INPUTS := {'x34','x24','x12','x13','x14','x23'};
set OUTPUTS := {'w'};
param tmax := 24;
param lmax := 23;
param bits := 2;
param c{INPUTS};
param d{OUTPUTS};
var S{1..lmax,1..tmax},>=0,<=1;
var x34,>=0,<=1;
var x24,>=0,<=1;
var x12,>=0,<=1;
var x13,>=0,<=1;
var x14,>=0,<=1;
var x23,>=0,<=1;
var w,>=0,<=1;
var guard2{0..tmax-1},>=0,<=1;
var guard0{0..tmax-1},>=0,<=1;
var guard4{0..tmax-1},>=0,<=1;
maximize obj: 0+c['x34']*x34+c['x24']*x24+c['x12']*x12+c['x13']*x13+c['x14']*x14+c['x23']*x23+d['w']*w;
C_0 : 0 = guard2[0];
C_1 : 0 = guard0[0];
C_2 : 0 = guard4[0];
D1 : 1 = S[1,1];
D2 : 0 = S[2,1];
D3 : 0 = S[3,1];
D4 : 0 = S[4,1];
D5 : 0 = S[5,1];
D6 : 0 = S[6,1];
D7 : 0 = S[7,1];
D8 : 0 = S[8,1];
D9 : 0 = S[9,1];
D10 : 0 = S[10,1];
D11 : 0 = S[11,1];
D12 : 0 = S[12,1];
D13 : 0 = S[13,1];
D14 : 0 = S[14,1];
D15 : 0 = S[15,1];
D16 : 0 = S[16,1];
D17 : 0 = S[17,1];
D18 : 0 = S[18,1];
D19 : 0 = S[19,1];
D20 : 0 = S[20,1];
D21 : 0 = S[21,1];
D22 : 0 = S[22,1];
E1 : 1 = S[1,1] + S[10,1] + S[11,1] + S[12,1] + S[13,1] + S[14,1] + S[15,1] + S[16,1] + S[17,1] + S[18,1] + S[19,1] + S[2,1] + S[20,1] + S[21,1] + S[22,1] + S[23,1] + S[3,1] + S[4,1] + S[5,1] + S[6,1] + S[7,1] + S[8,1] + S[9,1];
E2 : 1 = S[1,2] + S[10,2] + S[11,2] + S[12,2] + S[13,2] + S[14,2] + S[15,2] + S[16,2] + S[17,2] + S[18,2] + S[19,2] + S[2,2] + S[20,2] + S[21,2] + S[22,2] + S[23,2] + S[3,2] + S[4,2] + S[5,2] + S[6,2] + S[7,2] + S[8,2] + S[9,2];
E3 : 1 = S[1,3] + S[10,3] + S[11,3] + S[12,3] + S[13,3] + S[14,3] + S[15,3] + S[16,3] + S[17,3] + S[18,3] + S[19,3] + S[2,3] + S[20,3] + S[21,3] + S[22,3] + S[23,3] + S[3,3] + S[4,3] + S[5,3] + S[6,3] + S[7,3] + S[8,3] + S[9,3];
E4 : 1 = S[1,4] + S[10,4] + S[11,4] + S[12,4] + S[13,4] + S[14,4] + S[15,4] + S[16,4] + S[17,4] + S[18,4] + S[19,4] + S[2,4] + S[20,4] + S[21,4] + S[22,4] + S[23,4] + S[3,4] + S[4,4] + S[5,4] + S[6,4] + S[7,4] + S[8,4] + S[9,4];
E5 : 1 = S[1,5] + S[10,5] + S[11,5] + S[12,5] + S[13,5] + S[14,5] + S[15,5] + S[16,5] + S[17,5] + S[18,5] + S[19,5] + S[2,5] + S[20,5] + S[21,5] + S[22,5] + S[23,5] + S[3,5] + S[4,5] + S[5,5] + S[6,5] + S[7,5] + S[8,5] + S[9,5];
E6 : 1 = S[1,6] + S[10,6] + S[11,6] + S[12,6] + S[13,6] + S[14,6] + S[15,6] + S[16,6] + S[17,6] + S[18,6] + S[19,6] + S[2,6] + S[20,6] + S[21,6] + S[22,6] + S[23,6] + S[3,6] + S[4,6] + S[5,6] + S[6,6] + S[7,6] + S[8,6] + S[9,6];
E7 : 1 = S[1,7] + S[10,7] + S[11,7] + S[12,7] + S[13,7] + S[14,7] + S[15,7] + S[16,7] + S[17,7] + S[18,7] + S[19,7] + S[2,7] + S[20,7] + S[21,7] + S[22,7] + S[23,7] + S[3,7] + S[4,7] + S[5,7] + S[6,7] + S[7,7] + S[8,7] + S[9,7];
E8 : 1 = S[1,8] + S[10,8] + S[11,8] + S[12,8] + S[13,8] + S[14,8] + S[15,8] + S[16,8] + S[17,8] + S[18,8] + S[19,8] + S[2,8] + S[20,8] + S[21,8] + S[22,8] + S[23,8] + S[3,8] + S[4,8] + S[5,8] + S[6,8] + S[7,8] + S[8,8] + S[9,8];
E9 : 1 = S[1,9] + S[10,9] + S[11,9] + S[12,9] + S[13,9] + S[14,9] + S[15,9] + S[16,9] + S[17,9] + S[18,9] + S[19,9] + S[2,9] + S[20,9] + S[21,9] + S[22,9] + S[23,9] + S[3,9] + S[4,9] + S[5,9] + S[6,9] + S[7,9] + S[8,9] + S[9,9];
E10 : 1 = S[1,10] + S[10,10] + S[11,10] + S[12,10] + S[13,10] + S[14,10] + S[15,10] + S[16,10] + S[17,10] + S[18,10] + S[19,10] + S[2,10] + S[20,10] + S[21,10] + S[22,10] + S[23,10] + S[3,10] + S[4,10] + S[5,10] + S[6,10] + S[7,10] + S[8,10] + S[9,10];
E11 : 1 = S[1,11] + S[10,11] + S[11,11] + S[12,11] + S[13,11] + S[14,11] + S[15,11] + S[16,11] + S[17,11] + S[18,11] + S[19,11] + S[2,11] + S[20,11] + S[21,11] + S[22,11] + S[23,11] + S[3,11] + S[4,11] + S[5,11] + S[6,11] + S[7,11] + S[8,11] + S[9,11];
E12 : 1 = S[1,12] + S[10,12] + S[11,12] + S[12,12] + S[13,12] + S[14,12] + S[15,12] + S[16,12] + S[17,12] + S[18,12] + S[19,12] + S[2,12] + S[20,12] + S[21,12] + S[22,12] + S[23,12] + S[3,12] + S[4,12] + S[5,12] + S[6,12] + S[7,12] + S[8,12] + S[9,12];
E13 : 1 = S[1,13] + S[10,13] + S[11,13] + S[12,13] + S[13,13] + S[14,13] + S[15,13] + S[16,13] + S[17,13] + S[18,13] + S[19,13] + S[2,13] + S[20,13] + S[21,13] + S[22,13] + S[23,13] + S[3,13] + S[4,13] + S[5,13] + S[6,13] + S[7,13] + S[8,13] + S[9,13];
E14 : 1 = S[1,14] + S[10,14] + S[11,14] + S[12,14] + S[13,14] + S[14,14] + S[15,14] + S[16,14] + S[17,14] + S[18,14] + S[19,14] + S[2,14] + S[20,14] + S[21,14] + S[22,14] + S[23,14] + S[3,14] + S[4,14] + S[5,14] + S[6,14] + S[7,14] + S[8,14] + S[9,14];
E15 : 1 = S[1,15] + S[10,15] + S[11,15] + S[12,15] + S[13,15] + S[14,15] + S[15,15] + S[16,15] + S[17,15] + S[18,15] + S[19,15] + S[2,15] + S[20,15] + S[21,15] + S[22,15] + S[23,15] + S[3,15] + S[4,15] + S[5,15] + S[6,15] + S[7,15] + S[8,15] + S[9,15];
E16 : 1 = S[1,16] + S[10,16] + S[11,16] + S[12,16] + S[13,16] + S[14,16] + S[15,16] + S[16,16] + S[17,16] + S[18,16] + S[19,16] + S[2,16] + S[20,16] + S[21,16] + S[22,16] + S[23,16] + S[3,16] + S[4,16] + S[5,16] + S[6,16] + S[7,16] + S[8,16] + S[9,16];
E17 : 1 = S[1,17] + S[10,17] + S[11,17] + S[12,17] + S[13,17] + S[14,17] + S[15,17] + S[16,17] + S[17,17] + S[18,17] + S[19,17] + S[2,17] + S[20,17] + S[21,17] + S[22,17] + S[23,17] + S[3,17] + S[4,17] + S[5,17] + S[6,17] + S[7,17] + S[8,17] + S[9,17];
E18 : 1 = S[1,18] + S[10,18] + S[11,18] + S[12,18] + S[13,18] + S[14,18] + S[15,18] + S[16,18] + S[17,18] + S[18,18] + S[19,18] + S[2,18] + S[20,18] + S[21,18] + S[22,18] + S[23,18] + S[3,18] + S[4,18] + S[5,18] + S[6,18] + S[7,18] + S[8,18] + S[9,18];
E19 : 1 = S[1,19] + S[10,19] + S[11,19] + S[12,19] + S[13,19] + S[14,19] + S[15,19] + S[16,19] + S[17,19] + S[18,19] + S[19,19] + S[2,19] + S[20,19] + S[21,19] + S[22,19] + S[23,19] + S[3,19] + S[4,19] + S[5,19] + S[6,19] + S[7,19] + S[8,19] + S[9,19];
E20 : 1 = S[1,20] + S[10,20] + S[11,20] + S[12,20] + S[13,20] + S[14,20] + S[15,20] + S[16,20] + S[17,20] + S[18,20] + S[19,20] + S[2,20] + S[20,20] + S[21,20] + S[22,20] + S[23,20] + S[3,20] + S[4,20] + S[5,20] + S[6,20] + S[7,20] + S[8,20] + S[9,20];
E21 : 1 = S[1,21] + S[10,21] + S[11,21] + S[12,21] + S[13,21] + S[14,21] + S[15,21] + S[16,21] + S[17,21] + S[18,21] + S[19,21] + S[2,21] + S[20,21] + S[21,21] + S[22,21] + S[23,21] + S[3,21] + S[4,21] + S[5,21] + S[6,21] + S[7,21] + S[8,21] + S[9,21];
E22 : 1 = S[1,22] + S[10,22] + S[11,22] + S[12,22] + S[13,22] + S[14,22] + S[15,22] + S[16,22] + S[17,22] + S[18,22] + S[19,22] + S[2,22] + S[20,22] + S[21,22] + S[22,22] + S[23,22] + S[3,22] + S[4,22] + S[5,22] + S[6,22] + S[7,22] + S[8,22] + S[9,22];
E23 : 1 = S[1,23] + S[10,23] + S[11,23] + S[12,23] + S[13,23] + S[14,23] + S[15,23] + S[16,23] + S[17,23] + S[18,23] + S[19,23] + S[2,23] + S[20,23] + S[21,23] + S[22,23] + S[23,23] + S[3,23] + S[4,23] + S[5,23] + S[6,23] + S[7,23] + S[8,23] + S[9,23];
E24 : 1 = S[1,24] + S[10,24] + S[11,24] + S[12,24] + S[13,24] + S[14,24] + S[15,24] + S[16,24] + S[17,24] + S[18,24] + S[19,24] + S[2,24] + S[20,24] + S[21,24] + S[22,24] + S[23,24] + S[3,24] + S[4,24] + S[5,24] + S[6,24] + S[7,24] + S[8,24] + S[9,24];
F_o_1_1 : 0 <= -S[1,1] + S[2,2];
F_o_1_2 : 0 <= -S[1,2] + S[2,3];
F_o_1_3 : 0 <= -S[1,3] + S[2,4];
F_o_1_4 : 0 <= -S[1,4] + S[2,5];
F_o_1_5 : 0 <= -S[1,5] + S[2,6];
F_o_1_6 : 0 <= -S[1,6] + S[2,7];
F_o_1_7 : 0 <= -S[1,7] + S[2,8];
F_o_1_8 : 0 <= -S[1,8] + S[2,9];
F_o_1_9 : 0 <= -S[1,9] + S[2,10];
F_o_1_10 : 0 <= -S[1,10] + S[2,11];
F_o_1_11 : 0 <= -S[1,11] + S[2,12];
F_o_1_12 : 0 <= -S[1,12] + S[2,13];
F_o_1_13 : 0 <= -S[1,13] + S[2,14];
F_o_1_14 : 0 <= -S[1,14] + S[2,15];
F_o_1_15 : 0 <= -S[1,15] + S[2,16];
F_o_1_16 : 0 <= -S[1,16] + S[2,17];
F_o_1_17 : 0 <= -S[1,17] + S[2,18];
F_o_1_18 : 0 <= -S[1,18] + S[2,19];
F_o_1_19 : 0 <= -S[1,19] + S[2,20];
F_o_1_20 : 0 <= -S[1,20] + S[2,21];
F_o_1_21 : 0 <= -S[1,21] + S[2,22];
F_o_1_22 : 0 <= -S[1,22] + S[2,23];
F_o_1_23 : 0 <= -S[1,23] + S[2,24];
F_o_2_1 : 0 <= -S[2,1] + S[3,2];
F_o_2_2 : 0 <= -S[2,2] + S[3,3];
F_o_2_3 : 0 <= -S[2,3] + S[3,4];
F_o_2_4 : 0 <= -S[2,4] + S[3,5];
F_o_2_5 : 0 <= -S[2,5] + S[3,6];
F_o_2_6 : 0 <= -S[2,6] + S[3,7];
F_o_2_7 : 0 <= -S[2,7] + S[3,8];
F_o_2_8 : 0 <= -S[2,8] + S[3,9];
F_o_2_9 : 0 <= -S[2,9] + S[3,10];
F_o_2_10 : 0 <= -S[2,10] + S[3,11];
F_o_2_11 : 0 <= -S[2,11] + S[3,12];
F_o_2_12 : 0 <= -S[2,12] + S[3,13];
F_o_2_13 : 0 <= -S[2,13] + S[3,14];
F_o_2_14 : 0 <= -S[2,14] + S[3,15];
F_o_2_15 : 0 <= -S[2,15] + S[3,16];
F_o_2_16 : 0 <= -S[2,16] + S[3,17];
F_o_2_17 : 0 <= -S[2,17] + S[3,18];
F_o_2_18 : 0 <= -S[2,18] + S[3,19];
F_o_2_19 : 0 <= -S[2,19] + S[3,20];
F_o_2_20 : 0 <= -S[2,20] + S[3,21];
F_o_2_21 : 0 <= -S[2,21] + S[3,22];
F_o_2_22 : 0 <= -S[2,22] + S[3,23];
F_o_2_23 : 0 <= -S[2,23] + S[3,24];
F_o_3_1 : 0 <= -S[3,1] + S[4,2];
F_o_3_2 : 0 <= -S[3,2] + S[4,3];
F_o_3_3 : 0 <= -S[3,3] + S[4,4];
F_o_3_4 : 0 <= -S[3,4] + S[4,5];
F_o_3_5 : 0 <= -S[3,5] + S[4,6];
F_o_3_6 : 0 <= -S[3,6] + S[4,7];
F_o_3_7 : 0 <= -S[3,7] + S[4,8];
F_o_3_8 : 0 <= -S[3,8] + S[4,9];
F_o_3_9 : 0 <= -S[3,9] + S[4,10];
F_o_3_10 : 0 <= -S[3,10] + S[4,11];
F_o_3_11 : 0 <= -S[3,11] + S[4,12];
F_o_3_12 : 0 <= -S[3,12] + S[4,13];
F_o_3_13 : 0 <= -S[3,13] + S[4,14];
F_o_3_14 : 0 <= -S[3,14] + S[4,15];
F_o_3_15 : 0 <= -S[3,15] + S[4,16];
F_o_3_16 : 0 <= -S[3,16] + S[4,17];
F_o_3_17 : 0 <= -S[3,17] + S[4,18];
F_o_3_18 : 0 <= -S[3,18] + S[4,19];
F_o_3_19 : 0 <= -S[3,19] + S[4,20];
F_o_3_20 : 0 <= -S[3,20] + S[4,21];
F_o_3_21 : 0 <= -S[3,21] + S[4,22];
F_o_3_22 : 0 <= -S[3,22] + S[4,23];
F_o_3_23 : 0 <= -S[3,23] + S[4,24];
F_o_4_1 : 0 <= -S[4,1] + S[5,2];
F_o_4_2 : 0 <= -S[4,2] + S[5,3];
F_o_4_3 : 0 <= -S[4,3] + S[5,4];
F_o_4_4 : 0 <= -S[4,4] + S[5,5];
F_o_4_5 : 0 <= -S[4,5] + S[5,6];
F_o_4_6 : 0 <= -S[4,6] + S[5,7];
F_o_4_7 : 0 <= -S[4,7] + S[5,8];
F_o_4_8 : 0 <= -S[4,8] + S[5,9];
F_o_4_9 : 0 <= -S[4,9] + S[5,10];
F_o_4_10 : 0 <= -S[4,10] + S[5,11];
F_o_4_11 : 0 <= -S[4,11] + S[5,12];
F_o_4_12 : 0 <= -S[4,12] + S[5,13];
F_o_4_13 : 0 <= -S[4,13] + S[5,14];
F_o_4_14 : 0 <= -S[4,14] + S[5,15];
F_o_4_15 : 0 <= -S[4,15] + S[5,16];
F_o_4_16 : 0 <= -S[4,16] + S[5,17];
F_o_4_17 : 0 <= -S[4,17] + S[5,18];
F_o_4_18 : 0 <= -S[4,18] + S[5,19];
F_o_4_19 : 0 <= -S[4,19] + S[5,20];
F_o_4_20 : 0 <= -S[4,20] + S[5,21];
F_o_4_21 : 0 <= -S[4,21] + S[5,22];
F_o_4_22 : 0 <= -S[4,22] + S[5,23];
F_o_4_23 : 0 <= -S[4,23] + S[5,24];
F_o_5_1 : 0 <= -S[5,1] + S[6,2];
F_o_5_2 : 0 <= -S[5,2] + S[6,3];
F_o_5_3 : 0 <= -S[5,3] + S[6,4];
F_o_5_4 : 0 <= -S[5,4] + S[6,5];
F_o_5_5 : 0 <= -S[5,5] + S[6,6];
F_o_5_6 : 0 <= -S[5,6] + S[6,7];
F_o_5_7 : 0 <= -S[5,7] + S[6,8];
F_o_5_8 : 0 <= -S[5,8] + S[6,9];
F_o_5_9 : 0 <= -S[5,9] + S[6,10];
F_o_5_10 : 0 <= -S[5,10] + S[6,11];
F_o_5_11 : 0 <= -S[5,11] + S[6,12];
F_o_5_12 : 0 <= -S[5,12] + S[6,13];
F_o_5_13 : 0 <= -S[5,13] + S[6,14];
F_o_5_14 : 0 <= -S[5,14] + S[6,15];
F_o_5_15 : 0 <= -S[5,15] + S[6,16];
F_o_5_16 : 0 <= -S[5,16] + S[6,17];
F_o_5_17 : 0 <= -S[5,17] + S[6,18];
F_o_5_18 : 0 <= -S[5,18] + S[6,19];
F_o_5_19 : 0 <= -S[5,19] + S[6,20];
F_o_5_20 : 0 <= -S[5,20] + S[6,21];
F_o_5_21 : 0 <= -S[5,21] + S[6,22];
F_o_5_22 : 0 <= -S[5,22] + S[6,23];
F_o_5_23 : 0 <= -S[5,23] + S[6,24];
F_o_6_1 : 0 <= -S[6,1] + S[7,2];
F_o_6_2 : 0 <= -S[6,2] + S[7,3];
F_o_6_3 : 0 <= -S[6,3] + S[7,4];
F_o_6_4 : 0 <= -S[6,4] + S[7,5];
F_o_6_5 : 0 <= -S[6,5] + S[7,6];
F_o_6_6 : 0 <= -S[6,6] + S[7,7];
F_o_6_7 : 0 <= -S[6,7] + S[7,8];
F_o_6_8 : 0 <= -S[6,8] + S[7,9];
F_o_6_9 : 0 <= -S[6,9] + S[7,10];
F_o_6_10 : 0 <= -S[6,10] + S[7,11];
F_o_6_11 : 0 <= -S[6,11] + S[7,12];
F_o_6_12 : 0 <= -S[6,12] + S[7,13];
F_o_6_13 : 0 <= -S[6,13] + S[7,14];
F_o_6_14 : 0 <= -S[6,14] + S[7,15];
F_o_6_15 : 0 <= -S[6,15] + S[7,16];
F_o_6_16 : 0 <= -S[6,16] + S[7,17];
F_o_6_17 : 0 <= -S[6,17] + S[7,18];
F_o_6_18 : 0 <= -S[6,18] + S[7,19];
F_o_6_19 : 0 <= -S[6,19] + S[7,20];
F_o_6_20 : 0 <= -S[6,20] + S[7,21];
F_o_6_21 : 0 <= -S[6,21] + S[7,22];
F_o_6_22 : 0 <= -S[6,22] + S[7,23];
F_o_6_23 : 0 <= -S[6,23] + S[7,24];
F_o_7_1 : 0 <= -S[7,1] + S[8,2];
F_o_7_2 : 0 <= -S[7,2] + S[8,3];
F_o_7_3 : 0 <= -S[7,3] + S[8,4];
F_o_7_4 : 0 <= -S[7,4] + S[8,5];
F_o_7_5 : 0 <= -S[7,5] + S[8,6];
F_o_7_6 : 0 <= -S[7,6] + S[8,7];
F_o_7_7 : 0 <= -S[7,7] + S[8,8];
F_o_7_8 : 0 <= -S[7,8] + S[8,9];
F_o_7_9 : 0 <= -S[7,9] + S[8,10];
F_o_7_10 : 0 <= -S[7,10] + S[8,11];
F_o_7_11 : 0 <= -S[7,11] + S[8,12];
F_o_7_12 : 0 <= -S[7,12] + S[8,13];
F_o_7_13 : 0 <= -S[7,13] + S[8,14];
F_o_7_14 : 0 <= -S[7,14] + S[8,15];
F_o_7_15 : 0 <= -S[7,15] + S[8,16];
F_o_7_16 : 0 <= -S[7,16] + S[8,17];
F_o_7_17 : 0 <= -S[7,17] + S[8,18];
F_o_7_18 : 0 <= -S[7,18] + S[8,19];
F_o_7_19 : 0 <= -S[7,19] + S[8,20];
F_o_7_20 : 0 <= -S[7,20] + S[8,21];
F_o_7_21 : 0 <= -S[7,21] + S[8,22];
F_o_7_22 : 0 <= -S[7,22] + S[8,23];
F_o_7_23 : 0 <= -S[7,23] + S[8,24];
F_o_8_1 : 0 <= -S[8,1] + S[9,2];
F_o_8_2 : 0 <= -S[8,2] + S[9,3];
F_o_8_3 : 0 <= -S[8,3] + S[9,4];
F_o_8_4 : 0 <= -S[8,4] + S[9,5];
F_o_8_5 : 0 <= -S[8,5] + S[9,6];
F_o_8_6 : 0 <= -S[8,6] + S[9,7];
F_o_8_7 : 0 <= -S[8,7] + S[9,8];
F_o_8_8 : 0 <= -S[8,8] + S[9,9];
F_o_8_9 : 0 <= -S[8,9] + S[9,10];
F_o_8_10 : 0 <= -S[8,10] + S[9,11];
F_o_8_11 : 0 <= -S[8,11] + S[9,12];
F_o_8_12 : 0 <= -S[8,12] + S[9,13];
F_o_8_13 : 0 <= -S[8,13] + S[9,14];
F_o_8_14 : 0 <= -S[8,14] + S[9,15];
F_o_8_15 : 0 <= -S[8,15] + S[9,16];
F_o_8_16 : 0 <= -S[8,16] + S[9,17];
F_o_8_17 : 0 <= -S[8,17] + S[9,18];
F_o_8_18 : 0 <= -S[8,18] + S[9,19];
F_o_8_19 : 0 <= -S[8,19] + S[9,20];
F_o_8_20 : 0 <= -S[8,20] + S[9,21];
F_o_8_21 : 0 <= -S[8,21] + S[9,22];
F_o_8_22 : 0 <= -S[8,22] + S[9,23];
F_o_8_23 : 0 <= -S[8,23] + S[9,24];
F_o_9_1 : 0 <= S[10,2]-S[9,1];
F_o_9_2 : 0 <= S[10,3]-S[9,2];
F_o_9_3 : 0 <= S[10,4]-S[9,3];
F_o_9_4 : 0 <= S[10,5]-S[9,4];
F_o_9_5 : 0 <= S[10,6]-S[9,5];
F_o_9_6 : 0 <= S[10,7]-S[9,6];
F_o_9_7 : 0 <= S[10,8]-S[9,7];
F_o_9_8 : 0 <= S[10,9]-S[9,8];
F_o_9_9 : 0 <= S[10,10]-S[9,9];
F_o_9_10 : 0 <= S[10,11]-S[9,10];
F_o_9_11 : 0 <= S[10,12]-S[9,11];
F_o_9_12 : 0 <= S[10,13]-S[9,12];
F_o_9_13 : 0 <= S[10,14]-S[9,13];
F_o_9_14 : 0 <= S[10,15]-S[9,14];
F_o_9_15 : 0 <= S[10,16]-S[9,15];
F_o_9_16 : 0 <= S[10,17]-S[9,16];
F_o_9_17 : 0 <= S[10,18]-S[9,17];
F_o_9_18 : 0 <= S[10,19]-S[9,18];
F_o_9_19 : 0 <= S[10,20]-S[9,19];
F_o_9_20 : 0 <= S[10,21]-S[9,20];
F_o_9_21 : 0 <= S[10,22]-S[9,21];
F_o_9_22 : 0 <= S[10,23]-S[9,22];
F_o_9_23 : 0 <= S[10,24]-S[9,23];
F_iii_10_1_1 : -1 <= -S[10,1] + S[12,2]-guard0[1];
F_iii_10_1_2 : 0 <= -S[10,1] + S[11,2] + guard0[1];
F_iii_10_2_1 : -1 <= -S[10,2] + S[12,3]-guard0[2];
F_iii_10_2_2 : 0 <= -S[10,2] + S[11,3] + guard0[2];
F_iii_10_3_1 : -1 <= -S[10,3] + S[12,4]-guard0[3];
F_iii_10_3_2 : 0 <= -S[10,3] + S[11,4] + guard0[3];
F_iii_10_4_1 : -1 <= -S[10,4] + S[12,5]-guard0[4];
F_iii_10_4_2 : 0 <= -S[10,4] + S[11,5] + guard0[4];
F_iii_10_5_1 : -1 <= -S[10,5] + S[12,6]-guard0[5];
F_iii_10_5_2 : 0 <= -S[10,5] + S[11,6] + guard0[5];
F_iii_10_6_1 : -1 <= -S[10,6] + S[12,7]-guard0[6];
F_iii_10_6_2 : 0 <= -S[10,6] + S[11,7] + guard0[6];
F_iii_10_7_1 : -1 <= -S[10,7] + S[12,8]-guard0[7];
F_iii_10_7_2 : 0 <= -S[10,7] + S[11,8] + guard0[7];
F_iii_10_8_1 : -1 <= -S[10,8] + S[12,9]-guard0[8];
F_iii_10_8_2 : 0 <= -S[10,8] + S[11,9] + guard0[8];
F_iii_10_9_1 : -1 <= -S[10,9] + S[12,10]-guard0[9];
F_iii_10_9_2 : 0 <= -S[10,9] + S[11,10] + guard0[9];
F_iii_10_10_1 : -1 <= -S[10,10] + S[12,11]-guard0[10];
F_iii_10_10_2 : 0 <= -S[10,10] + S[11,11] + guard0[10];
F_iii_10_11_1 : -1 <= -S[10,11] + S[12,12]-guard0[11];
F_iii_10_11_2 : 0 <= -S[10,11] + S[11,12] + guard0[11];
F_iii_10_12_1 : -1 <= -S[10,12] + S[12,13]-guard0[12];
F_iii_10_12_2 : 0 <= -S[10,12] + S[11,13] + guard0[12];
F_iii_10_13_1 : -1 <= -S[10,13] + S[12,14]-guard0[13];
F_iii_10_13_2 : 0 <= -S[10,13] + S[11,14] + guard0[13];
F_iii_10_14_1 : -1 <= -S[10,14] + S[12,15]-guard0[14];
F_iii_10_14_2 : 0 <= -S[10,14] + S[11,15] + guard0[14];
F_iii_10_15_1 : -1 <= -S[10,15] + S[12,16]-guard0[15];
F_iii_10_15_2 : 0 <= -S[10,15] + S[11,16] + guard0[15];
F_iii_10_16_1 : -1 <= -S[10,16] + S[12,17]-guard0[16];
F_iii_10_16_2 : 0 <= -S[10,16] + S[11,17] + guard0[16];
F_iii_10_17_1 : -1 <= -S[10,17] + S[12,18]-guard0[17];
F_iii_10_17_2 : 0 <= -S[10,17] + S[11,18] + guard0[17];
F_iii_10_18_1 : -1 <= -S[10,18] + S[12,19]-guard0[18];
F_iii_10_18_2 : 0 <= -S[10,18] + S[11,19] + guard0[18];
F_iii_10_19_1 : -1 <= -S[10,19] + S[12,20]-guard0[19];
F_iii_10_19_2 : 0 <= -S[10,19] + S[11,20] + guard0[19];
F_iii_10_20_1 : -1 <= -S[10,20] + S[12,21]-guard0[20];
F_iii_10_20_2 : 0 <= -S[10,20] + S[11,21] + guard0[20];
F_iii_10_21_1 : -1 <= -S[10,21] + S[12,22]-guard0[21];
F_iii_10_21_2 : 0 <= -S[10,21] + S[11,22] + guard0[21];
F_iii_10_22_1 : -1 <= -S[10,22] + S[12,23]-guard0[22];
F_iii_10_22_2 : 0 <= -S[10,22] + S[11,23] + guard0[22];
F_iii_10_23_1 : -1 <= -S[10,23] + S[12,24]-guard0[23];
F_iii_10_23_2 : 0 <= -S[10,23] + S[11,24] + guard0[23];
F_o_11_1 : 0 <= -S[11,1] + S[11,2];
F_o_11_2 : 0 <= -S[11,2] + S[11,3];
F_o_11_3 : 0 <= -S[11,3] + S[11,4];
F_o_11_4 : 0 <= -S[11,4] + S[11,5];
F_o_11_5 : 0 <= -S[11,5] + S[11,6];
F_o_11_6 : 0 <= -S[11,6] + S[11,7];
F_o_11_7 : 0 <= -S[11,7] + S[11,8];
F_o_11_8 : 0 <= -S[11,8] + S[11,9];
F_o_11_9 : 0 <= S[11,10]-S[11,9];
F_o_11_10 : 0 <= -S[11,10] + S[11,11];
F_o_11_11 : 0 <= -S[11,11] + S[11,12];
F_o_11_12 : 0 <= -S[11,12] + S[11,13];
F_o_11_13 : 0 <= -S[11,13] + S[11,14];
F_o_11_14 : 0 <= -S[11,14] + S[11,15];
F_o_11_15 : 0 <= -S[11,15] + S[11,16];
F_o_11_16 : 0 <= -S[11,16] + S[11,17];
F_o_11_17 : 0 <= -S[11,17] + S[11,18];
F_o_11_18 : 0 <= -S[11,18] + S[11,19];
F_o_11_19 : 0 <= -S[11,19] + S[11,20];
F_o_11_20 : 0 <= -S[11,20] + S[11,21];
F_o_11_21 : 0 <= -S[11,21] + S[11,22];
F_o_11_22 : 0 <= -S[11,22] + S[11,23];
F_o_11_23 : 0 <= -S[11,23] + S[11,24];
F_o_12_1 : 0 <= -S[12,1] + S[13,2];
F_o_12_2 : 0 <= -S[12,2] + S[13,3];
F_o_12_3 : 0 <= -S[12,3] + S[13,4];
F_o_12_4 : 0 <= -S[12,4] + S[13,5];
F_o_12_5 : 0 <= -S[12,5] + S[13,6];
F_o_12_6 : 0 <= -S[12,6] + S[13,7];
F_o_12_7 : 0 <= -S[12,7] + S[13,8];
F_o_12_8 : 0 <= -S[12,8] + S[13,9];
F_o_12_9 : 0 <= -S[12,9] + S[13,10];
F_o_12_10 : 0 <= -S[12,10] + S[13,11];
F_o_12_11 : 0 <= -S[12,11] + S[13,12];
F_o_12_12 : 0 <= -S[12,12] + S[13,13];
F_o_12_13 : 0 <= -S[12,13] + S[13,14];
F_o_12_14 : 0 <= -S[12,14] + S[13,15];
F_o_12_15 : 0 <= -S[12,15] + S[13,16];
F_o_12_16 : 0 <= -S[12,16] + S[13,17];
F_o_12_17 : 0 <= -S[12,17] + S[13,18];
F_o_12_18 : 0 <= -S[12,18] + S[13,19];
F_o_12_19 : 0 <= -S[12,19] + S[13,20];
F_o_12_20 : 0 <= -S[12,20] + S[13,21];
F_o_12_21 : 0 <= -S[12,21] + S[13,22];
F_o_12_22 : 0 <= -S[12,22] + S[13,23];
F_o_12_23 : 0 <= -S[12,23] + S[13,24];
F_o_13_1 : 0 <= -S[13,1] + S[14,2];
F_o_13_2 : 0 <= -S[13,2] + S[14,3];
F_o_13_3 : 0 <= -S[13,3] + S[14,4];
F_o_13_4 : 0 <= -S[13,4] + S[14,5];
F_o_13_5 : 0 <= -S[13,5] + S[14,6];
F_o_13_6 : 0 <= -S[13,6] + S[14,7];
F_o_13_7 : 0 <= -S[13,7] + S[14,8];
F_o_13_8 : 0 <= -S[13,8] + S[14,9];
F_o_13_9 : 0 <= -S[13,9] + S[14,10];
F_o_13_10 : 0 <= -S[13,10] + S[14,11];
F_o_13_11 : 0 <= -S[13,11] + S[14,12];
F_o_13_12 : 0 <= -S[13,12] + S[14,13];
F_o_13_13 : 0 <= -S[13,13] + S[14,14];
F_o_13_14 : 0 <= -S[13,14] + S[14,15];
F_o_13_15 : 0 <= -S[13,15] + S[14,16];
F_o_13_16 : 0 <= -S[13,16] + S[14,17];
F_o_13_17 : 0 <= -S[13,17] + S[14,18];
F_o_13_18 : 0 <= -S[13,18] + S[14,19];
F_o_13_19 : 0 <= -S[13,19] + S[14,20];
F_o_13_20 : 0 <= -S[13,20] + S[14,21];
F_o_13_21 : 0 <= -S[13,21] + S[14,22];
F_o_13_22 : 0 <= -S[13,22] + S[14,23];
F_o_13_23 : 0 <= -S[13,23] + S[14,24];
F_o_14_1 : 0 <= -S[14,1] + S[15,2];
F_o_14_2 : 0 <= -S[14,2] + S[15,3];
F_o_14_3 : 0 <= -S[14,3] + S[15,4];
F_o_14_4 : 0 <= -S[14,4] + S[15,5];
F_o_14_5 : 0 <= -S[14,5] + S[15,6];
F_o_14_6 : 0 <= -S[14,6] + S[15,7];
F_o_14_7 : 0 <= -S[14,7] + S[15,8];
F_o_14_8 : 0 <= -S[14,8] + S[15,9];
F_o_14_9 : 0 <= -S[14,9] + S[15,10];
F_o_14_10 : 0 <= -S[14,10] + S[15,11];
F_o_14_11 : 0 <= -S[14,11] + S[15,12];
F_o_14_12 : 0 <= -S[14,12] + S[15,13];
F_o_14_13 : 0 <= -S[14,13] + S[15,14];
F_o_14_14 : 0 <= -S[14,14] + S[15,15];
F_o_14_15 : 0 <= -S[14,15] + S[15,16];
F_o_14_16 : 0 <= -S[14,16] + S[15,17];
F_o_14_17 : 0 <= -S[14,17] + S[15,18];
F_o_14_18 : 0 <= -S[14,18] + S[15,19];
F_o_14_19 : 0 <= -S[14,19] + S[15,20];
F_o_14_20 : 0 <= -S[14,20] + S[15,21];
F_o_14_21 : 0 <= -S[14,21] + S[15,22];
F_o_14_22 : 0 <= -S[14,22] + S[15,23];
F_o_14_23 : 0 <= -S[14,23] + S[15,24];
F_iii_15_1_1 : -1 <= -S[15,1] + S[17,2]-guard2[1];
F_iii_15_1_2 : 0 <= -S[15,1] + S[16,2] + guard2[1];
F_iii_15_2_1 : -1 <= -S[15,2] + S[17,3]-guard2[2];
F_iii_15_2_2 : 0 <= -S[15,2] + S[16,3] + guard2[2];
F_iii_15_3_1 : -1 <= -S[15,3] + S[17,4]-guard2[3];
F_iii_15_3_2 : 0 <= -S[15,3] + S[16,4] + guard2[3];
F_iii_15_4_1 : -1 <= -S[15,4] + S[17,5]-guard2[4];
F_iii_15_4_2 : 0 <= -S[15,4] + S[16,5] + guard2[4];
F_iii_15_5_1 : -1 <= -S[15,5] + S[17,6]-guard2[5];
F_iii_15_5_2 : 0 <= -S[15,5] + S[16,6] + guard2[5];
F_iii_15_6_1 : -1 <= -S[15,6] + S[17,7]-guard2[6];
F_iii_15_6_2 : 0 <= -S[15,6] + S[16,7] + guard2[6];
F_iii_15_7_1 : -1 <= -S[15,7] + S[17,8]-guard2[7];
F_iii_15_7_2 : 0 <= -S[15,7] + S[16,8] + guard2[7];
F_iii_15_8_1 : -1 <= -S[15,8] + S[17,9]-guard2[8];
F_iii_15_8_2 : 0 <= -S[15,8] + S[16,9] + guard2[8];
F_iii_15_9_1 : -1 <= -S[15,9] + S[17,10]-guard2[9];
F_iii_15_9_2 : 0 <= -S[15,9] + S[16,10] + guard2[9];
F_iii_15_10_1 : -1 <= -S[15,10] + S[17,11]-guard2[10];
F_iii_15_10_2 : 0 <= -S[15,10] + S[16,11] + guard2[10];
F_iii_15_11_1 : -1 <= -S[15,11] + S[17,12]-guard2[11];
F_iii_15_11_2 : 0 <= -S[15,11] + S[16,12] + guard2[11];
F_iii_15_12_1 : -1 <= -S[15,12] + S[17,13]-guard2[12];
F_iii_15_12_2 : 0 <= -S[15,12] + S[16,13] + guard2[12];
F_iii_15_13_1 : -1 <= -S[15,13] + S[17,14]-guard2[13];
F_iii_15_13_2 : 0 <= -S[15,13] + S[16,14] + guard2[13];
F_iii_15_14_1 : -1 <= -S[15,14] + S[17,15]-guard2[14];
F_iii_15_14_2 : 0 <= -S[15,14] + S[16,15] + guard2[14];
F_iii_15_15_1 : -1 <= -S[15,15] + S[17,16]-guard2[15];
F_iii_15_15_2 : 0 <= -S[15,15] + S[16,16] + guard2[15];
F_iii_15_16_1 : -1 <= -S[15,16] + S[17,17]-guard2[16];
F_iii_15_16_2 : 0 <= -S[15,16] + S[16,17] + guard2[16];
F_iii_15_17_1 : -1 <= -S[15,17] + S[17,18]-guard2[17];
F_iii_15_17_2 : 0 <= -S[15,17] + S[16,18] + guard2[17];
F_iii_15_18_1 : -1 <= -S[15,18] + S[17,19]-guard2[18];
F_iii_15_18_2 : 0 <= -S[15,18] + S[16,19] + guard2[18];
F_iii_15_19_1 : -1 <= -S[15,19] + S[17,20]-guard2[19];
F_iii_15_19_2 : 0 <= -S[15,19] + S[16,20] + guard2[19];
F_iii_15_20_1 : -1 <= -S[15,20] + S[17,21]-guard2[20];
F_iii_15_20_2 : 0 <= -S[15,20] + S[16,21] + guard2[20];
F_iii_15_21_1 : -1 <= -S[15,21] + S[17,22]-guard2[21];
F_iii_15_21_2 : 0 <= -S[15,21] + S[16,22] + guard2[21];
F_iii_15_22_1 : -1 <= -S[15,22] + S[17,23]-guard2[22];
F_iii_15_22_2 : 0 <= -S[15,22] + S[16,23] + guard2[22];
F_iii_15_23_1 : -1 <= -S[15,23] + S[17,24]-guard2[23];
F_iii_15_23_2 : 0 <= -S[15,23] + S[16,24] + guard2[23];
F_o_16_1 : 0 <= -S[16,1] + S[16,2];
F_o_16_2 : 0 <= -S[16,2] + S[16,3];
F_o_16_3 : 0 <= -S[16,3] + S[16,4];
F_o_16_4 : 0 <= -S[16,4] + S[16,5];
F_o_16_5 : 0 <= -S[16,5] + S[16,6];
F_o_16_6 : 0 <= -S[16,6] + S[16,7];
F_o_16_7 : 0 <= -S[16,7] + S[16,8];
F_o_16_8 : 0 <= -S[16,8] + S[16,9];
F_o_16_9 : 0 <= S[16,10]-S[16,9];
F_o_16_10 : 0 <= -S[16,10] + S[16,11];
F_o_16_11 : 0 <= -S[16,11] + S[16,12];
F_o_16_12 : 0 <= -S[16,12] + S[16,13];
F_o_16_13 : 0 <= -S[16,13] + S[16,14];
F_o_16_14 : 0 <= -S[16,14] + S[16,15];
F_o_16_15 : 0 <= -S[16,15] + S[16,16];
F_o_16_16 : 0 <= -S[16,16] + S[16,17];
F_o_16_17 : 0 <= -S[16,17] + S[16,18];
F_o_16_18 : 0 <= -S[16,18] + S[16,19];
F_o_16_19 : 0 <= -S[16,19] + S[16,20];
F_o_16_20 : 0 <= -S[16,20] + S[16,21];
F_o_16_21 : 0 <= -S[16,21] + S[16,22];
F_o_16_22 : 0 <= -S[16,22] + S[16,23];
F_o_16_23 : 0 <= -S[16,23] + S[16,24];
F_o_17_1 : 0 <= -S[17,1] + S[18,2];
F_o_17_2 : 0 <= -S[17,2] + S[18,3];
F_o_17_3 : 0 <= -S[17,3] + S[18,4];
F_o_17_4 : 0 <= -S[17,4] + S[18,5];
F_o_17_5 : 0 <= -S[17,5] + S[18,6];
F_o_17_6 : 0 <= -S[17,6] + S[18,7];
F_o_17_7 : 0 <= -S[17,7] + S[18,8];
F_o_17_8 : 0 <= -S[17,8] + S[18,9];
F_o_17_9 : 0 <= -S[17,9] + S[18,10];
F_o_17_10 : 0 <= -S[17,10] + S[18,11];
F_o_17_11 : 0 <= -S[17,11] + S[18,12];
F_o_17_12 : 0 <= -S[17,12] + S[18,13];
F_o_17_13 : 0 <= -S[17,13] + S[18,14];
F_o_17_14 : 0 <= -S[17,14] + S[18,15];
F_o_17_15 : 0 <= -S[17,15] + S[18,16];
F_o_17_16 : 0 <= -S[17,16] + S[18,17];
F_o_17_17 : 0 <= -S[17,17] + S[18,18];
F_o_17_18 : 0 <= -S[17,18] + S[18,19];
F_o_17_19 : 0 <= -S[17,19] + S[18,20];
F_o_17_20 : 0 <= -S[17,20] + S[18,21];
F_o_17_21 : 0 <= -S[17,21] + S[18,22];
F_o_17_22 : 0 <= -S[17,22] + S[18,23];
F_o_17_23 : 0 <= -S[17,23] + S[18,24];
F_o_18_1 : 0 <= -S[18,1] + S[19,2];
F_o_18_2 : 0 <= -S[18,2] + S[19,3];
F_o_18_3 : 0 <= -S[18,3] + S[19,4];
F_o_18_4 : 0 <= -S[18,4] + S[19,5];
F_o_18_5 : 0 <= -S[18,5] + S[19,6];
F_o_18_6 : 0 <= -S[18,6] + S[19,7];
F_o_18_7 : 0 <= -S[18,7] + S[19,8];
F_o_18_8 : 0 <= -S[18,8] + S[19,9];
F_o_18_9 : 0 <= -S[18,9] + S[19,10];
F_o_18_10 : 0 <= -S[18,10] + S[19,11];
F_o_18_11 : 0 <= -S[18,11] + S[19,12];
F_o_18_12 : 0 <= -S[18,12] + S[19,13];
F_o_18_13 : 0 <= -S[18,13] + S[19,14];
F_o_18_14 : 0 <= -S[18,14] + S[19,15];
F_o_18_15 : 0 <= -S[18,15] + S[19,16];
F_o_18_16 : 0 <= -S[18,16] + S[19,17];
F_o_18_17 : 0 <= -S[18,17] + S[19,18];
F_o_18_18 : 0 <= -S[18,18] + S[19,19];
F_o_18_19 : 0 <= -S[18,19] + S[19,20];
F_o_18_20 : 0 <= -S[18,20] + S[19,21];
F_o_18_21 : 0 <= -S[18,21] + S[19,22];
F_o_18_22 : 0 <= -S[18,22] + S[19,23];
F_o_18_23 : 0 <= -S[18,23] + S[19,24];
F_o_19_1 : 0 <= -S[19,1] + S[20,2];
F_o_19_2 : 0 <= -S[19,2] + S[20,3];
F_o_19_3 : 0 <= -S[19,3] + S[20,4];
F_o_19_4 : 0 <= -S[19,4] + S[20,5];
F_o_19_5 : 0 <= -S[19,5] + S[20,6];
F_o_19_6 : 0 <= -S[19,6] + S[20,7];
F_o_19_7 : 0 <= -S[19,7] + S[20,8];
F_o_19_8 : 0 <= -S[19,8] + S[20,9];
F_o_19_9 : 0 <= -S[19,9] + S[20,10];
F_o_19_10 : 0 <= -S[19,10] + S[20,11];
F_o_19_11 : 0 <= -S[19,11] + S[20,12];
F_o_19_12 : 0 <= -S[19,12] + S[20,13];
F_o_19_13 : 0 <= -S[19,13] + S[20,14];
F_o_19_14 : 0 <= -S[19,14] + S[20,15];
F_o_19_15 : 0 <= -S[19,15] + S[20,16];
F_o_19_16 : 0 <= -S[19,16] + S[20,17];
F_o_19_17 : 0 <= -S[19,17] + S[20,18];
F_o_19_18 : 0 <= -S[19,18] + S[20,19];
F_o_19_19 : 0 <= -S[19,19] + S[20,20];
F_o_19_20 : 0 <= -S[19,20] + S[20,21];
F_o_19_21 : 0 <= -S[19,21] + S[20,22];
F_o_19_22 : 0 <= -S[19,22] + S[20,23];
F_o_19_23 : 0 <= -S[19,23] + S[20,24];
F_iii_20_1_1 : -1 <= -S[20,1] + S[22,2]-guard4[1];
F_iii_20_1_2 : 0 <= -S[20,1] + S[21,2] + guard4[1];
F_iii_20_2_1 : -1 <= -S[20,2] + S[22,3]-guard4[2];
F_iii_20_2_2 : 0 <= -S[20,2] + S[21,3] + guard4[2];
F_iii_20_3_1 : -1 <= -S[20,3] + S[22,4]-guard4[3];
F_iii_20_3_2 : 0 <= -S[20,3] + S[21,4] + guard4[3];
F_iii_20_4_1 : -1 <= -S[20,4] + S[22,5]-guard4[4];
F_iii_20_4_2 : 0 <= -S[20,4] + S[21,5] + guard4[4];
F_iii_20_5_1 : -1 <= -S[20,5] + S[22,6]-guard4[5];
F_iii_20_5_2 : 0 <= -S[20,5] + S[21,6] + guard4[5];
F_iii_20_6_1 : -1 <= -S[20,6] + S[22,7]-guard4[6];
F_iii_20_6_2 : 0 <= -S[20,6] + S[21,7] + guard4[6];
F_iii_20_7_1 : -1 <= -S[20,7] + S[22,8]-guard4[7];
F_iii_20_7_2 : 0 <= -S[20,7] + S[21,8] + guard4[7];
F_iii_20_8_1 : -1 <= -S[20,8] + S[22,9]-guard4[8];
F_iii_20_8_2 : 0 <= -S[20,8] + S[21,9] + guard4[8];
F_iii_20_9_1 : -1 <= -S[20,9] + S[22,10]-guard4[9];
F_iii_20_9_2 : 0 <= -S[20,9] + S[21,10] + guard4[9];
F_iii_20_10_1 : -1 <= -S[20,10] + S[22,11]-guard4[10];
F_iii_20_10_2 : 0 <= -S[20,10] + S[21,11] + guard4[10];
F_iii_20_11_1 : -1 <= -S[20,11] + S[22,12]-guard4[11];
F_iii_20_11_2 : 0 <= -S[20,11] + S[21,12] + guard4[11];
F_iii_20_12_1 : -1 <= -S[20,12] + S[22,13]-guard4[12];
F_iii_20_12_2 : 0 <= -S[20,12] + S[21,13] + guard4[12];
F_iii_20_13_1 : -1 <= -S[20,13] + S[22,14]-guard4[13];
F_iii_20_13_2 : 0 <= -S[20,13] + S[21,14] + guard4[13];
F_iii_20_14_1 : -1 <= -S[20,14] + S[22,15]-guard4[14];
F_iii_20_14_2 : 0 <= -S[20,14] + S[21,15] + guard4[14];
F_iii_20_15_1 : -1 <= -S[20,15] + S[22,16]-guard4[15];
F_iii_20_15_2 : 0 <= -S[20,15] + S[21,16] + guard4[15];
F_iii_20_16_1 : -1 <= -S[20,16] + S[22,17]-guard4[16];
F_iii_20_16_2 : 0 <= -S[20,16] + S[21,17] + guard4[16];
F_iii_20_17_1 : -1 <= -S[20,17] + S[22,18]-guard4[17];
F_iii_20_17_2 : 0 <= -S[20,17] + S[21,18] + guard4[17];
F_iii_20_18_1 : -1 <= -S[20,18] + S[22,19]-guard4[18];
F_iii_20_18_2 : 0 <= -S[20,18] + S[21,19] + guard4[18];
F_iii_20_19_1 : -1 <= -S[20,19] + S[22,20]-guard4[19];
F_iii_20_19_2 : 0 <= -S[20,19] + S[21,20] + guard4[19];
F_iii_20_20_1 : -1 <= -S[20,20] + S[22,21]-guard4[20];
F_iii_20_20_2 : 0 <= -S[20,20] + S[21,21] + guard4[20];
F_iii_20_21_1 : -1 <= -S[20,21] + S[22,22]-guard4[21];
F_iii_20_21_2 : 0 <= -S[20,21] + S[21,22] + guard4[21];
F_iii_20_22_1 : -1 <= -S[20,22] + S[22,23]-guard4[22];
F_iii_20_22_2 : 0 <= -S[20,22] + S[21,23] + guard4[22];
F_iii_20_23_1 : -1 <= -S[20,23] + S[22,24]-guard4[23];
F_iii_20_23_2 : 0 <= -S[20,23] + S[21,24] + guard4[23];
F_o_21_1 : 0 <= -S[21,1] + S[21,2];
F_o_21_2 : 0 <= -S[21,2] + S[21,3];
F_o_21_3 : 0 <= -S[21,3] + S[21,4];
F_o_21_4 : 0 <= -S[21,4] + S[21,5];
F_o_21_5 : 0 <= -S[21,5] + S[21,6];
F_o_21_6 : 0 <= -S[21,6] + S[21,7];
F_o_21_7 : 0 <= -S[21,7] + S[21,8];
F_o_21_8 : 0 <= -S[21,8] + S[21,9];
F_o_21_9 : 0 <= S[21,10]-S[21,9];
F_o_21_10 : 0 <= -S[21,10] + S[21,11];
F_o_21_11 : 0 <= -S[21,11] + S[21,12];
F_o_21_12 : 0 <= -S[21,12] + S[21,13];
F_o_21_13 : 0 <= -S[21,13] + S[21,14];
F_o_21_14 : 0 <= -S[21,14] + S[21,15];
F_o_21_15 : 0 <= -S[21,15] + S[21,16];
F_o_21_16 : 0 <= -S[21,16] + S[21,17];
F_o_21_17 : 0 <= -S[21,17] + S[21,18];
F_o_21_18 : 0 <= -S[21,18] + S[21,19];
F_o_21_19 : 0 <= -S[21,19] + S[21,20];
F_o_21_20 : 0 <= -S[21,20] + S[21,21];
F_o_21_21 : 0 <= -S[21,21] + S[21,22];
F_o_21_22 : 0 <= -S[21,22] + S[21,23];
F_o_21_23 : 0 <= -S[21,23] + S[21,24];
F_o_22_1 : 0 <= -S[22,1] + S[23,2];
F_o_22_2 : 0 <= -S[22,2] + S[23,3];
F_o_22_3 : 0 <= -S[22,3] + S[23,4];
F_o_22_4 : 0 <= -S[22,4] + S[23,5];
F_o_22_5 : 0 <= -S[22,5] + S[23,6];
F_o_22_6 : 0 <= -S[22,6] + S[23,7];
F_o_22_7 : 0 <= -S[22,7] + S[23,8];
F_o_22_8 : 0 <= -S[22,8] + S[23,9];
F_o_22_9 : 0 <= -S[22,9] + S[23,10];
F_o_22_10 : 0 <= -S[22,10] + S[23,11];
F_o_22_11 : 0 <= -S[22,11] + S[23,12];
F_o_22_12 : 0 <= -S[22,12] + S[23,13];
F_o_22_13 : 0 <= -S[22,13] + S[23,14];
F_o_22_14 : 0 <= -S[22,14] + S[23,15];
F_o_22_15 : 0 <= -S[22,15] + S[23,16];
F_o_22_16 : 0 <= -S[22,16] + S[23,17];
F_o_22_17 : 0 <= -S[22,17] + S[23,18];
F_o_22_18 : 0 <= -S[22,18] + S[23,19];
F_o_22_19 : 0 <= -S[22,19] + S[23,20];
F_o_22_20 : 0 <= -S[22,20] + S[23,21];
F_o_22_21 : 0 <= -S[22,21] + S[23,22];
F_o_22_22 : 0 <= -S[22,22] + S[23,23];
F_o_22_23 : 0 <= -S[22,23] + S[23,24];
F_o_23_1 : 0 <= -S[23,1] + S[23,2];
F_o_23_2 : 0 <= -S[23,2] + S[23,3];
F_o_23_3 : 0 <= -S[23,3] + S[23,4];
F_o_23_4 : 0 <= -S[23,4] + S[23,5];
F_o_23_5 : 0 <= -S[23,5] + S[23,6];
F_o_23_6 : 0 <= -S[23,6] + S[23,7];
F_o_23_7 : 0 <= -S[23,7] + S[23,8];
F_o_23_8 : 0 <= -S[23,8] + S[23,9];
F_o_23_9 : 0 <= S[23,10]-S[23,9];
F_o_23_10 : 0 <= -S[23,10] + S[23,11];
F_o_23_11 : 0 <= -S[23,11] + S[23,12];
F_o_23_12 : 0 <= -S[23,12] + S[23,13];
F_o_23_13 : 0 <= -S[23,13] + S[23,14];
F_o_23_14 : 0 <= -S[23,14] + S[23,15];
F_o_23_15 : 0 <= -S[23,15] + S[23,16];
F_o_23_16 : 0 <= -S[23,16] + S[23,17];
F_o_23_17 : 0 <= -S[23,17] + S[23,18];
F_o_23_18 : 0 <= -S[23,18] + S[23,19];
F_o_23_19 : 0 <= -S[23,19] + S[23,20];
F_o_23_20 : 0 <= -S[23,20] + S[23,21];
F_o_23_21 : 0 <= -S[23,21] + S[23,22];
F_o_23_22 : 0 <= -S[23,22] + S[23,23];
F_o_23_23 : 0 <= -S[23,23] + S[23,24];
keep_1_2_1_1 : -1 <= -S[1,1]-guard2[0] + guard2[1];
keep_1_2_1_2 : -1 <= -S[1,1] + guard2[0]-guard2[1];
keep_1_1_1_1 : -1 <= -S[1,1]-guard0[0] + guard0[1];
keep_1_1_1_2 : -1 <= -S[1,1] + guard0[0]-guard0[1];
keep_1_3_1_1 : -1 <= -S[1,1]-guard4[0] + guard4[1];
keep_1_3_1_2 : -1 <= -S[1,1] + guard4[0]-guard4[1];
keep_1_2_2_1 : -1 <= -S[1,2]-guard2[1] + guard2[2];
keep_1_2_2_2 : -1 <= -S[1,2] + guard2[1]-guard2[2];
keep_1_1_2_1 : -1 <= -S[1,2]-guard0[1] + guard0[2];
keep_1_1_2_2 : -1 <= -S[1,2] + guard0[1]-guard0[2];
keep_1_3_2_1 : -1 <= -S[1,2]-guard4[1] + guard4[2];
keep_1_3_2_2 : -1 <= -S[1,2] + guard4[1]-guard4[2];
keep_1_2_3_1 : -1 <= -S[1,3]-guard2[2] + guard2[3];
keep_1_2_3_2 : -1 <= -S[1,3] + guard2[2]-guard2[3];
keep_1_1_3_1 : -1 <= -S[1,3]-guard0[2] + guard0[3];
keep_1_1_3_2 : -1 <= -S[1,3] + guard0[2]-guard0[3];
keep_1_3_3_1 : -1 <= -S[1,3]-guard4[2] + guard4[3];
keep_1_3_3_2 : -1 <= -S[1,3] + guard4[2]-guard4[3];
keep_1_2_4_1 : -1 <= -S[1,4]-guard2[3] + guard2[4];
keep_1_2_4_2 : -1 <= -S[1,4] + guard2[3]-guard2[4];
keep_1_1_4_1 : -1 <= -S[1,4]-guard0[3] + guard0[4];
keep_1_1_4_2 : -1 <= -S[1,4] + guard0[3]-guard0[4];
keep_1_3_4_1 : -1 <= -S[1,4]-guard4[3] + guard4[4];
keep_1_3_4_2 : -1 <= -S[1,4] + guard4[3]-guard4[4];
keep_1_2_5_1 : -1 <= -S[1,5]-guard2[4] + guard2[5];
keep_1_2_5_2 : -1 <= -S[1,5] + guard2[4]-guard2[5];
keep_1_1_5_1 : -1 <= -S[1,5]-guard0[4] + guard0[5];
keep_1_1_5_2 : -1 <= -S[1,5] + guard0[4]-guard0[5];
keep_1_3_5_1 : -1 <= -S[1,5]-guard4[4] + guard4[5];
keep_1_3_5_2 : -1 <= -S[1,5] + guard4[4]-guard4[5];
keep_1_2_6_1 : -1 <= -S[1,6]-guard2[5] + guard2[6];
keep_1_2_6_2 : -1 <= -S[1,6] + guard2[5]-guard2[6];
keep_1_1_6_1 : -1 <= -S[1,6]-guard0[5] + guard0[6];
keep_1_1_6_2 : -1 <= -S[1,6] + guard0[5]-guard0[6];
keep_1_3_6_1 : -1 <= -S[1,6]-guard4[5] + guard4[6];
keep_1_3_6_2 : -1 <= -S[1,6] + guard4[5]-guard4[6];
keep_1_2_7_1 : -1 <= -S[1,7]-guard2[6] + guard2[7];
keep_1_2_7_2 : -1 <= -S[1,7] + guard2[6]-guard2[7];
keep_1_1_7_1 : -1 <= -S[1,7]-guard0[6] + guard0[7];
keep_1_1_7_2 : -1 <= -S[1,7] + guard0[6]-guard0[7];
keep_1_3_7_1 : -1 <= -S[1,7]-guard4[6] + guard4[7];
keep_1_3_7_2 : -1 <= -S[1,7] + guard4[6]-guard4[7];
keep_1_2_8_1 : -1 <= -S[1,8]-guard2[7] + guard2[8];
keep_1_2_8_2 : -1 <= -S[1,8] + guard2[7]-guard2[8];
keep_1_1_8_1 : -1 <= -S[1,8]-guard0[7] + guard0[8];
keep_1_1_8_2 : -1 <= -S[1,8] + guard0[7]-guard0[8];
keep_1_3_8_1 : -1 <= -S[1,8]-guard4[7] + guard4[8];
keep_1_3_8_2 : -1 <= -S[1,8] + guard4[7]-guard4[8];
keep_1_2_9_1 : -1 <= -S[1,9]-guard2[8] + guard2[9];
keep_1_2_9_2 : -1 <= -S[1,9] + guard2[8]-guard2[9];
keep_1_1_9_1 : -1 <= -S[1,9]-guard0[8] + guard0[9];
keep_1_1_9_2 : -1 <= -S[1,9] + guard0[8]-guard0[9];
keep_1_3_9_1 : -1 <= -S[1,9]-guard4[8] + guard4[9];
keep_1_3_9_2 : -1 <= -S[1,9] + guard4[8]-guard4[9];
keep_1_2_10_1 : -1 <= -S[1,10] + guard2[10]-guard2[9];
keep_1_2_10_2 : -1 <= -S[1,10]-guard2[10] + guard2[9];
keep_1_1_10_1 : -1 <= -S[1,10] + guard0[10]-guard0[9];
keep_1_1_10_2 : -1 <= -S[1,10]-guard0[10] + guard0[9];
keep_1_3_10_1 : -1 <= -S[1,10] + guard4[10]-guard4[9];
keep_1_3_10_2 : -1 <= -S[1,10]-guard4[10] + guard4[9];
keep_1_2_11_1 : -1 <= -S[1,11]-guard2[10] + guard2[11];
keep_1_2_11_2 : -1 <= -S[1,11] + guard2[10]-guard2[11];
keep_1_1_11_1 : -1 <= -S[1,11]-guard0[10] + guard0[11];
keep_1_1_11_2 : -1 <= -S[1,11] + guard0[10]-guard0[11];
keep_1_3_11_1 : -1 <= -S[1,11]-guard4[10] + guard4[11];
keep_1_3_11_2 : -1 <= -S[1,11] + guard4[10]-guard4[11];
keep_1_2_12_1 : -1 <= -S[1,12]-guard2[11] + guard2[12];
keep_1_2_12_2 : -1 <= -S[1,12] + guard2[11]-guard2[12];
keep_1_1_12_1 : -1 <= -S[1,12]-guard0[11] + guard0[12];
keep_1_1_12_2 : -1 <= -S[1,12] + guard0[11]-guard0[12];
keep_1_3_12_1 : -1 <= -S[1,12]-guard4[11] + guard4[12];
keep_1_3_12_2 : -1 <= -S[1,12] + guard4[11]-guard4[12];
keep_1_2_13_1 : -1 <= -S[1,13]-guard2[12] + guard2[13];
keep_1_2_13_2 : -1 <= -S[1,13] + guard2[12]-guard2[13];
keep_1_1_13_1 : -1 <= -S[1,13]-guard0[12] + guard0[13];
keep_1_1_13_2 : -1 <= -S[1,13] + guard0[12]-guard0[13];
keep_1_3_13_1 : -1 <= -S[1,13]-guard4[12] + guard4[13];
keep_1_3_13_2 : -1 <= -S[1,13] + guard4[12]-guard4[13];
keep_1_2_14_1 : -1 <= -S[1,14]-guard2[13] + guard2[14];
keep_1_2_14_2 : -1 <= -S[1,14] + guard2[13]-guard2[14];
keep_1_1_14_1 : -1 <= -S[1,14]-guard0[13] + guard0[14];
keep_1_1_14_2 : -1 <= -S[1,14] + guard0[13]-guard0[14];
keep_1_3_14_1 : -1 <= -S[1,14]-guard4[13] + guard4[14];
keep_1_3_14_2 : -1 <= -S[1,14] + guard4[13]-guard4[14];
keep_1_2_15_1 : -1 <= -S[1,15]-guard2[14] + guard2[15];
keep_1_2_15_2 : -1 <= -S[1,15] + guard2[14]-guard2[15];
keep_1_1_15_1 : -1 <= -S[1,15]-guard0[14] + guard0[15];
keep_1_1_15_2 : -1 <= -S[1,15] + guard0[14]-guard0[15];
keep_1_3_15_1 : -1 <= -S[1,15]-guard4[14] + guard4[15];
keep_1_3_15_2 : -1 <= -S[1,15] + guard4[14]-guard4[15];
keep_1_2_16_1 : -1 <= -S[1,16]-guard2[15] + guard2[16];
keep_1_2_16_2 : -1 <= -S[1,16] + guard2[15]-guard2[16];
keep_1_1_16_1 : -1 <= -S[1,16]-guard0[15] + guard0[16];
keep_1_1_16_2 : -1 <= -S[1,16] + guard0[15]-guard0[16];
keep_1_3_16_1 : -1 <= -S[1,16]-guard4[15] + guard4[16];
keep_1_3_16_2 : -1 <= -S[1,16] + guard4[15]-guard4[16];
keep_1_2_17_1 : -1 <= -S[1,17]-guard2[16] + guard2[17];
keep_1_2_17_2 : -1 <= -S[1,17] + guard2[16]-guard2[17];
keep_1_1_17_1 : -1 <= -S[1,17]-guard0[16] + guard0[17];
keep_1_1_17_2 : -1 <= -S[1,17] + guard0[16]-guard0[17];
keep_1_3_17_1 : -1 <= -S[1,17]-guard4[16] + guard4[17];
keep_1_3_17_2 : -1 <= -S[1,17] + guard4[16]-guard4[17];
keep_1_2_18_1 : -1 <= -S[1,18]-guard2[17] + guard2[18];
keep_1_2_18_2 : -1 <= -S[1,18] + guard2[17]-guard2[18];
keep_1_1_18_1 : -1 <= -S[1,18]-guard0[17] + guard0[18];
keep_1_1_18_2 : -1 <= -S[1,18] + guard0[17]-guard0[18];
keep_1_3_18_1 : -1 <= -S[1,18]-guard4[17] + guard4[18];
keep_1_3_18_2 : -1 <= -S[1,18] + guard4[17]-guard4[18];
keep_1_2_19_1 : -1 <= -S[1,19]-guard2[18] + guard2[19];
keep_1_2_19_2 : -1 <= -S[1,19] + guard2[18]-guard2[19];
keep_1_1_19_1 : -1 <= -S[1,19]-guard0[18] + guard0[19];
keep_1_1_19_2 : -1 <= -S[1,19] + guard0[18]-guard0[19];
keep_1_3_19_1 : -1 <= -S[1,19]-guard4[18] + guard4[19];
keep_1_3_19_2 : -1 <= -S[1,19] + guard4[18]-guard4[19];
keep_1_2_20_1 : -1 <= -S[1,20]-guard2[19] + guard2[20];
keep_1_2_20_2 : -1 <= -S[1,20] + guard2[19]-guard2[20];
keep_1_1_20_1 : -1 <= -S[1,20]-guard0[19] + guard0[20];
keep_1_1_20_2 : -1 <= -S[1,20] + guard0[19]-guard0[20];
keep_1_3_20_1 : -1 <= -S[1,20]-guard4[19] + guard4[20];
keep_1_3_20_2 : -1 <= -S[1,20] + guard4[19]-guard4[20];
keep_1_2_21_1 : -1 <= -S[1,21]-guard2[20] + guard2[21];
keep_1_2_21_2 : -1 <= -S[1,21] + guard2[20]-guard2[21];
keep_1_1_21_1 : -1 <= -S[1,21]-guard0[20] + guard0[21];
keep_1_1_21_2 : -1 <= -S[1,21] + guard0[20]-guard0[21];
keep_1_3_21_1 : -1 <= -S[1,21]-guard4[20] + guard4[21];
keep_1_3_21_2 : -1 <= -S[1,21] + guard4[20]-guard4[21];
keep_1_2_22_1 : -1 <= -S[1,22]-guard2[21] + guard2[22];
keep_1_2_22_2 : -1 <= -S[1,22] + guard2[21]-guard2[22];
keep_1_1_22_1 : -1 <= -S[1,22]-guard0[21] + guard0[22];
keep_1_1_22_2 : -1 <= -S[1,22] + guard0[21]-guard0[22];
keep_1_3_22_1 : -1 <= -S[1,22]-guard4[21] + guard4[22];
keep_1_3_22_2 : -1 <= -S[1,22] + guard4[21]-guard4[22];
keep_1_2_23_1 : -1 <= -S[1,23]-guard2[22] + guard2[23];
keep_1_2_23_2 : -1 <= -S[1,23] + guard2[22]-guard2[23];
keep_1_1_23_1 : -1 <= -S[1,23]-guard0[22] + guard0[23];
keep_1_1_23_2 : -1 <= -S[1,23] + guard0[22]-guard0[23];
keep_1_3_23_1 : -1 <= -S[1,23]-guard4[22] + guard4[23];
keep_1_3_23_2 : -1 <= -S[1,23] + guard4[22]-guard4[23];
keep_2_2_1_1 : -1 <= -S[2,1]-guard2[0] + guard2[1];
keep_2_2_1_2 : -1 <= -S[2,1] + guard2[0]-guard2[1];
keep_2_1_1_1 : -1 <= -S[2,1]-guard0[0] + guard0[1];
keep_2_1_1_2 : -1 <= -S[2,1] + guard0[0]-guard0[1];
keep_2_3_1_1 : -1 <= -S[2,1]-guard4[0] + guard4[1];
keep_2_3_1_2 : -1 <= -S[2,1] + guard4[0]-guard4[1];
keep_2_2_2_1 : -1 <= -S[2,2]-guard2[1] + guard2[2];
keep_2_2_2_2 : -1 <= -S[2,2] + guard2[1]-guard2[2];
keep_2_1_2_1 : -1 <= -S[2,2]-guard0[1] + guard0[2];
keep_2_1_2_2 : -1 <= -S[2,2] + guard0[1]-guard0[2];
keep_2_3_2_1 : -1 <= -S[2,2]-guard4[1] + guard4[2];
keep_2_3_2_2 : -1 <= -S[2,2] + guard4[1]-guard4[2];
keep_2_2_3_1 : -1 <= -S[2,3]-guard2[2] + guard2[3];
keep_2_2_3_2 : -1 <= -S[2,3] + guard2[2]-guard2[3];
keep_2_1_3_1 : -1 <= -S[2,3]-guard0[2] + guard0[3];
keep_2_1_3_2 : -1 <= -S[2,3] + guard0[2]-guard0[3];
keep_2_3_3_1 : -1 <= -S[2,3]-guard4[2] + guard4[3];
keep_2_3_3_2 : -1 <= -S[2,3] + guard4[2]-guard4[3];
keep_2_2_4_1 : -1 <= -S[2,4]-guard2[3] + guard2[4];
keep_2_2_4_2 : -1 <= -S[2,4] + guard2[3]-guard2[4];
keep_2_1_4_1 : -1 <= -S[2,4]-guard0[3] + guard0[4];
keep_2_1_4_2 : -1 <= -S[2,4] + guard0[3]-guard0[4];
keep_2_3_4_1 : -1 <= -S[2,4]-guard4[3] + guard4[4];
keep_2_3_4_2 : -1 <= -S[2,4] + guard4[3]-guard4[4];
keep_2_2_5_1 : -1 <= -S[2,5]-guard2[4] + guard2[5];
keep_2_2_5_2 : -1 <= -S[2,5] + guard2[4]-guard2[5];
keep_2_1_5_1 : -1 <= -S[2,5]-guard0[4] + guard0[5];
keep_2_1_5_2 : -1 <= -S[2,5] + guard0[4]-guard0[5];
keep_2_3_5_1 : -1 <= -S[2,5]-guard4[4] + guard4[5];
keep_2_3_5_2 : -1 <= -S[2,5] + guard4[4]-guard4[5];
keep_2_2_6_1 : -1 <= -S[2,6]-guard2[5] + guard2[6];
keep_2_2_6_2 : -1 <= -S[2,6] + guard2[5]-guard2[6];
keep_2_1_6_1 : -1 <= -S[2,6]-guard0[5] + guard0[6];
keep_2_1_6_2 : -1 <= -S[2,6] + guard0[5]-guard0[6];
keep_2_3_6_1 : -1 <= -S[2,6]-guard4[5] + guard4[6];
keep_2_3_6_2 : -1 <= -S[2,6] + guard4[5]-guard4[6];
keep_2_2_7_1 : -1 <= -S[2,7]-guard2[6] + guard2[7];
keep_2_2_7_2 : -1 <= -S[2,7] + guard2[6]-guard2[7];
keep_2_1_7_1 : -1 <= -S[2,7]-guard0[6] + guard0[7];
keep_2_1_7_2 : -1 <= -S[2,7] + guard0[6]-guard0[7];
keep_2_3_7_1 : -1 <= -S[2,7]-guard4[6] + guard4[7];
keep_2_3_7_2 : -1 <= -S[2,7] + guard4[6]-guard4[7];
keep_2_2_8_1 : -1 <= -S[2,8]-guard2[7] + guard2[8];
keep_2_2_8_2 : -1 <= -S[2,8] + guard2[7]-guard2[8];
keep_2_1_8_1 : -1 <= -S[2,8]-guard0[7] + guard0[8];
keep_2_1_8_2 : -1 <= -S[2,8] + guard0[7]-guard0[8];
keep_2_3_8_1 : -1 <= -S[2,8]-guard4[7] + guard4[8];
keep_2_3_8_2 : -1 <= -S[2,8] + guard4[7]-guard4[8];
keep_2_2_9_1 : -1 <= -S[2,9]-guard2[8] + guard2[9];
keep_2_2_9_2 : -1 <= -S[2,9] + guard2[8]-guard2[9];
keep_2_1_9_1 : -1 <= -S[2,9]-guard0[8] + guard0[9];
keep_2_1_9_2 : -1 <= -S[2,9] + guard0[8]-guard0[9];
keep_2_3_9_1 : -1 <= -S[2,9]-guard4[8] + guard4[9];
keep_2_3_9_2 : -1 <= -S[2,9] + guard4[8]-guard4[9];
keep_2_2_10_1 : -1 <= -S[2,10] + guard2[10]-guard2[9];
keep_2_2_10_2 : -1 <= -S[2,10]-guard2[10] + guard2[9];
keep_2_1_10_1 : -1 <= -S[2,10] + guard0[10]-guard0[9];
keep_2_1_10_2 : -1 <= -S[2,10]-guard0[10] + guard0[9];
keep_2_3_10_1 : -1 <= -S[2,10] + guard4[10]-guard4[9];
keep_2_3_10_2 : -1 <= -S[2,10]-guard4[10] + guard4[9];
keep_2_2_11_1 : -1 <= -S[2,11]-guard2[10] + guard2[11];
keep_2_2_11_2 : -1 <= -S[2,11] + guard2[10]-guard2[11];
keep_2_1_11_1 : -1 <= -S[2,11]-guard0[10] + guard0[11];
keep_2_1_11_2 : -1 <= -S[2,11] + guard0[10]-guard0[11];
keep_2_3_11_1 : -1 <= -S[2,11]-guard4[10] + guard4[11];
keep_2_3_11_2 : -1 <= -S[2,11] + guard4[10]-guard4[11];
keep_2_2_12_1 : -1 <= -S[2,12]-guard2[11] + guard2[12];
keep_2_2_12_2 : -1 <= -S[2,12] + guard2[11]-guard2[12];
keep_2_1_12_1 : -1 <= -S[2,12]-guard0[11] + guard0[12];
keep_2_1_12_2 : -1 <= -S[2,12] + guard0[11]-guard0[12];
keep_2_3_12_1 : -1 <= -S[2,12]-guard4[11] + guard4[12];
keep_2_3_12_2 : -1 <= -S[2,12] + guard4[11]-guard4[12];
keep_2_2_13_1 : -1 <= -S[2,13]-guard2[12] + guard2[13];
keep_2_2_13_2 : -1 <= -S[2,13] + guard2[12]-guard2[13];
keep_2_1_13_1 : -1 <= -S[2,13]-guard0[12] + guard0[13];
keep_2_1_13_2 : -1 <= -S[2,13] + guard0[12]-guard0[13];
keep_2_3_13_1 : -1 <= -S[2,13]-guard4[12] + guard4[13];
keep_2_3_13_2 : -1 <= -S[2,13] + guard4[12]-guard4[13];
keep_2_2_14_1 : -1 <= -S[2,14]-guard2[13] + guard2[14];
keep_2_2_14_2 : -1 <= -S[2,14] + guard2[13]-guard2[14];
keep_2_1_14_1 : -1 <= -S[2,14]-guard0[13] + guard0[14];
keep_2_1_14_2 : -1 <= -S[2,14] + guard0[13]-guard0[14];
keep_2_3_14_1 : -1 <= -S[2,14]-guard4[13] + guard4[14];
keep_2_3_14_2 : -1 <= -S[2,14] + guard4[13]-guard4[14];
keep_2_2_15_1 : -1 <= -S[2,15]-guard2[14] + guard2[15];
keep_2_2_15_2 : -1 <= -S[2,15] + guard2[14]-guard2[15];
keep_2_1_15_1 : -1 <= -S[2,15]-guard0[14] + guard0[15];
keep_2_1_15_2 : -1 <= -S[2,15] + guard0[14]-guard0[15];
keep_2_3_15_1 : -1 <= -S[2,15]-guard4[14] + guard4[15];
keep_2_3_15_2 : -1 <= -S[2,15] + guard4[14]-guard4[15];
keep_2_2_16_1 : -1 <= -S[2,16]-guard2[15] + guard2[16];
keep_2_2_16_2 : -1 <= -S[2,16] + guard2[15]-guard2[16];
keep_2_1_16_1 : -1 <= -S[2,16]-guard0[15] + guard0[16];
keep_2_1_16_2 : -1 <= -S[2,16] + guard0[15]-guard0[16];
keep_2_3_16_1 : -1 <= -S[2,16]-guard4[15] + guard4[16];
keep_2_3_16_2 : -1 <= -S[2,16] + guard4[15]-guard4[16];
keep_2_2_17_1 : -1 <= -S[2,17]-guard2[16] + guard2[17];
keep_2_2_17_2 : -1 <= -S[2,17] + guard2[16]-guard2[17];
keep_2_1_17_1 : -1 <= -S[2,17]-guard0[16] + guard0[17];
keep_2_1_17_2 : -1 <= -S[2,17] + guard0[16]-guard0[17];
keep_2_3_17_1 : -1 <= -S[2,17]-guard4[16] + guard4[17];
keep_2_3_17_2 : -1 <= -S[2,17] + guard4[16]-guard4[17];
keep_2_2_18_1 : -1 <= -S[2,18]-guard2[17] + guard2[18];
keep_2_2_18_2 : -1 <= -S[2,18] + guard2[17]-guard2[18];
keep_2_1_18_1 : -1 <= -S[2,18]-guard0[17] + guard0[18];
keep_2_1_18_2 : -1 <= -S[2,18] + guard0[17]-guard0[18];
keep_2_3_18_1 : -1 <= -S[2,18]-guard4[17] + guard4[18];
keep_2_3_18_2 : -1 <= -S[2,18] + guard4[17]-guard4[18];
keep_2_2_19_1 : -1 <= -S[2,19]-guard2[18] + guard2[19];
keep_2_2_19_2 : -1 <= -S[2,19] + guard2[18]-guard2[19];
keep_2_1_19_1 : -1 <= -S[2,19]-guard0[18] + guard0[19];
keep_2_1_19_2 : -1 <= -S[2,19] + guard0[18]-guard0[19];
keep_2_3_19_1 : -1 <= -S[2,19]-guard4[18] + guard4[19];
keep_2_3_19_2 : -1 <= -S[2,19] + guard4[18]-guard4[19];
keep_2_2_20_1 : -1 <= -S[2,20]-guard2[19] + guard2[20];
keep_2_2_20_2 : -1 <= -S[2,20] + guard2[19]-guard2[20];
keep_2_1_20_1 : -1 <= -S[2,20]-guard0[19] + guard0[20];
keep_2_1_20_2 : -1 <= -S[2,20] + guard0[19]-guard0[20];
keep_2_3_20_1 : -1 <= -S[2,20]-guard4[19] + guard4[20];
keep_2_3_20_2 : -1 <= -S[2,20] + guard4[19]-guard4[20];
keep_2_2_21_1 : -1 <= -S[2,21]-guard2[20] + guard2[21];
keep_2_2_21_2 : -1 <= -S[2,21] + guard2[20]-guard2[21];
keep_2_1_21_1 : -1 <= -S[2,21]-guard0[20] + guard0[21];
keep_2_1_21_2 : -1 <= -S[2,21] + guard0[20]-guard0[21];
keep_2_3_21_1 : -1 <= -S[2,21]-guard4[20] + guard4[21];
keep_2_3_21_2 : -1 <= -S[2,21] + guard4[20]-guard4[21];
keep_2_2_22_1 : -1 <= -S[2,22]-guard2[21] + guard2[22];
keep_2_2_22_2 : -1 <= -S[2,22] + guard2[21]-guard2[22];
keep_2_1_22_1 : -1 <= -S[2,22]-guard0[21] + guard0[22];
keep_2_1_22_2 : -1 <= -S[2,22] + guard0[21]-guard0[22];
keep_2_3_22_1 : -1 <= -S[2,22]-guard4[21] + guard4[22];
keep_2_3_22_2 : -1 <= -S[2,22] + guard4[21]-guard4[22];
keep_2_2_23_1 : -1 <= -S[2,23]-guard2[22] + guard2[23];
keep_2_2_23_2 : -1 <= -S[2,23] + guard2[22]-guard2[23];
keep_2_1_23_1 : -1 <= -S[2,23]-guard0[22] + guard0[23];
keep_2_1_23_2 : -1 <= -S[2,23] + guard0[22]-guard0[23];
keep_2_3_23_1 : -1 <= -S[2,23]-guard4[22] + guard4[23];
keep_2_3_23_2 : -1 <= -S[2,23] + guard4[22]-guard4[23];
keep_3_2_1_1 : -1 <= -S[3,1]-guard2[0] + guard2[1];
keep_3_2_1_2 : -1 <= -S[3,1] + guard2[0]-guard2[1];
keep_3_1_1_1 : -1 <= -S[3,1]-guard0[0] + guard0[1];
keep_3_1_1_2 : -1 <= -S[3,1] + guard0[0]-guard0[1];
keep_3_3_1_1 : -1 <= -S[3,1]-guard4[0] + guard4[1];
keep_3_3_1_2 : -1 <= -S[3,1] + guard4[0]-guard4[1];
keep_3_2_2_1 : -1 <= -S[3,2]-guard2[1] + guard2[2];
keep_3_2_2_2 : -1 <= -S[3,2] + guard2[1]-guard2[2];
keep_3_1_2_1 : -1 <= -S[3,2]-guard0[1] + guard0[2];
keep_3_1_2_2 : -1 <= -S[3,2] + guard0[1]-guard0[2];
keep_3_3_2_1 : -1 <= -S[3,2]-guard4[1] + guard4[2];
keep_3_3_2_2 : -1 <= -S[3,2] + guard4[1]-guard4[2];
keep_3_2_3_1 : -1 <= -S[3,3]-guard2[2] + guard2[3];
keep_3_2_3_2 : -1 <= -S[3,3] + guard2[2]-guard2[3];
keep_3_1_3_1 : -1 <= -S[3,3]-guard0[2] + guard0[3];
keep_3_1_3_2 : -1 <= -S[3,3] + guard0[2]-guard0[3];
keep_3_3_3_1 : -1 <= -S[3,3]-guard4[2] + guard4[3];
keep_3_3_3_2 : -1 <= -S[3,3] + guard4[2]-guard4[3];
keep_3_2_4_1 : -1 <= -S[3,4]-guard2[3] + guard2[4];
keep_3_2_4_2 : -1 <= -S[3,4] + guard2[3]-guard2[4];
keep_3_1_4_1 : -1 <= -S[3,4]-guard0[3] + guard0[4];
keep_3_1_4_2 : -1 <= -S[3,4] + guard0[3]-guard0[4];
keep_3_3_4_1 : -1 <= -S[3,4]-guard4[3] + guard4[4];
keep_3_3_4_2 : -1 <= -S[3,4] + guard4[3]-guard4[4];
keep_3_2_5_1 : -1 <= -S[3,5]-guard2[4] + guard2[5];
keep_3_2_5_2 : -1 <= -S[3,5] + guard2[4]-guard2[5];
keep_3_1_5_1 : -1 <= -S[3,5]-guard0[4] + guard0[5];
keep_3_1_5_2 : -1 <= -S[3,5] + guard0[4]-guard0[5];
keep_3_3_5_1 : -1 <= -S[3,5]-guard4[4] + guard4[5];
keep_3_3_5_2 : -1 <= -S[3,5] + guard4[4]-guard4[5];
keep_3_2_6_1 : -1 <= -S[3,6]-guard2[5] + guard2[6];
keep_3_2_6_2 : -1 <= -S[3,6] + guard2[5]-guard2[6];
keep_3_1_6_1 : -1 <= -S[3,6]-guard0[5] + guard0[6];
keep_3_1_6_2 : -1 <= -S[3,6] + guard0[5]-guard0[6];
keep_3_3_6_1 : -1 <= -S[3,6]-guard4[5] + guard4[6];
keep_3_3_6_2 : -1 <= -S[3,6] + guard4[5]-guard4[6];
keep_3_2_7_1 : -1 <= -S[3,7]-guard2[6] + guard2[7];
keep_3_2_7_2 : -1 <= -S[3,7] + guard2[6]-guard2[7];
keep_3_1_7_1 : -1 <= -S[3,7]-guard0[6] + guard0[7];
keep_3_1_7_2 : -1 <= -S[3,7] + guard0[6]-guard0[7];
keep_3_3_7_1 : -1 <= -S[3,7]-guard4[6] + guard4[7];
keep_3_3_7_2 : -1 <= -S[3,7] + guard4[6]-guard4[7];
keep_3_2_8_1 : -1 <= -S[3,8]-guard2[7] + guard2[8];
keep_3_2_8_2 : -1 <= -S[3,8] + guard2[7]-guard2[8];
keep_3_1_8_1 : -1 <= -S[3,8]-guard0[7] + guard0[8];
keep_3_1_8_2 : -1 <= -S[3,8] + guard0[7]-guard0[8];
keep_3_3_8_1 : -1 <= -S[3,8]-guard4[7] + guard4[8];
keep_3_3_8_2 : -1 <= -S[3,8] + guard4[7]-guard4[8];
keep_3_2_9_1 : -1 <= -S[3,9]-guard2[8] + guard2[9];
keep_3_2_9_2 : -1 <= -S[3,9] + guard2[8]-guard2[9];
keep_3_1_9_1 : -1 <= -S[3,9]-guard0[8] + guard0[9];
keep_3_1_9_2 : -1 <= -S[3,9] + guard0[8]-guard0[9];
keep_3_3_9_1 : -1 <= -S[3,9]-guard4[8] + guard4[9];
keep_3_3_9_2 : -1 <= -S[3,9] + guard4[8]-guard4[9];
keep_3_2_10_1 : -1 <= -S[3,10] + guard2[10]-guard2[9];
keep_3_2_10_2 : -1 <= -S[3,10]-guard2[10] + guard2[9];
keep_3_1_10_1 : -1 <= -S[3,10] + guard0[10]-guard0[9];
keep_3_1_10_2 : -1 <= -S[3,10]-guard0[10] + guard0[9];
keep_3_3_10_1 : -1 <= -S[3,10] + guard4[10]-guard4[9];
keep_3_3_10_2 : -1 <= -S[3,10]-guard4[10] + guard4[9];
keep_3_2_11_1 : -1 <= -S[3,11]-guard2[10] + guard2[11];
keep_3_2_11_2 : -1 <= -S[3,11] + guard2[10]-guard2[11];
keep_3_1_11_1 : -1 <= -S[3,11]-guard0[10] + guard0[11];
keep_3_1_11_2 : -1 <= -S[3,11] + guard0[10]-guard0[11];
keep_3_3_11_1 : -1 <= -S[3,11]-guard4[10] + guard4[11];
keep_3_3_11_2 : -1 <= -S[3,11] + guard4[10]-guard4[11];
keep_3_2_12_1 : -1 <= -S[3,12]-guard2[11] + guard2[12];
keep_3_2_12_2 : -1 <= -S[3,12] + guard2[11]-guard2[12];
keep_3_1_12_1 : -1 <= -S[3,12]-guard0[11] + guard0[12];
keep_3_1_12_2 : -1 <= -S[3,12] + guard0[11]-guard0[12];
keep_3_3_12_1 : -1 <= -S[3,12]-guard4[11] + guard4[12];
keep_3_3_12_2 : -1 <= -S[3,12] + guard4[11]-guard4[12];
keep_3_2_13_1 : -1 <= -S[3,13]-guard2[12] + guard2[13];
keep_3_2_13_2 : -1 <= -S[3,13] + guard2[12]-guard2[13];
keep_3_1_13_1 : -1 <= -S[3,13]-guard0[12] + guard0[13];
keep_3_1_13_2 : -1 <= -S[3,13] + guard0[12]-guard0[13];
keep_3_3_13_1 : -1 <= -S[3,13]-guard4[12] + guard4[13];
keep_3_3_13_2 : -1 <= -S[3,13] + guard4[12]-guard4[13];
keep_3_2_14_1 : -1 <= -S[3,14]-guard2[13] + guard2[14];
keep_3_2_14_2 : -1 <= -S[3,14] + guard2[13]-guard2[14];
keep_3_1_14_1 : -1 <= -S[3,14]-guard0[13] + guard0[14];
keep_3_1_14_2 : -1 <= -S[3,14] + guard0[13]-guard0[14];
keep_3_3_14_1 : -1 <= -S[3,14]-guard4[13] + guard4[14];
keep_3_3_14_2 : -1 <= -S[3,14] + guard4[13]-guard4[14];
keep_3_2_15_1 : -1 <= -S[3,15]-guard2[14] + guard2[15];
keep_3_2_15_2 : -1 <= -S[3,15] + guard2[14]-guard2[15];
keep_3_1_15_1 : -1 <= -S[3,15]-guard0[14] + guard0[15];
keep_3_1_15_2 : -1 <= -S[3,15] + guard0[14]-guard0[15];
keep_3_3_15_1 : -1 <= -S[3,15]-guard4[14] + guard4[15];
keep_3_3_15_2 : -1 <= -S[3,15] + guard4[14]-guard4[15];
keep_3_2_16_1 : -1 <= -S[3,16]-guard2[15] + guard2[16];
keep_3_2_16_2 : -1 <= -S[3,16] + guard2[15]-guard2[16];
keep_3_1_16_1 : -1 <= -S[3,16]-guard0[15] + guard0[16];
keep_3_1_16_2 : -1 <= -S[3,16] + guard0[15]-guard0[16];
keep_3_3_16_1 : -1 <= -S[3,16]-guard4[15] + guard4[16];
keep_3_3_16_2 : -1 <= -S[3,16] + guard4[15]-guard4[16];
keep_3_2_17_1 : -1 <= -S[3,17]-guard2[16] + guard2[17];
keep_3_2_17_2 : -1 <= -S[3,17] + guard2[16]-guard2[17];
keep_3_1_17_1 : -1 <= -S[3,17]-guard0[16] + guard0[17];
keep_3_1_17_2 : -1 <= -S[3,17] + guard0[16]-guard0[17];
keep_3_3_17_1 : -1 <= -S[3,17]-guard4[16] + guard4[17];
keep_3_3_17_2 : -1 <= -S[3,17] + guard4[16]-guard4[17];
keep_3_2_18_1 : -1 <= -S[3,18]-guard2[17] + guard2[18];
keep_3_2_18_2 : -1 <= -S[3,18] + guard2[17]-guard2[18];
keep_3_1_18_1 : -1 <= -S[3,18]-guard0[17] + guard0[18];
keep_3_1_18_2 : -1 <= -S[3,18] + guard0[17]-guard0[18];
keep_3_3_18_1 : -1 <= -S[3,18]-guard4[17] + guard4[18];
keep_3_3_18_2 : -1 <= -S[3,18] + guard4[17]-guard4[18];
keep_3_2_19_1 : -1 <= -S[3,19]-guard2[18] + guard2[19];
keep_3_2_19_2 : -1 <= -S[3,19] + guard2[18]-guard2[19];
keep_3_1_19_1 : -1 <= -S[3,19]-guard0[18] + guard0[19];
keep_3_1_19_2 : -1 <= -S[3,19] + guard0[18]-guard0[19];
keep_3_3_19_1 : -1 <= -S[3,19]-guard4[18] + guard4[19];
keep_3_3_19_2 : -1 <= -S[3,19] + guard4[18]-guard4[19];
keep_3_2_20_1 : -1 <= -S[3,20]-guard2[19] + guard2[20];
keep_3_2_20_2 : -1 <= -S[3,20] + guard2[19]-guard2[20];
keep_3_1_20_1 : -1 <= -S[3,20]-guard0[19] + guard0[20];
keep_3_1_20_2 : -1 <= -S[3,20] + guard0[19]-guard0[20];
keep_3_3_20_1 : -1 <= -S[3,20]-guard4[19] + guard4[20];
keep_3_3_20_2 : -1 <= -S[3,20] + guard4[19]-guard4[20];
keep_3_2_21_1 : -1 <= -S[3,21]-guard2[20] + guard2[21];
keep_3_2_21_2 : -1 <= -S[3,21] + guard2[20]-guard2[21];
keep_3_1_21_1 : -1 <= -S[3,21]-guard0[20] + guard0[21];
keep_3_1_21_2 : -1 <= -S[3,21] + guard0[20]-guard0[21];
keep_3_3_21_1 : -1 <= -S[3,21]-guard4[20] + guard4[21];
keep_3_3_21_2 : -1 <= -S[3,21] + guard4[20]-guard4[21];
keep_3_2_22_1 : -1 <= -S[3,22]-guard2[21] + guard2[22];
keep_3_2_22_2 : -1 <= -S[3,22] + guard2[21]-guard2[22];
keep_3_1_22_1 : -1 <= -S[3,22]-guard0[21] + guard0[22];
keep_3_1_22_2 : -1 <= -S[3,22] + guard0[21]-guard0[22];
keep_3_3_22_1 : -1 <= -S[3,22]-guard4[21] + guard4[22];
keep_3_3_22_2 : -1 <= -S[3,22] + guard4[21]-guard4[22];
keep_3_2_23_1 : -1 <= -S[3,23]-guard2[22] + guard2[23];
keep_3_2_23_2 : -1 <= -S[3,23] + guard2[22]-guard2[23];
keep_3_1_23_1 : -1 <= -S[3,23]-guard0[22] + guard0[23];
keep_3_1_23_2 : -1 <= -S[3,23] + guard0[22]-guard0[23];
keep_3_3_23_1 : -1 <= -S[3,23]-guard4[22] + guard4[23];
keep_3_3_23_2 : -1 <= -S[3,23] + guard4[22]-guard4[23];
keep_4_2_1_1 : -1 <= -S[4,1]-guard2[0] + guard2[1];
keep_4_2_1_2 : -1 <= -S[4,1] + guard2[0]-guard2[1];
keep_4_1_1_1 : -1 <= -S[4,1]-guard0[0] + guard0[1];
keep_4_1_1_2 : -1 <= -S[4,1] + guard0[0]-guard0[1];
keep_4_3_1_1 : -1 <= -S[4,1]-guard4[0] + guard4[1];
keep_4_3_1_2 : -1 <= -S[4,1] + guard4[0]-guard4[1];
keep_4_2_2_1 : -1 <= -S[4,2]-guard2[1] + guard2[2];
keep_4_2_2_2 : -1 <= -S[4,2] + guard2[1]-guard2[2];
keep_4_1_2_1 : -1 <= -S[4,2]-guard0[1] + guard0[2];
keep_4_1_2_2 : -1 <= -S[4,2] + guard0[1]-guard0[2];
keep_4_3_2_1 : -1 <= -S[4,2]-guard4[1] + guard4[2];
keep_4_3_2_2 : -1 <= -S[4,2] + guard4[1]-guard4[2];
keep_4_2_3_1 : -1 <= -S[4,3]-guard2[2] + guard2[3];
keep_4_2_3_2 : -1 <= -S[4,3] + guard2[2]-guard2[3];
keep_4_1_3_1 : -1 <= -S[4,3]-guard0[2] + guard0[3];
keep_4_1_3_2 : -1 <= -S[4,3] + guard0[2]-guard0[3];
keep_4_3_3_1 : -1 <= -S[4,3]-guard4[2] + guard4[3];
keep_4_3_3_2 : -1 <= -S[4,3] + guard4[2]-guard4[3];
keep_4_2_4_1 : -1 <= -S[4,4]-guard2[3] + guard2[4];
keep_4_2_4_2 : -1 <= -S[4,4] + guard2[3]-guard2[4];
keep_4_1_4_1 : -1 <= -S[4,4]-guard0[3] + guard0[4];
keep_4_1_4_2 : -1 <= -S[4,4] + guard0[3]-guard0[4];
keep_4_3_4_1 : -1 <= -S[4,4]-guard4[3] + guard4[4];
keep_4_3_4_2 : -1 <= -S[4,4] + guard4[3]-guard4[4];
keep_4_2_5_1 : -1 <= -S[4,5]-guard2[4] + guard2[5];
keep_4_2_5_2 : -1 <= -S[4,5] + guard2[4]-guard2[5];
keep_4_1_5_1 : -1 <= -S[4,5]-guard0[4] + guard0[5];
keep_4_1_5_2 : -1 <= -S[4,5] + guard0[4]-guard0[5];
keep_4_3_5_1 : -1 <= -S[4,5]-guard4[4] + guard4[5];
keep_4_3_5_2 : -1 <= -S[4,5] + guard4[4]-guard4[5];
keep_4_2_6_1 : -1 <= -S[4,6]-guard2[5] + guard2[6];
keep_4_2_6_2 : -1 <= -S[4,6] + guard2[5]-guard2[6];
keep_4_1_6_1 : -1 <= -S[4,6]-guard0[5] + guard0[6];
keep_4_1_6_2 : -1 <= -S[4,6] + guard0[5]-guard0[6];
keep_4_3_6_1 : -1 <= -S[4,6]-guard4[5] + guard4[6];
keep_4_3_6_2 : -1 <= -S[4,6] + guard4[5]-guard4[6];
keep_4_2_7_1 : -1 <= -S[4,7]-guard2[6] + guard2[7];
keep_4_2_7_2 : -1 <= -S[4,7] + guard2[6]-guard2[7];
keep_4_1_7_1 : -1 <= -S[4,7]-guard0[6] + guard0[7];
keep_4_1_7_2 : -1 <= -S[4,7] + guard0[6]-guard0[7];
keep_4_3_7_1 : -1 <= -S[4,7]-guard4[6] + guard4[7];
keep_4_3_7_2 : -1 <= -S[4,7] + guard4[6]-guard4[7];
keep_4_2_8_1 : -1 <= -S[4,8]-guard2[7] + guard2[8];
keep_4_2_8_2 : -1 <= -S[4,8] + guard2[7]-guard2[8];
keep_4_1_8_1 : -1 <= -S[4,8]-guard0[7] + guard0[8];
keep_4_1_8_2 : -1 <= -S[4,8] + guard0[7]-guard0[8];
keep_4_3_8_1 : -1 <= -S[4,8]-guard4[7] + guard4[8];
keep_4_3_8_2 : -1 <= -S[4,8] + guard4[7]-guard4[8];
keep_4_2_9_1 : -1 <= -S[4,9]-guard2[8] + guard2[9];
keep_4_2_9_2 : -1 <= -S[4,9] + guard2[8]-guard2[9];
keep_4_1_9_1 : -1 <= -S[4,9]-guard0[8] + guard0[9];
keep_4_1_9_2 : -1 <= -S[4,9] + guard0[8]-guard0[9];
keep_4_3_9_1 : -1 <= -S[4,9]-guard4[8] + guard4[9];
keep_4_3_9_2 : -1 <= -S[4,9] + guard4[8]-guard4[9];
keep_4_2_10_1 : -1 <= -S[4,10] + guard2[10]-guard2[9];
keep_4_2_10_2 : -1 <= -S[4,10]-guard2[10] + guard2[9];
keep_4_1_10_1 : -1 <= -S[4,10] + guard0[10]-guard0[9];
keep_4_1_10_2 : -1 <= -S[4,10]-guard0[10] + guard0[9];
keep_4_3_10_1 : -1 <= -S[4,10] + guard4[10]-guard4[9];
keep_4_3_10_2 : -1 <= -S[4,10]-guard4[10] + guard4[9];
keep_4_2_11_1 : -1 <= -S[4,11]-guard2[10] + guard2[11];
keep_4_2_11_2 : -1 <= -S[4,11] + guard2[10]-guard2[11];
keep_4_1_11_1 : -1 <= -S[4,11]-guard0[10] + guard0[11];
keep_4_1_11_2 : -1 <= -S[4,11] + guard0[10]-guard0[11];
keep_4_3_11_1 : -1 <= -S[4,11]-guard4[10] + guard4[11];
keep_4_3_11_2 : -1 <= -S[4,11] + guard4[10]-guard4[11];
keep_4_2_12_1 : -1 <= -S[4,12]-guard2[11] + guard2[12];
keep_4_2_12_2 : -1 <= -S[4,12] + guard2[11]-guard2[12];
keep_4_1_12_1 : -1 <= -S[4,12]-guard0[11] + guard0[12];
keep_4_1_12_2 : -1 <= -S[4,12] + guard0[11]-guard0[12];
keep_4_3_12_1 : -1 <= -S[4,12]-guard4[11] + guard4[12];
keep_4_3_12_2 : -1 <= -S[4,12] + guard4[11]-guard4[12];
keep_4_2_13_1 : -1 <= -S[4,13]-guard2[12] + guard2[13];
keep_4_2_13_2 : -1 <= -S[4,13] + guard2[12]-guard2[13];
keep_4_1_13_1 : -1 <= -S[4,13]-guard0[12] + guard0[13];
keep_4_1_13_2 : -1 <= -S[4,13] + guard0[12]-guard0[13];
keep_4_3_13_1 : -1 <= -S[4,13]-guard4[12] + guard4[13];
keep_4_3_13_2 : -1 <= -S[4,13] + guard4[12]-guard4[13];
keep_4_2_14_1 : -1 <= -S[4,14]-guard2[13] + guard2[14];
keep_4_2_14_2 : -1 <= -S[4,14] + guard2[13]-guard2[14];
keep_4_1_14_1 : -1 <= -S[4,14]-guard0[13] + guard0[14];
keep_4_1_14_2 : -1 <= -S[4,14] + guard0[13]-guard0[14];
keep_4_3_14_1 : -1 <= -S[4,14]-guard4[13] + guard4[14];
keep_4_3_14_2 : -1 <= -S[4,14] + guard4[13]-guard4[14];
keep_4_2_15_1 : -1 <= -S[4,15]-guard2[14] + guard2[15];
keep_4_2_15_2 : -1 <= -S[4,15] + guard2[14]-guard2[15];
keep_4_1_15_1 : -1 <= -S[4,15]-guard0[14] + guard0[15];
keep_4_1_15_2 : -1 <= -S[4,15] + guard0[14]-guard0[15];
keep_4_3_15_1 : -1 <= -S[4,15]-guard4[14] + guard4[15];
keep_4_3_15_2 : -1 <= -S[4,15] + guard4[14]-guard4[15];
keep_4_2_16_1 : -1 <= -S[4,16]-guard2[15] + guard2[16];
keep_4_2_16_2 : -1 <= -S[4,16] + guard2[15]-guard2[16];
keep_4_1_16_1 : -1 <= -S[4,16]-guard0[15] + guard0[16];
keep_4_1_16_2 : -1 <= -S[4,16] + guard0[15]-guard0[16];
keep_4_3_16_1 : -1 <= -S[4,16]-guard4[15] + guard4[16];
keep_4_3_16_2 : -1 <= -S[4,16] + guard4[15]-guard4[16];
keep_4_2_17_1 : -1 <= -S[4,17]-guard2[16] + guard2[17];
keep_4_2_17_2 : -1 <= -S[4,17] + guard2[16]-guard2[17];
keep_4_1_17_1 : -1 <= -S[4,17]-guard0[16] + guard0[17];
keep_4_1_17_2 : -1 <= -S[4,17] + guard0[16]-guard0[17];
keep_4_3_17_1 : -1 <= -S[4,17]-guard4[16] + guard4[17];
keep_4_3_17_2 : -1 <= -S[4,17] + guard4[16]-guard4[17];
keep_4_2_18_1 : -1 <= -S[4,18]-guard2[17] + guard2[18];
keep_4_2_18_2 : -1 <= -S[4,18] + guard2[17]-guard2[18];
keep_4_1_18_1 : -1 <= -S[4,18]-guard0[17] + guard0[18];
keep_4_1_18_2 : -1 <= -S[4,18] + guard0[17]-guard0[18];
keep_4_3_18_1 : -1 <= -S[4,18]-guard4[17] + guard4[18];
keep_4_3_18_2 : -1 <= -S[4,18] + guard4[17]-guard4[18];
keep_4_2_19_1 : -1 <= -S[4,19]-guard2[18] + guard2[19];
keep_4_2_19_2 : -1 <= -S[4,19] + guard2[18]-guard2[19];
keep_4_1_19_1 : -1 <= -S[4,19]-guard0[18] + guard0[19];
keep_4_1_19_2 : -1 <= -S[4,19] + guard0[18]-guard0[19];
keep_4_3_19_1 : -1 <= -S[4,19]-guard4[18] + guard4[19];
keep_4_3_19_2 : -1 <= -S[4,19] + guard4[18]-guard4[19];
keep_4_2_20_1 : -1 <= -S[4,20]-guard2[19] + guard2[20];
keep_4_2_20_2 : -1 <= -S[4,20] + guard2[19]-guard2[20];
keep_4_1_20_1 : -1 <= -S[4,20]-guard0[19] + guard0[20];
keep_4_1_20_2 : -1 <= -S[4,20] + guard0[19]-guard0[20];
keep_4_3_20_1 : -1 <= -S[4,20]-guard4[19] + guard4[20];
keep_4_3_20_2 : -1 <= -S[4,20] + guard4[19]-guard4[20];
keep_4_2_21_1 : -1 <= -S[4,21]-guard2[20] + guard2[21];
keep_4_2_21_2 : -1 <= -S[4,21] + guard2[20]-guard2[21];
keep_4_1_21_1 : -1 <= -S[4,21]-guard0[20] + guard0[21];
keep_4_1_21_2 : -1 <= -S[4,21] + guard0[20]-guard0[21];
keep_4_3_21_1 : -1 <= -S[4,21]-guard4[20] + guard4[21];
keep_4_3_21_2 : -1 <= -S[4,21] + guard4[20]-guard4[21];
keep_4_2_22_1 : -1 <= -S[4,22]-guard2[21] + guard2[22];
keep_4_2_22_2 : -1 <= -S[4,22] + guard2[21]-guard2[22];
keep_4_1_22_1 : -1 <= -S[4,22]-guard0[21] + guard0[22];
keep_4_1_22_2 : -1 <= -S[4,22] + guard0[21]-guard0[22];
keep_4_3_22_1 : -1 <= -S[4,22]-guard4[21] + guard4[22];
keep_4_3_22_2 : -1 <= -S[4,22] + guard4[21]-guard4[22];
keep_4_2_23_1 : -1 <= -S[4,23]-guard2[22] + guard2[23];
keep_4_2_23_2 : -1 <= -S[4,23] + guard2[22]-guard2[23];
keep_4_1_23_1 : -1 <= -S[4,23]-guard0[22] + guard0[23];
keep_4_1_23_2 : -1 <= -S[4,23] + guard0[22]-guard0[23];
keep_4_3_23_1 : -1 <= -S[4,23]-guard4[22] + guard4[23];
keep_4_3_23_2 : -1 <= -S[4,23] + guard4[22]-guard4[23];
keep_5_2_1_1 : -1 <= -S[5,1]-guard2[0] + guard2[1];
keep_5_2_1_2 : -1 <= -S[5,1] + guard2[0]-guard2[1];
keep_5_1_1_1 : -1 <= -S[5,1]-guard0[0] + guard0[1];
keep_5_1_1_2 : -1 <= -S[5,1] + guard0[0]-guard0[1];
keep_5_3_1_1 : -1 <= -S[5,1]-guard4[0] + guard4[1];
keep_5_3_1_2 : -1 <= -S[5,1] + guard4[0]-guard4[1];
keep_5_2_2_1 : -1 <= -S[5,2]-guard2[1] + guard2[2];
keep_5_2_2_2 : -1 <= -S[5,2] + guard2[1]-guard2[2];
keep_5_1_2_1 : -1 <= -S[5,2]-guard0[1] + guard0[2];
keep_5_1_2_2 : -1 <= -S[5,2] + guard0[1]-guard0[2];
keep_5_3_2_1 : -1 <= -S[5,2]-guard4[1] + guard4[2];
keep_5_3_2_2 : -1 <= -S[5,2] + guard4[1]-guard4[2];
keep_5_2_3_1 : -1 <= -S[5,3]-guard2[2] + guard2[3];
keep_5_2_3_2 : -1 <= -S[5,3] + guard2[2]-guard2[3];
keep_5_1_3_1 : -1 <= -S[5,3]-guard0[2] + guard0[3];
keep_5_1_3_2 : -1 <= -S[5,3] + guard0[2]-guard0[3];
keep_5_3_3_1 : -1 <= -S[5,3]-guard4[2] + guard4[3];
keep_5_3_3_2 : -1 <= -S[5,3] + guard4[2]-guard4[3];
keep_5_2_4_1 : -1 <= -S[5,4]-guard2[3] + guard2[4];
keep_5_2_4_2 : -1 <= -S[5,4] + guard2[3]-guard2[4];
keep_5_1_4_1 : -1 <= -S[5,4]-guard0[3] + guard0[4];
keep_5_1_4_2 : -1 <= -S[5,4] + guard0[3]-guard0[4];
keep_5_3_4_1 : -1 <= -S[5,4]-guard4[3] + guard4[4];
keep_5_3_4_2 : -1 <= -S[5,4] + guard4[3]-guard4[4];
keep_5_2_5_1 : -1 <= -S[5,5]-guard2[4] + guard2[5];
keep_5_2_5_2 : -1 <= -S[5,5] + guard2[4]-guard2[5];
keep_5_1_5_1 : -1 <= -S[5,5]-guard0[4] + guard0[5];
keep_5_1_5_2 : -1 <= -S[5,5] + guard0[4]-guard0[5];
keep_5_3_5_1 : -1 <= -S[5,5]-guard4[4] + guard4[5];
keep_5_3_5_2 : -1 <= -S[5,5] + guard4[4]-guard4[5];
keep_5_2_6_1 : -1 <= -S[5,6]-guard2[5] + guard2[6];
keep_5_2_6_2 : -1 <= -S[5,6] + guard2[5]-guard2[6];
keep_5_1_6_1 : -1 <= -S[5,6]-guard0[5] + guard0[6];
keep_5_1_6_2 : -1 <= -S[5,6] + guard0[5]-guard0[6];
keep_5_3_6_1 : -1 <= -S[5,6]-guard4[5] + guard4[6];
keep_5_3_6_2 : -1 <= -S[5,6] + guard4[5]-guard4[6];
keep_5_2_7_1 : -1 <= -S[5,7]-guard2[6] + guard2[7];
keep_5_2_7_2 : -1 <= -S[5,7] + guard2[6]-guard2[7];
keep_5_1_7_1 : -1 <= -S[5,7]-guard0[6] + guard0[7];
keep_5_1_7_2 : -1 <= -S[5,7] + guard0[6]-guard0[7];
keep_5_3_7_1 : -1 <= -S[5,7]-guard4[6] + guard4[7];
keep_5_3_7_2 : -1 <= -S[5,7] + guard4[6]-guard4[7];
keep_5_2_8_1 : -1 <= -S[5,8]-guard2[7] + guard2[8];
keep_5_2_8_2 : -1 <= -S[5,8] + guard2[7]-guard2[8];
keep_5_1_8_1 : -1 <= -S[5,8]-guard0[7] + guard0[8];
keep_5_1_8_2 : -1 <= -S[5,8] + guard0[7]-guard0[8];
keep_5_3_8_1 : -1 <= -S[5,8]-guard4[7] + guard4[8];
keep_5_3_8_2 : -1 <= -S[5,8] + guard4[7]-guard4[8];
keep_5_2_9_1 : -1 <= -S[5,9]-guard2[8] + guard2[9];
keep_5_2_9_2 : -1 <= -S[5,9] + guard2[8]-guard2[9];
keep_5_1_9_1 : -1 <= -S[5,9]-guard0[8] + guard0[9];
keep_5_1_9_2 : -1 <= -S[5,9] + guard0[8]-guard0[9];
keep_5_3_9_1 : -1 <= -S[5,9]-guard4[8] + guard4[9];
keep_5_3_9_2 : -1 <= -S[5,9] + guard4[8]-guard4[9];
keep_5_2_10_1 : -1 <= -S[5,10] + guard2[10]-guard2[9];
keep_5_2_10_2 : -1 <= -S[5,10]-guard2[10] + guard2[9];
keep_5_1_10_1 : -1 <= -S[5,10] + guard0[10]-guard0[9];
keep_5_1_10_2 : -1 <= -S[5,10]-guard0[10] + guard0[9];
keep_5_3_10_1 : -1 <= -S[5,10] + guard4[10]-guard4[9];
keep_5_3_10_2 : -1 <= -S[5,10]-guard4[10] + guard4[9];
keep_5_2_11_1 : -1 <= -S[5,11]-guard2[10] + guard2[11];
keep_5_2_11_2 : -1 <= -S[5,11] + guard2[10]-guard2[11];
keep_5_1_11_1 : -1 <= -S[5,11]-guard0[10] + guard0[11];
keep_5_1_11_2 : -1 <= -S[5,11] + guard0[10]-guard0[11];
keep_5_3_11_1 : -1 <= -S[5,11]-guard4[10] + guard4[11];
keep_5_3_11_2 : -1 <= -S[5,11] + guard4[10]-guard4[11];
keep_5_2_12_1 : -1 <= -S[5,12]-guard2[11] + guard2[12];
keep_5_2_12_2 : -1 <= -S[5,12] + guard2[11]-guard2[12];
keep_5_1_12_1 : -1 <= -S[5,12]-guard0[11] + guard0[12];
keep_5_1_12_2 : -1 <= -S[5,12] + guard0[11]-guard0[12];
keep_5_3_12_1 : -1 <= -S[5,12]-guard4[11] + guard4[12];
keep_5_3_12_2 : -1 <= -S[5,12] + guard4[11]-guard4[12];
keep_5_2_13_1 : -1 <= -S[5,13]-guard2[12] + guard2[13];
keep_5_2_13_2 : -1 <= -S[5,13] + guard2[12]-guard2[13];
keep_5_1_13_1 : -1 <= -S[5,13]-guard0[12] + guard0[13];
keep_5_1_13_2 : -1 <= -S[5,13] + guard0[12]-guard0[13];
keep_5_3_13_1 : -1 <= -S[5,13]-guard4[12] + guard4[13];
keep_5_3_13_2 : -1 <= -S[5,13] + guard4[12]-guard4[13];
keep_5_2_14_1 : -1 <= -S[5,14]-guard2[13] + guard2[14];
keep_5_2_14_2 : -1 <= -S[5,14] + guard2[13]-guard2[14];
keep_5_1_14_1 : -1 <= -S[5,14]-guard0[13] + guard0[14];
keep_5_1_14_2 : -1 <= -S[5,14] + guard0[13]-guard0[14];
keep_5_3_14_1 : -1 <= -S[5,14]-guard4[13] + guard4[14];
keep_5_3_14_2 : -1 <= -S[5,14] + guard4[13]-guard4[14];
keep_5_2_15_1 : -1 <= -S[5,15]-guard2[14] + guard2[15];
keep_5_2_15_2 : -1 <= -S[5,15] + guard2[14]-guard2[15];
keep_5_1_15_1 : -1 <= -S[5,15]-guard0[14] + guard0[15];
keep_5_1_15_2 : -1 <= -S[5,15] + guard0[14]-guard0[15];
keep_5_3_15_1 : -1 <= -S[5,15]-guard4[14] + guard4[15];
keep_5_3_15_2 : -1 <= -S[5,15] + guard4[14]-guard4[15];
keep_5_2_16_1 : -1 <= -S[5,16]-guard2[15] + guard2[16];
keep_5_2_16_2 : -1 <= -S[5,16] + guard2[15]-guard2[16];
keep_5_1_16_1 : -1 <= -S[5,16]-guard0[15] + guard0[16];
keep_5_1_16_2 : -1 <= -S[5,16] + guard0[15]-guard0[16];
keep_5_3_16_1 : -1 <= -S[5,16]-guard4[15] + guard4[16];
keep_5_3_16_2 : -1 <= -S[5,16] + guard4[15]-guard4[16];
keep_5_2_17_1 : -1 <= -S[5,17]-guard2[16] + guard2[17];
keep_5_2_17_2 : -1 <= -S[5,17] + guard2[16]-guard2[17];
keep_5_1_17_1 : -1 <= -S[5,17]-guard0[16] + guard0[17];
keep_5_1_17_2 : -1 <= -S[5,17] + guard0[16]-guard0[17];
keep_5_3_17_1 : -1 <= -S[5,17]-guard4[16] + guard4[17];
keep_5_3_17_2 : -1 <= -S[5,17] + guard4[16]-guard4[17];
keep_5_2_18_1 : -1 <= -S[5,18]-guard2[17] + guard2[18];
keep_5_2_18_2 : -1 <= -S[5,18] + guard2[17]-guard2[18];
keep_5_1_18_1 : -1 <= -S[5,18]-guard0[17] + guard0[18];
keep_5_1_18_2 : -1 <= -S[5,18] + guard0[17]-guard0[18];
keep_5_3_18_1 : -1 <= -S[5,18]-guard4[17] + guard4[18];
keep_5_3_18_2 : -1 <= -S[5,18] + guard4[17]-guard4[18];
keep_5_2_19_1 : -1 <= -S[5,19]-guard2[18] + guard2[19];
keep_5_2_19_2 : -1 <= -S[5,19] + guard2[18]-guard2[19];
keep_5_1_19_1 : -1 <= -S[5,19]-guard0[18] + guard0[19];
keep_5_1_19_2 : -1 <= -S[5,19] + guard0[18]-guard0[19];
keep_5_3_19_1 : -1 <= -S[5,19]-guard4[18] + guard4[19];
keep_5_3_19_2 : -1 <= -S[5,19] + guard4[18]-guard4[19];
keep_5_2_20_1 : -1 <= -S[5,20]-guard2[19] + guard2[20];
keep_5_2_20_2 : -1 <= -S[5,20] + guard2[19]-guard2[20];
keep_5_1_20_1 : -1 <= -S[5,20]-guard0[19] + guard0[20];
keep_5_1_20_2 : -1 <= -S[5,20] + guard0[19]-guard0[20];
keep_5_3_20_1 : -1 <= -S[5,20]-guard4[19] + guard4[20];
keep_5_3_20_2 : -1 <= -S[5,20] + guard4[19]-guard4[20];
keep_5_2_21_1 : -1 <= -S[5,21]-guard2[20] + guard2[21];
keep_5_2_21_2 : -1 <= -S[5,21] + guard2[20]-guard2[21];
keep_5_1_21_1 : -1 <= -S[5,21]-guard0[20] + guard0[21];
keep_5_1_21_2 : -1 <= -S[5,21] + guard0[20]-guard0[21];
keep_5_3_21_1 : -1 <= -S[5,21]-guard4[20] + guard4[21];
keep_5_3_21_2 : -1 <= -S[5,21] + guard4[20]-guard4[21];
keep_5_2_22_1 : -1 <= -S[5,22]-guard2[21] + guard2[22];
keep_5_2_22_2 : -1 <= -S[5,22] + guard2[21]-guard2[22];
keep_5_1_22_1 : -1 <= -S[5,22]-guard0[21] + guard0[22];
keep_5_1_22_2 : -1 <= -S[5,22] + guard0[21]-guard0[22];
keep_5_3_22_1 : -1 <= -S[5,22]-guard4[21] + guard4[22];
keep_5_3_22_2 : -1 <= -S[5,22] + guard4[21]-guard4[22];
keep_5_2_23_1 : -1 <= -S[5,23]-guard2[22] + guard2[23];
keep_5_2_23_2 : -1 <= -S[5,23] + guard2[22]-guard2[23];
keep_5_1_23_1 : -1 <= -S[5,23]-guard0[22] + guard0[23];
keep_5_1_23_2 : -1 <= -S[5,23] + guard0[22]-guard0[23];
keep_5_3_23_1 : -1 <= -S[5,23]-guard4[22] + guard4[23];
keep_5_3_23_2 : -1 <= -S[5,23] + guard4[22]-guard4[23];
keep_6_2_1_1 : -1 <= -S[6,1]-guard2[0] + guard2[1];
keep_6_2_1_2 : -1 <= -S[6,1] + guard2[0]-guard2[1];
keep_6_1_1_1 : -1 <= -S[6,1]-guard0[0] + guard0[1];
keep_6_1_1_2 : -1 <= -S[6,1] + guard0[0]-guard0[1];
keep_6_3_1_1 : -1 <= -S[6,1]-guard4[0] + guard4[1];
keep_6_3_1_2 : -1 <= -S[6,1] + guard4[0]-guard4[1];
keep_6_2_2_1 : -1 <= -S[6,2]-guard2[1] + guard2[2];
keep_6_2_2_2 : -1 <= -S[6,2] + guard2[1]-guard2[2];
keep_6_1_2_1 : -1 <= -S[6,2]-guard0[1] + guard0[2];
keep_6_1_2_2 : -1 <= -S[6,2] + guard0[1]-guard0[2];
keep_6_3_2_1 : -1 <= -S[6,2]-guard4[1] + guard4[2];
keep_6_3_2_2 : -1 <= -S[6,2] + guard4[1]-guard4[2];
keep_6_2_3_1 : -1 <= -S[6,3]-guard2[2] + guard2[3];
keep_6_2_3_2 : -1 <= -S[6,3] + guard2[2]-guard2[3];
keep_6_1_3_1 : -1 <= -S[6,3]-guard0[2] + guard0[3];
keep_6_1_3_2 : -1 <= -S[6,3] + guard0[2]-guard0[3];
keep_6_3_3_1 : -1 <= -S[6,3]-guard4[2] + guard4[3];
keep_6_3_3_2 : -1 <= -S[6,3] + guard4[2]-guard4[3];
keep_6_2_4_1 : -1 <= -S[6,4]-guard2[3] + guard2[4];
keep_6_2_4_2 : -1 <= -S[6,4] + guard2[3]-guard2[4];
keep_6_1_4_1 : -1 <= -S[6,4]-guard0[3] + guard0[4];
keep_6_1_4_2 : -1 <= -S[6,4] + guard0[3]-guard0[4];
keep_6_3_4_1 : -1 <= -S[6,4]-guard4[3] + guard4[4];
keep_6_3_4_2 : -1 <= -S[6,4] + guard4[3]-guard4[4];
keep_6_2_5_1 : -1 <= -S[6,5]-guard2[4] + guard2[5];
keep_6_2_5_2 : -1 <= -S[6,5] + guard2[4]-guard2[5];
keep_6_1_5_1 : -1 <= -S[6,5]-guard0[4] + guard0[5];
keep_6_1_5_2 : -1 <= -S[6,5] + guard0[4]-guard0[5];
keep_6_3_5_1 : -1 <= -S[6,5]-guard4[4] + guard4[5];
keep_6_3_5_2 : -1 <= -S[6,5] + guard4[4]-guard4[5];
keep_6_2_6_1 : -1 <= -S[6,6]-guard2[5] + guard2[6];
keep_6_2_6_2 : -1 <= -S[6,6] + guard2[5]-guard2[6];
keep_6_1_6_1 : -1 <= -S[6,6]-guard0[5] + guard0[6];
keep_6_1_6_2 : -1 <= -S[6,6] + guard0[5]-guard0[6];
keep_6_3_6_1 : -1 <= -S[6,6]-guard4[5] + guard4[6];
keep_6_3_6_2 : -1 <= -S[6,6] + guard4[5]-guard4[6];
keep_6_2_7_1 : -1 <= -S[6,7]-guard2[6] + guard2[7];
keep_6_2_7_2 : -1 <= -S[6,7] + guard2[6]-guard2[7];
keep_6_1_7_1 : -1 <= -S[6,7]-guard0[6] + guard0[7];
keep_6_1_7_2 : -1 <= -S[6,7] + guard0[6]-guard0[7];
keep_6_3_7_1 : -1 <= -S[6,7]-guard4[6] + guard4[7];
keep_6_3_7_2 : -1 <= -S[6,7] + guard4[6]-guard4[7];
keep_6_2_8_1 : -1 <= -S[6,8]-guard2[7] + guard2[8];
keep_6_2_8_2 : -1 <= -S[6,8] + guard2[7]-guard2[8];
keep_6_1_8_1 : -1 <= -S[6,8]-guard0[7] + guard0[8];
keep_6_1_8_2 : -1 <= -S[6,8] + guard0[7]-guard0[8];
keep_6_3_8_1 : -1 <= -S[6,8]-guard4[7] + guard4[8];
keep_6_3_8_2 : -1 <= -S[6,8] + guard4[7]-guard4[8];
keep_6_2_9_1 : -1 <= -S[6,9]-guard2[8] + guard2[9];
keep_6_2_9_2 : -1 <= -S[6,9] + guard2[8]-guard2[9];
keep_6_1_9_1 : -1 <= -S[6,9]-guard0[8] + guard0[9];
keep_6_1_9_2 : -1 <= -S[6,9] + guard0[8]-guard0[9];
keep_6_3_9_1 : -1 <= -S[6,9]-guard4[8] + guard4[9];
keep_6_3_9_2 : -1 <= -S[6,9] + guard4[8]-guard4[9];
keep_6_2_10_1 : -1 <= -S[6,10] + guard2[10]-guard2[9];
keep_6_2_10_2 : -1 <= -S[6,10]-guard2[10] + guard2[9];
keep_6_1_10_1 : -1 <= -S[6,10] + guard0[10]-guard0[9];
keep_6_1_10_2 : -1 <= -S[6,10]-guard0[10] + guard0[9];
keep_6_3_10_1 : -1 <= -S[6,10] + guard4[10]-guard4[9];
keep_6_3_10_2 : -1 <= -S[6,10]-guard4[10] + guard4[9];
keep_6_2_11_1 : -1 <= -S[6,11]-guard2[10] + guard2[11];
keep_6_2_11_2 : -1 <= -S[6,11] + guard2[10]-guard2[11];
keep_6_1_11_1 : -1 <= -S[6,11]-guard0[10] + guard0[11];
keep_6_1_11_2 : -1 <= -S[6,11] + guard0[10]-guard0[11];
keep_6_3_11_1 : -1 <= -S[6,11]-guard4[10] + guard4[11];
keep_6_3_11_2 : -1 <= -S[6,11] + guard4[10]-guard4[11];
keep_6_2_12_1 : -1 <= -S[6,12]-guard2[11] + guard2[12];
keep_6_2_12_2 : -1 <= -S[6,12] + guard2[11]-guard2[12];
keep_6_1_12_1 : -1 <= -S[6,12]-guard0[11] + guard0[12];
keep_6_1_12_2 : -1 <= -S[6,12] + guard0[11]-guard0[12];
keep_6_3_12_1 : -1 <= -S[6,12]-guard4[11] + guard4[12];
keep_6_3_12_2 : -1 <= -S[6,12] + guard4[11]-guard4[12];
keep_6_2_13_1 : -1 <= -S[6,13]-guard2[12] + guard2[13];
keep_6_2_13_2 : -1 <= -S[6,13] + guard2[12]-guard2[13];
keep_6_1_13_1 : -1 <= -S[6,13]-guard0[12] + guard0[13];
keep_6_1_13_2 : -1 <= -S[6,13] + guard0[12]-guard0[13];
keep_6_3_13_1 : -1 <= -S[6,13]-guard4[12] + guard4[13];
keep_6_3_13_2 : -1 <= -S[6,13] + guard4[12]-guard4[13];
keep_6_2_14_1 : -1 <= -S[6,14]-guard2[13] + guard2[14];
keep_6_2_14_2 : -1 <= -S[6,14] + guard2[13]-guard2[14];
keep_6_1_14_1 : -1 <= -S[6,14]-guard0[13] + guard0[14];
keep_6_1_14_2 : -1 <= -S[6,14] + guard0[13]-guard0[14];
keep_6_3_14_1 : -1 <= -S[6,14]-guard4[13] + guard4[14];
keep_6_3_14_2 : -1 <= -S[6,14] + guard4[13]-guard4[14];
keep_6_2_15_1 : -1 <= -S[6,15]-guard2[14] + guard2[15];
keep_6_2_15_2 : -1 <= -S[6,15] + guard2[14]-guard2[15];
keep_6_1_15_1 : -1 <= -S[6,15]-guard0[14] + guard0[15];
keep_6_1_15_2 : -1 <= -S[6,15] + guard0[14]-guard0[15];
keep_6_3_15_1 : -1 <= -S[6,15]-guard4[14] + guard4[15];
keep_6_3_15_2 : -1 <= -S[6,15] + guard4[14]-guard4[15];
keep_6_2_16_1 : -1 <= -S[6,16]-guard2[15] + guard2[16];
keep_6_2_16_2 : -1 <= -S[6,16] + guard2[15]-guard2[16];
keep_6_1_16_1 : -1 <= -S[6,16]-guard0[15] + guard0[16];
keep_6_1_16_2 : -1 <= -S[6,16] + guard0[15]-guard0[16];
keep_6_3_16_1 : -1 <= -S[6,16]-guard4[15] + guard4[16];
keep_6_3_16_2 : -1 <= -S[6,16] + guard4[15]-guard4[16];
keep_6_2_17_1 : -1 <= -S[6,17]-guard2[16] + guard2[17];
keep_6_2_17_2 : -1 <= -S[6,17] + guard2[16]-guard2[17];
keep_6_1_17_1 : -1 <= -S[6,17]-guard0[16] + guard0[17];
keep_6_1_17_2 : -1 <= -S[6,17] + guard0[16]-guard0[17];
keep_6_3_17_1 : -1 <= -S[6,17]-guard4[16] + guard4[17];
keep_6_3_17_2 : -1 <= -S[6,17] + guard4[16]-guard4[17];
keep_6_2_18_1 : -1 <= -S[6,18]-guard2[17] + guard2[18];
keep_6_2_18_2 : -1 <= -S[6,18] + guard2[17]-guard2[18];
keep_6_1_18_1 : -1 <= -S[6,18]-guard0[17] + guard0[18];
keep_6_1_18_2 : -1 <= -S[6,18] + guard0[17]-guard0[18];
keep_6_3_18_1 : -1 <= -S[6,18]-guard4[17] + guard4[18];
keep_6_3_18_2 : -1 <= -S[6,18] + guard4[17]-guard4[18];
keep_6_2_19_1 : -1 <= -S[6,19]-guard2[18] + guard2[19];
keep_6_2_19_2 : -1 <= -S[6,19] + guard2[18]-guard2[19];
keep_6_1_19_1 : -1 <= -S[6,19]-guard0[18] + guard0[19];
keep_6_1_19_2 : -1 <= -S[6,19] + guard0[18]-guard0[19];
keep_6_3_19_1 : -1 <= -S[6,19]-guard4[18] + guard4[19];
keep_6_3_19_2 : -1 <= -S[6,19] + guard4[18]-guard4[19];
keep_6_2_20_1 : -1 <= -S[6,20]-guard2[19] + guard2[20];
keep_6_2_20_2 : -1 <= -S[6,20] + guard2[19]-guard2[20];
keep_6_1_20_1 : -1 <= -S[6,20]-guard0[19] + guard0[20];
keep_6_1_20_2 : -1 <= -S[6,20] + guard0[19]-guard0[20];
keep_6_3_20_1 : -1 <= -S[6,20]-guard4[19] + guard4[20];
keep_6_3_20_2 : -1 <= -S[6,20] + guard4[19]-guard4[20];
keep_6_2_21_1 : -1 <= -S[6,21]-guard2[20] + guard2[21];
keep_6_2_21_2 : -1 <= -S[6,21] + guard2[20]-guard2[21];
keep_6_1_21_1 : -1 <= -S[6,21]-guard0[20] + guard0[21];
keep_6_1_21_2 : -1 <= -S[6,21] + guard0[20]-guard0[21];
keep_6_3_21_1 : -1 <= -S[6,21]-guard4[20] + guard4[21];
keep_6_3_21_2 : -1 <= -S[6,21] + guard4[20]-guard4[21];
keep_6_2_22_1 : -1 <= -S[6,22]-guard2[21] + guard2[22];
keep_6_2_22_2 : -1 <= -S[6,22] + guard2[21]-guard2[22];
keep_6_1_22_1 : -1 <= -S[6,22]-guard0[21] + guard0[22];
keep_6_1_22_2 : -1 <= -S[6,22] + guard0[21]-guard0[22];
keep_6_3_22_1 : -1 <= -S[6,22]-guard4[21] + guard4[22];
keep_6_3_22_2 : -1 <= -S[6,22] + guard4[21]-guard4[22];
keep_6_2_23_1 : -1 <= -S[6,23]-guard2[22] + guard2[23];
keep_6_2_23_2 : -1 <= -S[6,23] + guard2[22]-guard2[23];
keep_6_1_23_1 : -1 <= -S[6,23]-guard0[22] + guard0[23];
keep_6_1_23_2 : -1 <= -S[6,23] + guard0[22]-guard0[23];
keep_6_3_23_1 : -1 <= -S[6,23]-guard4[22] + guard4[23];
keep_6_3_23_2 : -1 <= -S[6,23] + guard4[22]-guard4[23];
keep_7_2_1_1 : -1 <= -S[7,1]-guard2[0] + guard2[1];
keep_7_2_1_2 : -1 <= -S[7,1] + guard2[0]-guard2[1];
keep_7_1_1_1 : -1 <= -S[7,1]-guard0[0] + guard0[1];
keep_7_1_1_2 : -1 <= -S[7,1] + guard0[0]-guard0[1];
keep_7_3_1_1 : -1 <= -S[7,1]-guard4[0] + guard4[1];
keep_7_3_1_2 : -1 <= -S[7,1] + guard4[0]-guard4[1];
keep_7_2_2_1 : -1 <= -S[7,2]-guard2[1] + guard2[2];
keep_7_2_2_2 : -1 <= -S[7,2] + guard2[1]-guard2[2];
keep_7_1_2_1 : -1 <= -S[7,2]-guard0[1] + guard0[2];
keep_7_1_2_2 : -1 <= -S[7,2] + guard0[1]-guard0[2];
keep_7_3_2_1 : -1 <= -S[7,2]-guard4[1] + guard4[2];
keep_7_3_2_2 : -1 <= -S[7,2] + guard4[1]-guard4[2];
keep_7_2_3_1 : -1 <= -S[7,3]-guard2[2] + guard2[3];
keep_7_2_3_2 : -1 <= -S[7,3] + guard2[2]-guard2[3];
keep_7_1_3_1 : -1 <= -S[7,3]-guard0[2] + guard0[3];
keep_7_1_3_2 : -1 <= -S[7,3] + guard0[2]-guard0[3];
keep_7_3_3_1 : -1 <= -S[7,3]-guard4[2] + guard4[3];
keep_7_3_3_2 : -1 <= -S[7,3] + guard4[2]-guard4[3];
keep_7_2_4_1 : -1 <= -S[7,4]-guard2[3] + guard2[4];
keep_7_2_4_2 : -1 <= -S[7,4] + guard2[3]-guard2[4];
keep_7_1_4_1 : -1 <= -S[7,4]-guard0[3] + guard0[4];
keep_7_1_4_2 : -1 <= -S[7,4] + guard0[3]-guard0[4];
keep_7_3_4_1 : -1 <= -S[7,4]-guard4[3] + guard4[4];
keep_7_3_4_2 : -1 <= -S[7,4] + guard4[3]-guard4[4];
keep_7_2_5_1 : -1 <= -S[7,5]-guard2[4] + guard2[5];
keep_7_2_5_2 : -1 <= -S[7,5] + guard2[4]-guard2[5];
keep_7_1_5_1 : -1 <= -S[7,5]-guard0[4] + guard0[5];
keep_7_1_5_2 : -1 <= -S[7,5] + guard0[4]-guard0[5];
keep_7_3_5_1 : -1 <= -S[7,5]-guard4[4] + guard4[5];
keep_7_3_5_2 : -1 <= -S[7,5] + guard4[4]-guard4[5];
keep_7_2_6_1 : -1 <= -S[7,6]-guard2[5] + guard2[6];
keep_7_2_6_2 : -1 <= -S[7,6] + guard2[5]-guard2[6];
keep_7_1_6_1 : -1 <= -S[7,6]-guard0[5] + guard0[6];
keep_7_1_6_2 : -1 <= -S[7,6] + guard0[5]-guard0[6];
keep_7_3_6_1 : -1 <= -S[7,6]-guard4[5] + guard4[6];
keep_7_3_6_2 : -1 <= -S[7,6] + guard4[5]-guard4[6];
keep_7_2_7_1 : -1 <= -S[7,7]-guard2[6] + guard2[7];
keep_7_2_7_2 : -1 <= -S[7,7] + guard2[6]-guard2[7];
keep_7_1_7_1 : -1 <= -S[7,7]-guard0[6] + guard0[7];
keep_7_1_7_2 : -1 <= -S[7,7] + guard0[6]-guard0[7];
keep_7_3_7_1 : -1 <= -S[7,7]-guard4[6] + guard4[7];
keep_7_3_7_2 : -1 <= -S[7,7] + guard4[6]-guard4[7];
keep_7_2_8_1 : -1 <= -S[7,8]-guard2[7] + guard2[8];
keep_7_2_8_2 : -1 <= -S[7,8] + guard2[7]-guard2[8];
keep_7_1_8_1 : -1 <= -S[7,8]-guard0[7] + guard0[8];
keep_7_1_8_2 : -1 <= -S[7,8] + guard0[7]-guard0[8];
keep_7_3_8_1 : -1 <= -S[7,8]-guard4[7] + guard4[8];
keep_7_3_8_2 : -1 <= -S[7,8] + guard4[7]-guard4[8];
keep_7_2_9_1 : -1 <= -S[7,9]-guard2[8] + guard2[9];
keep_7_2_9_2 : -1 <= -S[7,9] + guard2[8]-guard2[9];
keep_7_1_9_1 : -1 <= -S[7,9]-guard0[8] + guard0[9];
keep_7_1_9_2 : -1 <= -S[7,9] + guard0[8]-guard0[9];
keep_7_3_9_1 : -1 <= -S[7,9]-guard4[8] + guard4[9];
keep_7_3_9_2 : -1 <= -S[7,9] + guard4[8]-guard4[9];
keep_7_2_10_1 : -1 <= -S[7,10] + guard2[10]-guard2[9];
keep_7_2_10_2 : -1 <= -S[7,10]-guard2[10] + guard2[9];
keep_7_1_10_1 : -1 <= -S[7,10] + guard0[10]-guard0[9];
keep_7_1_10_2 : -1 <= -S[7,10]-guard0[10] + guard0[9];
keep_7_3_10_1 : -1 <= -S[7,10] + guard4[10]-guard4[9];
keep_7_3_10_2 : -1 <= -S[7,10]-guard4[10] + guard4[9];
keep_7_2_11_1 : -1 <= -S[7,11]-guard2[10] + guard2[11];
keep_7_2_11_2 : -1 <= -S[7,11] + guard2[10]-guard2[11];
keep_7_1_11_1 : -1 <= -S[7,11]-guard0[10] + guard0[11];
keep_7_1_11_2 : -1 <= -S[7,11] + guard0[10]-guard0[11];
keep_7_3_11_1 : -1 <= -S[7,11]-guard4[10] + guard4[11];
keep_7_3_11_2 : -1 <= -S[7,11] + guard4[10]-guard4[11];
keep_7_2_12_1 : -1 <= -S[7,12]-guard2[11] + guard2[12];
keep_7_2_12_2 : -1 <= -S[7,12] + guard2[11]-guard2[12];
keep_7_1_12_1 : -1 <= -S[7,12]-guard0[11] + guard0[12];
keep_7_1_12_2 : -1 <= -S[7,12] + guard0[11]-guard0[12];
keep_7_3_12_1 : -1 <= -S[7,12]-guard4[11] + guard4[12];
keep_7_3_12_2 : -1 <= -S[7,12] + guard4[11]-guard4[12];
keep_7_2_13_1 : -1 <= -S[7,13]-guard2[12] + guard2[13];
keep_7_2_13_2 : -1 <= -S[7,13] + guard2[12]-guard2[13];
keep_7_1_13_1 : -1 <= -S[7,13]-guard0[12] + guard0[13];
keep_7_1_13_2 : -1 <= -S[7,13] + guard0[12]-guard0[13];
keep_7_3_13_1 : -1 <= -S[7,13]-guard4[12] + guard4[13];
keep_7_3_13_2 : -1 <= -S[7,13] + guard4[12]-guard4[13];
keep_7_2_14_1 : -1 <= -S[7,14]-guard2[13] + guard2[14];
keep_7_2_14_2 : -1 <= -S[7,14] + guard2[13]-guard2[14];
keep_7_1_14_1 : -1 <= -S[7,14]-guard0[13] + guard0[14];
keep_7_1_14_2 : -1 <= -S[7,14] + guard0[13]-guard0[14];
keep_7_3_14_1 : -1 <= -S[7,14]-guard4[13] + guard4[14];
keep_7_3_14_2 : -1 <= -S[7,14] + guard4[13]-guard4[14];
keep_7_2_15_1 : -1 <= -S[7,15]-guard2[14] + guard2[15];
keep_7_2_15_2 : -1 <= -S[7,15] + guard2[14]-guard2[15];
keep_7_1_15_1 : -1 <= -S[7,15]-guard0[14] + guard0[15];
keep_7_1_15_2 : -1 <= -S[7,15] + guard0[14]-guard0[15];
keep_7_3_15_1 : -1 <= -S[7,15]-guard4[14] + guard4[15];
keep_7_3_15_2 : -1 <= -S[7,15] + guard4[14]-guard4[15];
keep_7_2_16_1 : -1 <= -S[7,16]-guard2[15] + guard2[16];
keep_7_2_16_2 : -1 <= -S[7,16] + guard2[15]-guard2[16];
keep_7_1_16_1 : -1 <= -S[7,16]-guard0[15] + guard0[16];
keep_7_1_16_2 : -1 <= -S[7,16] + guard0[15]-guard0[16];
keep_7_3_16_1 : -1 <= -S[7,16]-guard4[15] + guard4[16];
keep_7_3_16_2 : -1 <= -S[7,16] + guard4[15]-guard4[16];
keep_7_2_17_1 : -1 <= -S[7,17]-guard2[16] + guard2[17];
keep_7_2_17_2 : -1 <= -S[7,17] + guard2[16]-guard2[17];
keep_7_1_17_1 : -1 <= -S[7,17]-guard0[16] + guard0[17];
keep_7_1_17_2 : -1 <= -S[7,17] + guard0[16]-guard0[17];
keep_7_3_17_1 : -1 <= -S[7,17]-guard4[16] + guard4[17];
keep_7_3_17_2 : -1 <= -S[7,17] + guard4[16]-guard4[17];
keep_7_2_18_1 : -1 <= -S[7,18]-guard2[17] + guard2[18];
keep_7_2_18_2 : -1 <= -S[7,18] + guard2[17]-guard2[18];
keep_7_1_18_1 : -1 <= -S[7,18]-guard0[17] + guard0[18];
keep_7_1_18_2 : -1 <= -S[7,18] + guard0[17]-guard0[18];
keep_7_3_18_1 : -1 <= -S[7,18]-guard4[17] + guard4[18];
keep_7_3_18_2 : -1 <= -S[7,18] + guard4[17]-guard4[18];
keep_7_2_19_1 : -1 <= -S[7,19]-guard2[18] + guard2[19];
keep_7_2_19_2 : -1 <= -S[7,19] + guard2[18]-guard2[19];
keep_7_1_19_1 : -1 <= -S[7,19]-guard0[18] + guard0[19];
keep_7_1_19_2 : -1 <= -S[7,19] + guard0[18]-guard0[19];
keep_7_3_19_1 : -1 <= -S[7,19]-guard4[18] + guard4[19];
keep_7_3_19_2 : -1 <= -S[7,19] + guard4[18]-guard4[19];
keep_7_2_20_1 : -1 <= -S[7,20]-guard2[19] + guard2[20];
keep_7_2_20_2 : -1 <= -S[7,20] + guard2[19]-guard2[20];
keep_7_1_20_1 : -1 <= -S[7,20]-guard0[19] + guard0[20];
keep_7_1_20_2 : -1 <= -S[7,20] + guard0[19]-guard0[20];
keep_7_3_20_1 : -1 <= -S[7,20]-guard4[19] + guard4[20];
keep_7_3_20_2 : -1 <= -S[7,20] + guard4[19]-guard4[20];
keep_7_2_21_1 : -1 <= -S[7,21]-guard2[20] + guard2[21];
keep_7_2_21_2 : -1 <= -S[7,21] + guard2[20]-guard2[21];
keep_7_1_21_1 : -1 <= -S[7,21]-guard0[20] + guard0[21];
keep_7_1_21_2 : -1 <= -S[7,21] + guard0[20]-guard0[21];
keep_7_3_21_1 : -1 <= -S[7,21]-guard4[20] + guard4[21];
keep_7_3_21_2 : -1 <= -S[7,21] + guard4[20]-guard4[21];
keep_7_2_22_1 : -1 <= -S[7,22]-guard2[21] + guard2[22];
keep_7_2_22_2 : -1 <= -S[7,22] + guard2[21]-guard2[22];
keep_7_1_22_1 : -1 <= -S[7,22]-guard0[21] + guard0[22];
keep_7_1_22_2 : -1 <= -S[7,22] + guard0[21]-guard0[22];
keep_7_3_22_1 : -1 <= -S[7,22]-guard4[21] + guard4[22];
keep_7_3_22_2 : -1 <= -S[7,22] + guard4[21]-guard4[22];
keep_7_2_23_1 : -1 <= -S[7,23]-guard2[22] + guard2[23];
keep_7_2_23_2 : -1 <= -S[7,23] + guard2[22]-guard2[23];
keep_7_1_23_1 : -1 <= -S[7,23]-guard0[22] + guard0[23];
keep_7_1_23_2 : -1 <= -S[7,23] + guard0[22]-guard0[23];
keep_7_3_23_1 : -1 <= -S[7,23]-guard4[22] + guard4[23];
keep_7_3_23_2 : -1 <= -S[7,23] + guard4[22]-guard4[23];
keep_8_2_1_1 : -1 <= -S[8,1]-guard2[0] + guard2[1];
keep_8_2_1_2 : -1 <= -S[8,1] + guard2[0]-guard2[1];
set_and_8_1_1 : -2 <= -S[8,1] + guard0[1]-x12-x34;
set_and_8_1_2 : -1 <= -S[8,1]-guard0[1] + x12;
set_and_8_1_3 : -1 <= -S[8,1]-guard0[1] + x34;
keep_8_3_1_1 : -1 <= -S[8,1]-guard4[0] + guard4[1];
keep_8_3_1_2 : -1 <= -S[8,1] + guard4[0]-guard4[1];
keep_8_2_2_1 : -1 <= -S[8,2]-guard2[1] + guard2[2];
keep_8_2_2_2 : -1 <= -S[8,2] + guard2[1]-guard2[2];
set_and_8_2_1 : -2 <= -S[8,2] + guard0[2]-x12-x34;
set_and_8_2_2 : -1 <= -S[8,2]-guard0[2] + x12;
set_and_8_2_3 : -1 <= -S[8,2]-guard0[2] + x34;
keep_8_3_2_1 : -1 <= -S[8,2]-guard4[1] + guard4[2];
keep_8_3_2_2 : -1 <= -S[8,2] + guard4[1]-guard4[2];
keep_8_2_3_1 : -1 <= -S[8,3]-guard2[2] + guard2[3];
keep_8_2_3_2 : -1 <= -S[8,3] + guard2[2]-guard2[3];
set_and_8_3_1 : -2 <= -S[8,3] + guard0[3]-x12-x34;
set_and_8_3_2 : -1 <= -S[8,3]-guard0[3] + x12;
set_and_8_3_3 : -1 <= -S[8,3]-guard0[3] + x34;
keep_8_3_3_1 : -1 <= -S[8,3]-guard4[2] + guard4[3];
keep_8_3_3_2 : -1 <= -S[8,3] + guard4[2]-guard4[3];
keep_8_2_4_1 : -1 <= -S[8,4]-guard2[3] + guard2[4];
keep_8_2_4_2 : -1 <= -S[8,4] + guard2[3]-guard2[4];
set_and_8_4_1 : -2 <= -S[8,4] + guard0[4]-x12-x34;
set_and_8_4_2 : -1 <= -S[8,4]-guard0[4] + x12;
set_and_8_4_3 : -1 <= -S[8,4]-guard0[4] + x34;
keep_8_3_4_1 : -1 <= -S[8,4]-guard4[3] + guard4[4];
keep_8_3_4_2 : -1 <= -S[8,4] + guard4[3]-guard4[4];
keep_8_2_5_1 : -1 <= -S[8,5]-guard2[4] + guard2[5];
keep_8_2_5_2 : -1 <= -S[8,5] + guard2[4]-guard2[5];
set_and_8_5_1 : -2 <= -S[8,5] + guard0[5]-x12-x34;
set_and_8_5_2 : -1 <= -S[8,5]-guard0[5] + x12;
set_and_8_5_3 : -1 <= -S[8,5]-guard0[5] + x34;
keep_8_3_5_1 : -1 <= -S[8,5]-guard4[4] + guard4[5];
keep_8_3_5_2 : -1 <= -S[8,5] + guard4[4]-guard4[5];
keep_8_2_6_1 : -1 <= -S[8,6]-guard2[5] + guard2[6];
keep_8_2_6_2 : -1 <= -S[8,6] + guard2[5]-guard2[6];
set_and_8_6_1 : -2 <= -S[8,6] + guard0[6]-x12-x34;
set_and_8_6_2 : -1 <= -S[8,6]-guard0[6] + x12;
set_and_8_6_3 : -1 <= -S[8,6]-guard0[6] + x34;
keep_8_3_6_1 : -1 <= -S[8,6]-guard4[5] + guard4[6];
keep_8_3_6_2 : -1 <= -S[8,6] + guard4[5]-guard4[6];
keep_8_2_7_1 : -1 <= -S[8,7]-guard2[6] + guard2[7];
keep_8_2_7_2 : -1 <= -S[8,7] + guard2[6]-guard2[7];
set_and_8_7_1 : -2 <= -S[8,7] + guard0[7]-x12-x34;
set_and_8_7_2 : -1 <= -S[8,7]-guard0[7] + x12;
set_and_8_7_3 : -1 <= -S[8,7]-guard0[7] + x34;
keep_8_3_7_1 : -1 <= -S[8,7]-guard4[6] + guard4[7];
keep_8_3_7_2 : -1 <= -S[8,7] + guard4[6]-guard4[7];
keep_8_2_8_1 : -1 <= -S[8,8]-guard2[7] + guard2[8];
keep_8_2_8_2 : -1 <= -S[8,8] + guard2[7]-guard2[8];
set_and_8_8_1 : -2 <= -S[8,8] + guard0[8]-x12-x34;
set_and_8_8_2 : -1 <= -S[8,8]-guard0[8] + x12;
set_and_8_8_3 : -1 <= -S[8,8]-guard0[8] + x34;
keep_8_3_8_1 : -1 <= -S[8,8]-guard4[7] + guard4[8];
keep_8_3_8_2 : -1 <= -S[8,8] + guard4[7]-guard4[8];
keep_8_2_9_1 : -1 <= -S[8,9]-guard2[8] + guard2[9];
keep_8_2_9_2 : -1 <= -S[8,9] + guard2[8]-guard2[9];
set_and_8_9_1 : -2 <= -S[8,9] + guard0[9]-x12-x34;
set_and_8_9_2 : -1 <= -S[8,9]-guard0[9] + x12;
set_and_8_9_3 : -1 <= -S[8,9]-guard0[9] + x34;
keep_8_3_9_1 : -1 <= -S[8,9]-guard4[8] + guard4[9];
keep_8_3_9_2 : -1 <= -S[8,9] + guard4[8]-guard4[9];
keep_8_2_10_1 : -1 <= -S[8,10] + guard2[10]-guard2[9];
keep_8_2_10_2 : -1 <= -S[8,10]-guard2[10] + guard2[9];
set_and_8_10_1 : -2 <= -S[8,10] + guard0[10]-x12-x34;
set_and_8_10_2 : -1 <= -S[8,10]-guard0[10] + x12;
set_and_8_10_3 : -1 <= -S[8,10]-guard0[10] + x34;
keep_8_3_10_1 : -1 <= -S[8,10] + guard4[10]-guard4[9];
keep_8_3_10_2 : -1 <= -S[8,10]-guard4[10] + guard4[9];
keep_8_2_11_1 : -1 <= -S[8,11]-guard2[10] + guard2[11];
keep_8_2_11_2 : -1 <= -S[8,11] + guard2[10]-guard2[11];
set_and_8_11_1 : -2 <= -S[8,11] + guard0[11]-x12-x34;
set_and_8_11_2 : -1 <= -S[8,11]-guard0[11] + x12;
set_and_8_11_3 : -1 <= -S[8,11]-guard0[11] + x34;
keep_8_3_11_1 : -1 <= -S[8,11]-guard4[10] + guard4[11];
keep_8_3_11_2 : -1 <= -S[8,11] + guard4[10]-guard4[11];
keep_8_2_12_1 : -1 <= -S[8,12]-guard2[11] + guard2[12];
keep_8_2_12_2 : -1 <= -S[8,12] + guard2[11]-guard2[12];
set_and_8_12_1 : -2 <= -S[8,12] + guard0[12]-x12-x34;
set_and_8_12_2 : -1 <= -S[8,12]-guard0[12] + x12;
set_and_8_12_3 : -1 <= -S[8,12]-guard0[12] + x34;
keep_8_3_12_1 : -1 <= -S[8,12]-guard4[11] + guard4[12];
keep_8_3_12_2 : -1 <= -S[8,12] + guard4[11]-guard4[12];
keep_8_2_13_1 : -1 <= -S[8,13]-guard2[12] + guard2[13];
keep_8_2_13_2 : -1 <= -S[8,13] + guard2[12]-guard2[13];
set_and_8_13_1 : -2 <= -S[8,13] + guard0[13]-x12-x34;
set_and_8_13_2 : -1 <= -S[8,13]-guard0[13] + x12;
set_and_8_13_3 : -1 <= -S[8,13]-guard0[13] + x34;
keep_8_3_13_1 : -1 <= -S[8,13]-guard4[12] + guard4[13];
keep_8_3_13_2 : -1 <= -S[8,13] + guard4[12]-guard4[13];
keep_8_2_14_1 : -1 <= -S[8,14]-guard2[13] + guard2[14];
keep_8_2_14_2 : -1 <= -S[8,14] + guard2[13]-guard2[14];
set_and_8_14_1 : -2 <= -S[8,14] + guard0[14]-x12-x34;
set_and_8_14_2 : -1 <= -S[8,14]-guard0[14] + x12;
set_and_8_14_3 : -1 <= -S[8,14]-guard0[14] + x34;
keep_8_3_14_1 : -1 <= -S[8,14]-guard4[13] + guard4[14];
keep_8_3_14_2 : -1 <= -S[8,14] + guard4[13]-guard4[14];
keep_8_2_15_1 : -1 <= -S[8,15]-guard2[14] + guard2[15];
keep_8_2_15_2 : -1 <= -S[8,15] + guard2[14]-guard2[15];
set_and_8_15_1 : -2 <= -S[8,15] + guard0[15]-x12-x34;
set_and_8_15_2 : -1 <= -S[8,15]-guard0[15] + x12;
set_and_8_15_3 : -1 <= -S[8,15]-guard0[15] + x34;
keep_8_3_15_1 : -1 <= -S[8,15]-guard4[14] + guard4[15];
keep_8_3_15_2 : -1 <= -S[8,15] + guard4[14]-guard4[15];
keep_8_2_16_1 : -1 <= -S[8,16]-guard2[15] + guard2[16];
keep_8_2_16_2 : -1 <= -S[8,16] + guard2[15]-guard2[16];
set_and_8_16_1 : -2 <= -S[8,16] + guard0[16]-x12-x34;
set_and_8_16_2 : -1 <= -S[8,16]-guard0[16] + x12;
set_and_8_16_3 : -1 <= -S[8,16]-guard0[16] + x34;
keep_8_3_16_1 : -1 <= -S[8,16]-guard4[15] + guard4[16];
keep_8_3_16_2 : -1 <= -S[8,16] + guard4[15]-guard4[16];
keep_8_2_17_1 : -1 <= -S[8,17]-guard2[16] + guard2[17];
keep_8_2_17_2 : -1 <= -S[8,17] + guard2[16]-guard2[17];
set_and_8_17_1 : -2 <= -S[8,17] + guard0[17]-x12-x34;
set_and_8_17_2 : -1 <= -S[8,17]-guard0[17] + x12;
set_and_8_17_3 : -1 <= -S[8,17]-guard0[17] + x34;
keep_8_3_17_1 : -1 <= -S[8,17]-guard4[16] + guard4[17];
keep_8_3_17_2 : -1 <= -S[8,17] + guard4[16]-guard4[17];
keep_8_2_18_1 : -1 <= -S[8,18]-guard2[17] + guard2[18];
keep_8_2_18_2 : -1 <= -S[8,18] + guard2[17]-guard2[18];
set_and_8_18_1 : -2 <= -S[8,18] + guard0[18]-x12-x34;
set_and_8_18_2 : -1 <= -S[8,18]-guard0[18] + x12;
set_and_8_18_3 : -1 <= -S[8,18]-guard0[18] + x34;
keep_8_3_18_1 : -1 <= -S[8,18]-guard4[17] + guard4[18];
keep_8_3_18_2 : -1 <= -S[8,18] + guard4[17]-guard4[18];
keep_8_2_19_1 : -1 <= -S[8,19]-guard2[18] + guard2[19];
keep_8_2_19_2 : -1 <= -S[8,19] + guard2[18]-guard2[19];
set_and_8_19_1 : -2 <= -S[8,19] + guard0[19]-x12-x34;
set_and_8_19_2 : -1 <= -S[8,19]-guard0[19] + x12;
set_and_8_19_3 : -1 <= -S[8,19]-guard0[19] + x34;
keep_8_3_19_1 : -1 <= -S[8,19]-guard4[18] + guard4[19];
keep_8_3_19_2 : -1 <= -S[8,19] + guard4[18]-guard4[19];
keep_8_2_20_1 : -1 <= -S[8,20]-guard2[19] + guard2[20];
keep_8_2_20_2 : -1 <= -S[8,20] + guard2[19]-guard2[20];
set_and_8_20_1 : -2 <= -S[8,20] + guard0[20]-x12-x34;
set_and_8_20_2 : -1 <= -S[8,20]-guard0[20] + x12;
set_and_8_20_3 : -1 <= -S[8,20]-guard0[20] + x34;
keep_8_3_20_1 : -1 <= -S[8,20]-guard4[19] + guard4[20];
keep_8_3_20_2 : -1 <= -S[8,20] + guard4[19]-guard4[20];
keep_8_2_21_1 : -1 <= -S[8,21]-guard2[20] + guard2[21];
keep_8_2_21_2 : -1 <= -S[8,21] + guard2[20]-guard2[21];
set_and_8_21_1 : -2 <= -S[8,21] + guard0[21]-x12-x34;
set_and_8_21_2 : -1 <= -S[8,21]-guard0[21] + x12;
set_and_8_21_3 : -1 <= -S[8,21]-guard0[21] + x34;
keep_8_3_21_1 : -1 <= -S[8,21]-guard4[20] + guard4[21];
keep_8_3_21_2 : -1 <= -S[8,21] + guard4[20]-guard4[21];
keep_8_2_22_1 : -1 <= -S[8,22]-guard2[21] + guard2[22];
keep_8_2_22_2 : -1 <= -S[8,22] + guard2[21]-guard2[22];
set_and_8_22_1 : -2 <= -S[8,22] + guard0[22]-x12-x34;
set_and_8_22_2 : -1 <= -S[8,22]-guard0[22] + x12;
set_and_8_22_3 : -1 <= -S[8,22]-guard0[22] + x34;
keep_8_3_22_1 : -1 <= -S[8,22]-guard4[21] + guard4[22];
keep_8_3_22_2 : -1 <= -S[8,22] + guard4[21]-guard4[22];
keep_8_2_23_1 : -1 <= -S[8,23]-guard2[22] + guard2[23];
keep_8_2_23_2 : -1 <= -S[8,23] + guard2[22]-guard2[23];
set_and_8_23_1 : -2 <= -S[8,23] + guard0[23]-x12-x34;
set_and_8_23_2 : -1 <= -S[8,23]-guard0[23] + x12;
set_and_8_23_3 : -1 <= -S[8,23]-guard0[23] + x34;
keep_8_3_23_1 : -1 <= -S[8,23]-guard4[22] + guard4[23];
keep_8_3_23_2 : -1 <= -S[8,23] + guard4[22]-guard4[23];
keep_9_2_1_1 : -1 <= -S[9,1]-guard2[0] + guard2[1];
keep_9_2_1_2 : -1 <= -S[9,1] + guard2[0]-guard2[1];
set_not_9_1_1 : -2 <= -S[9,1]-guard0[0]-guard0[1];
set_not_9_1_2 : 0 <= -S[9,1] + guard0[0] + guard0[1];
keep_9_3_1_1 : -1 <= -S[9,1]-guard4[0] + guard4[1];
keep_9_3_1_2 : -1 <= -S[9,1] + guard4[0]-guard4[1];
keep_9_2_2_1 : -1 <= -S[9,2]-guard2[1] + guard2[2];
keep_9_2_2_2 : -1 <= -S[9,2] + guard2[1]-guard2[2];
set_not_9_2_1 : -2 <= -S[9,2]-guard0[1]-guard0[2];
set_not_9_2_2 : 0 <= -S[9,2] + guard0[1] + guard0[2];
keep_9_3_2_1 : -1 <= -S[9,2]-guard4[1] + guard4[2];
keep_9_3_2_2 : -1 <= -S[9,2] + guard4[1]-guard4[2];
keep_9_2_3_1 : -1 <= -S[9,3]-guard2[2] + guard2[3];
keep_9_2_3_2 : -1 <= -S[9,3] + guard2[2]-guard2[3];
set_not_9_3_1 : -2 <= -S[9,3]-guard0[2]-guard0[3];
set_not_9_3_2 : 0 <= -S[9,3] + guard0[2] + guard0[3];
keep_9_3_3_1 : -1 <= -S[9,3]-guard4[2] + guard4[3];
keep_9_3_3_2 : -1 <= -S[9,3] + guard4[2]-guard4[3];
keep_9_2_4_1 : -1 <= -S[9,4]-guard2[3] + guard2[4];
keep_9_2_4_2 : -1 <= -S[9,4] + guard2[3]-guard2[4];
set_not_9_4_1 : -2 <= -S[9,4]-guard0[3]-guard0[4];
set_not_9_4_2 : 0 <= -S[9,4] + guard0[3] + guard0[4];
keep_9_3_4_1 : -1 <= -S[9,4]-guard4[3] + guard4[4];
keep_9_3_4_2 : -1 <= -S[9,4] + guard4[3]-guard4[4];
keep_9_2_5_1 : -1 <= -S[9,5]-guard2[4] + guard2[5];
keep_9_2_5_2 : -1 <= -S[9,5] + guard2[4]-guard2[5];
set_not_9_5_1 : -2 <= -S[9,5]-guard0[4]-guard0[5];
set_not_9_5_2 : 0 <= -S[9,5] + guard0[4] + guard0[5];
keep_9_3_5_1 : -1 <= -S[9,5]-guard4[4] + guard4[5];
keep_9_3_5_2 : -1 <= -S[9,5] + guard4[4]-guard4[5];
keep_9_2_6_1 : -1 <= -S[9,6]-guard2[5] + guard2[6];
keep_9_2_6_2 : -1 <= -S[9,6] + guard2[5]-guard2[6];
set_not_9_6_1 : -2 <= -S[9,6]-guard0[5]-guard0[6];
set_not_9_6_2 : 0 <= -S[9,6] + guard0[5] + guard0[6];
keep_9_3_6_1 : -1 <= -S[9,6]-guard4[5] + guard4[6];
keep_9_3_6_2 : -1 <= -S[9,6] + guard4[5]-guard4[6];
keep_9_2_7_1 : -1 <= -S[9,7]-guard2[6] + guard2[7];
keep_9_2_7_2 : -1 <= -S[9,7] + guard2[6]-guard2[7];
set_not_9_7_1 : -2 <= -S[9,7]-guard0[6]-guard0[7];
set_not_9_7_2 : 0 <= -S[9,7] + guard0[6] + guard0[7];
keep_9_3_7_1 : -1 <= -S[9,7]-guard4[6] + guard4[7];
keep_9_3_7_2 : -1 <= -S[9,7] + guard4[6]-guard4[7];
keep_9_2_8_1 : -1 <= -S[9,8]-guard2[7] + guard2[8];
keep_9_2_8_2 : -1 <= -S[9,8] + guard2[7]-guard2[8];
set_not_9_8_1 : -2 <= -S[9,8]-guard0[7]-guard0[8];
set_not_9_8_2 : 0 <= -S[9,8] + guard0[7] + guard0[8];
keep_9_3_8_1 : -1 <= -S[9,8]-guard4[7] + guard4[8];
keep_9_3_8_2 : -1 <= -S[9,8] + guard4[7]-guard4[8];
keep_9_2_9_1 : -1 <= -S[9,9]-guard2[8] + guard2[9];
keep_9_2_9_2 : -1 <= -S[9,9] + guard2[8]-guard2[9];
set_not_9_9_1 : -2 <= -S[9,9]-guard0[8]-guard0[9];
set_not_9_9_2 : 0 <= -S[9,9] + guard0[8] + guard0[9];
keep_9_3_9_1 : -1 <= -S[9,9]-guard4[8] + guard4[9];
keep_9_3_9_2 : -1 <= -S[9,9] + guard4[8]-guard4[9];
keep_9_2_10_1 : -1 <= -S[9,10] + guard2[10]-guard2[9];
keep_9_2_10_2 : -1 <= -S[9,10]-guard2[10] + guard2[9];
set_not_9_10_1 : -2 <= -S[9,10]-guard0[10]-guard0[9];
set_not_9_10_2 : 0 <= -S[9,10] + guard0[10] + guard0[9];
keep_9_3_10_1 : -1 <= -S[9,10] + guard4[10]-guard4[9];
keep_9_3_10_2 : -1 <= -S[9,10]-guard4[10] + guard4[9];
keep_9_2_11_1 : -1 <= -S[9,11]-guard2[10] + guard2[11];
keep_9_2_11_2 : -1 <= -S[9,11] + guard2[10]-guard2[11];
set_not_9_11_1 : -2 <= -S[9,11]-guard0[10]-guard0[11];
set_not_9_11_2 : 0 <= -S[9,11] + guard0[10] + guard0[11];
keep_9_3_11_1 : -1 <= -S[9,11]-guard4[10] + guard4[11];
keep_9_3_11_2 : -1 <= -S[9,11] + guard4[10]-guard4[11];
keep_9_2_12_1 : -1 <= -S[9,12]-guard2[11] + guard2[12];
keep_9_2_12_2 : -1 <= -S[9,12] + guard2[11]-guard2[12];
set_not_9_12_1 : -2 <= -S[9,12]-guard0[11]-guard0[12];
set_not_9_12_2 : 0 <= -S[9,12] + guard0[11] + guard0[12];
keep_9_3_12_1 : -1 <= -S[9,12]-guard4[11] + guard4[12];
keep_9_3_12_2 : -1 <= -S[9,12] + guard4[11]-guard4[12];
keep_9_2_13_1 : -1 <= -S[9,13]-guard2[12] + guard2[13];
keep_9_2_13_2 : -1 <= -S[9,13] + guard2[12]-guard2[13];
set_not_9_13_1 : -2 <= -S[9,13]-guard0[12]-guard0[13];
set_not_9_13_2 : 0 <= -S[9,13] + guard0[12] + guard0[13];
keep_9_3_13_1 : -1 <= -S[9,13]-guard4[12] + guard4[13];
keep_9_3_13_2 : -1 <= -S[9,13] + guard4[12]-guard4[13];
keep_9_2_14_1 : -1 <= -S[9,14]-guard2[13] + guard2[14];
keep_9_2_14_2 : -1 <= -S[9,14] + guard2[13]-guard2[14];
set_not_9_14_1 : -2 <= -S[9,14]-guard0[13]-guard0[14];
set_not_9_14_2 : 0 <= -S[9,14] + guard0[13] + guard0[14];
keep_9_3_14_1 : -1 <= -S[9,14]-guard4[13] + guard4[14];
keep_9_3_14_2 : -1 <= -S[9,14] + guard4[13]-guard4[14];
keep_9_2_15_1 : -1 <= -S[9,15]-guard2[14] + guard2[15];
keep_9_2_15_2 : -1 <= -S[9,15] + guard2[14]-guard2[15];
set_not_9_15_1 : -2 <= -S[9,15]-guard0[14]-guard0[15];
set_not_9_15_2 : 0 <= -S[9,15] + guard0[14] + guard0[15];
keep_9_3_15_1 : -1 <= -S[9,15]-guard4[14] + guard4[15];
keep_9_3_15_2 : -1 <= -S[9,15] + guard4[14]-guard4[15];
keep_9_2_16_1 : -1 <= -S[9,16]-guard2[15] + guard2[16];
keep_9_2_16_2 : -1 <= -S[9,16] + guard2[15]-guard2[16];
set_not_9_16_1 : -2 <= -S[9,16]-guard0[15]-guard0[16];
set_not_9_16_2 : 0 <= -S[9,16] + guard0[15] + guard0[16];
keep_9_3_16_1 : -1 <= -S[9,16]-guard4[15] + guard4[16];
keep_9_3_16_2 : -1 <= -S[9,16] + guard4[15]-guard4[16];
keep_9_2_17_1 : -1 <= -S[9,17]-guard2[16] + guard2[17];
keep_9_2_17_2 : -1 <= -S[9,17] + guard2[16]-guard2[17];
set_not_9_17_1 : -2 <= -S[9,17]-guard0[16]-guard0[17];
set_not_9_17_2 : 0 <= -S[9,17] + guard0[16] + guard0[17];
keep_9_3_17_1 : -1 <= -S[9,17]-guard4[16] + guard4[17];
keep_9_3_17_2 : -1 <= -S[9,17] + guard4[16]-guard4[17];
keep_9_2_18_1 : -1 <= -S[9,18]-guard2[17] + guard2[18];
keep_9_2_18_2 : -1 <= -S[9,18] + guard2[17]-guard2[18];
set_not_9_18_1 : -2 <= -S[9,18]-guard0[17]-guard0[18];
set_not_9_18_2 : 0 <= -S[9,18] + guard0[17] + guard0[18];
keep_9_3_18_1 : -1 <= -S[9,18]-guard4[17] + guard4[18];
keep_9_3_18_2 : -1 <= -S[9,18] + guard4[17]-guard4[18];
keep_9_2_19_1 : -1 <= -S[9,19]-guard2[18] + guard2[19];
keep_9_2_19_2 : -1 <= -S[9,19] + guard2[18]-guard2[19];
set_not_9_19_1 : -2 <= -S[9,19]-guard0[18]-guard0[19];
set_not_9_19_2 : 0 <= -S[9,19] + guard0[18] + guard0[19];
keep_9_3_19_1 : -1 <= -S[9,19]-guard4[18] + guard4[19];
keep_9_3_19_2 : -1 <= -S[9,19] + guard4[18]-guard4[19];
keep_9_2_20_1 : -1 <= -S[9,20]-guard2[19] + guard2[20];
keep_9_2_20_2 : -1 <= -S[9,20] + guard2[19]-guard2[20];
set_not_9_20_1 : -2 <= -S[9,20]-guard0[19]-guard0[20];
set_not_9_20_2 : 0 <= -S[9,20] + guard0[19] + guard0[20];
keep_9_3_20_1 : -1 <= -S[9,20]-guard4[19] + guard4[20];
keep_9_3_20_2 : -1 <= -S[9,20] + guard4[19]-guard4[20];
keep_9_2_21_1 : -1 <= -S[9,21]-guard2[20] + guard2[21];
keep_9_2_21_2 : -1 <= -S[9,21] + guard2[20]-guard2[21];
set_not_9_21_1 : -2 <= -S[9,21]-guard0[20]-guard0[21];
set_not_9_21_2 : 0 <= -S[9,21] + guard0[20] + guard0[21];
keep_9_3_21_1 : -1 <= -S[9,21]-guard4[20] + guard4[21];
keep_9_3_21_2 : -1 <= -S[9,21] + guard4[20]-guard4[21];
keep_9_2_22_1 : -1 <= -S[9,22]-guard2[21] + guard2[22];
keep_9_2_22_2 : -1 <= -S[9,22] + guard2[21]-guard2[22];
set_not_9_22_1 : -2 <= -S[9,22]-guard0[21]-guard0[22];
set_not_9_22_2 : 0 <= -S[9,22] + guard0[21] + guard0[22];
keep_9_3_22_1 : -1 <= -S[9,22]-guard4[21] + guard4[22];
keep_9_3_22_2 : -1 <= -S[9,22] + guard4[21]-guard4[22];
keep_9_2_23_1 : -1 <= -S[9,23]-guard2[22] + guard2[23];
keep_9_2_23_2 : -1 <= -S[9,23] + guard2[22]-guard2[23];
set_not_9_23_1 : -2 <= -S[9,23]-guard0[22]-guard0[23];
set_not_9_23_2 : 0 <= -S[9,23] + guard0[22] + guard0[23];
keep_9_3_23_1 : -1 <= -S[9,23]-guard4[22] + guard4[23];
keep_9_3_23_2 : -1 <= -S[9,23] + guard4[22]-guard4[23];
keep_10_2_1_1 : -1 <= -S[10,1]-guard2[0] + guard2[1];
keep_10_2_1_2 : -1 <= -S[10,1] + guard2[0]-guard2[1];
keep_10_1_1_1 : -1 <= -S[10,1]-guard0[0] + guard0[1];
keep_10_1_1_2 : -1 <= -S[10,1] + guard0[0]-guard0[1];
keep_10_3_1_1 : -1 <= -S[10,1]-guard4[0] + guard4[1];
keep_10_3_1_2 : -1 <= -S[10,1] + guard4[0]-guard4[1];
keep_10_2_2_1 : -1 <= -S[10,2]-guard2[1] + guard2[2];
keep_10_2_2_2 : -1 <= -S[10,2] + guard2[1]-guard2[2];
keep_10_1_2_1 : -1 <= -S[10,2]-guard0[1] + guard0[2];
keep_10_1_2_2 : -1 <= -S[10,2] + guard0[1]-guard0[2];
keep_10_3_2_1 : -1 <= -S[10,2]-guard4[1] + guard4[2];
keep_10_3_2_2 : -1 <= -S[10,2] + guard4[1]-guard4[2];
keep_10_2_3_1 : -1 <= -S[10,3]-guard2[2] + guard2[3];
keep_10_2_3_2 : -1 <= -S[10,3] + guard2[2]-guard2[3];
keep_10_1_3_1 : -1 <= -S[10,3]-guard0[2] + guard0[3];
keep_10_1_3_2 : -1 <= -S[10,3] + guard0[2]-guard0[3];
keep_10_3_3_1 : -1 <= -S[10,3]-guard4[2] + guard4[3];
keep_10_3_3_2 : -1 <= -S[10,3] + guard4[2]-guard4[3];
keep_10_2_4_1 : -1 <= -S[10,4]-guard2[3] + guard2[4];
keep_10_2_4_2 : -1 <= -S[10,4] + guard2[3]-guard2[4];
keep_10_1_4_1 : -1 <= -S[10,4]-guard0[3] + guard0[4];
keep_10_1_4_2 : -1 <= -S[10,4] + guard0[3]-guard0[4];
keep_10_3_4_1 : -1 <= -S[10,4]-guard4[3] + guard4[4];
keep_10_3_4_2 : -1 <= -S[10,4] + guard4[3]-guard4[4];
keep_10_2_5_1 : -1 <= -S[10,5]-guard2[4] + guard2[5];
keep_10_2_5_2 : -1 <= -S[10,5] + guard2[4]-guard2[5];
keep_10_1_5_1 : -1 <= -S[10,5]-guard0[4] + guard0[5];
keep_10_1_5_2 : -1 <= -S[10,5] + guard0[4]-guard0[5];
keep_10_3_5_1 : -1 <= -S[10,5]-guard4[4] + guard4[5];
keep_10_3_5_2 : -1 <= -S[10,5] + guard4[4]-guard4[5];
keep_10_2_6_1 : -1 <= -S[10,6]-guard2[5] + guard2[6];
keep_10_2_6_2 : -1 <= -S[10,6] + guard2[5]-guard2[6];
keep_10_1_6_1 : -1 <= -S[10,6]-guard0[5] + guard0[6];
keep_10_1_6_2 : -1 <= -S[10,6] + guard0[5]-guard0[6];
keep_10_3_6_1 : -1 <= -S[10,6]-guard4[5] + guard4[6];
keep_10_3_6_2 : -1 <= -S[10,6] + guard4[5]-guard4[6];
keep_10_2_7_1 : -1 <= -S[10,7]-guard2[6] + guard2[7];
keep_10_2_7_2 : -1 <= -S[10,7] + guard2[6]-guard2[7];
keep_10_1_7_1 : -1 <= -S[10,7]-guard0[6] + guard0[7];
keep_10_1_7_2 : -1 <= -S[10,7] + guard0[6]-guard0[7];
keep_10_3_7_1 : -1 <= -S[10,7]-guard4[6] + guard4[7];
keep_10_3_7_2 : -1 <= -S[10,7] + guard4[6]-guard4[7];
keep_10_2_8_1 : -1 <= -S[10,8]-guard2[7] + guard2[8];
keep_10_2_8_2 : -1 <= -S[10,8] + guard2[7]-guard2[8];
keep_10_1_8_1 : -1 <= -S[10,8]-guard0[7] + guard0[8];
keep_10_1_8_2 : -1 <= -S[10,8] + guard0[7]-guard0[8];
keep_10_3_8_1 : -1 <= -S[10,8]-guard4[7] + guard4[8];
keep_10_3_8_2 : -1 <= -S[10,8] + guard4[7]-guard4[8];
keep_10_2_9_1 : -1 <= -S[10,9]-guard2[8] + guard2[9];
keep_10_2_9_2 : -1 <= -S[10,9] + guard2[8]-guard2[9];
keep_10_1_9_1 : -1 <= -S[10,9]-guard0[8] + guard0[9];
keep_10_1_9_2 : -1 <= -S[10,9] + guard0[8]-guard0[9];
keep_10_3_9_1 : -1 <= -S[10,9]-guard4[8] + guard4[9];
keep_10_3_9_2 : -1 <= -S[10,9] + guard4[8]-guard4[9];
keep_10_2_10_1 : -1 <= -S[10,10] + guard2[10]-guard2[9];
keep_10_2_10_2 : -1 <= -S[10,10]-guard2[10] + guard2[9];
keep_10_1_10_1 : -1 <= -S[10,10] + guard0[10]-guard0[9];
keep_10_1_10_2 : -1 <= -S[10,10]-guard0[10] + guard0[9];
keep_10_3_10_1 : -1 <= -S[10,10] + guard4[10]-guard4[9];
keep_10_3_10_2 : -1 <= -S[10,10]-guard4[10] + guard4[9];
keep_10_2_11_1 : -1 <= -S[10,11]-guard2[10] + guard2[11];
keep_10_2_11_2 : -1 <= -S[10,11] + guard2[10]-guard2[11];
keep_10_1_11_1 : -1 <= -S[10,11]-guard0[10] + guard0[11];
keep_10_1_11_2 : -1 <= -S[10,11] + guard0[10]-guard0[11];
keep_10_3_11_1 : -1 <= -S[10,11]-guard4[10] + guard4[11];
keep_10_3_11_2 : -1 <= -S[10,11] + guard4[10]-guard4[11];
keep_10_2_12_1 : -1 <= -S[10,12]-guard2[11] + guard2[12];
keep_10_2_12_2 : -1 <= -S[10,12] + guard2[11]-guard2[12];
keep_10_1_12_1 : -1 <= -S[10,12]-guard0[11] + guard0[12];
keep_10_1_12_2 : -1 <= -S[10,12] + guard0[11]-guard0[12];
keep_10_3_12_1 : -1 <= -S[10,12]-guard4[11] + guard4[12];
keep_10_3_12_2 : -1 <= -S[10,12] + guard4[11]-guard4[12];
keep_10_2_13_1 : -1 <= -S[10,13]-guard2[12] + guard2[13];
keep_10_2_13_2 : -1 <= -S[10,13] + guard2[12]-guard2[13];
keep_10_1_13_1 : -1 <= -S[10,13]-guard0[12] + guard0[13];
keep_10_1_13_2 : -1 <= -S[10,13] + guard0[12]-guard0[13];
keep_10_3_13_1 : -1 <= -S[10,13]-guard4[12] + guard4[13];
keep_10_3_13_2 : -1 <= -S[10,13] + guard4[12]-guard4[13];
keep_10_2_14_1 : -1 <= -S[10,14]-guard2[13] + guard2[14];
keep_10_2_14_2 : -1 <= -S[10,14] + guard2[13]-guard2[14];
keep_10_1_14_1 : -1 <= -S[10,14]-guard0[13] + guard0[14];
keep_10_1_14_2 : -1 <= -S[10,14] + guard0[13]-guard0[14];
keep_10_3_14_1 : -1 <= -S[10,14]-guard4[13] + guard4[14];
keep_10_3_14_2 : -1 <= -S[10,14] + guard4[13]-guard4[14];
keep_10_2_15_1 : -1 <= -S[10,15]-guard2[14] + guard2[15];
keep_10_2_15_2 : -1 <= -S[10,15] + guard2[14]-guard2[15];
keep_10_1_15_1 : -1 <= -S[10,15]-guard0[14] + guard0[15];
keep_10_1_15_2 : -1 <= -S[10,15] + guard0[14]-guard0[15];
keep_10_3_15_1 : -1 <= -S[10,15]-guard4[14] + guard4[15];
keep_10_3_15_2 : -1 <= -S[10,15] + guard4[14]-guard4[15];
keep_10_2_16_1 : -1 <= -S[10,16]-guard2[15] + guard2[16];
keep_10_2_16_2 : -1 <= -S[10,16] + guard2[15]-guard2[16];
keep_10_1_16_1 : -1 <= -S[10,16]-guard0[15] + guard0[16];
keep_10_1_16_2 : -1 <= -S[10,16] + guard0[15]-guard0[16];
keep_10_3_16_1 : -1 <= -S[10,16]-guard4[15] + guard4[16];
keep_10_3_16_2 : -1 <= -S[10,16] + guard4[15]-guard4[16];
keep_10_2_17_1 : -1 <= -S[10,17]-guard2[16] + guard2[17];
keep_10_2_17_2 : -1 <= -S[10,17] + guard2[16]-guard2[17];
keep_10_1_17_1 : -1 <= -S[10,17]-guard0[16] + guard0[17];
keep_10_1_17_2 : -1 <= -S[10,17] + guard0[16]-guard0[17];
keep_10_3_17_1 : -1 <= -S[10,17]-guard4[16] + guard4[17];
keep_10_3_17_2 : -1 <= -S[10,17] + guard4[16]-guard4[17];
keep_10_2_18_1 : -1 <= -S[10,18]-guard2[17] + guard2[18];
keep_10_2_18_2 : -1 <= -S[10,18] + guard2[17]-guard2[18];
keep_10_1_18_1 : -1 <= -S[10,18]-guard0[17] + guard0[18];
keep_10_1_18_2 : -1 <= -S[10,18] + guard0[17]-guard0[18];
keep_10_3_18_1 : -1 <= -S[10,18]-guard4[17] + guard4[18];
keep_10_3_18_2 : -1 <= -S[10,18] + guard4[17]-guard4[18];
keep_10_2_19_1 : -1 <= -S[10,19]-guard2[18] + guard2[19];
keep_10_2_19_2 : -1 <= -S[10,19] + guard2[18]-guard2[19];
keep_10_1_19_1 : -1 <= -S[10,19]-guard0[18] + guard0[19];
keep_10_1_19_2 : -1 <= -S[10,19] + guard0[18]-guard0[19];
keep_10_3_19_1 : -1 <= -S[10,19]-guard4[18] + guard4[19];
keep_10_3_19_2 : -1 <= -S[10,19] + guard4[18]-guard4[19];
keep_10_2_20_1 : -1 <= -S[10,20]-guard2[19] + guard2[20];
keep_10_2_20_2 : -1 <= -S[10,20] + guard2[19]-guard2[20];
keep_10_1_20_1 : -1 <= -S[10,20]-guard0[19] + guard0[20];
keep_10_1_20_2 : -1 <= -S[10,20] + guard0[19]-guard0[20];
keep_10_3_20_1 : -1 <= -S[10,20]-guard4[19] + guard4[20];
keep_10_3_20_2 : -1 <= -S[10,20] + guard4[19]-guard4[20];
keep_10_2_21_1 : -1 <= -S[10,21]-guard2[20] + guard2[21];
keep_10_2_21_2 : -1 <= -S[10,21] + guard2[20]-guard2[21];
keep_10_1_21_1 : -1 <= -S[10,21]-guard0[20] + guard0[21];
keep_10_1_21_2 : -1 <= -S[10,21] + guard0[20]-guard0[21];
keep_10_3_21_1 : -1 <= -S[10,21]-guard4[20] + guard4[21];
keep_10_3_21_2 : -1 <= -S[10,21] + guard4[20]-guard4[21];
keep_10_2_22_1 : -1 <= -S[10,22]-guard2[21] + guard2[22];
keep_10_2_22_2 : -1 <= -S[10,22] + guard2[21]-guard2[22];
keep_10_1_22_1 : -1 <= -S[10,22]-guard0[21] + guard0[22];
keep_10_1_22_2 : -1 <= -S[10,22] + guard0[21]-guard0[22];
keep_10_3_22_1 : -1 <= -S[10,22]-guard4[21] + guard4[22];
keep_10_3_22_2 : -1 <= -S[10,22] + guard4[21]-guard4[22];
keep_10_2_23_1 : -1 <= -S[10,23]-guard2[22] + guard2[23];
keep_10_2_23_2 : -1 <= -S[10,23] + guard2[22]-guard2[23];
keep_10_1_23_1 : -1 <= -S[10,23]-guard0[22] + guard0[23];
keep_10_1_23_2 : -1 <= -S[10,23] + guard0[22]-guard0[23];
keep_10_3_23_1 : -1 <= -S[10,23]-guard4[22] + guard4[23];
keep_10_3_23_2 : -1 <= -S[10,23] + guard4[22]-guard4[23];
keep_11_2_1_1 : -1 <= -S[11,1]-guard2[0] + guard2[1];
keep_11_2_1_2 : -1 <= -S[11,1] + guard2[0]-guard2[1];
keep_11_1_1_1 : -1 <= -S[11,1]-guard0[0] + guard0[1];
keep_11_1_1_2 : -1 <= -S[11,1] + guard0[0]-guard0[1];
keep_11_3_1_1 : -1 <= -S[11,1]-guard4[0] + guard4[1];
keep_11_3_1_2 : -1 <= -S[11,1] + guard4[0]-guard4[1];
keep_11_2_2_1 : -1 <= -S[11,2]-guard2[1] + guard2[2];
keep_11_2_2_2 : -1 <= -S[11,2] + guard2[1]-guard2[2];
keep_11_1_2_1 : -1 <= -S[11,2]-guard0[1] + guard0[2];
keep_11_1_2_2 : -1 <= -S[11,2] + guard0[1]-guard0[2];
keep_11_3_2_1 : -1 <= -S[11,2]-guard4[1] + guard4[2];
keep_11_3_2_2 : -1 <= -S[11,2] + guard4[1]-guard4[2];
keep_11_2_3_1 : -1 <= -S[11,3]-guard2[2] + guard2[3];
keep_11_2_3_2 : -1 <= -S[11,3] + guard2[2]-guard2[3];
keep_11_1_3_1 : -1 <= -S[11,3]-guard0[2] + guard0[3];
keep_11_1_3_2 : -1 <= -S[11,3] + guard0[2]-guard0[3];
keep_11_3_3_1 : -1 <= -S[11,3]-guard4[2] + guard4[3];
keep_11_3_3_2 : -1 <= -S[11,3] + guard4[2]-guard4[3];
keep_11_2_4_1 : -1 <= -S[11,4]-guard2[3] + guard2[4];
keep_11_2_4_2 : -1 <= -S[11,4] + guard2[3]-guard2[4];
keep_11_1_4_1 : -1 <= -S[11,4]-guard0[3] + guard0[4];
keep_11_1_4_2 : -1 <= -S[11,4] + guard0[3]-guard0[4];
keep_11_3_4_1 : -1 <= -S[11,4]-guard4[3] + guard4[4];
keep_11_3_4_2 : -1 <= -S[11,4] + guard4[3]-guard4[4];
keep_11_2_5_1 : -1 <= -S[11,5]-guard2[4] + guard2[5];
keep_11_2_5_2 : -1 <= -S[11,5] + guard2[4]-guard2[5];
keep_11_1_5_1 : -1 <= -S[11,5]-guard0[4] + guard0[5];
keep_11_1_5_2 : -1 <= -S[11,5] + guard0[4]-guard0[5];
keep_11_3_5_1 : -1 <= -S[11,5]-guard4[4] + guard4[5];
keep_11_3_5_2 : -1 <= -S[11,5] + guard4[4]-guard4[5];
keep_11_2_6_1 : -1 <= -S[11,6]-guard2[5] + guard2[6];
keep_11_2_6_2 : -1 <= -S[11,6] + guard2[5]-guard2[6];
keep_11_1_6_1 : -1 <= -S[11,6]-guard0[5] + guard0[6];
keep_11_1_6_2 : -1 <= -S[11,6] + guard0[5]-guard0[6];
keep_11_3_6_1 : -1 <= -S[11,6]-guard4[5] + guard4[6];
keep_11_3_6_2 : -1 <= -S[11,6] + guard4[5]-guard4[6];
keep_11_2_7_1 : -1 <= -S[11,7]-guard2[6] + guard2[7];
keep_11_2_7_2 : -1 <= -S[11,7] + guard2[6]-guard2[7];
keep_11_1_7_1 : -1 <= -S[11,7]-guard0[6] + guard0[7];
keep_11_1_7_2 : -1 <= -S[11,7] + guard0[6]-guard0[7];
keep_11_3_7_1 : -1 <= -S[11,7]-guard4[6] + guard4[7];
keep_11_3_7_2 : -1 <= -S[11,7] + guard4[6]-guard4[7];
keep_11_2_8_1 : -1 <= -S[11,8]-guard2[7] + guard2[8];
keep_11_2_8_2 : -1 <= -S[11,8] + guard2[7]-guard2[8];
keep_11_1_8_1 : -1 <= -S[11,8]-guard0[7] + guard0[8];
keep_11_1_8_2 : -1 <= -S[11,8] + guard0[7]-guard0[8];
keep_11_3_8_1 : -1 <= -S[11,8]-guard4[7] + guard4[8];
keep_11_3_8_2 : -1 <= -S[11,8] + guard4[7]-guard4[8];
keep_11_2_9_1 : -1 <= -S[11,9]-guard2[8] + guard2[9];
keep_11_2_9_2 : -1 <= -S[11,9] + guard2[8]-guard2[9];
keep_11_1_9_1 : -1 <= -S[11,9]-guard0[8] + guard0[9];
keep_11_1_9_2 : -1 <= -S[11,9] + guard0[8]-guard0[9];
keep_11_3_9_1 : -1 <= -S[11,9]-guard4[8] + guard4[9];
keep_11_3_9_2 : -1 <= -S[11,9] + guard4[8]-guard4[9];
keep_11_2_10_1 : -1 <= -S[11,10] + guard2[10]-guard2[9];
keep_11_2_10_2 : -1 <= -S[11,10]-guard2[10] + guard2[9];
keep_11_1_10_1 : -1 <= -S[11,10] + guard0[10]-guard0[9];
keep_11_1_10_2 : -1 <= -S[11,10]-guard0[10] + guard0[9];
keep_11_3_10_1 : -1 <= -S[11,10] + guard4[10]-guard4[9];
keep_11_3_10_2 : -1 <= -S[11,10]-guard4[10] + guard4[9];
keep_11_2_11_1 : -1 <= -S[11,11]-guard2[10] + guard2[11];
keep_11_2_11_2 : -1 <= -S[11,11] + guard2[10]-guard2[11];
keep_11_1_11_1 : -1 <= -S[11,11]-guard0[10] + guard0[11];
keep_11_1_11_2 : -1 <= -S[11,11] + guard0[10]-guard0[11];
keep_11_3_11_1 : -1 <= -S[11,11]-guard4[10] + guard4[11];
keep_11_3_11_2 : -1 <= -S[11,11] + guard4[10]-guard4[11];
keep_11_2_12_1 : -1 <= -S[11,12]-guard2[11] + guard2[12];
keep_11_2_12_2 : -1 <= -S[11,12] + guard2[11]-guard2[12];
keep_11_1_12_1 : -1 <= -S[11,12]-guard0[11] + guard0[12];
keep_11_1_12_2 : -1 <= -S[11,12] + guard0[11]-guard0[12];
keep_11_3_12_1 : -1 <= -S[11,12]-guard4[11] + guard4[12];
keep_11_3_12_2 : -1 <= -S[11,12] + guard4[11]-guard4[12];
keep_11_2_13_1 : -1 <= -S[11,13]-guard2[12] + guard2[13];
keep_11_2_13_2 : -1 <= -S[11,13] + guard2[12]-guard2[13];
keep_11_1_13_1 : -1 <= -S[11,13]-guard0[12] + guard0[13];
keep_11_1_13_2 : -1 <= -S[11,13] + guard0[12]-guard0[13];
keep_11_3_13_1 : -1 <= -S[11,13]-guard4[12] + guard4[13];
keep_11_3_13_2 : -1 <= -S[11,13] + guard4[12]-guard4[13];
keep_11_2_14_1 : -1 <= -S[11,14]-guard2[13] + guard2[14];
keep_11_2_14_2 : -1 <= -S[11,14] + guard2[13]-guard2[14];
keep_11_1_14_1 : -1 <= -S[11,14]-guard0[13] + guard0[14];
keep_11_1_14_2 : -1 <= -S[11,14] + guard0[13]-guard0[14];
keep_11_3_14_1 : -1 <= -S[11,14]-guard4[13] + guard4[14];
keep_11_3_14_2 : -1 <= -S[11,14] + guard4[13]-guard4[14];
keep_11_2_15_1 : -1 <= -S[11,15]-guard2[14] + guard2[15];
keep_11_2_15_2 : -1 <= -S[11,15] + guard2[14]-guard2[15];
keep_11_1_15_1 : -1 <= -S[11,15]-guard0[14] + guard0[15];
keep_11_1_15_2 : -1 <= -S[11,15] + guard0[14]-guard0[15];
keep_11_3_15_1 : -1 <= -S[11,15]-guard4[14] + guard4[15];
keep_11_3_15_2 : -1 <= -S[11,15] + guard4[14]-guard4[15];
keep_11_2_16_1 : -1 <= -S[11,16]-guard2[15] + guard2[16];
keep_11_2_16_2 : -1 <= -S[11,16] + guard2[15]-guard2[16];
keep_11_1_16_1 : -1 <= -S[11,16]-guard0[15] + guard0[16];
keep_11_1_16_2 : -1 <= -S[11,16] + guard0[15]-guard0[16];
keep_11_3_16_1 : -1 <= -S[11,16]-guard4[15] + guard4[16];
keep_11_3_16_2 : -1 <= -S[11,16] + guard4[15]-guard4[16];
keep_11_2_17_1 : -1 <= -S[11,17]-guard2[16] + guard2[17];
keep_11_2_17_2 : -1 <= -S[11,17] + guard2[16]-guard2[17];
keep_11_1_17_1 : -1 <= -S[11,17]-guard0[16] + guard0[17];
keep_11_1_17_2 : -1 <= -S[11,17] + guard0[16]-guard0[17];
keep_11_3_17_1 : -1 <= -S[11,17]-guard4[16] + guard4[17];
keep_11_3_17_2 : -1 <= -S[11,17] + guard4[16]-guard4[17];
keep_11_2_18_1 : -1 <= -S[11,18]-guard2[17] + guard2[18];
keep_11_2_18_2 : -1 <= -S[11,18] + guard2[17]-guard2[18];
keep_11_1_18_1 : -1 <= -S[11,18]-guard0[17] + guard0[18];
keep_11_1_18_2 : -1 <= -S[11,18] + guard0[17]-guard0[18];
keep_11_3_18_1 : -1 <= -S[11,18]-guard4[17] + guard4[18];
keep_11_3_18_2 : -1 <= -S[11,18] + guard4[17]-guard4[18];
keep_11_2_19_1 : -1 <= -S[11,19]-guard2[18] + guard2[19];
keep_11_2_19_2 : -1 <= -S[11,19] + guard2[18]-guard2[19];
keep_11_1_19_1 : -1 <= -S[11,19]-guard0[18] + guard0[19];
keep_11_1_19_2 : -1 <= -S[11,19] + guard0[18]-guard0[19];
keep_11_3_19_1 : -1 <= -S[11,19]-guard4[18] + guard4[19];
keep_11_3_19_2 : -1 <= -S[11,19] + guard4[18]-guard4[19];
keep_11_2_20_1 : -1 <= -S[11,20]-guard2[19] + guard2[20];
keep_11_2_20_2 : -1 <= -S[11,20] + guard2[19]-guard2[20];
keep_11_1_20_1 : -1 <= -S[11,20]-guard0[19] + guard0[20];
keep_11_1_20_2 : -1 <= -S[11,20] + guard0[19]-guard0[20];
keep_11_3_20_1 : -1 <= -S[11,20]-guard4[19] + guard4[20];
keep_11_3_20_2 : -1 <= -S[11,20] + guard4[19]-guard4[20];
keep_11_2_21_1 : -1 <= -S[11,21]-guard2[20] + guard2[21];
keep_11_2_21_2 : -1 <= -S[11,21] + guard2[20]-guard2[21];
keep_11_1_21_1 : -1 <= -S[11,21]-guard0[20] + guard0[21];
keep_11_1_21_2 : -1 <= -S[11,21] + guard0[20]-guard0[21];
keep_11_3_21_1 : -1 <= -S[11,21]-guard4[20] + guard4[21];
keep_11_3_21_2 : -1 <= -S[11,21] + guard4[20]-guard4[21];
keep_11_2_22_1 : -1 <= -S[11,22]-guard2[21] + guard2[22];
keep_11_2_22_2 : -1 <= -S[11,22] + guard2[21]-guard2[22];
keep_11_1_22_1 : -1 <= -S[11,22]-guard0[21] + guard0[22];
keep_11_1_22_2 : -1 <= -S[11,22] + guard0[21]-guard0[22];
keep_11_3_22_1 : -1 <= -S[11,22]-guard4[21] + guard4[22];
keep_11_3_22_2 : -1 <= -S[11,22] + guard4[21]-guard4[22];
keep_11_2_23_1 : -1 <= -S[11,23]-guard2[22] + guard2[23];
keep_11_2_23_2 : -1 <= -S[11,23] + guard2[22]-guard2[23];
keep_11_1_23_1 : -1 <= -S[11,23]-guard0[22] + guard0[23];
keep_11_1_23_2 : -1 <= -S[11,23] + guard0[22]-guard0[23];
keep_11_3_23_1 : -1 <= -S[11,23]-guard4[22] + guard4[23];
keep_11_3_23_2 : -1 <= -S[11,23] + guard4[22]-guard4[23];
keep_12_2_1_1 : -1 <= -S[12,1]-guard2[0] + guard2[1];
keep_12_2_1_2 : -1 <= -S[12,1] + guard2[0]-guard2[1];
keep_12_1_1_1 : -1 <= -S[12,1]-guard0[0] + guard0[1];
keep_12_1_1_2 : -1 <= -S[12,1] + guard0[0]-guard0[1];
keep_12_3_1_1 : -1 <= -S[12,1]-guard4[0] + guard4[1];
keep_12_3_1_2 : -1 <= -S[12,1] + guard4[0]-guard4[1];
keep_12_2_2_1 : -1 <= -S[12,2]-guard2[1] + guard2[2];
keep_12_2_2_2 : -1 <= -S[12,2] + guard2[1]-guard2[2];
keep_12_1_2_1 : -1 <= -S[12,2]-guard0[1] + guard0[2];
keep_12_1_2_2 : -1 <= -S[12,2] + guard0[1]-guard0[2];
keep_12_3_2_1 : -1 <= -S[12,2]-guard4[1] + guard4[2];
keep_12_3_2_2 : -1 <= -S[12,2] + guard4[1]-guard4[2];
keep_12_2_3_1 : -1 <= -S[12,3]-guard2[2] + guard2[3];
keep_12_2_3_2 : -1 <= -S[12,3] + guard2[2]-guard2[3];
keep_12_1_3_1 : -1 <= -S[12,