set INPUTS := {'x[0,1]','x[0,0]','x[1,1]','x[1,0]'};
set OUTPUTS := {'w'};
param tmax := 60;
param lmax := 23;
param bits := 2;
param c{INPUTS};
param d{OUTPUTS};
var S{1..lmax,1..tmax},>=0,<=1;
var x{0..1,0..1},>=0,<=1;
var w,>=0,<=1;
var test1{0..tmax-1},>=0,<=1;
var parity{0..tmax-1},>=0,<=1;
var sentinel2{0..bits-1,0..tmax-1},>=0,<=1;
var i{0..bits-1,0..tmax-1},>=0,<=1;
var j{0..bits-1,0..tmax-1},>=0,<=1;
var sentinel1{0..bits-1,0..tmax-1},>=0,<=1;
var test2{0..tmax-1},>=0,<=1;
var temp4{0..tmax-1},>=0,<=1;
var _N15{0..1,0..tmax-1},>=0,<=1;
var _M15{0..1,0..tmax-1},>=0,<=1;
maximize obj: 0+c['x[0,1]']*x[0,1]+c['x[0,0]']*x[0,0]+c['x[1,1]']*x[1,1]+c['x[1,0]']*x[1,0]+d['w']*w;
C_0 : 0 = test1[0];
C_1 : 0 = parity[0];
C_2 : 0 = sentinel2[0,0] + sentinel2[1,0];
C_3 : 0 = i[0,0] + i[1,0];
C_4 : 0 = j[0,0] + j[1,0];
C_5 : 0 = sentinel1[0,0] + sentinel1[1,0];
C_6 : 0 = test2[0];
C_7 : 0 = temp4[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];
E25 : 1 = S[1,25] + S[10,25] + S[11,25] + S[12,25] + S[13,25] + S[14,25] + S[15,25] + S[16,25] + S[17,25] + S[18,25] + S[19,25] + S[2,25] + S[20,25] + S[21,25] + S[22,25] + S[23,25] + S[3,25] + S[4,25] + S[5,25] + S[6,25] + S[7,25] + S[8,25] + S[9,25];
E26 : 1 = S[1,26] + S[10,26] + S[11,26] + S[12,26] + S[13,26] + S[14,26] + S[15,26] + S[16,26] + S[17,26] + S[18,26] + S[19,26] + S[2,26] + S[20,26] + S[21,26] + S[22,26] + S[23,26] + S[3,26] + S[4,26] + S[5,26] + S[6,26] + S[7,26] + S[8,26] + S[9,26];
E27 : 1 = S[1,27] + S[10,27] + S[11,27] + S[12,27] + S[13,27] + S[14,27] + S[15,27] + S[16,27] + S[17,27] + S[18,27] + S[19,27] + S[2,27] + S[20,27] + S[21,27] + S[22,27] + S[23,27] + S[3,27] + S[4,27] + S[5,27] + S[6,27] + S[7,27] + S[8,27] + S[9,27];
E28 : 1 = S[1,28] + S[10,28] + S[11,28] + S[12,28] + S[13,28] + S[14,28] + S[15,28] + S[16,28] + S[17,28] + S[18,28] + S[19,28] + S[2,28] + S[20,28] + S[21,28] + S[22,28] + S[23,28] + S[3,28] + S[4,28] + S[5,28] + S[6,28] + S[7,28] + S[8,28] + S[9,28];
E29 : 1 = S[1,29] + S[10,29] + S[11,29] + S[12,29] + S[13,29] + S[14,29] + S[15,29] + S[16,29] + S[17,29] + S[18,29] + S[19,29] + S[2,29] + S[20,29] + S[21,29] + S[22,29] + S[23,29] + S[3,29] + S[4,29] + S[5,29] + S[6,29] + S[7,29] + S[8,29] + S[9,29];
E30 : 1 = S[1,30] + S[10,30] + S[11,30] + S[12,30] + S[13,30] + S[14,30] + S[15,30] + S[16,30] + S[17,30] + S[18,30] + S[19,30] + S[2,30] + S[20,30] + S[21,30] + S[22,30] + S[23,30] + S[3,30] + S[4,30] + S[5,30] + S[6,30] + S[7,30] + S[8,30] + S[9,30];
E31 : 1 = S[1,31] + S[10,31] + S[11,31] + S[12,31] + S[13,31] + S[14,31] + S[15,31] + S[16,31] + S[17,31] + S[18,31] + S[19,31] + S[2,31] + S[20,31] + S[21,31] + S[22,31] + S[23,31] + S[3,31] + S[4,31] + S[5,31] + S[6,31] + S[7,31] + S[8,31] + S[9,31];
E32 : 1 = S[1,32] + S[10,32] + S[11,32] + S[12,32] + S[13,32] + S[14,32] + S[15,32] + S[16,32] + S[17,32] + S[18,32] + S[19,32] + S[2,32] + S[20,32] + S[21,32] + S[22,32] + S[23,32] + S[3,32] + S[4,32] + S[5,32] + S[6,32] + S[7,32] + S[8,32] + S[9,32];
E33 : 1 = S[1,33] + S[10,33] + S[11,33] + S[12,33] + S[13,33] + S[14,33] + S[15,33] + S[16,33] + S[17,33] + S[18,33] + S[19,33] + S[2,33] + S[20,33] + S[21,33] + S[22,33] + S[23,33] + S[3,33] + S[4,33] + S[5,33] + S[6,33] + S[7,33] + S[8,33] + S[9,33];
E34 : 1 = S[1,34] + S[10,34] + S[11,34] + S[12,34] + S[13,34] + S[14,34] + S[15,34] + S[16,34] + S[17,34] + S[18,34] + S[19,34] + S[2,34] + S[20,34] + S[21,34] + S[22,34] + S[23,34] + S[3,34] + S[4,34] + S[5,34] + S[6,34] + S[7,34] + S[8,34] + S[9,34];
E35 : 1 = S[1,35] + S[10,35] + S[11,35] + S[12,35] + S[13,35] + S[14,35] + S[15,35] + S[16,35] + S[17,35] + S[18,35] + S[19,35] + S[2,35] + S[20,35] + S[21,35] + S[22,35] + S[23,35] + S[3,35] + S[4,35] + S[5,35] + S[6,35] + S[7,35] + S[8,35] + S[9,35];
E36 : 1 = S[1,36] + S[10,36] + S[11,36] + S[12,36] + S[13,36] + S[14,36] + S[15,36] + S[16,36] + S[17,36] + S[18,36] + S[19,36] + S[2,36] + S[20,36] + S[21,36] + S[22,36] + S[23,36] + S[3,36] + S[4,36] + S[5,36] + S[6,36] + S[7,36] + S[8,36] + S[9,36];
E37 : 1 = S[1,37] + S[10,37] + S[11,37] + S[12,37] + S[13,37] + S[14,37] + S[15,37] + S[16,37] + S[17,37] + S[18,37] + S[19,37] + S[2,37] + S[20,37] + S[21,37] + S[22,37] + S[23,37] + S[3,37] + S[4,37] + S[5,37] + S[6,37] + S[7,37] + S[8,37] + S[9,37];
E38 : 1 = S[1,38] + S[10,38] + S[11,38] + S[12,38] + S[13,38] + S[14,38] + S[15,38] + S[16,38] + S[17,38] + S[18,38] + S[19,38] + S[2,38] + S[20,38] + S[21,38] + S[22,38] + S[23,38] + S[3,38] + S[4,38] + S[5,38] + S[6,38] + S[7,38] + S[8,38] + S[9,38];
E39 : 1 = S[1,39] + S[10,39] + S[11,39] + S[12,39] + S[13,39] + S[14,39] + S[15,39] + S[16,39] + S[17,39] + S[18,39] + S[19,39] + S[2,39] + S[20,39] + S[21,39] + S[22,39] + S[23,39] + S[3,39] + S[4,39] + S[5,39] + S[6,39] + S[7,39] + S[8,39] + S[9,39];
E40 : 1 = S[1,40] + S[10,40] + S[11,40] + S[12,40] + S[13,40] + S[14,40] + S[15,40] + S[16,40] + S[17,40] + S[18,40] + S[19,40] + S[2,40] + S[20,40] + S[21,40] + S[22,40] + S[23,40] + S[3,40] + S[4,40] + S[5,40] + S[6,40] + S[7,40] + S[8,40] + S[9,40];
E41 : 1 = S[1,41] + S[10,41] + S[11,41] + S[12,41] + S[13,41] + S[14,41] + S[15,41] + S[16,41] + S[17,41] + S[18,41] + S[19,41] + S[2,41] + S[20,41] + S[21,41] + S[22,41] + S[23,41] + S[3,41] + S[4,41] + S[5,41] + S[6,41] + S[7,41] + S[8,41] + S[9,41];
E42 : 1 = S[1,42] + S[10,42] + S[11,42] + S[12,42] + S[13,42] + S[14,42] + S[15,42] + S[16,42] + S[17,42] + S[18,42] + S[19,42] + S[2,42] + S[20,42] + S[21,42] + S[22,42] + S[23,42] + S[3,42] + S[4,42] + S[5,42] + S[6,42] + S[7,42] + S[8,42] + S[9,42];
E43 : 1 = S[1,43] + S[10,43] + S[11,43] + S[12,43] + S[13,43] + S[14,43] + S[15,43] + S[16,43] + S[17,43] + S[18,43] + S[19,43] + S[2,43] + S[20,43] + S[21,43] + S[22,43] + S[23,43] + S[3,43] + S[4,43] + S[5,43] + S[6,43] + S[7,43] + S[8,43] + S[9,43];
E44 : 1 = S[1,44] + S[10,44] + S[11,44] + S[12,44] + S[13,44] + S[14,44] + S[15,44] + S[16,44] + S[17,44] + S[18,44] + S[19,44] + S[2,44] + S[20,44] + S[21,44] + S[22,44] + S[23,44] + S[3,44] + S[4,44] + S[5,44] + S[6,44] + S[7,44] + S[8,44] + S[9,44];
E45 : 1 = S[1,45] + S[10,45] + S[11,45] + S[12,45] + S[13,45] + S[14,45] + S[15,45] + S[16,45] + S[17,45] + S[18,45] + S[19,45] + S[2,45] + S[20,45] + S[21,45] + S[22,45] + S[23,45] + S[3,45] + S[4,45] + S[5,45] + S[6,45] + S[7,45] + S[8,45] + S[9,45];
E46 : 1 = S[1,46] + S[10,46] + S[11,46] + S[12,46] + S[13,46] + S[14,46] + S[15,46] + S[16,46] + S[17,46] + S[18,46] + S[19,46] + S[2,46] + S[20,46] + S[21,46] + S[22,46] + S[23,46] + S[3,46] + S[4,46] + S[5,46] + S[6,46] + S[7,46] + S[8,46] + S[9,46];
E47 : 1 = S[1,47] + S[10,47] + S[11,47] + S[12,47] + S[13,47] + S[14,47] + S[15,47] + S[16,47] + S[17,47] + S[18,47] + S[19,47] + S[2,47] + S[20,47] + S[21,47] + S[22,47] + S[23,47] + S[3,47] + S[4,47] + S[5,47] + S[6,47] + S[7,47] + S[8,47] + S[9,47];
E48 : 1 = S[1,48] + S[10,48] + S[11,48] + S[12,48] + S[13,48] + S[14,48] + S[15,48] + S[16,48] + S[17,48] + S[18,48] + S[19,48] + S[2,48] + S[20,48] + S[21,48] + S[22,48] + S[23,48] + S[3,48] + S[4,48] + S[5,48] + S[6,48] + S[7,48] + S[8,48] + S[9,48];
E49 : 1 = S[1,49] + S[10,49] + S[11,49] + S[12,49] + S[13,49] + S[14,49] + S[15,49] + S[16,49] + S[17,49] + S[18,49] + S[19,49] + S[2,49] + S[20,49] + S[21,49] + S[22,49] + S[23,49] + S[3,49] + S[4,49] + S[5,49] + S[6,49] + S[7,49] + S[8,49] + S[9,49];
E50 : 1 = S[1,50] + S[10,50] + S[11,50] + S[12,50] + S[13,50] + S[14,50] + S[15,50] + S[16,50] + S[17,50] + S[18,50] + S[19,50] + S[2,50] + S[20,50] + S[21,50] + S[22,50] + S[23,50] + S[3,50] + S[4,50] + S[5,50] + S[6,50] + S[7,50] + S[8,50] + S[9,50];
E51 : 1 = S[1,51] + S[10,51] + S[11,51] + S[12,51] + S[13,51] + S[14,51] + S[15,51] + S[16,51] + S[17,51] + S[18,51] + S[19,51] + S[2,51] + S[20,51] + S[21,51] + S[22,51] + S[23,51] + S[3,51] + S[4,51] + S[5,51] + S[6,51] + S[7,51] + S[8,51] + S[9,51];
E52 : 1 = S[1,52] + S[10,52] + S[11,52] + S[12,52] + S[13,52] + S[14,52] + S[15,52] + S[16,52] + S[17,52] + S[18,52] + S[19,52] + S[2,52] + S[20,52] + S[21,52] + S[22,52] + S[23,52] + S[3,52] + S[4,52] + S[5,52] + S[6,52] + S[7,52] + S[8,52] + S[9,52];
E53 : 1 = S[1,53] + S[10,53] + S[11,53] + S[12,53] + S[13,53] + S[14,53] + S[15,53] + S[16,53] + S[17,53] + S[18,53] + S[19,53] + S[2,53] + S[20,53] + S[21,53] + S[22,53] + S[23,53] + S[3,53] + S[4,53] + S[5,53] + S[6,53] + S[7,53] + S[8,53] + S[9,53];
E54 : 1 = S[1,54] + S[10,54] + S[11,54] + S[12,54] + S[13,54] + S[14,54] + S[15,54] + S[16,54] + S[17,54] + S[18,54] + S[19,54] + S[2,54] + S[20,54] + S[21,54] + S[22,54] + S[23,54] + S[3,54] + S[4,54] + S[5,54] + S[6,54] + S[7,54] + S[8,54] + S[9,54];
E55 : 1 = S[1,55] + S[10,55] + S[11,55] + S[12,55] + S[13,55] + S[14,55] + S[15,55] + S[16,55] + S[17,55] + S[18,55] + S[19,55] + S[2,55] + S[20,55] + S[21,55] + S[22,55] + S[23,55] + S[3,55] + S[4,55] + S[5,55] + S[6,55] + S[7,55] + S[8,55] + S[9,55];
E56 : 1 = S[1,56] + S[10,56] + S[11,56] + S[12,56] + S[13,56] + S[14,56] + S[15,56] + S[16,56] + S[17,56] + S[18,56] + S[19,56] + S[2,56] + S[20,56] + S[21,56] + S[22,56] + S[23,56] + S[3,56] + S[4,56] + S[5,56] + S[6,56] + S[7,56] + S[8,56] + S[9,56];
E57 : 1 = S[1,57] + S[10,57] + S[11,57] + S[12,57] + S[13,57] + S[14,57] + S[15,57] + S[16,57] + S[17,57] + S[18,57] + S[19,57] + S[2,57] + S[20,57] + S[21,57] + S[22,57] + S[23,57] + S[3,57] + S[4,57] + S[5,57] + S[6,57] + S[7,57] + S[8,57] + S[9,57];
E58 : 1 = S[1,58] + S[10,58] + S[11,58] + S[12,58] + S[13,58] + S[14,58] + S[15,58] + S[16,58] + S[17,58] + S[18,58] + S[19,58] + S[2,58] + S[20,58] + S[21,58] + S[22,58] + S[23,58] + S[3,58] + S[4,58] + S[5,58] + S[6,58] + S[7,58] + S[8,58] + S[9,58];
E59 : 1 = S[1,59] + S[10,59] + S[11,59] + S[12,59] + S[13,59] + S[14,59] + S[15,59] + S[16,59] + S[17,59] + S[18,59] + S[19,59] + S[2,59] + S[20,59] + S[21,59] + S[22,59] + S[23,59] + S[3,59] + S[4,59] + S[5,59] + S[6,59] + S[7,59] + S[8,59] + S[9,59];
E60 : 1 = S[1,60] + S[10,60] + S[11,60] + S[12,60] + S[13,60] + S[14,60] + S[15,60] + S[16,60] + S[17,60] + S[18,60] + S[19,60] + S[2,60] + S[20,60] + S[21,60] + S[22,60] + S[23,60] + S[3,60] + S[4,60] + S[5,60] + S[6,60] + S[7,60] + S[8,60] + S[9,60];
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_1_24 : 0 <= -S[1,24] + S[2,25];
F_o_1_25 : 0 <= -S[1,25] + S[2,26];
F_o_1_26 : 0 <= -S[1,26] + S[2,27];
F_o_1_27 : 0 <= -S[1,27] + S[2,28];
F_o_1_28 : 0 <= -S[1,28] + S[2,29];
F_o_1_29 : 0 <= -S[1,29] + S[2,30];
F_o_1_30 : 0 <= -S[1,30] + S[2,31];
F_o_1_31 : 0 <= -S[1,31] + S[2,32];
F_o_1_32 : 0 <= -S[1,32] + S[2,33];
F_o_1_33 : 0 <= -S[1,33] + S[2,34];
F_o_1_34 : 0 <= -S[1,34] + S[2,35];
F_o_1_35 : 0 <= -S[1,35] + S[2,36];
F_o_1_36 : 0 <= -S[1,36] + S[2,37];
F_o_1_37 : 0 <= -S[1,37] + S[2,38];
F_o_1_38 : 0 <= -S[1,38] + S[2,39];
F_o_1_39 : 0 <= -S[1,39] + S[2,40];
F_o_1_40 : 0 <= -S[1,40] + S[2,41];
F_o_1_41 : 0 <= -S[1,41] + S[2,42];
F_o_1_42 : 0 <= -S[1,42] + S[2,43];
F_o_1_43 : 0 <= -S[1,43] + S[2,44];
F_o_1_44 : 0 <= -S[1,44] + S[2,45];
F_o_1_45 : 0 <= -S[1,45] + S[2,46];
F_o_1_46 : 0 <= -S[1,46] + S[2,47];
F_o_1_47 : 0 <= -S[1,47] + S[2,48];
F_o_1_48 : 0 <= -S[1,48] + S[2,49];
F_o_1_49 : 0 <= -S[1,49] + S[2,50];
F_o_1_50 : 0 <= -S[1,50] + S[2,51];
F_o_1_51 : 0 <= -S[1,51] + S[2,52];
F_o_1_52 : 0 <= -S[1,52] + S[2,53];
F_o_1_53 : 0 <= -S[1,53] + S[2,54];
F_o_1_54 : 0 <= -S[1,54] + S[2,55];
F_o_1_55 : 0 <= -S[1,55] + S[2,56];
F_o_1_56 : 0 <= -S[1,56] + S[2,57];
F_o_1_57 : 0 <= -S[1,57] + S[2,58];
F_o_1_58 : 0 <= -S[1,58] + S[2,59];
F_o_1_59 : 0 <= -S[1,59] + S[2,60];
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_2_24 : 0 <= -S[2,24] + S[3,25];
F_o_2_25 : 0 <= -S[2,25] + S[3,26];
F_o_2_26 : 0 <= -S[2,26] + S[3,27];
F_o_2_27 : 0 <= -S[2,27] + S[3,28];
F_o_2_28 : 0 <= -S[2,28] + S[3,29];
F_o_2_29 : 0 <= -S[2,29] + S[3,30];
F_o_2_30 : 0 <= -S[2,30] + S[3,31];
F_o_2_31 : 0 <= -S[2,31] + S[3,32];
F_o_2_32 : 0 <= -S[2,32] + S[3,33];
F_o_2_33 : 0 <= -S[2,33] + S[3,34];
F_o_2_34 : 0 <= -S[2,34] + S[3,35];
F_o_2_35 : 0 <= -S[2,35] + S[3,36];
F_o_2_36 : 0 <= -S[2,36] + S[3,37];
F_o_2_37 : 0 <= -S[2,37] + S[3,38];
F_o_2_38 : 0 <= -S[2,38] + S[3,39];
F_o_2_39 : 0 <= -S[2,39] + S[3,40];
F_o_2_40 : 0 <= -S[2,40] + S[3,41];
F_o_2_41 : 0 <= -S[2,41] + S[3,42];
F_o_2_42 : 0 <= -S[2,42] + S[3,43];
F_o_2_43 : 0 <= -S[2,43] + S[3,44];
F_o_2_44 : 0 <= -S[2,44] + S[3,45];
F_o_2_45 : 0 <= -S[2,45] + S[3,46];
F_o_2_46 : 0 <= -S[2,46] + S[3,47];
F_o_2_47 : 0 <= -S[2,47] + S[3,48];
F_o_2_48 : 0 <= -S[2,48] + S[3,49];
F_o_2_49 : 0 <= -S[2,49] + S[3,50];
F_o_2_50 : 0 <= -S[2,50] + S[3,51];
F_o_2_51 : 0 <= -S[2,51] + S[3,52];
F_o_2_52 : 0 <= -S[2,52] + S[3,53];
F_o_2_53 : 0 <= -S[2,53] + S[3,54];
F_o_2_54 : 0 <= -S[2,54] + S[3,55];
F_o_2_55 : 0 <= -S[2,55] + S[3,56];
F_o_2_56 : 0 <= -S[2,56] + S[3,57];
F_o_2_57 : 0 <= -S[2,57] + S[3,58];
F_o_2_58 : 0 <= -S[2,58] + S[3,59];
F_o_2_59 : 0 <= -S[2,59] + S[3,60];
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_3_24 : 0 <= -S[3,24] + S[4,25];
F_o_3_25 : 0 <= -S[3,25] + S[4,26];
F_o_3_26 : 0 <= -S[3,26] + S[4,27];
F_o_3_27 : 0 <= -S[3,27] + S[4,28];
F_o_3_28 : 0 <= -S[3,28] + S[4,29];
F_o_3_29 : 0 <= -S[3,29] + S[4,30];
F_o_3_30 : 0 <= -S[3,30] + S[4,31];
F_o_3_31 : 0 <= -S[3,31] + S[4,32];
F_o_3_32 : 0 <= -S[3,32] + S[4,33];
F_o_3_33 : 0 <= -S[3,33] + S[4,34];
F_o_3_34 : 0 <= -S[3,34] + S[4,35];
F_o_3_35 : 0 <= -S[3,35] + S[4,36];
F_o_3_36 : 0 <= -S[3,36] + S[4,37];
F_o_3_37 : 0 <= -S[3,37] + S[4,38];
F_o_3_38 : 0 <= -S[3,38] + S[4,39];
F_o_3_39 : 0 <= -S[3,39] + S[4,40];
F_o_3_40 : 0 <= -S[3,40] + S[4,41];
F_o_3_41 : 0 <= -S[3,41] + S[4,42];
F_o_3_42 : 0 <= -S[3,42] + S[4,43];
F_o_3_43 : 0 <= -S[3,43] + S[4,44];
F_o_3_44 : 0 <= -S[3,44] + S[4,45];
F_o_3_45 : 0 <= -S[3,45] + S[4,46];
F_o_3_46 : 0 <= -S[3,46] + S[4,47];
F_o_3_47 : 0 <= -S[3,47] + S[4,48];
F_o_3_48 : 0 <= -S[3,48] + S[4,49];
F_o_3_49 : 0 <= -S[3,49] + S[4,50];
F_o_3_50 : 0 <= -S[3,50] + S[4,51];
F_o_3_51 : 0 <= -S[3,51] + S[4,52];
F_o_3_52 : 0 <= -S[3,52] + S[4,53];
F_o_3_53 : 0 <= -S[3,53] + S[4,54];
F_o_3_54 : 0 <= -S[3,54] + S[4,55];
F_o_3_55 : 0 <= -S[3,55] + S[4,56];
F_o_3_56 : 0 <= -S[3,56] + S[4,57];
F_o_3_57 : 0 <= -S[3,57] + S[4,58];
F_o_3_58 : 0 <= -S[3,58] + S[4,59];
F_o_3_59 : 0 <= -S[3,59] + S[4,60];
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_4_24 : 0 <= -S[4,24] + S[5,25];
F_o_4_25 : 0 <= -S[4,25] + S[5,26];
F_o_4_26 : 0 <= -S[4,26] + S[5,27];
F_o_4_27 : 0 <= -S[4,27] + S[5,28];
F_o_4_28 : 0 <= -S[4,28] + S[5,29];
F_o_4_29 : 0 <= -S[4,29] + S[5,30];
F_o_4_30 : 0 <= -S[4,30] + S[5,31];
F_o_4_31 : 0 <= -S[4,31] + S[5,32];
F_o_4_32 : 0 <= -S[4,32] + S[5,33];
F_o_4_33 : 0 <= -S[4,33] + S[5,34];
F_o_4_34 : 0 <= -S[4,34] + S[5,35];
F_o_4_35 : 0 <= -S[4,35] + S[5,36];
F_o_4_36 : 0 <= -S[4,36] + S[5,37];
F_o_4_37 : 0 <= -S[4,37] + S[5,38];
F_o_4_38 : 0 <= -S[4,38] + S[5,39];
F_o_4_39 : 0 <= -S[4,39] + S[5,40];
F_o_4_40 : 0 <= -S[4,40] + S[5,41];
F_o_4_41 : 0 <= -S[4,41] + S[5,42];
F_o_4_42 : 0 <= -S[4,42] + S[5,43];
F_o_4_43 : 0 <= -S[4,43] + S[5,44];
F_o_4_44 : 0 <= -S[4,44] + S[5,45];
F_o_4_45 : 0 <= -S[4,45] + S[5,46];
F_o_4_46 : 0 <= -S[4,46] + S[5,47];
F_o_4_47 : 0 <= -S[4,47] + S[5,48];
F_o_4_48 : 0 <= -S[4,48] + S[5,49];
F_o_4_49 : 0 <= -S[4,49] + S[5,50];
F_o_4_50 : 0 <= -S[4,50] + S[5,51];
F_o_4_51 : 0 <= -S[4,51] + S[5,52];
F_o_4_52 : 0 <= -S[4,52] + S[5,53];
F_o_4_53 : 0 <= -S[4,53] + S[5,54];
F_o_4_54 : 0 <= -S[4,54] + S[5,55];
F_o_4_55 : 0 <= -S[4,55] + S[5,56];
F_o_4_56 : 0 <= -S[4,56] + S[5,57];
F_o_4_57 : 0 <= -S[4,57] + S[5,58];
F_o_4_58 : 0 <= -S[4,58] + S[5,59];
F_o_4_59 : 0 <= -S[4,59] + S[5,60];
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_5_24 : 0 <= -S[5,24] + S[6,25];
F_o_5_25 : 0 <= -S[5,25] + S[6,26];
F_o_5_26 : 0 <= -S[5,26] + S[6,27];
F_o_5_27 : 0 <= -S[5,27] + S[6,28];
F_o_5_28 : 0 <= -S[5,28] + S[6,29];
F_o_5_29 : 0 <= -S[5,29] + S[6,30];
F_o_5_30 : 0 <= -S[5,30] + S[6,31];
F_o_5_31 : 0 <= -S[5,31] + S[6,32];
F_o_5_32 : 0 <= -S[5,32] + S[6,33];
F_o_5_33 : 0 <= -S[5,33] + S[6,34];
F_o_5_34 : 0 <= -S[5,34] + S[6,35];
F_o_5_35 : 0 <= -S[5,35] + S[6,36];
F_o_5_36 : 0 <= -S[5,36] + S[6,37];
F_o_5_37 : 0 <= -S[5,37] + S[6,38];
F_o_5_38 : 0 <= -S[5,38] + S[6,39];
F_o_5_39 : 0 <= -S[5,39] + S[6,40];
F_o_5_40 : 0 <= -S[5,40] + S[6,41];
F_o_5_41 : 0 <= -S[5,41] + S[6,42];
F_o_5_42 : 0 <= -S[5,42] + S[6,43];
F_o_5_43 : 0 <= -S[5,43] + S[6,44];
F_o_5_44 : 0 <= -S[5,44] + S[6,45];
F_o_5_45 : 0 <= -S[5,45] + S[6,46];
F_o_5_46 : 0 <= -S[5,46] + S[6,47];
F_o_5_47 : 0 <= -S[5,47] + S[6,48];
F_o_5_48 : 0 <= -S[5,48] + S[6,49];
F_o_5_49 : 0 <= -S[5,49] + S[6,50];
F_o_5_50 : 0 <= -S[5,50] + S[6,51];
F_o_5_51 : 0 <= -S[5,51] + S[6,52];
F_o_5_52 : 0 <= -S[5,52] + S[6,53];
F_o_5_53 : 0 <= -S[5,53] + S[6,54];
F_o_5_54 : 0 <= -S[5,54] + S[6,55];
F_o_5_55 : 0 <= -S[5,55] + S[6,56];
F_o_5_56 : 0 <= -S[5,56] + S[6,57];
F_o_5_57 : 0 <= -S[5,57] + S[6,58];
F_o_5_58 : 0 <= -S[5,58] + S[6,59];
F_o_5_59 : 0 <= -S[5,59] + S[6,60];
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_6_24 : 0 <= -S[6,24] + S[7,25];
F_o_6_25 : 0 <= -S[6,25] + S[7,26];
F_o_6_26 : 0 <= -S[6,26] + S[7,27];
F_o_6_27 : 0 <= -S[6,27] + S[7,28];
F_o_6_28 : 0 <= -S[6,28] + S[7,29];
F_o_6_29 : 0 <= -S[6,29] + S[7,30];
F_o_6_30 : 0 <= -S[6,30] + S[7,31];
F_o_6_31 : 0 <= -S[6,31] + S[7,32];
F_o_6_32 : 0 <= -S[6,32] + S[7,33];
F_o_6_33 : 0 <= -S[6,33] + S[7,34];
F_o_6_34 : 0 <= -S[6,34] + S[7,35];
F_o_6_35 : 0 <= -S[6,35] + S[7,36];
F_o_6_36 : 0 <= -S[6,36] + S[7,37];
F_o_6_37 : 0 <= -S[6,37] + S[7,38];
F_o_6_38 : 0 <= -S[6,38] + S[7,39];
F_o_6_39 : 0 <= -S[6,39] + S[7,40];
F_o_6_40 : 0 <= -S[6,40] + S[7,41];
F_o_6_41 : 0 <= -S[6,41] + S[7,42];
F_o_6_42 : 0 <= -S[6,42] + S[7,43];
F_o_6_43 : 0 <= -S[6,43] + S[7,44];
F_o_6_44 : 0 <= -S[6,44] + S[7,45];
F_o_6_45 : 0 <= -S[6,45] + S[7,46];
F_o_6_46 : 0 <= -S[6,46] + S[7,47];
F_o_6_47 : 0 <= -S[6,47] + S[7,48];
F_o_6_48 : 0 <= -S[6,48] + S[7,49];
F_o_6_49 : 0 <= -S[6,49] + S[7,50];
F_o_6_50 : 0 <= -S[6,50] + S[7,51];
F_o_6_51 : 0 <= -S[6,51] + S[7,52];
F_o_6_52 : 0 <= -S[6,52] + S[7,53];
F_o_6_53 : 0 <= -S[6,53] + S[7,54];
F_o_6_54 : 0 <= -S[6,54] + S[7,55];
F_o_6_55 : 0 <= -S[6,55] + S[7,56];
F_o_6_56 : 0 <= -S[6,56] + S[7,57];
F_o_6_57 : 0 <= -S[6,57] + S[7,58];
F_o_6_58 : 0 <= -S[6,58] + S[7,59];
F_o_6_59 : 0 <= -S[6,59] + S[7,60];
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_7_24 : 0 <= -S[7,24] + S[8,25];
F_o_7_25 : 0 <= -S[7,25] + S[8,26];
F_o_7_26 : 0 <= -S[7,26] + S[8,27];
F_o_7_27 : 0 <= -S[7,27] + S[8,28];
F_o_7_28 : 0 <= -S[7,28] + S[8,29];
F_o_7_29 : 0 <= -S[7,29] + S[8,30];
F_o_7_30 : 0 <= -S[7,30] + S[8,31];
F_o_7_31 : 0 <= -S[7,31] + S[8,32];
F_o_7_32 : 0 <= -S[7,32] + S[8,33];
F_o_7_33 : 0 <= -S[7,33] + S[8,34];
F_o_7_34 : 0 <= -S[7,34] + S[8,35];
F_o_7_35 : 0 <= -S[7,35] + S[8,36];
F_o_7_36 : 0 <= -S[7,36] + S[8,37];
F_o_7_37 : 0 <= -S[7,37] + S[8,38];
F_o_7_38 : 0 <= -S[7,38] + S[8,39];
F_o_7_39 : 0 <= -S[7,39] + S[8,40];
F_o_7_40 : 0 <= -S[7,40] + S[8,41];
F_o_7_41 : 0 <= -S[7,41] + S[8,42];
F_o_7_42 : 0 <= -S[7,42] + S[8,43];
F_o_7_43 : 0 <= -S[7,43] + S[8,44];
F_o_7_44 : 0 <= -S[7,44] + S[8,45];
F_o_7_45 : 0 <= -S[7,45] + S[8,46];
F_o_7_46 : 0 <= -S[7,46] + S[8,47];
F_o_7_47 : 0 <= -S[7,47] + S[8,48];
F_o_7_48 : 0 <= -S[7,48] + S[8,49];
F_o_7_49 : 0 <= -S[7,49] + S[8,50];
F_o_7_50 : 0 <= -S[7,50] + S[8,51];
F_o_7_51 : 0 <= -S[7,51] + S[8,52];
F_o_7_52 : 0 <= -S[7,52] + S[8,53];
F_o_7_53 : 0 <= -S[7,53] + S[8,54];
F_o_7_54 : 0 <= -S[7,54] + S[8,55];
F_o_7_55 : 0 <= -S[7,55] + S[8,56];
F_o_7_56 : 0 <= -S[7,56] + S[8,57];
F_o_7_57 : 0 <= -S[7,57] + S[8,58];
F_o_7_58 : 0 <= -S[7,58] + S[8,59];
F_o_7_59 : 0 <= -S[7,59] + S[8,60];
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_8_24 : 0 <= -S[8,24] + S[9,25];
F_o_8_25 : 0 <= -S[8,25] + S[9,26];
F_o_8_26 : 0 <= -S[8,26] + S[9,27];
F_o_8_27 : 0 <= -S[8,27] + S[9,28];
F_o_8_28 : 0 <= -S[8,28] + S[9,29];
F_o_8_29 : 0 <= -S[8,29] + S[9,30];
F_o_8_30 : 0 <= -S[8,30] + S[9,31];
F_o_8_31 : 0 <= -S[8,31] + S[9,32];
F_o_8_32 : 0 <= -S[8,32] + S[9,33];
F_o_8_33 : 0 <= -S[8,33] + S[9,34];
F_o_8_34 : 0 <= -S[8,34] + S[9,35];
F_o_8_35 : 0 <= -S[8,35] + S[9,36];
F_o_8_36 : 0 <= -S[8,36] + S[9,37];
F_o_8_37 : 0 <= -S[8,37] + S[9,38];
F_o_8_38 : 0 <= -S[8,38] + S[9,39];
F_o_8_39 : 0 <= -S[8,39] + S[9,40];
F_o_8_40 : 0 <= -S[8,40] + S[9,41];
F_o_8_41 : 0 <= -S[8,41] + S[9,42];
F_o_8_42 : 0 <= -S[8,42] + S[9,43];
F_o_8_43 : 0 <= -S[8,43] + S[9,44];
F_o_8_44 : 0 <= -S[8,44] + S[9,45];
F_o_8_45 : 0 <= -S[8,45] + S[9,46];
F_o_8_46 : 0 <= -S[8,46] + S[9,47];
F_o_8_47 : 0 <= -S[8,47] + S[9,48];
F_o_8_48 : 0 <= -S[8,48] + S[9,49];
F_o_8_49 : 0 <= -S[8,49] + S[9,50];
F_o_8_50 : 0 <= -S[8,50] + S[9,51];
F_o_8_51 : 0 <= -S[8,51] + S[9,52];
F_o_8_52 : 0 <= -S[8,52] + S[9,53];
F_o_8_53 : 0 <= -S[8,53] + S[9,54];
F_o_8_54 : 0 <= -S[8,54] + S[9,55];
F_o_8_55 : 0 <= -S[8,55] + S[9,56];
F_o_8_56 : 0 <= -S[8,56] + S[9,57];
F_o_8_57 : 0 <= -S[8,57] + S[9,58];
F_o_8_58 : 0 <= -S[8,58] + S[9,59];
F_o_8_59 : 0 <= -S[8,59] + S[9,60];
F_iii_9_1_1 : -1 <=  + S[22,2]-S[9,1]-test1[1];
F_iii_9_1_2 : 0 <= S[10,2]-S[9,1] + test1[1];
F_iii_9_2_1 : -1 <=  + S[22,3]-S[9,2]-test1[2];
F_iii_9_2_2 : 0 <= S[10,3]-S[9,2] + test1[2];
F_iii_9_3_1 : -1 <=  + S[22,4]-S[9,3]-test1[3];
F_iii_9_3_2 : 0 <= S[10,4]-S[9,3] + test1[3];
F_iii_9_4_1 : -1 <=  + S[22,5]-S[9,4]-test1[4];
F_iii_9_4_2 : 0 <= S[10,5]-S[9,4] + test1[4];
F_iii_9_5_1 : -1 <=  + S[22,6]-S[9,5]-test1[5];
F_iii_9_5_2 : 0 <= S[10,6]-S[9,5] + test1[5];
F_iii_9_6_1 : -1 <=  + S[22,7]-S[9,6]-test1[6];
F_iii_9_6_2 : 0 <= S[10,7]-S[9,6] + test1[6];
F_iii_9_7_1 : -1 <=  + S[22,8]-S[9,7]-test1[7];
F_iii_9_7_2 : 0 <= S[10,8]-S[9,7] + test1[7];
F_iii_9_8_1 : -1 <=  + S[22,9]-S[9,8]-test1[8];
F_iii_9_8_2 : 0 <= S[10,9]-S[9,8] + test1[8];
F_iii_9_9_1 : -1 <=  + S[22,10]-S[9,9]-test1[9];
F_iii_9_9_2 : 0 <= S[10,10]-S[9,9] + test1[9];
F_iii_9_10_1 : -1 <=  + S[22,11]-S[9,10]-test1[10];
F_iii_9_10_2 : 0 <= S[10,11]-S[9,10] + test1[10];
F_iii_9_11_1 : -1 <=  + S[22,12]-S[9,11]-test1[11];
F_iii_9_11_2 : 0 <= S[10,12]-S[9,11] + test1[11];
F_iii_9_12_1 : -1 <=  + S[22,13]-S[9,12]-test1[12];
F_iii_9_12_2 : 0 <= S[10,13]-S[9,12] + test1[12];
F_iii_9_13_1 : -1 <=  + S[22,14]-S[9,13]-test1[13];
F_iii_9_13_2 : 0 <= S[10,14]-S[9,13] + test1[13];
F_iii_9_14_1 : -1 <=  + S[22,15]-S[9,14]-test1[14];
F_iii_9_14_2 : 0 <= S[10,15]-S[9,14] + test1[14];
F_iii_9_15_1 : -1 <=  + S[22,16]-S[9,15]-test1[15];
F_iii_9_15_2 : 0 <= S[10,16]-S[9,15] + test1[15];
F_iii_9_16_1 : -1 <=  + S[22,17]-S[9,16]-test1[16];
F_iii_9_16_2 : 0 <= S[10,17]-S[9,16] + test1[16];
F_iii_9_17_1 : -1 <=  + S[22,18]-S[9,17]-test1[17];
F_iii_9_17_2 : 0 <= S[10,18]-S[9,17] + test1[17];
F_iii_9_18_1 : -1 <=  + S[22,19]-S[9,18]-test1[18];
F_iii_9_18_2 : 0 <= S[10,19]-S[9,18] + test1[18];
F_iii_9_19_1 : -1 <=  + S[22,20]-S[9,19]-test1[19];
F_iii_9_19_2 : 0 <= S[10,20]-S[9,19] + test1[19];
F_iii_9_20_1 : -1 <=  + S[22,21]-S[9,20]-test1[20];
F_iii_9_20_2 : 0 <= S[10,21]-S[9,20] + test1[20];
F_iii_9_21_1 : -1 <=  + S[22,22]-S[9,21]-test1[21];
F_iii_9_21_2 : 0 <= S[10,22]-S[9,21] + test1[21];
F_iii_9_22_1 : -1 <=  + S[22,23]-S[9,22]-test1[22];
F_iii_9_22_2 : 0 <= S[10,23]-S[9,22] + test1[22];
F_iii_9_23_1 : -1 <=  + S[22,24]-S[9,23]-test1[23];
F_iii_9_23_2 : 0 <= S[10,24]-S[9,23] + test1[23];
F_iii_9_24_1 : -1 <=  + S[22,25]-S[9,24]-test1[24];
F_iii_9_24_2 : 0 <= S[10,25]-S[9,24] + test1[24];
F_iii_9_25_1 : -1 <=  + S[22,26]-S[9,25]-test1[25];
F_iii_9_25_2 : 0 <= S[10,26]-S[9,25] + test1[25];
F_iii_9_26_1 : -1 <=  + S[22,27]-S[9,26]-test1[26];
F_iii_9_26_2 : 0 <= S[10,27]-S[9,26] + test1[26];
F_iii_9_27_1 : -1 <=  + S[22,28]-S[9,27]-test1[27];
F_iii_9_27_2 : 0 <= S[10,28]-S[9,27] + test1[27];
F_iii_9_28_1 : -1 <=  + S[22,29]-S[9,28]-test1[28];
F_iii_9_28_2 : 0 <= S[10,29]-S[9,28] + test1[28];
F_iii_9_29_1 : -1 <=  + S[22,30]-S[9,29]-test1[29];
F_iii_9_29_2 : 0 <= S[10,30]-S[9,29] + test1[29];
F_iii_9_30_1 : -1 <=  + S[22,31]-S[9,30]-test1[30];
F_iii_9_30_2 : 0 <= S[10,31]-S[9,30] + test1[30];
F_iii_9_31_1 : -1 <=  + S[22,32]-S[9,31]-test1[31];
F_iii_9_31_2 : 0 <= S[10,32]-S[9,31] + test1[31];
F_iii_9_32_1 : -1 <=  + S[22,33]-S[9,32]-test1[32];
F_iii_9_32_2 : 0 <= S[10,33]-S[9,32] + test1[32];
F_iii_9_33_1 : -1 <=  + S[22,34]-S[9,33]-test1[33];
F_iii_9_33_2 : 0 <= S[10,34]-S[9,33] + test1[33];
F_iii_9_34_1 : -1 <=  + S[22,35]-S[9,34]-test1[34];
F_iii_9_34_2 : 0 <= S[10,35]-S[9,34] + test1[34];
F_iii_9_35_1 : -1 <=  + S[22,36]-S[9,35]-test1[35];
F_iii_9_35_2 : 0 <= S[10,36]-S[9,35] + test1[35];
F_iii_9_36_1 : -1 <=  + S[22,37]-S[9,36]-test1[36];
F_iii_9_36_2 : 0 <= S[10,37]-S[9,36] + test1[36];
F_iii_9_37_1 : -1 <=  + S[22,38]-S[9,37]-test1[37];
F_iii_9_37_2 : 0 <= S[10,38]-S[9,37] + test1[37];
F_iii_9_38_1 : -1 <=  + S[22,39]-S[9,38]-test1[38];
F_iii_9_38_2 : 0 <= S[10,39]-S[9,38] + test1[38];
F_iii_9_39_1 : -1 <=  + S[22,40]-S[9,39]-test1[39];
F_iii_9_39_2 : 0 <= S[10,40]-S[9,39] + test1[39];
F_iii_9_40_1 : -1 <=  + S[22,41]-S[9,40]-test1[40];
F_iii_9_40_2 : 0 <= S[10,41]-S[9,40] + test1[40];
F_iii_9_41_1 : -1 <=  + S[22,42]-S[9,41]-test1[41];
F_iii_9_41_2 : 0 <= S[10,42]-S[9,41] + test1[41];
F_iii_9_42_1 : -1 <=  + S[22,43]-S[9,42]-test1[42];
F_iii_9_42_2 : 0 <= S[10,43]-S[9,42] + test1[42];
F_iii_9_43_1 : -1 <=  + S[22,44]-S[9,43]-test1[43];
F_iii_9_43_2 : 0 <= S[10,44]-S[9,43] + test1[43];
F_iii_9_44_1 : -1 <=  + S[22,45]-S[9,44]-test1[44];
F_iii_9_44_2 : 0 <= S[10,45]-S[9,44] + test1[44];
F_iii_9_45_1 : -1 <=  + S[22,46]-S[9,45]-test1[45];
F_iii_9_45_2 : 0 <= S[10,46]-S[9,45] + test1[45];
F_iii_9_46_1 : -1 <=  + S[22,47]-S[9,46]-test1[46];
F_iii_9_46_2 : 0 <= S[10,47]-S[9,46] + test1[46];
F_iii_9_47_1 : -1 <=  + S[22,48]-S[9,47]-test1[47];
F_iii_9_47_2 : 0 <= S[10,48]-S[9,47] + test1[47];
F_iii_9_48_1 : -1 <=  + S[22,49]-S[9,48]-test1[48];
F_iii_9_48_2 : 0 <= S[10,49]-S[9,48] + test1[48];
F_iii_9_49_1 : -1 <=  + S[22,50]-S[9,49]-test1[49];
F_iii_9_49_2 : 0 <= S[10,50]-S[9,49] + test1[49];
F_iii_9_50_1 : -1 <=  + S[22,51]-S[9,50]-test1[50];
F_iii_9_50_2 : 0 <= S[10,51]-S[9,50] + test1[50];
F_iii_9_51_1 : -1 <=  + S[22,52]-S[9,51]-test1[51];
F_iii_9_51_2 : 0 <= S[10,52]-S[9,51] + test1[51];
F_iii_9_52_1 : -1 <=  + S[22,53]-S[9,52]-test1[52];
F_iii_9_52_2 : 0 <= S[10,53]-S[9,52] + test1[52];
F_iii_9_53_1 : -1 <=  + S[22,54]-S[9,53]-test1[53];
F_iii_9_53_2 : 0 <= S[10,54]-S[9,53] + test1[53];
F_iii_9_54_1 : -1 <=  + S[22,55]-S[9,54]-test1[54];
F_iii_9_54_2 : 0 <= S[10,55]-S[9,54] + test1[54];
F_iii_9_55_1 : -1 <=  + S[22,56]-S[9,55]-test1[55];
F_iii_9_55_2 : 0 <= S[10,56]-S[9,55] + test1[55];
F_iii_9_56_1 : -1 <=  + S[22,57]-S[9,56]-test1[56];
F_iii_9_56_2 : 0 <= S[10,57]-S[9,56] + test1[56];
F_iii_9_57_1 : -1 <=  + S[22,58]-S[9,57]-test1[57];
F_iii_9_57_2 : 0 <= S[10,58]-S[9,57] + test1[57];
F_iii_9_58_1 : -1 <=  + S[22,59]-S[9,58]-test1[58];
F_iii_9_58_2 : 0 <= S[10,59]-S[9,58] + test1[58];
F_iii_9_59_1 : -1 <=  + S[22,60]-S[9,59]-test1[59];
F_iii_9_59_2 : 0 <= S[10,60]-S[9,59] + test1[59];
F_o_10_1 : 0 <= -S[10,1] + S[11,2];
F_o_10_2 : 0 <= -S[10,2] + S[11,3];
F_o_10_3 : 0 <= -S[10,3] + S[11,4];
F_o_10_4 : 0 <= -S[10,4] + S[11,5];
F_o_10_5 : 0 <= -S[10,5] + S[11,6];
F_o_10_6 : 0 <= -S[10,6] + S[11,7];
F_o_10_7 : 0 <= -S[10,7] + S[11,8];
F_o_10_8 : 0 <= -S[10,8] + S[11,9];
F_o_10_9 : 0 <= -S[10,9] + S[11,10];
F_o_10_10 : 0 <= -S[10,10] + S[11,11];
F_o_10_11 : 0 <= -S[10,11] + S[11,12];
F_o_10_12 : 0 <= -S[10,12] + S[11,13];
F_o_10_13 : 0 <= -S[10,13] + S[11,14];
F_o_10_14 : 0 <= -S[10,14] + S[11,15];
F_o_10_15 : 0 <= -S[10,15] + S[11,16];
F_o_10_16 : 0 <= -S[10,16] + S[11,17];
F_o_10_17 : 0 <= -S[10,17] + S[11,18];
F_o_10_18 : 0 <= -S[10,18] + S[11,19];
F_o_10_19 : 0 <= -S[10,19] + S[11,20];
F_o_10_20 : 0 <= -S[10,20] + S[11,21];
F_o_10_21 : 0 <= -S[10,21] + S[11,22];
F_o_10_22 : 0 <= -S[10,22] + S[11,23];
F_o_10_23 : 0 <= -S[10,23] + S[11,24];
F_o_10_24 : 0 <= -S[10,24] + S[11,25];
F_o_10_25 : 0 <= -S[10,25] + S[11,26];
F_o_10_26 : 0 <= -S[10,26] + S[11,27];
F_o_10_27 : 0 <= -S[10,27] + S[11,28];
F_o_10_28 : 0 <= -S[10,28] + S[11,29];
F_o_10_29 : 0 <= -S[10,29] + S[11,30];
F_o_10_30 : 0 <= -S[10,30] + S[11,31];
F_o_10_31 : 0 <= -S[10,31] + S[11,32];
F_o_10_32 : 0 <= -S[10,32] + S[11,33];
F_o_10_33 : 0 <= -S[10,33] + S[11,34];
F_o_10_34 : 0 <= -S[10,34] + S[11,35];
F_o_10_35 : 0 <= -S[10,35] + S[11,36];
F_o_10_36 : 0 <= -S[10,36] + S[11,37];
F_o_10_37 : 0 <= -S[10,37] + S[11,38];
F_o_10_38 : 0 <= -S[10,38] + S[11,39];
F_o_10_39 : 0 <= -S[10,39] + S[11,40];
F_o_10_40 : 0 <= -S[10,40] + S[11,41];
F_o_10_41 : 0 <= -S[10,41] + S[11,42];
F_o_10_42 : 0 <= -S[10,42] + S[11,43];
F_o_10_43 : 0 <= -S[10,43] + S[11,44];
F_o_10_44 : 0 <= -S[10,44] + S[11,45];
F_o_10_45 : 0 <= -S[10,45] + S[11,46];
F_o_10_46 : 0 <= -S[10,46] + S[11,47];
F_o_10_47 : 0 <= -S[10,47] + S[11,48];
F_o_10_48 : 0 <= -S[10,48] + S[11,49];
F_o_10_49 : 0 <= -S[10,49] + S[11,50];
F_o_10_50 : 0 <= -S[10,50] + S[11,51];
F_o_10_51 : 0 <= -S[10,51] + S[11,52];
F_o_10_52 : 0 <= -S[10,52] + S[11,53];
F_o_10_53 : 0 <= -S[10,53] + S[11,54];
F_o_10_54 : 0 <= -S[10,54] + S[11,55];
F_o_10_55 : 0 <= -S[10,55] + S[11,56];
F_o_10_56 : 0 <= -S[10,56] + S[11,57];
F_o_10_57 : 0 <= -S[10,57] + S[11,58];
F_o_10_58 : 0 <= -S[10,58] + S[11,59];
F_o_10_59 : 0 <= -S[10,59] + S[11,60];
F_o_11_1 : 0 <= -S[11,1] + S[12,2];
F_o_11_2 : 0 <= -S[11,2] + S[12,3];
F_o_11_3 : 0 <= -S[11,3] + S[12,4];
F_o_11_4 : 0 <= -S[11,4] + S[12,5];
F_o_11_5 : 0 <= -S[11,5] + S[12,6];
F_o_11_6 : 0 <= -S[11,6] + S[12,7];
F_o_11_7 : 0 <= -S[11,7] + S[12,8];
F_o_11_8 : 0 <= -S[11,8] + S[12,9];
F_o_11_9 : 0 <= -S[11,9] + S[12,10];
F_o_11_10 : 0 <= -S[11,10] + S[12,11];
F_o_11_11 : 0 <= -S[11,11] + S[12,12];
F_o_11_12 : 0 <= -S[11,12] + S[12,13];
F_o_11_13 : 0 <= -S[11,13] + S[12,14];
F_o_11_14 : 0 <= -S[11,14] + S[12,15];
F_o_11_15 : 0 <= -S[11,15] + S[12,16];
F_o_11_16 : 0 <= -S[11,16] + S[12,17];
F_o_11_17 : 0 <= -S[11,17] + S[12,18];
F_o_11_18 : 0 <= -S[11,18] + S[12,19];
F_o_11_19 : 0 <= -S[11,19] + S[12,20];
F_o_11_20 : 0 <= -S[11,20] + S[12,21];
F_o_11_21 : 0 <= -S[11,21] + S[12,22];
F_o_11_22 : 0 <= -S[11,22] + S[12,23];
F_o_11_23 : 0 <= -S[11,23] + S[12,24];
F_o_11_24 : 0 <= -S[11,24] + S[12,25];
F_o_11_25 : 0 <= -S[11,25] + S[12,26];
F_o_11_26 : 0 <= -S[11,26] + S[12,27];
F_o_11_27 : 0 <= -S[11,27] + S[12,28];
F_o_11_28 : 0 <= -S[11,28] + S[12,29];
F_o_11_29 : 0 <= -S[11,29] + S[12,30];
F_o_11_30 : 0 <= -S[11,30] + S[12,31];
F_o_11_31 : 0 <= -S[11,31] + S[12,32];
F_o_11_32 : 0 <= -S[11,32] + S[12,33];
F_o_11_33 : 0 <= -S[11,33] + S[12,34];
F_o_11_34 : 0 <= -S[11,34] + S[12,35];
F_o_11_35 : 0 <= -S[11,35] + S[12,36];
F_o_11_36 : 0 <= -S[11,36] + S[12,37];
F_o_11_37 : 0 <= -S[11,37] + S[12,38];
F_o_11_38 : 0 <= -S[11,38] + S[12,39];
F_o_11_39 : 0 <= -S[11,39] + S[12,40];
F_o_11_40 : 0 <= -S[11,40] + S[12,41];
F_o_11_41 : 0 <= -S[11,41] + S[12,42];
F_o_11_42 : 0 <= -S[11,42] + S[12,43];
F_o_11_43 : 0 <= -S[11,43] + S[12,44];
F_o_11_44 : 0 <= -S[11,44] + S[12,45];
F_o_11_45 : 0 <= -S[11,45] + S[12,46];
F_o_11_46 : 0 <= -S[11,46] + S[12,47];
F_o_11_47 : 0 <= -S[11,47] + S[12,48];
F_o_11_48 : 0 <= -S[11,48] + S[12,49];
F_o_11_49 : 0 <= -S[11,49] + S[12,50];
F_o_11_50 : 0 <= -S[11,50] + S[12,51];
F_o_11_51 : 0 <= -S[11,51] + S[12,52];
F_o_11_52 : 0 <= -S[11,52] + S[12,53];
F_o_11_53 : 0 <= -S[11,53] + S[12,54];
F_o_11_54 : 0 <= -S[11,54] + S[12,55];
F_o_11_55 : 0 <= -S[11,55] + S[12,56];
F_o_11_56 : 0 <= -S[11,56] + S[12,57];
F_o_11_57 : 0 <= -S[11,57] + S[12,58];
F_o_11_58 : 0 <= -S[11,58] + S[12,59];
F_o_11_59 : 0 <= -S[11,59] + S[12,60];
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_12_24 : 0 <= -S[12,24] + S[13,25];
F_o_12_25 : 0 <= -S[12,25] + S[13,26];
F_o_12_26 : 0 <= -S[12,26] + S[13,27];
F_o_12_27 : 0 <= -S[12,27] + S[13,28];
F_o_12_28 : 0 <= -S[12,28] + S[13,29];
F_o_12_29 : 0 <= -S[12,29] + S[13,30];
F_o_12_30 : 0 <= -S[12,30] + S[13,31];
F_o_12_31 : 0 <= -S[12,31] + S[13,32];
F_o_12_32 : 0 <= -S[12,32] + S[13,33];
F_o_12_33 : 0 <= -S[12,33] + S[13,34];
F_o_12_34 : 0 <= -S[12,34] + S[13,35];
F_o_12_35 : 0 <= -S[12,35] + S[13,36];
F_o_12_36 : 0 <= -S[12,36] + S[13,37];
F_o_12_37 : 0 <= -S[12,37] + S[13,38];
F_o_12_38 : 0 <= -S[12,38] + S[13,39];
F_o_12_39 : 0 <= -S[12,39] + S[13,40];
F_o_12_40 : 0 <= -S[12,40] + S[13,41];
F_o_12_41 : 0 <= -S[12,41] + S[13,42];
F_o_12_42 : 0 <= -S[12,42] + S[13,43];
F_o_12_43 : 0 <= -S[12,43] + S[13,44];
F_o_12_44 : 0 <= -S[12,44] + S[13,45];
F_o_12_45 : 0 <= -S[12,45] + S[13,46];
F_o_12_46 : 0 <= -S[12,46] + S[13,47];
F_o_12_47 : 0 <= -S[12,47] + S[13,48];
F_o_12_48 : 0 <= -S[12,48] + S[13,49];
F_o_12_49 : 0 <= -S[12,49] + S[13,50];
F_o_12_50 : 0 <= -S[12,50] + S[13,51];
F_o_12_51 : 0 <= -S[12,51] + S[13,52];
F_o_12_52 : 0 <= -S[12,52] + S[13,53];
F_o_12_53 : 0 <= -S[12,53] + S[13,54];
F_o_12_54 : 0 <= -S[12,54] + S[13,55];
F_o_12_55 : 0 <= -S[12,55] + S[13,56];
F_o_12_56 : 0 <= -S[12,56] + S[13,57];
F_o_12_57 : 0 <= -S[12,57] + S[13,58];
F_o_12_58 : 0 <= -S[12,58] + S[13,59];
F_o_12_59 : 0 <= -S[12,59] + S[13,60];
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_13_24 : 0 <= -S[13,24] + S[14,25];
F_o_13_25 : 0 <= -S[13,25] + S[14,26];
F_o_13_26 : 0 <= -S[13,26] + S[14,27];
F_o_13_27 : 0 <= -S[13,27] + S[14,28];
F_o_13_28 : 0 <= -S[13,28] + S[14,29];
F_o_13_29 : 0 <= -S[13,29] + S[14,30];
F_o_13_30 : 0 <= -S[13,30] + S[14,31];
F_o_13_31 : 0 <= -S[13,31] + S[14,32];
F_o_13_32 : 0 <= -S[13,32] + S[14,33];
F_o_13_33 : 0 <= -S[13,33] + S[14,34];
F_o_13_34 : 0 <= -S[13,34] + S[14,35];
F_o_13_35 : 0 <= -S[13,35] + S[14,36];
F_o_13_36 : 0 <= -S[13,36] + S[14,37];
F_o_13_37 : 0 <= -S[13,37] + S[14,38];
F_o_13_38 : 0 <= -S[13,38] + S[14,39];
F_o_13_39 : 0 <= -S[13,39] + S[14,40];
F_o_13_40 : 0 <= -S[13,40] + S[14,41];
F_o_13_41 : 0 <= -S[13,41] + S[14,42];
F_o_13_42 : 0 <= -S[13,42] + S[14,43];
F_o_13_43 : 0 <= -S[13,43] + S[14,44];
F_o_13_44 : 0 <= -S[13,44] + S[14,45];
F_o_13_45 : 0 <= -S[13,45] + S[14,46];
F_o_13_46 : 0 <= -S[13,46] + S[14,47];
F_o_13_47 : 0 <= -S[13,47] + S[14,48];
F_o_13_48 : 0 <= -S[13,48] + S[14,49];
F_o_13_49 : 0 <= -S[13,49] + S[14,50];
F_o_13_50 : 0 <= -S[13,50] + S[14,51];
F_o_13_51 : 0 <= -S[13,51] + S[14,52];
F_o_13_52 : 0 <= -S[13,52] + S[14,53];
F_o_13_53 : 0 <= -S[13,53] + S[14,54];
F_o_13_54 : 0 <= -S[13,54] + S[14,55];
F_o_13_55 : 0 <= -S[13,55] + S[14,56];
F_o_13_56 : 0 <= -S[13,56] + S[14,57];
F_o_13_57 : 0 <= -S[13,57] + S[14,58];
F_o_13_58 : 0 <= -S[13,58] + S[14,59];
F_o_13_59 : 0 <= -S[13,59] + S[14,60];
F_iii_14_1_1 : -1 <= -S[14,1] + S[19,2]-test2[1];
F_iii_14_1_2 : 0 <= -S[14,1] + S[15,2] + test2[1];
F_iii_14_2_1 : -1 <= -S[14,2] + S[19,3]-test2[2];
F_iii_14_2_2 : 0 <= -S[14,2] + S[15,3] + test2[2];
F_iii_14_3_1 : -1 <= -S[14,3] + S[19,4]-test2[3];
F_iii_14_3_2 : 0 <= -S[14,3] + S[15,4] + test2[3];
F_iii_14_4_1 : -1 <= -S[14,4] + S[19,5]-test2[4];
F_iii_14_4_2 : 0 <= -S[14,4] + S[15,5] + test2[4];
F_iii_14_5_1 : -1 <= -S[14,5] + S[19,6]-test2[5];
F_iii_14_5_2 : 0 <= -S[14,5] + S[15,6] + test2[5];
F_iii_14_6_1 : -1 <= -S[14,6] + S[19,7]-test2[6];
F_iii_14_6_2 : 0 <= -S[14,6] + S[15,7] + test2[6];
F_iii_14_7_1 : -1 <= -S[14,7] + S[19,8]-test2[7];
F_iii_14_7_2 : 0 <= -S[14,7] + S[15,8] + test2[7];
F_iii_14_8_1 : -1 <= -S[14,8] + S[19,9]-test2[8];
F_iii_14_8_2 : 0 <= -S[14,8] + S[15,9] + test2[8];
F_iii_14_9_1 : -1 <= -S[14,9] + S[19,10]-test2[9];
F_iii_14_9_2 : 0 <= -S[14,9] + S[15,10] + test2[9];
F_iii_14_10_1 : -1 <= -S[14,10] + S[19,11]-test2[10];
F_iii_14_10_2 : 0 <= -S[14,10] + S[15,11] + test2[10];
F_iii_14_11_1 : -1 <= -S[14,11] + S[19,12]-test2[11];
F_iii_14_11_2 : 0 <= -S[14,11] + S[15,12] + test2[11];
F_iii_14_12_1 : -1 <= -S[14,12] + S[19,13]-test2[12];
F_iii_14_12_2 : 0 <= -S[14,12] + S[15,13] + test2[12];
F_iii_14_13_1 : -1 <= -S[14,13] + S[19,14]-test2[13];
F_iii_14_13_2 : 0 <= -S[14,13] + S[15,14] + test2[13];
F_iii_14_14_1 : -1 <= -S[14,14] + S[19,15]-test2[14];
F_iii_14_14_2 : 0 <= -S[14,14] + S[15,15] + test2[14];
F_iii_14_15_1 : -1 <= -S[14,15] + S[19,16]-test2[15];
F_iii_14_15_2 : 0 <= -S[14,15] + S[15,16] + test2[15];
F_iii_14_16_1 : -1 <= -S[14,16] + S[19,17]-test2[16];
F_iii_14_16_2 : 0 <= -S[14,16] + S[15,17] + test2[16];
F_iii_14_17_1 : -1 <= -S[14,17] + S[19,18]-test2[17];
F_iii_14_17_2 : 0 <= -S[14,17] + S[15,18] + test2[17];
F_iii_14_18_1 : -1 <= -S[14,18] + S[19,19]-test2[18];
F_iii_14_18_2 : 0 <= -S[14,18] + S[15,19] + test2[18];
F_iii_14_19_1 : -1 <= -S[14,19] + S[19,20]-test2[19];
F_iii_14_19_2 : 0 <= -S[14,19] + S[15,20] + test2[19];
F_iii_14_20_1 : -1 <= -S[14,20] + S[19,21]-test2[20];
F_iii_14_20_2 : 0 <= -S[14,20] + S[15,21] + test2[20];
F_iii_14_21_1 : -1 <= -S[14,21] + S[19,22]-test2[21];
F_iii_14_21_2 : 0 <= -S[14,21] + S[15,22] + test2[21];
F_iii_14_22_1 : -1 <= -S[14,22] + S[19,23]-test2[22];
F_iii_14_22_2 : 0 <= -S[14,22] + S[15,23] + test2[22];
F_iii_14_23_1 : -1 <= -S[14,23] + S[19,24]-test2[23];
F_iii_14_23_2 : 0 <= -S[14,23] + S[15,24] + test2[23];
F_iii_14_24_1 : -1 <= -S[14,24] + S[19,25]-test2[24];
F_iii_14_24_2 : 0 <= -S[14,24] + S[15,25] + test2[24];
F_iii_14_25_1 : -1 <= -S[14,25] + S[19,26]-test2[25];
F_iii_14_25_2 : 0 <= -S[14,25] + S[15,26] + test2[25];
F_iii_14_26_1 : -1 <= -S[14,26] + S[19,27]-test2[26];
F_iii_14_26_2 : 0 <= -S[14,26] + S[15,27] + test2[26];
F_iii_14_27_1 : -1 <= -S[14,27] + S[19,28]-test2[27];
F_iii_14_27_2 : 0 <= -S[14,27] + S[15,28] + test2[27];
F_iii_14_28_1 : -1 <= -S[14,28] + S[19,29]-test2[28];
F_iii_14_28_2 : 0 <= -S[14,28] + S[15,29] + test2[28];
F_iii_14_29_1 : -1 <= -S[14,29] + S[19,30]-test2[29];
F_iii_14_29_2 : 0 <= -S[14,29] + S[15,30] + test2[29];
F_iii_14_30_1 : -1 <= -S[14,30] + S[19,31]-test2[30];
F_iii_14_30_2 : 0 <= -S[14,30] + S[15,31] + test2[30];
F_iii_14_31_1 : -1 <= -S[14,31] + S[19,32]-test2[31];
F_iii_14_31_2 : 0 <= -S[14,31] + S[15,32] + test2[31];
F_iii_14_32_1 : -1 <= -S[14,32] + S[19,33]-test2[32];
F_iii_14_32_2 : 0 <= -S[14,32] + S[15,33] + test2[32];
F_iii_14_33_1 : -1 <= -S[14,33] + S[19,34]-test2[33];
F_iii_14_33_2 : 0 <= -S[14,33] + S[15,34] + test2[33];
F_iii_14_34_1 : -1 <= -S[14,34] + S[19,35]-test2[34];
F_iii_14_34_2 : 0 <= -S[14,34] + S[15,35] + test2[34];
F_iii_14_35_1 : -1 <= -S[14,35] + S[19,36]-test2[35];
F_iii_14_35_2 : 0 <= -S[14,35] + S[15,36] + test2[35];
F_iii_14_36_1 : -1 <= -S[14,36] + S[19,37]-test2[36];
F_iii_14_36_2 : 0 <= -S[14,36] + S[15,37] + test2[36];
F_iii_14_37_1 : -1 <= -S[14,37] + S[19,38]-test2[37];
F_iii_14_37_2 : 0 <= -S[14,37] + S[15,38] + test2[37];
F_iii_14_38_1 : -1 <= -S[14,38] + S[19,39]-test2[38];
F_iii_14_38_2 : 0 <= -S[14,38] + S[15,39] + test2[38];
F_iii_14_39_1 : -1 <= -S[14,39] + S[19,40]-test2[39];
F_iii_14_39_2 : 0 <= -S[14,39] + S[15,40] + test2[39];
F_iii_14_40_1 : -1 <= -S[14,40] + S[19,41]-test2[40];
F_iii_14_40_2 : 0 <= -S[14,40] + S[15,41] + test2[40];
F_iii_14_41_1 : -1 <= -S[14,41] + S[19,42]-test2[41];
F_iii_14_41_2 : 0 <= -S[14,41] + S[15,42] + test2[41];
F_iii_14_42_1 : -1 <= -S[14,42] + S[19,43]-test2[42];
F_iii_14_42_2 : 0 <= -S[14,42] + S[15,43] + test2[42];
F_iii_14_43_1 : -1 <= -S[14,43] + S[19,44]-test2[43];
F_iii_14_43_2 : 0 <= -S[14,43] + S[15,44] + test2[43];
F_iii_14_44_1 : -1 <= -S[14,44] + S[19,45]-test2[44];
F_iii_14_44_2 : 0 <= -S[14,44] + S[15,45] + test2[44];
F_iii_14_45_1 : -1 <= -S[14,45] + S[19,46]-test2[45];
F_iii_14_45_2 : 0 <= -S[14,45] + S[15,46] + test2[45];
F_iii_14_46_1 : -1 <= -S[14,46] + S[19,47]-test2[46];
F_iii_14_46_2 : 0 <= -S[14,46] + S[15,47] + test2[46];
F_iii_14_47_1 : -1 <= -S[14,47] + S[19,48]-test2[47];
F_iii_14_47_2 : 0 <= -S[14,47] + S[15,48] + test2[47];
F_iii_14_48_1 : -1 <= -S[14,48] + S[19,49]-test2[48];
F_iii_14_48_2 : 0 <= -S[14,48] + S[15,49] + test2[48];
F_iii_14_49_1 : -1 <= -S[14,49] + S[19,50]-test2[49];
F_iii_14_49_2 : 0 <= -S[14,49] + S[15,50] + test2[49];
F_iii_14_50_1 : -1 <= -S[14,50] + S[19,51]-test2[50];
F_iii_14_50_2 : 0 <= -S[14,50] + S[15,51] + test2[50];
F_iii_14_51_1 : -1 <= -S[14,51] + S[19,52]-test2[51];
F_iii_14_51_2 : 0 <= -S[14,51] + S[15,52] + test2[51];
F_iii_14_52_1 : -1 <= -S[14,52] + S[19,53]-test2[52];
F_iii_14_52_2 : 0 <= -S[14,52] + S[15,53] + test2[52];
F_iii_14_53_1 : -1 <= -S[14,53] + S[19,54]-test2[53];
F_iii_14_53_2 : 0 <= -S[14,53] + S[15,54] + test2[53];
F_iii_14_54_1 : -1 <= -S[14,54] + S[19,55]-test2[54];
F_iii_14_54_2 : 0 <= -S[14,54] + S[15,55] + test2[54];
F_iii_14_55_1 : -1 <= -S[14,55] + S[19,56]-test2[55];
F_iii_14_55_2 : 0 <= -S[14,55] + S[15,56] + test2[55];
F_iii_14_56_1 : -1 <= -S[14,56] + S[19,57]-test2[56];
F_iii_14_56_2 : 0 <= -S[14,56] + S[15,57] + test2[56];
F_iii_14_57_1 : -1 <= -S[14,57] + S[19,58]-test2[57];
F_iii_14_57_2 : 0 <= -S[14,57] + S[15,58] + test2[57];
F_iii_14_58_1 : -1 <= -S[14,58] + S[19,59]-test2[58];
F_iii_14_58_2 : 0 <= -S[14,58] + S[15,59] + test2[58];
F_iii_14_59_1 : -1 <= -S[14,59] + S[19,60]-test2[59];
F_iii_14_59_2 : 0 <= -S[14,59] + S[15,60] + test2[59];
F_o_15_1 : 0 <= -S[15,1] + S[16,2];
F_o_15_2 : 0 <= -S[15,2] + S[16,3];
F_o_15_3 : 0 <= -S[15,3] + S[16,4];
F_o_15_4 : 0 <= -S[15,4] + S[16,5];
F_o_15_5 : 0 <= -S[15,5] + S[16,6];
F_o_15_6 : 0 <= -S[15,6] + S[16,7];
F_o_15_7 : 0 <= -S[15,7] + S[16,8];
F_o_15_8 : 0 <= -S[15,8] + S[16,9];
F_o_15_9 : 0 <= -S[15,9] + S[16,10];
F_o_15_10 : 0 <= -S[15,10] + S[16,11];
F_o_15_11 : 0 <= -S[15,11] + S[16,12];
F_o_15_12 : 0 <= -S[15,12] + S[16,13];
F_o_15_13 : 0 <= -S[15,13] + S[16,14];
F_o_15_14 : 0 <= -S[15,14] + S[16,15];
F_o_15_15 : 0 <= -S[15,15] + S[16,16];
F_o_15_16 : 0 <= -S[15,16] + S[16,17];
F_o_15_17 : 0 <= -S[15,17] + S[16,18];
F_o_15_18 : 0 <= -S[15,18] + S[16,19];
F_o_15_19 : 0 <= -S[15,19] + S[16,20];
F_o_15_20 : 0 <= -S[15,20] + S[16,21];
F_o_15_21 : 0 <= -S[15,21] + S[16,22];
F_o_15_22 : 0 <= -S[15,22] + S[16,23];
F_o_15_23 : 0 <= -S[15,23] + S[16,24];
F_o_15_24 : 0 <= -S[15,24] + S[16,25];
F_o_15_25 : 0 <= -S[15,25] + S[16,26];
F_o_15_26 : 0 <= -S[15,26] + S[16,27];
F_o_15_27 : 0 <= -S[15,27] + S[16,28];
F_o_15_28 : 0 <= -S[15,28] + S[16,29];
F_o_15_29 : 0 <= -S[15,29] + S[16,30];
F_o_15_30 : 0 <= -S[15,30] + S[16,31];
F_o_15_31 : 0 <= -S[15,31] + S[16,32];
F_o_15_32 : 0 <= -S[15,32] + S[16,33];
F_o_15_33 : 0 <= -S[15,33] + S[16,34];
F_o_15_34 : 0 <= -S[15,34] + S[16,35];
F_o_15_35 : 0 <= -S[15,35] + S[16,36];
F_o_15_36 : 0 <= -S[15,36] + S[16,37];
F_o_15_37 : 0 <= -S[15,37] + S[16,38];
F_o_15_38 : 0 <= -S[15,38] + S[16,39];
F_o_15_39 : 0 <= -S[15,39] + S[16,40];
F_o_15_40 : 0 <= -S[15,40] + S[16,41];
F_o_15_41 : 0 <= -S[15,41] + S[16,42];
F_o_15_42 : 0 <= -S[15,42] + S[16,43];
F_o_15_43 : 0 <= -S[15,43] + S[16,44];
F_o_15_44 : 0 <= -S[15,44] + S[16,45];
F_o_15_45 : 0 <= -S[15,45] + S[16,46];
F_o_15_46 : 0 <= -S[15,46] + S[16,47];
F_o_15_47 : 0 <= -S[15,47] + S[16,48];
F_o_15_48 : 0 <= -S[15,48] + S[16,49];
F_o_15_49 : 0 <= -S[15,49] + S[16,50];
F_o_15_50 : 0 <= -S[15,50] + S[16,51];
F_o_15_51 : 0 <= -S[15,51] + S[16,52];
F_o_15_52 : 0 <= -S[15,52] + S[16,53];
F_o_15_53 : 0 <= -S[15,53] + S[16,54];
F_o_15_54 : 0 <= -S[15,54] + S[16,55];
F_o_15_55 : 0 <= -S[15,55] + S[16,56];
F_o_15_56 : 0 <= -S[15,56] + S[16,57];
F_o_15_57 : 0 <= -S[15,57] + S[16,58];
F_o_15_58 : 0 <= -S[15,58] + S[16,59];
F_o_15_59 : 0 <= -S[15,59] + S[16,60];
F_o_16_1 : 0 <= -S[16,1] + S[17,2];
F_o_16_2 : 0 <= -S[16,2] + S[17,3];
F_o_16_3 : 0 <= -S[16,3] + S[17,4];
F_o_16_4 : 0 <= -S[16,4] + S[17,5];
F_o_16_5 : 0 <= -S[16,5] + S[17,6];
F_o_16_6 : 0 <= -S[16,6] + S[17,7];
F_o_16_7 : 0 <= -S[16,7] + S[17,8];
F_o_16_8 : 0 <= -S[16,8] + S[17,9];
F_o_16_9 : 0 <= -S[16,9] + S[17,10];
F_o_16_10 : 0 <= -S[16,10] + S[17,11];
F_o_16_11 : 0 <= -S[16,11] + S[17,12];
F_o_16_12 : 0 <= -S[16,12] + S[17,13];
F_o_16_13 : 0 <= -S[16,13] + S[17,14];
F_o_16_14 : 0 <= -S[16,14] + S[17,15];
F_o_16_15 : 0 <= -S[16,15] + S[17,16];
F_o_16_16 : 0 <= -S[16,16] + S[17,17];
F_o_16_17 : 0 <= -S[16,17] + S[17,18];
F_o_16_18 : 0 <= -S[16,18] + S[17,19];
F_o_16_19 : 0 <= -S[16,19] + S[17,20];
F_o_16_20 : 0 <= -S[16,20] + S[17,21];
F_o_16_21 : 0 <= -S[16,21] + S[17,22];
F_o_16_22 : 0 <= -S[16,22] + S[17,23];
F_o_16_23 : 0 <= -S[16,23] + S[17,24];
F_o_16_24 : 0 <= -S[16,24] + S[17,25];
F_o_16_25 : 0 <= -S[16,25] + S[17,26];
F_o_16_26 : 0 <= -S[16,26] + S[17,27];
F_o_16_27 : 0 <= -S[16,27] + S[17,28];
F_o_16_28 : 0 <= -S[16,28] + S[17,29];
F_o_16_29 : 0 <= -S[16,29] + S[17,30];
F_o_16_30 : 0 <= -S[16,30] + S[17,31];
F_o_16_31 : 0 <= -S[16,31] + S[17,32];
F_o_16_32 : 0 <= -S[16,32] + S[17,33];
F_o_16_33 : 0 <= -S[16,33] + S[17,34];
F_o_16_34 : 0 <= -S[16,34] + S[17,35];
F_o_16_35 : 0 <= -S[16,35] + S[17,36];
F_o_16_36 : 0 <= -S[16,36] + S[17,37];
F_o_16_37 : 0 <= -S[16,37] + S[17,38];
F_o_16_38 : 0 <= -S[16,38] + S[17,39];
F_o_16_39 : 0 <= -S[16,39] + S[17,40];
F_o_16_40 : 0 <= -S[16,40] + S[17,41];
F_o_16_41 : 0 <= -S[16,41] + S[17,42];
F_o_16_42 : 0 <= -S[16,42] + S[17,43];
F_o_16_43 : 0 <= -S[16,43] + S[17,44];
F_o_16_44 : 0 <= -S[16,44] + S[17,45];
F_o_16_45 : 0 <= -S[16,45] + S[17,46];
F_o_16_46 : 0 <= -S[16,46] + S[17,47];
F_o_16_47 : 0 <= -S[16,47] + S[17,48];
F_o_16_48 : 0 <= -S[16,48] + S[17,49];
F_o_16_49 : 0 <= -S[16,49] + S[17,50];
F_o_16_50 : 0 <= -S[16,50] + S[17,51];
F_o_16_51 : 0 <= -S[16,51] + S[17,52];
F_o_16_52 : 0 <= -S[16,52] + S[17,53];
F_o_16_53 : 0 <= -S[16,53] + S[17,54];
F_o_16_54 : 0 <= -S[16,54] + S[17,55];
F_o_16_55 : 0 <= -S[16,55] + S[17,56];
F_o_16_56 : 0 <= -S[16,56] + S[17,57];
F_o_16_57 : 0 <= -S[16,57] + S[17,58];
F_o_16_58 : 0 <= -S[16,58] + S[17,59];
F_o_16_59 : 0 <= -S[16,59] + S[17,60];
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_17_24 : 0 <= -S[17,24] + S[18,25];
F_o_17_25 : 0 <= -S[17,25] + S[18,26];
F_o_17_26 : 0 <= -S[17,26] + S[18,27];
F_o_17_27 : 0 <= -S[17,27] + S[18,28];
F_o_17_28 : 0 <= -S[17,28] + S[18,29];
F_o_17_29 : 0 <= -S[17,29] + S[18,30];
F_o_17_30 : 0 <= -S[17,30] + S[18,31];
F_o_17_31 : 0 <= -S[17,31] + S[18,32];
F_o_17_32 : 0 <= -S[17,32] + S[18,33];
F_o_17_33 : 0 <= -S[17,33] + S[18,34];
F_o_17_34 : 0 <= -S[17,34] + S[18,35];
F_o_17_35 : 0 <= -S[17,35] + S[18,36];
F_o_17_36 : 0 <= -S[17,36] + S[18,37];
F_o_17_37 : 0 <= -S[17,37] + S[18,38];
F_o_17_38 : 0 <= -S[17,38] + S[18,39];
F_o_17_39 : 0 <= -S[17,39] + S[18,40];
F_o_17_40 : 0 <= -S[17,40] + S[18,41];
F_o_17_41 : 0 <= -S[17,41] + S[18,42];
F_o_17_42 : 0 <= -S[17,42] + S[18,43];
F_o_17_43 : 0 <= -S[17,43] + S[18,44];
F_o_17_44 : 0 <= -S[17,44] + S[18,45];
F_o_17_45 : 0 <= -S[17,45] + S[18,46];
F_o_17_46 : 0 <= -S[17,46] + S[18,47];
F_o_17_47 : 0 <= -S[17,47] + S[18,48];
F_o_17_48 : 0 <= -S[17,48] + S[18,49];
F_o_17_49 : 0 <= -S[17,49] + S[18,50];
F_o_17_50 : 0 <= -S[17,50] + S[18,51];
F_o_17_51 : 0 <= -S[17,51] + S[18,52];
F_o_17_52 : 0 <= -S[17,52] + S[18,53];
F_o_17_53 : 0 <= -S[17,53] + S[18,54];
F_o_17_54 : 0 <= -S[17,54] + S[18,55];
F_o_17_55 : 0 <= -S[17,55] + S[18,56];
F_o_17_56 : 0 <= -S[17,56] + S[18,57];
F_o_17_57 : 0 <= -S[17,57] + S[18,58];
F_o_17_58 : 0 <= -S[17,58] + S[18,59];
F_o_17_59 : 0 <= -S[17,59] + S[18,60];
F_o_18_1 : 0 <= S[13,2]-S[18,1];
F_o_18_2 : 0 <= S[13,3]-S[18,2];
F_o_18_3 : 0 <= S[13,4]-S[18,3];
F_o_18_4 : 0 <= S[13,5]-S[18,4];
F_o_18_5 : 0 <= S[13,6]-S[18,5];
F_o_18_6 : 0 <= S[13,7]-S[18,6];
F_o_18_7 : 0 <= S[13,8]-S[18,7];
F_o_18_8 : 0 <= S[13,9]-S[18,8];
F_o_18_9 : 0 <= S[13,10]-S[18,9];
F_o_18_10 : 0 <= S[13,11]-S[18,10];
F_o_18_11 : 0 <= S[13,12]-S[18,11];
F_o_18_12 : 0 <= S[13,13]-S[18,12];
F_o_18_13 : 0 <= S[13,14]-S[18,13];
F_o_18_14 : 0 <= S[13,15]-S[18,14];
F_o_18_15 : 0 <= S[13,16]-S[18,15];
F_o_18_16 : 0 <= S[13,17]-S[18,16];
F_o_18_17 : 0 <= S[13,18]-S[18,17];
F_o_18_18 : 0 <= S[13,19]-S[18,18];
F_o_18_19 : 0 <= S[13,20]-S[18,19];
F_o_18_20 : 0 <= S[13,21]-S[18,20];
F_o_18_21 : 0 <= S[13,22]-S[18,21];
F_o_18_22 : 0 <= S[13,23]-S[18,22];
F_o_18_23 : 0 <= S[13,24]-S[18,23];
F_o_18_24 : 0 <= S[13,25]-S[18,24];
F_o_18_25 : 0 <= S[13,26]-S[18,25];
F_o_18_26 : 0 <= S[13,27]-S[18,26];
F_o_18_27 : 0 <= S[13,28]-S[18,27];
F_o_18_28 : 0 <= S[13,29]-S[18,28];
F_o_18_29 : 0 <= S[13,30]-S[18,29];
F_o_18_30 : 0 <= S[13,31]-S[18,30];
F_o_18_31 : 0 <= S[13,32]-S[18,31];
F_o_18_32 : 0 <= S[13,33]-S[18,32];
F_o_18_33 : 0 <= S[13,34]-S[18,33];
F_o_18_34 : 0 <= S[13,35]-S[18,34];
F_o_18_35 : 0 <= S[13,36]-S[18,35];
F_o_18_36 : 0 <= S[13,37]-S[18,36];
F_o_18_37 : 0 <= S[13,38]-S[18,37];
F_o_18_38 : 0 <= S[13,39]-S[18,38];
F_o_18_39 : 0 <= S[13,40]-S[18,39];
F_o_18_40 : 0 <= S[13,41]-S[18,40];
F_o_18_41 : 0 <= S[13,42]-S[18,41];
F_o_18_42 : 0 <= S[13,43]-S[18,42];
F_o_18_43 : 0 <= S[13,44]-S[18,43];
F_o_18_44 : 0 <= S[13,45]-S[18,44];
F_o_18_45 : 0 <= S[13,46]-S[18,45];
F_o_18_46 : 0 <= S[13,47]-S[18,46];
F_o_18_47 : 0 <= S[13,48]-S[18,47];
F_o_18_48 : 0 <= S[13,49]-S[18,48];
F_o_18_49 : 0 <= S[13,50]-S[18,49];
F_o_18_50 : 0 <= S[13,51]-S[18,50];
F_o_18_51 : 0 <= S[13,52]-S[18,51];
F_o_18_52 : 0 <= S[13,53]-S[18,52];
F_o_18_53 : 0 <= S[13,54]-S[18,53];
F_o_18_54 : 0 <= S[13,55]-S[18,54];
F_o_18_55 : 0 <= S[13,56]-S[18,55];
F_o_18_56 : 0 <= S[13,57]-S[18,56];
F_o_18_57 : 0 <= S[13,58]-S[18,57];
F_o_18_58 : 0 <= S[13,59]-S[18,58];
F_o_18_59 : 0 <= S[13,60]-S[18,59];
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_o_19_24 : 0 <= -S[19,24] + S[20,25];
F_o_19_25 : 0 <= -S[19,25] + S[20,26];
F_o_19_26 : 0 <= -S[19,26] + S[20,27];
F_o_19_27 : 0 <= -S[19,27] + S[20,28];
F_o_19_28 : 0 <= -S[19,28] + S[20,29];
F_o_19_29 : 0 <= -S[19,29] + S[20,30];
F_o_19_30 : 0 <= -S[19,30] + S[20,31];
F_o_19_31 : 0 <= -S[19,31] + S[20,32];
F_o_19_32 : 0 <= -S[19,32] + S[20,33];
F_o_19_33 : 0 <= -S[19,33] + S[20,34];
F_o_19_34 : 0 <= -S[19,34] + S[20,35];
F_o_19_35 : 0 <= -S[19,35] + S[20,36];
F_o_19_36 : 0 <= -S[19,36] + S[20,37];
F_o_19_37 : 0 <= -S[19,37] + S[20,38];
F_o_19_38 : 0 <= -S[19,38] + S[20,39];
F_o_19_39 : 0 <= -S[19,39] + S[20,40];
F_o_19_40 : 0 <= -S[19,40] + S[20,41];
F_o_19_41 : 0 <= -S[19,41] + S[20,42];
F_o_19_42 : 0 <= -S[19,42] + S[20,43];
F_o_19_43 : 0 <= -S[19,43] + S[20,44];
F_o_19_44 : 0 <= -S[19,44] + S[20,45];
F_o_19_45 : 0 <= -S[19,45] + S[20,46];
F_o_19_46 : 0 <= -S[19,46] + S[20,47];
F_o_19_47 : 0 <= -S[19,47] + S[20,48];
F_o_19_48 : 0 <= -S[19,48] + S[20,49];
F_o_19_49 : 0 <= -S[19,49] + S[20,50];
F_o_19_50 : 0 <= -S[19,50] + S[20,51];
F_o_19_51 : 0 <= -S[19,51] + S[20,52];
F_o_19_52 : 0 <= -S[19,52] + S[20,53];
F_o_19_53 : 0 <= -S[19,53] + S[20,54];
F_o_19_54 : 0 <= -S[19,54] + S[20,55];
F_o_19_55 : 0 <= -S[19,55] + S[20,56];
F_o_19_56 : 0 <= -S[19,56] + S[20,57];
F_o_19_57 : 0 <= -S[19,57] + S[20,58];
F_o_19_58 : 0 <= -S[19,58] + S[20,59];
F_o_19_59 : 0 <= -S[19,59] + S[20,60];
F_o_20_1 : 0 <= -S[20,1] + S[21,2];
F_o_20_2 : 0 <= -S[20,2] + S[21,3];
F_o_20_3 : 0 <= -S[20,3] + S[21,4];
F_o_20_4 : 0 <= -S[20,4] + S[21,5];
F_o_20_5 : 0 <= -S[20,5] + S[21,6];
F_o_20_6 : 0 <= -S[20,6] + S[21,7];
F_o_20_7 : 0 <= -S[20,7] + S[21,8];
F_o_20_8 : 0 <= -S[20,8] + S[21,9];
F_o_20_9 : 0 <= -S[20,9] + S[21,10];
F_o_20_10 : 0 <= -S[20,10] + S[21,11];
F_o_20_11 : 0 <= -S[20,11] + S[21,12];
F_o_20_12 : 0 <= -S[20,12] + S[21,13];
F_o_20_13 : 0 <= -S[20,13] + S[21,14];
F_o_20_14 : 0 <= -S[20,14] + S[21,15];
F_o_20_15 : 0 <= -S[20,15] + S[21,16];
F_o_20_16 : 0 <= -S[20,16] + S[21,17];
F_o_20_17 : 0 <= -S[20,17] + S[21,18];
F_o_20_18 : 0 <= -S[20,18] + S[21,19];
F_o_20_19 : 0 <= -S[20,19] + S[21,20];
F_o_20_20 : 0 <= -S[20,20] + S[21,21];
F_o_20_21 : 0 <= -S[20,21] + S[21,22];
F_o_20_22 : 0 <= -S[20,22] + S[21,23];
F_o_20_23 : 0 <= -S[20,23] + S[21,24];
F_o_20_24 : 0 <= -S[20,24] + S[21,25];
F_o_20_25 : 0 <= -S[20,25] + S[21,26];
F_o_20_26 : 0 <= -S[20,26] + S[21,27];
F_o_20_27 : 0 <= -S[20,27] + S[21,28];
F_o_20_28 : 0 <= -S[20,28] + S[21,29];
F_o_20_29 : 0 <= -S[20,29] + S[21,30];
F_o_20_30 : 0 <= -S[20,30] + S[21,31];
F_o_20_31 : 0 <= -S[20,31] + S[21,32];
F_o_20_32 : 0 <= -S[20,32] + S[21,33];
F_o_20_33 : 0 <= -S[20,33] + S[21,34];
F_o_20_34 : 0 <= -S[20,34] + S[21,35];
F_o_20_35 : 0 <= -S[20,35] + S[21,36];
F_o_20_36 : 0 <= -S[20,36] + S[21,37];
F_o_20_37 : 0 <= -S[20,37] + S[21,38];
F_o_20_38 : 0 <= -S[20,38] + S[21,39];
F_o_20_39 : 0 <= -S[20,39] + S[21,40];
F_o_20_40 : 0 <= -S[20,40] + S[21,41];
F_o_20_41 : 0 <= -S[20,41] + S[21,42];
F_o_20_42 : 0 <= -S[20,42] + S[21,43];
F_o_20_43 : 0 <= -S[20,43] + S[21,44];
F_o_20_44 : 0 <= -S[20,44] + S[21,45];
F_o_20_45 : 0 <= -S[20,45] + S[21,46];
F_o_20_46 : 0 <= -S[20,46] + S[21,47];
F_o_20_47 : 0 <= -S[20,47] + S[21,48];
F_o_20_48 : 0 <= -S[20,48] + S[21,49];
F_o_20_49 : 0 <= -S[20,49] + S[21,50];
F_o_20_50 : 0 <= -S[20,50] + S[21,51];
F_o_20_51 : 0 <= -S[20,51] + S[21,52];
F_o_20_52 : 0 <= -S[20,52] + S[21,53];
F_o_20_53 : 0 <= -S[20,53] + S[21,54];
F_o_20_54 : 0 <= -S[20,54] + S[21,55];
F_o_20_55 : 0 <= -S[20,55] + S[21,56];
F_o_20_56 : 0 <= -S[20,56] + S[21,57];
F_o_20_57 : 0 <= -S[20,57] + S[21,58];
F_o_20_58 : 0 <= -S[20,58] + S[21,59];
F_o_20_59 : 0 <= -S[20,59] + S[21,60];
F_o_21_1 : 0 <= -S[21,1] + S[8,2];
F_o_21_2 : 0 <= -S[21,2] + S[8,3];
F_o_21_3 : 0 <= -S[21,3] + S[8,4];
F_o_21_4 : 0 <= -S[21,4] + S[8,5];
F_o_21_5 : 0 <= -S[21,5] + S[8,6];
F_o_21_6 : 0 <= -S[21,6] + S[8,7];
F_o_21_7 : 0 <= -S[21,7] + S[8,8];
F_o_21_8 : 0 <= -S[21,8] + S[8,9];
F_o_21_9 : 0 <= -S[21,9] + S[8,10];
F_o_21_10 : 0 <= -S[21,10] + S[8,11];
F_o_21_11 : 0 <= -S[21,11] + S[8,12];
F_o_21_12 : 0 <= -S[21,12] + S[8,13];
F_o_21_13 : 0 <= -S[21,13] + S[8,14];
F_o_21_14 : 0 <= -S[21,14] + S[8,15];
F_o_21_15 : 0 <= -S[21,15] + S[8,16];
F_o_21_16 : 0 <= -S[21,16] + S[8,17];
F_o_21_17 : 0 <= -S[21,17] + S[8,18];
F_o_21_18 : 0 <= -S[21,18] + S[8,19];
F_o_21_19 : 0 <= -S[21,19] + S[8,20];
F_o_21_20 : 0 <= -S[21,20] + S[8,21];
F_o_21_21 : 0 <= -S[21,21] + S[8,22];
F_o_21_22 : 0 <= -S[21,22] + S[8,23];
F_o_21_23 : 0 <= -S[21,23] + S[8,24];
F_o_21_24 : 0 <= -S[21,24] + S[8,25];
F_o_21_25 : 0 <= -S[21,25] + S[8,26];
F_o_21_26 : 0 <= -S[21,26] + S[8,27];
F_o_21_27 : 0 <= -S[21,27] + S[8,28];
F_o_21_28 : 0 <= -S[21,28] + S[8,29];
F_o_21_29 : 0 <= -S[21,29] + S[8,30];
F_o_21_30 : 0 <= -S[21,30] + S[8,31];
F_o_21_31 : 0 <= -S[21,31] + S[8,32];
F_o_21_32 : 0 <= -S[21,32] + S[8,33];
F_o_21_33 : 0 <= -S[21,33] + S[8,34];
F_o_21_34 : 0 <= -S[21,34] + S[8,35];
F_o_21_35 : 0 <= -S[21,35] + S[8,36];
F_o_21_36 : 0 <= -S[21,36] + S[8,37];
F_o_21_37 : 0 <= -S[21,37] + S[8,38];
F_o_21_38 : 0 <= -S[21,38] + S[8,39];
F_o_21_39 : 0 <= -S[21,39] + S[8,40];
F_o_21_40 : 0 <= -S[21,40] + S[8,41];
F_o_21_41 : 0 <= -S[21,41] + S[8,42];
F_o_21_42 : 0 <= -S[21,42] + S[8,43];
F_o_21_43 : 0 <= -S[21,43] + S[8,44];
F_o_21_44 : 0 <= -S[21,44] + S[8,45];
F_o_21_45 : 0 <= -S[21,45] + S[8,46];
F_o_21_46 : 0 <= -S[21,46] + S[8,47];
F_o_21_47 : 0 <= -S[21,47] + S[8,48];
F_o_21_48 : 0 <= -S[21,48] + S[8,49];
F_o_21_49 : 0 <= -S[21,49] + S[8,50];
F_o_21_50 : 0 <= -S[21,50] + S[8,51];
F_o_21_51 : 0 <= -S[21,51] + S[8,52];
F_o_21_52 : 0 <= -S[21,52] + S[8,53];
F_o_21_53 : 0 <= -S[21,53] + S[8,54];
F_o_21_54 : 0 <= -S[21,54] + S[8,55];
F_o_21_55 : 0 <= -S[21,55] + S[8,56];
F_o_21_56 : 0 <= -S[21,56] + S[8,57];
F_o_21_57 : 0 <= -S[21,57] + S[8,58];
F_o_21_58 : 0 <= -S[21,58] + S[8,59];
F_o_21_59 : 0 <= -S[21,59] + S[8,60];
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_22_24 : 0 <= -S[22,24] + S[23,25];
F_o_22_25 : 0 <= -S[22,25] + S[23,26];
F_o_22_26 : 0 <= -S[22,26] + S[23,27];
F_o_22_27 : 0 <= -S[22,27] + S[23,28];
F_o_22_28 : 0 <= -S[22,28] + S[23,29];
F_o_22_29 : 0 <= -S[22,29] + S[23,30];
F_o_22_30 : 0 <= -S[22,30] + S[23,31];
F_o_22_31 : 0 <= -S[22,31] + S[23,32];
F_o_22_32 : 0 <= -S[22,32] + S[23,33];
F_o_22_33 : 0 <= -S[22,33] + S[23,34];
F_o_22_34 : 0 <= -S[22,34] + S[23,35];
F_o_22_35 : 0 <= -S[22,35] + S[23,36];
F_o_22_36 : 0 <= -S[22,36] + S[23,37];
F_o_22_37 : 0 <= -S[22,37] + S[23,38];
F_o_22_38 : 0 <= -S[22,38] + S[23,39];
F_o_22_39 : 0 <= -S[22,39] + S[23,40];
F_o_22_40 : 0 <= -S[22,40] + S[23,41];
F_o_22_41 : 0 <= -S[22,41] + S[23,42];
F_o_22_42 : 0 <= -S[22,42] + S[23,43];
F_o_22_43 : 0 <= -S[22,43] + S[23,44];
F_o_22_44 : 0 <= -S[22,44] + S[23,45];
F_o_22_45 : 0 <= -S[22,45] + S[23,46];
F_o_22_46 : 0 <= -S[22,46] + S[23,47];
F_o_22_47 : 0 <= -S[22,47] + S[23,48];
F_o_22_48 : 0 <= -S[22,48] + S[23,49];
F_o_22_49 : 0 <= -S[22,49] + S[23,50];
F_o_22_50 : 0 <= -S[22,50] + S[23,51];
F_o_22_51 : 0 <= -S[22,51] + S[23,52];
F_o_22_52 : 0 <= -S[22,52] + S[23,53];
F_o_22_53 : 0 <= -S[22,53] + S[23,54];
F_o_22_54 : 0 <= -S[22,54] + S[23,55];
F_o_22_55 : 0 <= -S[22,55] + S[23,56];
F_o_22_56 : 0 <= -S[22,56] + S[23,57];
F_o_22_57 : 0 <= -S[22,57] + S[23,58];
F_o_22_58 : 0 <= -S[22,58] + S[23,59];
F_o_22_59 : 0 <= -S[22,59] + S[23,60];
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];
F_o_23_24 : 0 <= -S[23,24] + S[23,25];
F_o_23_25 : 0 <= -S[23,25] + S[23,26];
F_o_23_26 : 0 <= -S[23,26] + S[23,27];
F_o_23_27 : 0 <= -S[23,27] + S[23,28];
F_o_23_28 : 0 <= -S[23,28] + S[23,29];
F_o_23_29 : 0 <= -S[23,29] + S[23,30];
F_o_23_30 : 0 <= -S[23,30] + S[23,31];
F_o_23_31 : 0 <= -S[23,31] + S[23,32];
F_o_23_32 : 0 <= -S[23,32] + S[23,33];
F_o_23_33 : 0 <= -S[23,33] + S[23,34];
F_o_23_34 : 0 <= -S[23,34] + S[23,35];
F_o_23_35 : 0 <= -S[23,35] + S[23,36];
F_o_23_36 : 0 <= -S[23,36] + S[23,37];
F_o_23_37 : 0 <= -S[23,37] + S[23,38];
F_o_23_38 : 0 <= -S[23,38] + S[23,39];
F_o_23_39 : 0 <= -S[23,39] + S[23,40];
F_o_23_40 : 0 <= -S[23,40] + S[23,41];
F_o_23_41 : 0 <= -S[23,41] + S[23,42];
F_o_23_42 : 0 <= -S[23,42] + S[23,43];
F_o_23_43 : 0 <= -S[23,43] + S[23,44];
F_o_23_44 : 0 <= -S[23,44] + S[23,45];
F_o_23_45 : 0 <= -S[23,45] + S[23,46];
F_o_23_46 : 0 <= -S[23,46] + S[23,47];
F_o_23_47 : 0 <= -S[23,47] + S[23,48];
F_o_23_48 : 0 <= -S[23,48] + S[23,49];
F_o_23_49 : 0 <= -S[23,49] + S[23,50];
F_o_23_50 : 0 <= -S[23,50] + S[23,51];
F_o_23_51 : 0 <= -S[23,51] + S[23,52];
F_o_23_52 : 0 <= -S[23,52] + S[23,53];
F_o_23_53 : 0 <= -S[23,53] + S[23,54];
F_o_23_54 : 0 <= -S[23,54] + S[23,55];
F_o_23_55 : 0 <= -S[23,55] + S[23,56];
F_o_23_56 : 0 <= -S[23,56] + S[23,57];
F_o_23_57 : 0 <= -S[23,57] + S[23,58];
F_o_23_58 : 0 <= -S[23,58] + S[23,59];
F_o_23_59 : 0 <= -S[23,59] + S[23,60];
keep_1_4_1_1 : -1 <= -S[1,1]-test1[0] + test1[1];
keep_1_4_1_2 : -1 <= -S[1,1] + test1[0]-test1[1];
keep_1_1_1_1 : -1 <= -S[1,1]-parity[0] + parity[1];
keep_1_1_1_2 : -1 <= -S[1,1] + parity[0]-parity[1];
keep_1_6_1_1 : -1 <= -S[1,1] + sentinel2[1,0]-sentinel2[1,1];
keep_1_6_1_2 : -1 <= -S[1,1] + sentinel2[0,0]-sentinel2[0,1];
keep_1_6_1_3 : -1 <= -S[1,1]-sentinel2[1,0] + sentinel2[1,1];
keep_1_6_1_4 : -1 <= -S[1,1]-sentinel2[0,0] + sentinel2[0,1];
keep_1_2_1_1 : -1 <= -S[1,1] + i[1,0]-i[1,1];
keep_1_2_1_2 : -1 <= -S[1,1] + i[0,0]-i[0,1];
keep_1_2_1_3 : -1 <= -S[1,1]-i[1,0] + i[1,1];
keep_1_2_1_4 : -1 <= -S[1,1]-i[0,0] + i[0,1];
keep_1_5_1_1 : -1 <= -S[1,1] + j[1,0]-j[1,1];
keep_1_5_1_2 : -1 <= -S[1,1] + j[0,0]-j[0,1];
keep_1_5_1_3 : -1 <= -S[1,1]-j[1,0] + j[1,1];
keep_1_5_1_4 : -1 <= -S[1,1]-j[0,0] + j[0,1];
keep_1_3_1_1 : -1 <= -S[1,1] + sentinel1[1,0]-sentinel1[1,1];
keep_1_3_1_2 : -1 <= -S[1,1] + sentinel1[0,0]-sentinel1[0,1];
keep_1_3_1_3 : -1 <= -S[1,1]-sentinel1[1,0] + sentinel1[1,1];
keep_1_3_1_4 : -1 <= -S[1,1]-sentinel1[0,0] + sentinel1[0,1];
keep_1_7_1_1 : -1 <= -S[1,1]-test2[0] + test2[1];
keep_1_7_1_2 : -1 <= -S[1,1] + test2[0]-test2[1];
keep_1_8_1_1 : -1 <= -S[1,1]-temp4[0] + temp4[1];
keep_1_8_1_2 : -1 <= -S[1,1] + temp4[0]-temp4[1];
keep_1_4_2_1 : -1 <= -S[1,2]-test1[1] + test1[2];
keep_1_4_2_2 : -1 <= -S[1,2] + test1[1]-test1[2];
keep_1_1_2_1 : -1 <= -S[1,2]-parity[1] + parity[2];
keep_1_1_2_2 : -1 <= -S[1,2] + parity[1]-parity[2];
keep_1_6_2_1 : -1 <= -S[1,2] + sentinel2[1,1]-sentinel2[1,2];
keep_1_6_2_2 : -1 <= -S[1,2] + sentinel2[0,1]-sentinel2[0,2];
keep_1_6_2_3 : -1 <= -S[1,2]-sentinel2[1,1] + sentinel2[1,2];
keep_1_6_2_4 : -1 <= -S[1,2]-sentinel2[0,1] + sentinel2[0,2];
keep_1_2_2_1 : -1 <= -S[1,2] + i[1,1]-i[1,2];
keep_1_2_2_2 : -1 <= -S[1,2] + i[0,1]-i[0,2];
keep_1_2_2_3 : -1 <= -S[1,2]-i[1,1] + i[1,2];
keep_1_2_2_4 : -1 <= -S[1,2]-i[0,1] + i[0,2];
keep_1_5_2_1 : -1 <= -S[1,2] + j[1,1]-j[1,2];
keep_1_5_2_2 : -1 <= -S[1,2] + j[0,1]-j[0,2];
keep_1_5_2_3 : -1 <= -S[1,2]-j[1,1] + j[1,2];
keep_1_5_2_4 : -1 <= -S[1,2]-j[0,1] + j[0,2];
keep_1_3_2_1 : -1 <= -S[1,2] + sentinel1[1,1]-sentinel1[1,2];
keep_1_3_2_2 : -1 <= -S[1,2] + sentinel1[0,1]-sentinel1[0,2];
keep_1_3_2_3 : -1 <= -S[1,2]-sentinel1[1,1] + sentinel1[1,2];
keep_1_3_2_4 : -1 <= -S[1,2]-sentinel1[0,1] + sentinel1[0,2];
keep_1_7_2_1 : -1 <= -S[1,2]-test2[1] + test2[2];
keep_1_7_2_2 : -1 <= -S[1,2] + test2[1]-test2[2];
keep_1_8_2_1 : -1 <= -S[1,2]-temp4[1] + temp4[2];
keep_1_8_2_2 : -1 <= -S[1,2] + temp4[1]-temp4[2];
keep_1_4_3_1 : -1 <= -S[1,3]-test1[2] + test1[3];
keep_1_4_3_2 : -1 <= -S[1,3] + test1[2]-test1[3];
keep_1_1_3_1 : -1 <= -S[1,3]-parity[2] + parity[3];
keep_1_1_3_2 : -1 <= -S[1,3] + parity[2]-parity[3];
keep_1_6_3_1 : -1 <= -S[1,3] + sentinel2[1,2]-sentinel2[1,3];
keep_1_6_3_2 : -1 <= -S[1,3] + sentinel2[0,2]-sentinel2[0,3];
keep_1_6_3_3 : -1 <= -S[1,3]-sentinel2[1,2] + sentinel2[1,3];
keep_1_6_3_4 : -1 <= -S[1,3]-sentinel2[0,2] + sentinel2[0,3];
keep_1_2_3_1 : -1 <= -S[1,3] + i[1,2]-i[1,3];
keep_1_2_3_2 : -1 <= -S[1,3] + i[0,2]-i[0,3];
keep_1_2_3_3 : -1 <= -S[1,3]-i[1,2] + i[1,3];
keep_1_2_3_4 : -1 <= -S[1,3]-i[0,2] + i[0,3];
keep_1_5_3_1 : -1 <= -S[1,3] + j[1,2]-j[1,3];
keep_1_5_3_2 : -1 <= -S[1,3] + j[0,2]-j[0,3];
keep_1_5_3_3 : -1 <= -S[1,3]-j[1,2] + j[1,3];
keep_1_5_3_4 : -1 <= -S[1,3]-j[0,2] + j[0,3];
keep_1_3_3_1 : -1 <= -S[1,3] + sentinel1[1,2]-sentinel1[1,3];
keep_1_3_3_2 : -1 <= -S[1,3] + sentinel1[0,2]-sentinel1[0,3];
keep_1_3_3_3 : -1 <= -S[1,3]-sentinel1[1,2] + sentinel1[1,3];
keep_1_3_3_4 : -1 <= -S[1,3]-sentinel1[0,2] + sentinel1[0,3];
keep_1_7_3_1 : -1 <= -S[1,3]-test2[2] + test2[3];
keep_1_7_3_2 : -1 <= -S[1,3] + test2[2]-test2[3];
keep_1_8_3_1 : -1 <= -S[1,3]-temp4[2] + temp4[3];
keep_1_8_3_2 : -1 <= -S[1,3] + temp4[2]-temp4[3];
keep_1_4_4_1 : -1 <= -S[1,4]-test1[3] + test1[4];
keep_1_4_4_2 : -1 <= -S[1,4] + test1[3]-test1[4];
keep_1_1_4_1 : -1 <= -S[1,4]-parity[3] + parity[4];
keep_1_1_4_2 : -1 <= -S[1,4] + parity[3]-parity[4];
keep_1_6_4_1 : -1 <= -S[1,4] + sentinel2[1,3]-sentinel2[1,4];
keep_1_6_4_2 : -1 <= -S[1,4] + sentinel2[0,3]-sentinel2[0,4];
keep_1_6_4_3 : -1 <= -S[1,4]-sentinel2[1,3] + sentinel2[1,4];
keep_1_6_4_4 : -1 <= -S[1,4]-sentinel2[0,3] + sentinel2[0,4];
keep_1_2_4_1 : -1 <= -S[1,4] + i[1,3]-i[1,4];
keep_1_2_4_2 : -1 <= -S[1,4] + i[0,3]-i[0,4];
keep_1_2_4_3 : -1 <= -S[1,4]-i[1,3] + i[1,4];
keep_1_2_4_4 : -1 <= -S[1,4]-i[0,3] + i[0,4];
keep_1_5_4_1 : -1 <= -S[1,4] + j[1,3]-j[1,4];
keep_1_5_4_2 : -1 <= -S[1,4] + j[0,3]-j[0,4];
keep_1_5_4_3 : -1 <= -S[1,4]-j[1,3] + j[1,4];
keep_1_5_4_4 : -1 <= -S[1,4]-j[0,3] + j[0,4];
keep_1_3_4_1 : -1 <= -S[1,4] + sentinel1[1,3]-sentinel1[1,4];
keep_1_3_4_2 : -1 <= -S[1,4] + sentinel1[0,3]-sentinel1[0,4];
keep_1_3_4_3 : -1 <= -S[1,4]-sentinel1[1,3] + sentinel1[1,4];
keep_1_3_4_4 : -1 <= -S[1,4]-sentinel1[0,3] + sentinel1[0,4];
keep_1_7_4_1 : -1 <= -S[1,4]-test2[3] + test2[4];
keep_1_7_4_2 : -1 <= -S[1,4] + test2[3]-test2[4];
keep_1_8_4_1 : -1 <= -S[1,4]-temp4[3] + temp4[4];
keep_1_8_4_2 : -1 <= -S[1,4] + temp4[3]-temp4[4];
keep_1_4_5_1 : -1 <= -S[1,5]-test1[4] + test1[5];
keep_1_4_5_2 : -1 <= -S[1,5] + test1[4]-test1[5];
keep_1_1_5_1 : -1 <= -S[1,5]-parity[4] + parity[5];
keep_1_1_5_2 : -1 <= -S[1,5] + parity[4]-parity[5];
keep_1_6_5_1 : -1 <= -S[1,5] + sentinel2[1,4]-sentinel2[1,5];
keep_1_6_5_2 : -1 <= -S[1,5] + sentinel2[0,4]-sentinel2[0,5];
keep_1_6_5_3 : -1 <= -S[1,5]-sentinel2[1,4] + sentinel2[1,5];
keep_1_6_5_4 : -1 <= -S[1,5]-sentinel2[0,4] + sentinel2[0,5];
keep_1_2_5_1 : -1 <= -S[1,5] + i[1,4]-i[1,5];
keep_1_2_5_2 : -1 <= -S[1,5] + i[0,4]-i[0,5];
keep_1_2_5_3 : -1 <= -S[1,5]-i[1,4] + i[1,5];
keep_1_2_5_4 : -1 <= -S[1,5]-i[0,4] + i[0,5];
keep_1_5_5_1 : -1 <= -S[1,5] + j[1,4]-j[1,5];
keep_1_5_5_2 : -1 <= -S[1,5] + j[0,4]-j[0,5];
keep_1_5_5_3 : -1 <= -S[1,5]-j[1,4] + j[1,5];
keep_1_5_5_4 : -1 <= -S[1,5]-j[0,4] + j[0,5];
keep_1_3_5_1 : -1 <= -S[1,5] + sentinel1[1,4]-sentinel1[1,5];
keep_1_3_5_2 : -1 <= -S[1,5] + sentinel1[0,4]-sentinel1[0,5];
keep_1_3_5_3 : -1 <= -S[1,5]-sentinel1[1,4] + sentinel1[1,5];
keep_1_3_5_4 : -1 <= -S[1,5]-sentinel1[0,4] + sentinel1[0,5];
keep_1_7_5_1 : -1 <= -S[1,5]-test2[4] + test2[5];
keep_1_7_5_2 : -1 <= -S[1,5] + test2[4]-test2[5];
keep_1_8_5_1 : -1 <= -S[1,5]-temp4[4] + temp4[5];
keep_1_8_5_2 : -1 <= -S[1,5] + temp4[4]-temp4[5];
keep_1_4_6_1 : -1 <= -S[1,6]-test1[5] + test1[6];
keep_1_4_6_2 : -1 <= -S[1,6] + test1[5]-test1[6];
keep_1_1_6_1 : -1 <= -S[1,6]-parity[5] + parity[6];
keep_1_1_6_2 : -1 <= -S[1,6] + parity[5]-parity[6];
keep_1_6_6_1 : -1 <= -S[1,6] + sentinel2[1,5]-sentinel2[1,6];
keep_1_6_6_2 : -1 <= -S[1,6] + sentinel2[0,5]-sentinel2[0,6];
keep_1_6_6_3 : -1 <= -S[1,6]-sentinel2[1,5] + sentinel2[1,6];
keep_1_6_6_4 : -1 <= -S[1,6]-sentinel2[0,5] + sentinel2[0,6];
keep_1_2_6_1 : -1 <= -S[1,6] + i[1,5]-i[1,6];
keep_1_2_6_2 : -1 <= -S[1,6] + i[0,5]-i[0,6];
keep_1_2_6_3 : -1 <= -S[1,6]-i[1,5] + i[1,6];
keep_1_2_6_4 : -1 <= -S[1,6]-i[0,5] + i[0,6];
keep_1_5_6_1 : -1 <= -S[1,6] + j[1,5]-j[1,6];
keep_1_5_6_2 : -1 <= -S[1,6] + j[0,5]-j[0,6];
keep_1_5_6_3 : -1 <= -S[1,6]-j[1,5] + j[1,6];
keep_1_5_6_4 : -1 <= -S[1,6]-j[0,5] + j[0,6];
keep_1_3_6_1 : -1 <= -S[1,6] + sentinel1[1,5]-sentinel1[1,6];
keep_1_3_6_2 : -1 <= -S[1,6] + sentinel1[0,5]-sentinel1[0,6];
keep_1_3_6_3 : -1 <= -S[1,6]-sentinel1[1,5] + sentinel1[1,6];
keep_1_3_6_4 : -1 <= -S[1,6]-sentinel1[0,5] + sentinel1[0,6];
keep_1_7_6_1 : -1 <= -S[1,6]-test2[5] + test2[6];
keep_1_7_6_2 : -1 <= -S[1,6] + test2[5]-test2[6];
keep_1_8_6_1 : -1 <= -S[1,6]-temp4[5] + temp4[6];
keep_1_8_6_2 : -1 <= -S[1,6] + temp4[5]-temp4[6];
keep_1_4_7_1 : -1 <= -S[1,7]-test1[6] + test1[7];
keep_1_4_7_2 : -1 <= -S[1,7] + test1[6]-test1[7];
keep_1_1_7_1 : -1 <= -S[1,7]-parity[6] + parity[7];
keep_1_1_7_2 : -1 <= -S[1,7] + parity[6]-parity[7];
keep_1_6_7_1 : -1 <= -S[1,7] + sentinel2[1,6]-sentinel2[1,7];
keep_1_6_7_2 : -1 <= -S[1,7] + sentinel2[0,6]-sentinel2[0,7];
keep_1_6_7_3 : -1 <= -S[1,7]-sentinel2[1,6] + sentinel2[1,7];
keep_1_6_7_4 : -1 <= -S[1,7]-sentinel2[0,6] + sentinel2[0,7];
keep_1_2_7_1 : -1 <= -S[1,7] + i[1,6]-i[1,7];
keep_1_2_7_2 : -1 <= -S[1,7] + i[0,6]-i[0,7];
keep_1_2_7_3 : -1 <= -S[1,7]-i[1,6] + i[1,7];
keep_1_2_7_4 : -1 <= -S[1,7]-i[0,6] + i[0,7];
keep_1_5_7_1 : -1 <= -S[1,7] + j[1,6]-j[1,7];
keep_1_5_7_2 : -1 <= -S[1,7] + j[0,6]-j[0,7];
keep_1_5_7_3 : -1 <= -S[1,7]-j[1,6] + j[1,7];
keep_1_5_7_4 : -1 <= -S[1,7]-j[0,6] + j[0,7];
keep_1_3_7_1 : -1 <= -S[1,7] + sentinel1[1,6]-sentinel1[1,7];
keep_1_3_7_2 : -1 <= -S[1,7] + sentinel1[0,6]-sentinel1[0,7];
keep_1_3_7_3 : -1 <= -S[1,7]-sentinel1[1,6] + sentinel1[1,7];
keep_1_3_7_4 : -1 <= -S[1,7]-sentinel1[0,6] + sentinel1[0,7];
keep_1_7_7_1 : -1 <= -S[1,7]-test2[6] + test2[7];
keep_1_7_7_2 : -1 <= -S[1,7] + test2[6]-test2[7];
keep_1_8_7_1 : -1 <= -S[1,7]-temp4[6] + temp4[7];
keep_1_8_7_2 : -1 <= -S[1,7] + temp4[6]-temp4[7];
keep_1_4_8_1 : -1 <= -S[1,8]-test1[7] + test1[8];
keep_1_4_8_2 : -1 <= -S[1,8] + test1[7]-test1[8];
keep_1_1_8_1 : -1 <= -S[1,8]-parity[7] + parity[8];
keep_1_1_8_2 : -1 <= -S[1,8] + parity[7]-parity[8];
keep_1_6_8_1 : -1 <= -S[1,8] + sentinel2[1,7]-sentinel2[1,8];
keep_1_6_8_2 : -1 <= -S[1,8] + sentinel2[0,7]-sentinel2[0,8];
keep_1_6_8_3 : -1 <= -S[1,8]-sentinel2[1,7] + sentinel2[1,8];
keep_1_6_8_4 : -1 <= -S[1,8]-sentinel2[0,7] + sentinel2[0,8];
keep_1_2_8_1 : -1 <= -S[1,8] + i[1,7]-i[1,8];
keep_1_2_8_2 : -1 <= -S[1,8] + i[0,7]-i[0,8];
keep_1_2_8_3 : -1 <= -S[1,8]-i[1,7] + i[1,8];
keep_1_2_8_4 : -1 <= -S[1,8]-i[0,7] + i[0,8];
keep_1_5_8_1 : -1 <= -S[1,8] + j[1,7]-j[1,8];
keep_1_5_8_2 : -1 <= -S[1,8] + j[0,7]-j[0,8];
keep_1_5_8_3 : -1 <= -S[1,8]-j[1,7] + j[1,8];
keep_1_5_8_4 : -1 <= -S[1,8]-j[0,7] + j[0,8];
keep_1_3_8_1 : -1 <= -S[1,8] + sentinel1[1,7]-sentinel1[1,8];
keep_1_3_8_2 : -1 <= -S[1,8] + sentinel1[0,7]-sentinel1[0,8];
keep_1_3_8_3 : -1 <= -S[1,8]-sentinel1[1,7] + sentinel1[1,8];
keep_1_3_8_4 : -1 <= -S[1,8]-sentinel1[0,7] + sentinel1[0,8];
keep_1_7_8_1 : -1 <= -S[1,8]-test2[7] + test2[8];
keep_1_7_8_2 : -1 <= -S[1,8] + test2[7]-test2[8];
keep_1_8_8_1 : -1 <= -S[1,8]-temp4[7] + temp4[8];
keep_1_8_8_2 : -1 <= -S[1,8] + temp4[7]-temp4[8];
keep_1_4_9_1 : -1 <= -S[1,9]-test1[8] + test1[9];
keep_1_4_9_2 : -1 <= -S[1,9] + test1[8]-test1[9];
keep_1_1_9_1 : -1 <= -S[1,9]-parity[8] + parity[9];
keep_1_1_9_2 : -1 <= -S[1,9] + parity[8]-parity[9];
keep_1_6_9_1 : -1 <= -S[1,9] + sentinel2[1,8]-sentinel2[1,9];
keep_1_6_9_2 : -1 <= -S[1,9] + sentinel2[0,8]-sentinel2[0,9];
keep_1_6_9_3 : -1 <= -S[1,9]-sentinel2[1,8] + sentinel2[1,9];
keep_1_6_9_4 : -1 <= -S[1,9]-sentinel2[0,8] + sentinel2[0,9];
keep_1_2_9_1 : -1 <= -S[1,9] + i[1,8]-i[1,9];
keep_1_2_9_2 : -1 <= -S[1,9] + i[0,8]-i[0,9];
keep_1_2_9_3 : -1 <= -S[1,9]-i[1,8] + i[1,9];
keep_1_2_9_4 : -1 <= -S[1,9]-i[0,8] + i[0,9];
keep_1_5_9_1 : -1 <= -S[1,9] + j[1,8]-j[1,9];
keep_1_5_9_2 : -1 <= -S[1,9] + j[0,8]-j[0,9];
keep_1_5_9_3 : -1 <= -S[1,9]-j[1,8] + j[1,9];
keep_1_5_9_4 : -1 <= -S[1,9]-j[0,8] + j[0,9];
keep_1_3_9_1 : -1 <= -S[1,9] + sentinel1[1,8]-sentinel1[1,9];
keep_1_3_9_2 : -1 <= -S[1,9] + sentinel1[0,8]-sentinel1[0,9];
keep_1_3_9_3 : -1 <= -S[1,9]-sentinel1[1,8] + sentinel1[1,9];
keep_1_3_9_4 : -1 <= -S[1,9]-sentinel1[0,8] + sentinel1[0,9];
keep_1_7_9_1 : -1 <= -S[1,9]-test2[8] + test2[9];
keep_1_7_9_2 : -1 <= -S[1,9] + test2[8]-test2[9];
keep_1_8_9_1 : -1 <= -S[1,9]-temp4[8] + temp4[9];
keep_1_8_9_2 : -1 <= -S[1,9] + temp4[8]-temp4[9];
keep_1_4_10_1 : -1 <= -S[1,10] + test1[10]-test1[9];
keep_1_4_10_2 : -1 <= -S[1,10]-test1[10] + test1[9];
keep_1_1_10_1 : -1 <= -S[1,10] + parity[10]-parity[9];
keep_1_1_10_2 : -1 <= -S[1,10]-parity[10] + parity[9];
keep_1_6_10_1 : -1 <= -S[1,10]-sentinel2[1,10] + sentinel2[1,9];
keep_1_6_10_2 : -1 <= -S[1,10]-sentinel2[0,10] + sentinel2[0,9];
keep_1_6_10_3 : -1 <= -S[1,10] + sentinel2[1,10]-sentinel2[1,9];
keep_1_6_10_4 : -1 <= -S[1,10] + sentinel2[0,10]-sentinel2[0,9];
keep_1_2_10_1 : -1 <= -S[1,10]-i[1,10] + i[1,9];
keep_1_2_10_2 : -1 <= -S[1,10]-i[0,10] + i[0,9];
keep_1_2_10_3 : -1 <= -S[1,10] + i[1,10]-i[1,9];
keep_1_2_10_4 : -1 <= -S[1,10] + i[0,10]-i[0,9];
keep_1_5_10_1 : -1 <= -S[1,10]-j[1,10] + j[1,9];
keep_1_5_10_2 : -1 <= -S[1,10]-j[0,10] + j[0,9];
keep_1_5_10_3 : -1 <= -S[1,10] + j[1,10]-j[1,9];
keep_1_5_10_4 : -1 <= -S[1,10] + j[0,10]-j[0,9];
keep_1_3_10_1 : -1 <= -S[1,10]-sentinel1[1,10] + sentinel1[1,9];
keep_1_3_10_2 : -1 <= -S[1,10]-sentinel1[0,10] + sentinel1[0,9];
keep_1_3_10_3 : -1 <= -S[1,10] + sentinel1[1,10]-sentinel1[1,9];
keep_1_3_10_4 : -1 <= -S[1,10] + sentinel1[0,10]-sentinel1[0,9];
keep_1_7_10_1 : -1 <= -S[1,10] + test2[10]-test2[9];
keep_1_7_10_2 : -1 <= -S[1,10]-test2[10] + test2[9];
keep_1_8_10_1 : -1 <= -S[1,10] + temp4[10]-temp4[9];
keep_1_8_10_2 : -1 <= -S[1,10]-temp4[10] + temp4[9];
keep_1_4_11_1 : -1 <= -S[1,11]-test1[10] + test1[11];
keep_1_4_11_2 : -1 <= -S[1,11] + test1[10]-test1[11];
keep_1_1_11_1 : -1 <= -S[1,11]-parity[10] + parity[11];
keep_1_1_11_2 : -1 <= -S[1,11] + parity[10]-parity[11];
keep_1_6_11_1 : -1 <= -S[1,11] + sentinel2[1,10]-sentinel2[1,11];
keep_1_6_11_2 : -1 <= -S[1,11] + sentinel2[0,10]-sentinel2[0,11];
keep_1_6_11_3 : -1 <= -S[1,11]-sentinel2[1,10] + sentinel2[1,11];
keep_1_6_11_4 : -1 <= -S[1,11]-sentinel2[0,10] + sentinel2[0,11];
keep_1_2_11_1 : -1 <= -S[1,11] + i[1,10]-i[1,11];
keep_1_2_11_2 : -1 <= -S[1,11] + i[0,10]-i[0,11];
keep_1_2_11_3 : -1 <= -S[1,11]-i[1,10] + i[1,11];
keep_1_2_11_4 : -1 <= -S[1,11]-i[0,10] + i[0,11];
keep_1_5_11_1 : -1 <= -S[1,11] + j[1,10]-j[1,11];
keep_1_5_11_2 : -1 <= -S[1,11] + j[0,10]-j[0,11];
keep_1_5_11_3 : -1 <= -S[1,11]-j[1,10] + j[1,11];
keep_1_5_11_4 : -1 <= -S[1,11]-j[0,10] + j[0,11];
keep_1_3_11_1 : -1 <= -S[1,11] + sentinel1[1,10]-sentinel1[1,11];
keep_1_3_11_2 : -1 <= -S[1,11] + sentinel1[0,10]-sentinel1[0,11];
keep_1_3_11_3 : -1 <= -S[1,11]-sentinel1[1,10] + sentinel1[1,11];
keep_1_3_11_4 : -1 <= -S[1,11]-sentinel1[0,10] + sentinel1[0,11];
keep_1_7_11_1 : -1 <= -S[1,11]-test2[10] + test2[11];
keep_1_7_11_2 : -1 <= -S[1,11] + test2[10]-test2[11];
keep_1_8_11_1 : -1 <= -S[1,11]-temp4[10] + temp4[11];
keep_1_8_11_2 : -1 <= -S[1,11] + temp4[10]-temp4[11];
keep_1_4_12_1 : -1 <= -S[1,12]-test1[11] + test1[12];
keep_1_4_12_2 : -1 <= -S[1,12] + test1[11]-test1[12];
keep_1_1_12_1 : -1 <= -S[1,12]-parity[11] + parity[12];
keep_1_1_12_2 : -1 <= -S[1,12] + parity[11]-parity[12];
keep_1_6_12_1 : -1 <= -S[1,12] + sentinel2[1,11]-sentinel2[1,12];
keep_1_6_12_2 : -1 <= -S[1,12] + sentinel2[0,11]-sentinel2[0,12];
keep_1_6_12_3 : -1 <= -S[1,12]-sentinel2[1,11] + sentinel2[1,12];
keep_1_6_12_4 : -1 <= -S[1,12]-sentinel2[0,11] + sentinel2[0,12];
keep_1_2_12_1 : -1 <= -S[1,12] + i[1,11]-i[1,12];
keep_1_2_12_2 : -1 <= -S[1,12] + i[0,11]-i[0,12];
keep_1_2_12_3 : -1 <= -S[1,12]-i[1,11] + i[1,12];
keep_1_2_12_4 : -1 <= -S[1,12]-i[0,11] + i[0,12];
keep_1_5_12_1 : -1 <= -S[1,12] + j[1,11]-j[1,12];
keep_1_5_12_2 : -1 <= -S[1,12] + j[0,11]-j[0,12];
keep_1_5_12_3 : -1 <= -S[1,12]-j[1,11] + j[1,12];
keep_1_5_12_4 : -1 <= -S[1,12]-j[0,11] + j[0,12];
keep_1_3_12_1 : -1 <= -S[1,12] + sentinel1[1,11]-sentinel1[1,12];
keep_1_3_12_2 : -1 <= -S[1,12] + sentinel1[0,11]-sentinel1[0,12];
keep_1_3_12_3 : -1 <= -S[1,12]-sentinel1[1,11] + sentinel1[1,12];
keep_1_3_12_4 : -1 <= -S[1,12]-sentinel1[0,11] + sentinel1[0,12];
keep_1_7_12_1 : -1 <= -S[1,12]-test2[11] + test2[12];
keep_1_7_12_2 : -1 <= -S[1,12] + test2[11]-test2[12];
keep_1_8_12_1 : -1 <= -S[1,12]-temp4[11] + temp4[12];
keep_1_8_12_2 : -1 <= -S[1,12] + temp4[11]-temp4[12];
keep_1_4_13_1 : -1 <= -S[1,13]-test1[12] + test1[13];
keep_1_4_13_2 : -1 <= -S[1,13] + test1[12]-test1[13];
keep_1_1_13_1 : -1 <= -S[1,13]-parity[12] + parity[13];
keep_1_1_13_2 : -1 <= -S[1,13] + parity[12]-parity[13];
keep_1_6_13_1 : -1 <= -S[1,13] + sentinel2[1,12]-sentinel2[1,13];
keep_1_6_13_2 : -1 <= -S[1,13] + sentinel2[0,12]-sentinel2[0,13];
keep_1_6_13_3 : -1 <= -S[1,13]-sentinel2[1,12] + sentinel2[1,13];
keep_1_6_13_4 : -1 <= -S[1,13]-sentinel2[0,12] + sentinel2[0,13];
keep_1_2_13_1 : -1 <= -S[1,13] + i[1,12]-i[1,13];
keep_1_2_13_2 : -1 <= -S[1,13] + i[0,12]-i[0,13];
keep_1_2_13_3 : -1 <= -S[1,13]-i[1,12] + i[1,13];
keep_1_2_13_4 : -1 <= -S[1,13]-i[0,12] + i[0,13];
keep_1_5_13_1 : -1 <= -S[1,13] + j[1,12]-j[1,13];
keep_1_5_13_2 : -1 <= -S[1,13] + j[0,12]-j[0,13];
keep_1_5_13_3 : -1 <= -S[1,13]-j[1,12] + j[1,13];
keep_1_5_13_4 : -1 <= -S[1,13]-j[0,12] + j[0,13];
keep_1_3_13_1 : -1 <= -S[1,13] + sentinel1[1,12]-sentinel1[1,13];
keep_1_3_13_2 : -1 <= -S[1,13] + sentinel1[0,12]-sentinel1[0,13];
keep_1_3_13_3 : -1 <= -S[1,13]-sentinel1[1,12] + sentinel1[1,13];
keep_1_3_13_4 : -1 <= -S[1,13]-sentinel1[0,12] + sentinel1[0,13];
keep_1_7_13_1 : -1 <= -S[1,13]-test2[12] + test2[13];
keep_1_7_13_2 : -1 <= -S[1,13] + test2[12]-test2[13];
keep_1_8_13_1 : -1 <= -S[1,13]-temp4[12] + temp4[13];
keep_1_8_13_2 : -1 <= -S[1,13] + temp4[12]-temp4[13];
keep_1_4_14_1 : -1 <= -S[1,14]-test1[13] + test1[14];
keep_1_4_14_2 : -1 <= -S[1,14] + test1[13]-test1[14];
keep_1_1_14_1 : -1 <= -S[1,14]-parity[13] + parity[14];
keep_1_1_14_2 : -1 <= -S[1,14] + parity[13]-parity[14];
keep_1_6_14_1 : -1 <= -S[1,14] + sentinel2[1,13]-sentinel2[1,14];
keep_1_6_14_2 : -1 <= -S[1,14] + sentinel2[0,13]-sentinel2[0,14];
keep_1_6_14_3 : -1 <= -S[1,14]-sentinel2[1,13] + sentinel2[1,14];
keep_1_6_14_4 : -1 <= -S[1,14]-sentinel2[0,13] + sentinel2[0,14];
keep_1_2_14_1 : -1 <= -S[1,14] + i[1,13]-i[1,14];
keep_1_2_14_2 : -1 <= -S[1,14] + i[0,13]-i[0,14];
keep_1_2_14_3 : -1 <= -S[1,14]-i[1,13] + i[1,14];
keep_1_2_14_4 : -1 <= -S[1,14]-i[0,13] + i[0,14];
keep_1_5_14_1 : -1 <= -S[1,14] + j[1,13]-j[1,14];
keep_1_5_14_2 : -1 <= -S[1,14] + j[0,13]-j[0,14];
keep_1_5_14_3 : -1 <= -S[1,14]-j[1,13] + j[1,14];
keep_1_5_14_4 : -1 <= -S[1,14]-j[0,13] + j[0,14];
keep_1_3_14_1 : -1 <= -S[1,14] + sentinel1[1,13]-sentinel1[1,14];
keep_1_3_14_2 : -1 <= -S[1,14] + sentinel1[0,13]-sentinel1[0,14];
keep_1_3_14_3 : -1 <= -S[1,14]-sentinel1[1,13] + sentinel1[1,14];
keep_1_3_14_4 : -1 <= -S[1,14]-sentinel1[0,13] + sentinel1[0,14];
keep_1_7_14_1 : -1 <= -S[1,14]-test2[13] + test2[14];
keep_1_7_14_2 : -1 <= -S[1,14] + test2[13]-test2[14];
keep_1_8_14_1 : -1 <= -S[1,14]-temp4[13] + temp4[14];
keep_1_8_14_2 : -1 <= -S[1,14] + temp4[13]-temp4[14];
keep_1_4_15_1 : -1 <= -S[1,15]-test1[14] + test1[15];
keep_1_4_15_2 : -1 <= -S[1,15] + test1[14]-test1[15];
keep_1_1_15_1 : -1 <= -S[1,15]-parity[14] + parity[15];
keep_1_1_15_2 : -1 <= -S[1,15] + parity[14]-parity[15];
keep_1_6_15_1 : -1 <= -S[1,15] + sentinel2[1,14]-sentinel2[1,15];
keep_1_6_15_2 : -1 <= -S[1,15] + sentinel2[0,14]-sentinel2[0,15];
keep_1_6_15_3 : -1 <= -S[1,15]-sentinel2[1,14] + sentinel2[1,15];
keep_1_6_15_4 : -1 <= -S[1,15]-sentinel2[0,14] + sentinel2[0,15];
keep_1_2_15_1 : -1 <= -S[1,15] + i[1,14]-i[1,15];
keep_1_2_15_2 : -1 <= -S[1,15] + i[0,14]-i[0,15];
keep_1_2_15_3 : -1 <= -S[1,15]-i[1,14] + i[1,15];
keep_1_2_15_4 : -1 <= -S[1,15]-i[0,14] + i[0,15];
keep_1_5_15_1 : -1 <= -S[1,15] + j[1,14]-j[1,15];
keep_1_5_15_2 : -1 <= -S[1,15] + j[0,14]-j[0,15];
keep_1_5_15_3 : -1 <= -S[1,15]-j[1,14] + j[1,15];
keep_1_5_15_4 : -1 <= -S[1,15]-j[0,14] + j[0,15];
keep_1_3_15_1 : -1 <= -S[1,15] + sentinel1[1,14]-sentinel1[1,15];
keep_1_3_15_2 : -1 <= -S[1,15] + sentinel1[0,14]-sentinel1[0,15];
keep_1_3_15_3 : -1 <= -S[1,15]-sentinel1[1,14] + sentinel1[1,15];
keep_1_3_15_4 : -1 <= -S[1,15]-sentinel1[0,14] + sentinel1[0,15];
keep_1_7_15_1 : -1 <= -S[1,15]-test2[14] + test2[15];
keep_1_7_15_2 : -1 <= -S[1,15] + test2[14]-test2[15];
keep_1_8_15_1 : -1 <= -S[1,15]-temp4[14] + temp4[15];
keep_1_8_15_2 : -1 <= -S[1,15] + temp4[14]-temp4[15];
keep_1_4_16_1 : -1 <= -S[1,16]-test1[15] + test1[16];
keep_1_4_16_2 : -1 <= -S[1,16] + test1[15]-test1[16];
keep_1_1_16_1 : -1 <= -S[1,16]-parity[15] + parity[16];
keep_1_1_16_2 : -1 <= -S[1,16] + parity[15]-parity[16];
keep_1_6_16_1 : -1 <= -S[1,16] + sentinel2[1,15]-sentinel2[1,16];
keep_1_6_16_2 : -1 <= -S[1,16] + sentinel2[0,15]-sentinel2[0,16];
keep_1_6_16_3 : -1 <= -S[1,16]-sentinel2[1,15] + sentinel2[1,16];
keep_1_6_16_4 : -1 <= -S[1,16]-sentinel2[0,15] + sentinel2[0,16];
keep_1_2_16_1 : -1 <= -S[1,16] + i[1,15]-i[1,16];
keep_1_2_16_2 : -1 <= -S[1,16] + i[0,15]-i[0,16];
keep_1_2_16_3 : -1 <= -S[1,16]-i[1,15] + i[1,16];
keep_1_2_16_4 : -1 <= -S[1,16]-i[0,15] + i[0,16];
keep_1_5_16_1 : -1 <= -S[1,16] + j[1,15]-j[1,16];
keep_1_5_16_2 : -1 <= -S[1,16] + j[0,15]-j[0,16];
keep_1_5_16_3 : -1 <= -S[1,16]-j[1,15] + j[1,16];
keep_1_5_16_4 : -1 <= -S[1,16]-j[0,15] + j[0,16];
keep_1_3_16_1 : -1 <= -S[1,16] + sentinel1[1,15]-sentinel1[1,16];
keep_1_3_16_2 : -1 <= -S[1,16] + sentinel1[0,15]-sentinel1[0,16];
keep_1_3_16_3 : -1 <= -S[1,16]-sentinel1[1,15] + sentinel1[1,16];
keep_1_3_16_4 : -1 <= -S[1,16]-sentinel1[0,15] + sentinel1[0,16];
keep_1_7_16_1 : -1 <= -S[1,16]-test2[15] + test2[16];
keep_1_7_16_2 : -1 <= -S[1,16] + t