text: //@ ltl invariant negative: (X (<> ([] (X AP(x_14 - x_15 > 1)))));
  float x_0;
  float x_1;
  float x_2;
  float x_3;
  float x_4;
  float x_5;
  float x_6;
  float x_7;
  float x_8;
  float x_9;
  float x_10;
  float x_11;
  float x_12;
  float x_13;
  float x_14;
  float x_15;
  float x_16;
  float x_17;
  float x_18;
  float x_19;
  float x_20;
  float x_21;
  float x_22;
  float x_23;
  int main()
  {
    float x_0_;
    float x_1_;
    float x_2_;
    float x_3_;
    float x_4_;
    float x_5_;
    float x_6_;
    float x_7_;
    float x_8_;
    float x_9_;
    float x_10_;
    float x_11_;
    float x_12_;
    float x_13_;
    float x_14_;
    float x_15_;
    float x_16_;
    float x_17_;
    float x_18_;
    float x_19_;
    float x_20_;
    float x_21_;
    float x_22_;
    float x_23_;
    while(1) {
  x_0_ = ((((19.0 + x_0) > ((16.0 + x_1) > (13.0 + x_2)? (16.0 + x_1) : (13.0 + x_2))? (19.0 + x_0) : ((16.0 + x_1) > (13.0 + x_2)? (16.0 + x_1) : (13.0 + x_2))) > ((3.0 + x_5) > ((4.0 + x_12) > (10.0 + x_13)? (4.0 + x_12) : (10.0 + x_13))? (3.0 + x_5) : ((4.0 + x_12) > (10.0 + x_13)? (4.0 + x_12) : (10.0 + x_13)))? ((19.0 + x_0) > ((16.0 + x_1) > (13.0 + x_2)? (16.0 + x_1) : (13.0 + x_2))? (19.0 + x_0) : ((16.0 + x_1) > (13.0 + x_2)? (16.0 + x_1) : (13.0 + x_2))) : ((3.0 + x_5) > ((4.0 + x_12) > (10.0 + x_13)? (4.0 + x_12) : (10.0 + x_13))? (3.0 + x_5) : ((4.0 + x_12) > (10.0 + x_13)? (4.0 + x_12) : (10.0 + x_13)))) > (((17.0 + x_14) > ((2.0 + x_15) > (20.0 + x_17)? (2.0 + x_15) : (20.0 + x_17))? (17.0 + x_14) : ((2.0 + x_15) > (20.0 + x_17)? (2.0 + x_15) : (20.0 + x_17))) > ((10.0 + x_21) > ((18.0 + x_22) > (11.0 + x_23)? (18.0 + x_22) : (11.0 + x_23))? (10.0 + x_21) : ((18.0 + x_22) > (11.0 + x_23)? (18.0 + x_22) : (11.0 + x_23)))? ((17.0 + x_14) > ((2.0 + x_15) > (20.0 + x_17)? (2.0 + x_15) : (20.0 + x_17))? (17.0 + x_14) : ((2.0 + x_15) > (20.0 + x_17)? (2.0 + x_15) : (20.0 + x_17))) : ((10.0 + x_21) > ((18.0 + x_22) > (11.0 + x_23)? (18.0 + x_22) : (11.0 + x_23))? (10.0 + x_21) : ((18.0 + x_22) > (11.0 + x_23)? (18.0 + x_22) : (11.0 + x_23))))? (((19.0 + x_0) > ((16.0 + x_1) > (13.0 + x_2)? (16.0 + x_1) : (13.0 + x_2))? (19.0 + x_0) : ((16.0 + x_1) > (13.0 + x_2)? (16.0 + x_1) : (13.0 + x_2))) > ((3.0 + x_5) > ((4.0 + x_12) > (10.0 + x_13)? (4.0 + x_12) : (10.0 + x_13))? (3.0 + x_5) : ((4.0 + x_12) > (10.0 + x_13)? (4.0 + x_12) : (10.0 + x_13)))? ((19.0 + x_0) > ((16.0 + x_1) > (13.0 + x_2)? (16.0 + x_1) : (13.0 + x_2))? (19.0 + x_0) : ((16.0 + x_1) > (13.0 + x_2)? (16.0 + x_1) : (13.0 + x_2))) : ((3.0 + x_5) > ((4.0 + x_12) > (10.0 + x_13)? (4.0 + x_12) : (10.0 + x_13))? (3.0 + x_5) : ((4.0 + x_12) > (10.0 + x_13)? (4.0 + x_12) : (10.0 + x_13)))) : (((17.0 + x_14) > ((2.0 + x_15) > (20.0 + x_17)? (2.0 + x_15) : (20.0 + x_17))? (17.0 + x_14) : ((2.0 + x_15) > (20.0 + x_17)? (2.0 + x_15) : (20.0 + x_17))) > ((10.0 + x_21) > ((18.0 + x_22) > (11.0 + x_23)? (18.0 + x_22) : (11.0 + x_23))? (10.0 + x_21) : ((18.0 + x_22) > (11.0 + x_23)? (18.0 + x_22) : (11.0 + x_23)))? ((17.0 + x_14) > ((2.0 + x_15) > (20.0 + x_17)? (2.0 + x_15) : (20.0 + x_17))? (17.0 + x_14) : ((2.0 + x_15) > (20.0 + x_17)? (2.0 + x_15) : (20.0 + x_17))) : ((10.0 + x_21) > ((18.0 + x_22) > (11.0 + x_23)? (18.0 + x_22) : (11.0 + x_23))? (10.0 + x_21) : ((18.0 + x_22) > (11.0 + x_23)? (18.0 + x_22) : (11.0 + x_23)))));
  x_1_ = ((((10.0 + x_3) > ((12.0 + x_4) > (9.0 + x_5)? (12.0 + x_4) : (9.0 + x_5))? (10.0 + x_3) : ((12.0 + x_4) > (9.0 + x_5)? (12.0 + x_4) : (9.0 + x_5))) > ((13.0 + x_9) > ((14.0 + x_10) > (9.0 + x_11)? (14.0 + x_10) : (9.0 + x_11))? (13.0 + x_9) : ((14.0 + x_10) > (9.0 + x_11)? (14.0 + x_10) : (9.0 + x_11)))? ((10.0 + x_3) > ((12.0 + x_4) > (9.0 + x_5)? (12.0 + x_4) : (9.0 + x_5))? (10.0 + x_3) : ((12.0 + x_4) > (9.0 + x_5)? (12.0 + x_4) : (9.0 + x_5))) : ((13.0 + x_9) > ((14.0 + x_10) > (9.0 + x_11)? (14.0 + x_10) : (9.0 + x_11))? (13.0 + x_9) : ((14.0 + x_10) > (9.0 + x_11)? (14.0 + x_10) : (9.0 + x_11)))) > (((14.0 + x_12) > ((12.0 + x_13) > (14.0 + x_16)? (12.0 + x_13) : (14.0 + x_16))? (14.0 + x_12) : ((12.0 + x_13) > (14.0 + x_16)? (12.0 + x_13) : (14.0 + x_16))) > ((2.0 + x_18) > ((20.0 + x_20) > (18.0 + x_21)? (20.0 + x_20) : (18.0 + x_21))? (2.0 + x_18) : ((20.0 + x_20) > (18.0 + x_21)? (20.0 + x_20) : (18.0 + x_21)))? ((14.0 + x_12) > ((12.0 + x_13) > (14.0 + x_16)? (12.0 + x_13) : (14.0 + x_16))? (14.0 + x_12) : ((12.0 + x_13) > (14.0 + x_16)? (12.0 + x_13) : (14.0 + x_16))) : ((2.0 + x_18) > ((20.0 + x_20) > (18.0 + x_21)? (20.0 + x_20) : (18.0 + x_21))? (2.0 + x_18) : ((20.0 + x_20) > (18.0 + x_21)? (20.0 + x_20) : (18.0 + x_21))))? (((10.0 + x_3) > ((12.0 + x_4) > (9.0 + x_5)? (12.0 + x_4) : (9.0 + x_5))? (10.0 + x_3) : ((12.0 + x_4) > (9.0 + x_5)? (12.0 + x_4) : (9.0 + x_5))) > ((13.0 + x_9) > ((14.0 + x_10) > (9.0 + x_11)? (14.0 + x_10) : (9.0 + x_11))? (13.0 + x_9) : ((14.0 + x_10) > (9.0 + x_11)? (14.0 + x_10) : (9.0 + x_11)))? ((10.0 + x_3) > ((12.0 + x_4) > (9.0 + x_5)? (12.0 + x_4) : (9.0 + x_5))? (10.0 + x_3) : ((12.0 + x_4) > (9.0 + x_5)? (12.0 + x_4) : (9.0 + x_5))) : ((13.0 + x_9) > ((14.0 + x_10) > (9.0 + x_11)? (14.0 + x_10) : (9.0 + x_11))? (13.0 + x_9) : ((14.0 + x_10) > (9.0 + x_11)? (14.0 + x_10) : (9.0 + x_11)))) : (((14.0 + x_12) > ((12.0 + x_13) > (14.0 + x_16)? (12.0 + x_13) : (14.0 + x_16))? (14.0 + x_12) : ((12.0 + x_13) > (14.0 + x_16)? (12.0 + x_13) : (14.0 + x_16))) > ((2.0 + x_18) > ((20.0 + x_20) > (18.0 + x_21)? (20.0 + x_20) : (18.0 + x_21))? (2.0 + x_18) : ((20.0 + x_20) > (18.0 + x_21)? (20.0 + x_20) : (18.0 + x_21)))? ((14.0 + x_12) > ((12.0 + x_13) > (14.0 + x_16)? (12.0 + x_13) : (14.0 + x_16))? (14.0 + x_12) : ((12.0 + x_13) > (14.0 + x_16)? (12.0 + x_13) : (14.0 + x_16))) : ((2.0 + x_18) > ((20.0 + x_20) > (18.0 + x_21)? (20.0 + x_20) : (18.0 + x_21))? (2.0 + x_18) : ((20.0 + x_20) > (18.0 + x_21)? (20.0 + x_20) : (18.0 + x_21)))));
  x_2_ = ((((12.0 + x_1) > ((6.0 + x_3) > (6.0 + x_8)? (6.0 + x_3) : (6.0 + x_8))? (12.0 + x_1) : ((6.0 + x_3) > (6.0 + x_8)? (6.0 + x_3) : (6.0 + x_8))) > ((11.0 + x_10) > ((6.0 + x_12) > (20.0 + x_13)? (6.0 + x_12) : (20.0 + x_13))? (11.0 + x_10) : ((6.0 + x_12) > (20.0 + x_13)? (6.0 + x_12) : (20.0 + x_13)))? ((12.0 + x_1) > ((6.0 + x_3) > (6.0 + x_8)? (6.0 + x_3) : (6.0 + x_8))? (12.0 + x_1) : ((6.0 + x_3) > (6.0 + x_8)? (6.0 + x_3) : (6.0 + x_8))) : ((11.0 + x_10) > ((6.0 + x_12) > (20.0 + x_13)? (6.0 + x_12) : (20.0 + x_13))? (11.0 + x_10) : ((6.0 + x_12) > (20.0 + x_13)? (6.0 + x_12) : (20.0 + x_13)))) > (((6.0 + x_15) > ((19.0 + x_16) > (13.0 + x_17)? (19.0 + x_16) : (13.0 + x_17))? (6.0 + x_15) : ((19.0 + x_16) > (13.0 + x_17)? (19.0 + x_16) : (13.0 + x_17))) > ((3.0 + x_18) > ((10.0 + x_19) > (5.0 + x_21)? (10.0 + x_19) : (5.0 + x_21))? (3.0 + x_18) : ((10.0 + x_19) > (5.0 + x_21)? (10.0 + x_19) : (5.0 + x_21)))? ((6.0 + x_15) > ((19.0 + x_16) > (13.0 + x_17)? (19.0 + x_16) : (13.0 + x_17))? (6.0 + x_15) : ((19.0 + x_16) > (13.0 + x_17)? (19.0 + x_16) : (13.0 + x_17))) : ((3.0 + x_18) > ((10.0 + x_19) > (5.0 + x_21)? (10.0 + x_19) : (5.0 + x_21))? (3.0 + x_18) : ((10.0 + x_19) > (5.0 + x_21)? (10.0 + x_19) : (5.0 + x_21))))? (((12.0 + x_1) > ((6.0 + x_3) > (6.0 + x_8)? (6.0 + x_3) : (6.0 + x_8))? (12.0 + x_1) : ((6.0 + x_3) > (6.0 + x_8)? (6.0 + x_3) : (6.0 + x_8))) > ((11.0 + x_10) > ((6.0 + x_12) > (20.0 + x_13)? (6.0 + x_12) : (20.0 + x_13))? (11.0 + x_10) : ((6.0 + x_12) > (20.0 + x_13)? (6.0 + x_12) : (20.0 + x_13)))? ((12.0 + x_1) > ((6.0 + x_3) > (6.0 + x_8)? (6.0 + x_3) : (6.0 + x_8))? (12.0 + x_1) : ((6.0 + x_3) > (6.0 + x_8)? (6.0 + x_3) : (6.0 + x_8))) : ((11.0 + x_10) > ((6.0 + x_12) > (20.0 + x_13)? (6.0 + x_12) : (20.0 + x_13))? (11.0 + x_10) : ((6.0 + x_12) > (20.0 + x_13)? (6.0 + x_12) : (20.0 + x_13)))) : (((6.0 + x_15) > ((19.0 + x_16) > (13.0 + x_17)? (19.0 + x_16) : (13.0 + x_17))? (6.0 + x_15) : ((19.0 + x_16) > (13.0 + x_17)? (19.0 + x_16) : (13.0 + x_17))) > ((3.0 + x_18) > ((10.0 + x_19) > (5.0 + x_21)? (10.0 + x_19) : (5.0 + x_21))? (3.0 + x_18) : ((10.0 + x_19) > (5.0 + x_21)? (10.0 + x_19) : (5.0 + x_21)))? ((6.0 + x_15) > ((19.0 + x_16) > (13.0 + x_17)? (19.0 + x_16) : (13.0 + x_17))? (6.0 + x_15) : ((19.0 + x_16) > (13.0 + x_17)? (19.0 + x_16) : (13.0 + x_17))) : ((3.0 + x_18) > ((10.0 + x_19) > (5.0 + x_21)? (10.0 + x_19) : (5.0 + x_21))? (3.0 + x_18) : ((10.0 + x_19) > (5.0 + x_21)? (10.0 + x_19) : (5.0 + x_21)))));
  x_3_ = ((((19.0 + x_1) > ((2.0 + x_2) > (6.0 + x_7)? (2.0 + x_2) : (6.0 + x_7))? (19.0 + x_1) : ((2.0 + x_2) > (6.0 + x_7)? (2.0 + x_2) : (6.0 + x_7))) > ((19.0 + x_8) > ((10.0 + x_10) > (9.0 + x_13)? (10.0 + x_10) : (9.0 + x_13))? (19.0 + x_8) : ((10.0 + x_10) > (9.0 + x_13)? (10.0 + x_10) : (9.0 + x_13)))? ((19.0 + x_1) > ((2.0 + x_2) > (6.0 + x_7)? (2.0 + x_2) : (6.0 + x_7))? (19.0 + x_1) : ((2.0 + x_2) > (6.0 + x_7)? (2.0 + x_2) : (6.0 + x_7))) : ((19.0 + x_8) > ((10.0 + x_10) > (9.0 + x_13)? (10.0 + x_10) : (9.0 + x_13))? (19.0 + x_8) : ((10.0 + x_10) > (9.0 + x_13)? (10.0 + x_10) : (9.0 + x_13)))) > (((19.0 + x_14) > ((15.0 + x_15) > (1.0 + x_16)? (15.0 + x_15) : (1.0 + x_16))? (19.0 + x_14) : ((15.0 + x_15) > (1.0 + x_16)? (15.0 + x_15) : (1.0 + x_16))) > ((11.0 + x_17) > ((11.0 + x_20) > (12.0 + x_21)? (11.0 + x_20) : (12.0 + x_21))? (11.0 + x_17) : ((11.0 + x_20) > (12.0 + x_21)? (11.0 + x_20) : (12.0 + x_21)))? ((19.0 + x_14) > ((15.0 + x_15) > (1.0 + x_16)? (15.0 + x_15) : (1.0 + x_16))? (19.0 + x_14) : ((15.0 + x_15) > (1.0 + x_16)? (15.0 + x_15) : (1.0 + x_16))) : ((11.0 + x_17) > ((11.0 + x_20) > (12.0 + x_21)? (11.0 + x_20) : (12.0 + x_21))? (11.0 + x_17) : ((11.0 + x_20) > (12.0 + x_21)? (11.0 + x_20) : (12.0 + x_21))))? (((19.0 + x_1) > ((2.0 + x_2) > (6.0 + x_7)? (2.0 + x_2) : (6.0 + x_7))? (19.0 + x_1) : ((2.0 + x_2) > (6.0 + x_7)? (2.0 + x_2) : (6.0 + x_7))) > ((19.0 + x_8) > ((10.0 + x_10) > (9.0 + x_13)? (10.0 + x_10) : (9.0 + x_13))? (19.0 + x_8) : ((10.0 + x_10) > (9.0 + x_13)? (10.0 + x_10) : (9.0 + x_13)))? ((19.0 + x_1) > ((2.0 + x_2) > (6.0 + x_7)? (2.0 + x_2) : (6.0 + x_7))? (19.0 + x_1) : ((2.0 + x_2) > (6.0 + x_7)? (2.0 + x_2) : (6.0 + x_7))) : ((19.0 + x_8) > ((10.0 + x_10) > (9.0 + x_13)? (10.0 + x_10) : (9.0 + x_13))? (19.0 + x_8) : ((10.0 + x_10) > (9.0 + x_13)? (10.0 + x_10) : (9.0 + x_13)))) : (((19.0 + x_14) > ((15.0 + x_15) > (1.0 + x_16)? (15.0 + x_15) : (1.0 + x_16))? (19.0 + x_14) : ((15.0 + x_15) > (1.0 + x_16)? (15.0 + x_15) : (1.0 + x_16))) > ((11.0 + x_17) > ((11.0 + x_20) > (12.0 + x_21)? (11.0 + x_20) : (12.0 + x_21))? (11.0 + x_17) : ((11.0 + x_20) > (12.0 + x_21)? (11.0 + x_20) : (12.0 + x_21)))? ((19.0 + x_14) > ((15.0 + x_15) > (1.0 + x_16)? (15.0 + x_15) : (1.0 + x_16))? (19.0 + x_14) : ((15.0 + x_15) > (1.0 + x_16)? (15.0 + x_15) : (1.0 + x_16))) : ((11.0 + x_17) > ((11.0 + x_20) > (12.0 + x_21)? (11.0 + x_20) : (12.0 + x_21))? (11.0 + x_17) : ((11.0 + x_20) > (12.0 + x_21)? (11.0 + x_20) : (12.0 + x_21)))));
  x_4_ = ((((17.0 + x_3) > ((4.0 + x_7) > (6.0 + x_9)? (4.0 + x_7) : (6.0 + x_9))? (17.0 + x_3) : ((4.0 + x_7) > (6.0 + x_9)? (4.0 + x_7) : (6.0 + x_9))) > ((18.0 + x_11) > ((15.0 + x_12) > (17.0 + x_13)? (15.0 + x_12) : (17.0 + x_13))? (18.0 + x_11) : ((15.0 + x_12) > (17.0 + x_13)? (15.0 + x_12) : (17.0 + x_13)))? ((17.0 + x_3) > ((4.0 + x_7) > (6.0 + x_9)? (4.0 + x_7) : (6.0 + x_9))? (17.0 + x_3) : ((4.0 + x_7) > (6.0 + x_9)? (4.0 + x_7) : (6.0 + x_9))) : ((18.0 + x_11) > ((15.0 + x_12) > (17.0 + x_13)? (15.0 + x_12) : (17.0 + x_13))? (18.0 + x_11) : ((15.0 + x_12) > (17.0 + x_13)? (15.0 + x_12) : (17.0 + x_13)))) > (((13.0 + x_15) > ((19.0 + x_17) > (2.0 + x_18)? (19.0 + x_17) : (2.0 + x_18))? (13.0 + x_15) : ((19.0 + x_17) > (2.0 + x_18)? (19.0 + x_17) : (2.0 + x_18))) > ((16.0 + x_19) > ((8.0 + x_20) > (17.0 + x_22)? (8.0 + x_20) : (17.0 + x_22))? (16.0 + x_19) : ((8.0 + x_20) > (17.0 + x_22)? (8.0 + x_20) : (17.0 + x_22)))? ((13.0 + x_15) > ((19.0 + x_17) > (2.0 + x_18)? (19.0 + x_17) : (2.0 + x_18))? (13.0 + x_15) : ((19.0 + x_17) > (2.0 + x_18)? (19.0 + x_17) : (2.0 + x_18))) : ((16.0 + x_19) > ((8.0 + x_20) > (17.0 + x_22)? (8.0 + x_20) : (17.0 + x_22))? (16.0 + x_19) : ((8.0 + x_20) > (17.0 + x_22)? (8.0 + x_20) : (17.0 + x_22))))? (((17.0 + x_3) > ((4.0 + x_7) > (6.0 + x_9)? (4.0 + x_7) : (6.0 + x_9))? (17.0 + x_3) : ((4.0 + x_7) > (6.0 + x_9)? (4.0 + x_7) : (6.0 + x_9))) > ((18.0 + x_11) > ((15.0 + x_12) > (17.0 + x_13)? (15.0 + x_12) : (17.0 + x_13))? (18.0 + x_11) : ((15.0 + x_12) > (17.0 + x_13)? (15.0 + x_12) : (17.0 + x_13)))? ((17.0 + x_3) > ((4.0 + x_7) > (6.0 + x_9)? (4.0 + x_7) : (6.0 + x_9))? (17.0 + x_3) : ((4.0 + x_7) > (6.0 + x_9)? (4.0 + x_7) : (6.0 + x_9))) : ((18.0 + x_11) > ((15.0 + x_12) > (17.0 + x_13)? (15.0 + x_12) : (17.0 + x_13))? (18.0 + x_11) : ((15.0 + x_12) > (17.0 + x_13)? (15.0 + x_12) : (17.0 + x_13)))) : (((13.0 + x_15) > ((19.0 + x_17) > (2.0 + x_18)? (19.0 + x_17) : (2.0 + x_18))? (13.0 + x_15) : ((19.0 + x_17) > (2.0 + x_18)? (19.0 + x_17) : (2.0 + x_18))) > ((16.0 + x_19) > ((8.0 + x_20) > (17.0 + x_22)? (8.0 + x_20) : (17.0 + x_22))? (16.0 + x_19) : ((8.0 + x_20) > (17.0 + x_22)? (8.0 + x_20) : (17.0 + x_22)))? ((13.0 + x_15) > ((19.0 + x_17) > (2.0 + x_18)? (19.0 + x_17) : (2.0 + x_18))? (13.0 + x_15) : ((19.0 + x_17) > (2.0 + x_18)? (19.0 + x_17) : (2.0 + x_18))) : ((16.0 + x_19) > ((8.0 + x_20) > (17.0 + x_22)? (8.0 + x_20) : (17.0 + x_22))? (16.0 + x_19) : ((8.0 + x_20) > (17.0 + x_22)? (8.0 + x_20) : (17.0 + x_22)))));
  x_5_ = ((((7.0 + x_2) > ((10.0 + x_3) > (10.0 + x_5)? (10.0 + x_3) : (10.0 + x_5))? (7.0 + x_2) : ((10.0 + x_3) > (10.0 + x_5)? (10.0 + x_3) : (10.0 + x_5))) > ((1.0 + x_7) > ((13.0 + x_9) > (7.0 + x_10)? (13.0 + x_9) : (7.0 + x_10))? (1.0 + x_7) : ((13.0 + x_9) > (7.0 + x_10)? (13.0 + x_9) : (7.0 + x_10)))? ((7.0 + x_2) > ((10.0 + x_3) > (10.0 + x_5)? (10.0 + x_3) : (10.0 + x_5))? (7.0 + x_2) : ((10.0 + x_3) > (10.0 + x_5)? (10.0 + x_3) : (10.0 + x_5))) : ((1.0 + x_7) > ((13.0 + x_9) > (7.0 + x_10)? (13.0 + x_9) : (7.0 + x_10))? (1.0 + x_7) : ((13.0 + x_9) > (7.0 + x_10)? (13.0 + x_9) : (7.0 + x_10)))) > (((7.0 + x_12) > ((7.0 + x_13) > (16.0 + x_15)? (7.0 + x_13) : (16.0 + x_15))? (7.0 + x_12) : ((7.0 + x_13) > (16.0 + x_15)? (7.0 + x_13) : (16.0 + x_15))) > ((2.0 + x_16) > ((9.0 + x_17) > (16.0 + x_23)? (9.0 + x_17) : (16.0 + x_23))? (2.0 + x_16) : ((9.0 + x_17) > (16.0 + x_23)? (9.0 + x_17) : (16.0 + x_23)))? ((7.0 + x_12) > ((7.0 + x_13) > (16.0 + x_15)? (7.0 + x_13) : (16.0 + x_15))? (7.0 + x_12) : ((7.0 + x_13) > (16.0 + x_15)? (7.0 + x_13) : (16.0 + x_15))) : ((2.0 + x_16) > ((9.0 + x_17) > (16.0 + x_23)? (9.0 + x_17) : (16.0 + x_23))? (2.0 + x_16) : ((9.0 + x_17) > (16.0 + x_23)? (9.0 + x_17) : (16.0 + x_23))))? (((7.0 + x_2) > ((10.0 + x_3) > (10.0 + x_5)? (10.0 + x_3) : (10.0 + x_5))? (7.0 + x_2) : ((10.0 + x_3) > (10.0 + x_5)? (10.0 + x_3) : (10.0 + x_5))) > ((1.0 + x_7) > ((13.0 + x_9) > (7.0 + x_10)? (13.0 + x_9) : (7.0 + x_10))? (1.0 + x_7) : ((13.0 + x_9) > (7.0 + x_10)? (13.0 + x_9) : (7.0 + x_10)))? ((7.0 + x_2) > ((10.0 + x_3) > (10.0 + x_5)? (10.0 + x_3) : (10.0 + x_5))? (7.0 + x_2) : ((10.0 + x_3) > (10.0 + x_5)? (10.0 + x_3) : (10.0 + x_5))) : ((1.0 + x_7) > ((13.0 + x_9) > (7.0 + x_10)? (13.0 + x_9) : (7.0 + x_10))? (1.0 + x_7) : ((13.0 + x_9) > (7.0 + x_10)? (13.0 + x_9) : (7.0 + x_10)))) : (((7.0 + x_12) > ((7.0 + x_13) > (16.0 + x_15)? (7.0 + x_13) : (16.0 + x_15))? (7.0 + x_12) : ((7.0 + x_13) > (16.0 + x_15)? (7.0 + x_13) : (16.0 + x_15))) > ((2.0 + x_16) > ((9.0 + x_17) > (16.0 + x_23)? (9.0 + x_17) : (16.0 + x_23))? (2.0 + x_16) : ((9.0 + x_17) > (16.0 + x_23)? (9.0 + x_17) : (16.0 + x_23)))? ((7.0 + x_12) > ((7.0 + x_13) > (16.0 + x_15)? (7.0 + x_13) : (16.0 + x_15))? (7.0 + x_12) : ((7.0 + x_13) > (16.0 + x_15)? (7.0 + x_13) : (16.0 + x_15))) : ((2.0 + x_16) > ((9.0 + x_17) > (16.0 + x_23)? (9.0 + x_17) : (16.0 + x_23))? (2.0 + x_16) : ((9.0 + x_17) > (16.0 + x_23)? (9.0 + x_17) : (16.0 + x_23)))));
  x_6_ = ((((5.0 + x_2) > ((16.0 + x_6) > (17.0 + x_7)? (16.0 + x_6) : (17.0 + x_7))? (5.0 + x_2) : ((16.0 + x_6) > (17.0 + x_7)? (16.0 + x_6) : (17.0 + x_7))) > ((18.0 + x_9) > ((1.0 + x_10) > (15.0 + x_11)? (1.0 + x_10) : (15.0 + x_11))? (18.0 + x_9) : ((1.0 + x_10) > (15.0 + x_11)? (1.0 + x_10) : (15.0 + x_11)))? ((5.0 + x_2) > ((16.0 + x_6) > (17.0 + x_7)? (16.0 + x_6) : (17.0 + x_7))? (5.0 + x_2) : ((16.0 + x_6) > (17.0 + x_7)? (16.0 + x_6) : (17.0 + x_7))) : ((18.0 + x_9) > ((1.0 + x_10) > (15.0 + x_11)? (1.0 + x_10) : (15.0 + x_11))? (18.0 + x_9) : ((1.0 + x_10) > (15.0 + x_11)? (1.0 + x_10) : (15.0 + x_11)))) > (((14.0 + x_12) > ((18.0 + x_14) > (20.0 + x_20)? (18.0 + x_14) : (20.0 + x_20))? (14.0 + x_12) : ((18.0 + x_14) > (20.0 + x_20)? (18.0 + x_14) : (20.0 + x_20))) > ((6.0 + x_21) > ((1.0 + x_22) > (4.0 + x_23)? (1.0 + x_22) : (4.0 + x_23))? (6.0 + x_21) : ((1.0 + x_22) > (4.0 + x_23)? (1.0 + x_22) : (4.0 + x_23)))? ((14.0 + x_12) > ((18.0 + x_14) > (20.0 + x_20)? (18.0 + x_14) : (20.0 + x_20))? (14.0 + x_12) : ((18.0 + x_14) > (20.0 + x_20)? (18.0 + x_14) : (20.0 + x_20))) : ((6.0 + x_21) > ((1.0 + x_22) > (4.0 + x_23)? (1.0 + x_22) : (4.0 + x_23))? (6.0 + x_21) : ((1.0 + x_22) > (4.0 + x_23)? (1.0 + x_22) : (4.0 + x_23))))? (((5.0 + x_2) > ((16.0 + x_6) > (17.0 + x_7)? (16.0 + x_6) : (17.0 + x_7))? (5.0 + x_2) : ((16.0 + x_6) > (17.0 + x_7)? (16.0 + x_6) : (17.0 + x_7))) > ((18.0 + x_9) > ((1.0 + x_10) > (15.0 + x_11)? (1.0 + x_10) : (15.0 + x_11))? (18.0 + x_9) : ((1.0 + x_10) > (15.0 + x_11)? (1.0 + x_10) : (15.0 + x_11)))? ((5.0 + x_2) > ((16.0 + x_6) > (17.0 + x_7)? (16.0 + x_6) : (17.0 + x_7))? (5.0 + x_2) : ((16.0 + x_6) > (17.0 + x_7)? (16.0 + x_6) : (17.0 + x_7))) : ((18.0 + x_9) > ((1.0 + x_10) > (15.0 + x_11)? (1.0 + x_10) : (15.0 + x_11))? (18.0 + x_9) : ((1.0 + x_10) > (15.0 + x_11)? (1.0 + x_10) : (15.0 + x_11)))) : (((14.0 + x_12) > ((18.0 + x_14) > (20.0 + x_20)? (18.0 + x_14) : (20.0 + x_20))? (14.0 + x_12) : ((18.0 + x_14) > (20.0 + x_20)? (18.0 + x_14) : (20.0 + x_20))) > ((6.0 + x_21) > ((1.0 + x_22) > (4.0 + x_23)? (1.0 + x_22) : (4.0 + x_23))? (6.0 + x_21) : ((1.0 + x_22) > (4.0 + x_23)? (1.0 + x_22) : (4.0 + x_23)))? ((14.0 + x_12) > ((18.0 + x_14) > (20.0 + x_20)? (18.0 + x_14) : (20.0 + x_20))? (14.0 + x_12) : ((18.0 + x_14) > (20.0 + x_20)? (18.0 + x_14) : (20.0 + x_20))) : ((6.0 + x_21) > ((1.0 + x_22) > (4.0 + x_23)? (1.0 + x_22) : (4.0 + x_23))? (6.0 + x_21) : ((1.0 + x_22) > (4.0 + x_23)? (1.0 + x_22) : (4.0 + x_23)))));
  x_7_ = ((((17.0 + x_3) > ((15.0 + x_5) > (11.0 + x_6)? (15.0 + x_5) : (11.0 + x_6))? (17.0 + x_3) : ((15.0 + x_5) > (11.0 + x_6)? (15.0 + x_5) : (11.0 + x_6))) > ((19.0 + x_11) > ((8.0 + x_12) > (1.0 + x_13)? (8.0 + x_12) : (1.0 + x_13))? (19.0 + x_11) : ((8.0 + x_12) > (1.0 + x_13)? (8.0 + x_12) : (1.0 + x_13)))? ((17.0 + x_3) > ((15.0 + x_5) > (11.0 + x_6)? (15.0 + x_5) : (11.0 + x_6))? (17.0 + x_3) : ((15.0 + x_5) > (11.0 + x_6)? (15.0 + x_5) : (11.0 + x_6))) : ((19.0 + x_11) > ((8.0 + x_12) > (1.0 + x_13)? (8.0 + x_12) : (1.0 + x_13))? (19.0 + x_11) : ((8.0 + x_12) > (1.0 + x_13)? (8.0 + x_12) : (1.0 + x_13)))) > (((5.0 + x_15) > ((10.0 + x_16) > (20.0 + x_17)? (10.0 + x_16) : (20.0 + x_17))? (5.0 + x_15) : ((10.0 + x_16) > (20.0 + x_17)? (10.0 + x_16) : (20.0 + x_17))) > ((7.0 + x_19) > ((7.0 + x_20) > (1.0 + x_21)? (7.0 + x_20) : (1.0 + x_21))? (7.0 + x_19) : ((7.0 + x_20) > (1.0 + x_21)? (7.0 + x_20) : (1.0 + x_21)))? ((5.0 + x_15) > ((10.0 + x_16) > (20.0 + x_17)? (10.0 + x_16) : (20.0 + x_17))? (5.0 + x_15) : ((10.0 + x_16) > (20.0 + x_17)? (10.0 + x_16) : (20.0 + x_17))) : ((7.0 + x_19) > ((7.0 + x_20) > (1.0 + x_21)? (7.0 + x_20) : (1.0 + x_21))? (7.0 + x_19) : ((7.0 + x_20) > (1.0 + x_21)? (7.0 + x_20) : (1.0 + x_21))))? (((17.0 + x_3) > ((15.0 + x_5) > (11.0 + x_6)? (15.0 + x_5) : (11.0 + x_6))? (17.0 + x_3) : ((15.0 + x_5) > (11.0 + x_6)? (15.0 + x_5) : (11.0 + x_6))) > ((19.0 + x_11) > ((8.0 + x_12) > (1.0 + x_13)? (8.0 + x_12) : (1.0 + x_13))? (19.0 + x_11) : ((8.0 + x_12) > (1.0 + x_13)? (8.0 + x_12) : (1.0 + x_13)))? ((17.0 + x_3) > ((15.0 + x_5) > (11.0 + x_6)? (15.0 + x_5) : (11.0 + x_6))? (17.0 + x_3) : ((15.0 + x_5) > (11.0 + x_6)? (15.0 + x_5) : (11.0 + x_6))) : ((19.0 + x_11) > ((8.0 + x_12) > (1.0 + x_13)? (8.0 + x_12) : (1.0 + x_13))? (19.0 + x_11) : ((8.0 + x_12) > (1.0 + x_13)? (8.0 + x_12) : (1.0 + x_13)))) : (((5.0 + x_15) > ((10.0 + x_16) > (20.0 + x_17)? (10.0 + x_16) : (20.0 + x_17))? (5.0 + x_15) : ((10.0 + x_16) > (20.0 + x_17)? (10.0 + x_16) : (20.0 + x_17))) > ((7.0 + x_19) > ((7.0 + x_20) > (1.0 + x_21)? (7.0 + x_20) : (1.0 + x_21))? (7.0 + x_19) : ((7.0 + x_20) > (1.0 + x_21)? (7.0 + x_20) : (1.0 + x_21)))? ((5.0 + x_15) > ((10.0 + x_16) > (20.0 + x_17)? (10.0 + x_16) : (20.0 + x_17))? (5.0 + x_15) : ((10.0 + x_16) > (20.0 + x_17)? (10.0 + x_16) : (20.0 + x_17))) : ((7.0 + x_19) > ((7.0 + x_20) > (1.0 + x_21)? (7.0 + x_20) : (1.0 + x_21))? (7.0 + x_19) : ((7.0 + x_20) > (1.0 + x_21)? (7.0 + x_20) : (1.0 + x_21)))));
  x_8_ = ((((4.0 + x_0) > ((3.0 + x_2) > (12.0 + x_3)? (3.0 + x_2) : (12.0 + x_3))? (4.0 + x_0) : ((3.0 + x_2) > (12.0 + x_3)? (3.0 + x_2) : (12.0 + x_3))) > ((11.0 + x_4) > ((8.0 + x_5) > (2.0 + x_8)? (8.0 + x_5) : (2.0 + x_8))? (11.0 + x_4) : ((8.0 + x_5) > (2.0 + x_8)? (8.0 + x_5) : (2.0 + x_8)))? ((4.0 + x_0) > ((3.0 + x_2) > (12.0 + x_3)? (3.0 + x_2) : (12.0 + x_3))? (4.0 + x_0) : ((3.0 + x_2) > (12.0 + x_3)? (3.0 + x_2) : (12.0 + x_3))) : ((11.0 + x_4) > ((8.0 + x_5) > (2.0 + x_8)? (8.0 + x_5) : (2.0 + x_8))? (11.0 + x_4) : ((8.0 + x_5) > (2.0 + x_8)? (8.0 + x_5) : (2.0 + x_8)))) > (((13.0 + x_11) > ((9.0 + x_12) > (18.0 + x_13)? (9.0 + x_12) : (18.0 + x_13))? (13.0 + x_11) : ((9.0 + x_12) > (18.0 + x_13)? (9.0 + x_12) : (18.0 + x_13))) > ((14.0 + x_14) > ((4.0 + x_17) > (3.0 + x_19)? (4.0 + x_17) : (3.0 + x_19))? (14.0 + x_14) : ((4.0 + x_17) > (3.0 + x_19)? (4.0 + x_17) : (3.0 + x_19)))? ((13.0 + x_11) > ((9.0 + x_12) > (18.0 + x_13)? (9.0 + x_12) : (18.0 + x_13))? (13.0 + x_11) : ((9.0 + x_12) > (18.0 + x_13)? (9.0 + x_12) : (18.0 + x_13))) : ((14.0 + x_14) > ((4.0 + x_17) > (3.0 + x_19)? (4.0 + x_17) : (3.0 + x_19))? (14.0 + x_14) : ((4.0 + x_17) > (3.0 + x_19)? (4.0 + x_17) : (3.0 + x_19))))? (((4.0 + x_0) > ((3.0 + x_2) > (12.0 + x_3)? (3.0 + x_2) : (12.0 + x_3))? (4.0 + x_0) : ((3.0 + x_2) > (12.0 + x_3)? (3.0 + x_2) : (12.0 + x_3))) > ((11.0 + x_4) > ((8.0 + x_5) > (2.0 + x_8)? (8.0 + x_5) : (2.0 + x_8))? (11.0 + x_4) : ((8.0 + x_5) > (2.0 + x_8)? (8.0 + x_5) : (2.0 + x_8)))? ((4.0 + x_0) > ((3.0 + x_2) > (12.0 + x_3)? (3.0 + x_2) : (12.0 + x_3))? (4.0 + x_0) : ((3.0 + x_2) > (12.0 + x_3)? (3.0 + x_2) : (12.0 + x_3))) : ((11.0 + x_4) > ((8.0 + x_5) > (2.0 + x_8)? (8.0 + x_5) : (2.0 + x_8))? (11.0 + x_4) : ((8.0 + x_5) > (2.0 + x_8)? (8.0 + x_5) : (2.0 + x_8)))) : (((13.0 + x_11) > ((9.0 + x_12) > (18.0 + x_13)? (9.0 + x_12) : (18.0 + x_13))? (13.0 + x_11) : ((9.0 + x_12) > (18.0 + x_13)? (9.0 + x_12) : (18.0 + x_13))) > ((14.0 + x_14) > ((4.0 + x_17) > (3.0 + x_19)? (4.0 + x_17) : (3.0 + x_19))? (14.0 + x_14) : ((4.0 + x_17) > (3.0 + x_19)? (4.0 + x_17) : (3.0 + x_19)))? ((13.0 + x_11) > ((9.0 + x_12) > (18.0 + x_13)? (9.0 + x_12) : (18.0 + x_13))? (13.0 + x_11) : ((9.0 + x_12) > (18.0 + x_13)? (9.0 + x_12) : (18.0 + x_13))) : ((14.0 + x_14) > ((4.0 + x_17) > (3.0 + x_19)? (4.0 + x_17) : (3.0 + x_19))? (14.0 + x_14) : ((4.0 + x_17) > (3.0 + x_19)? (4.0 + x_17) : (3.0 + x_19)))));
  x_9_ = ((((13.0 + x_0) > ((13.0 + x_2) > (8.0 + x_5)? (13.0 + x_2) : (8.0 + x_5))? (13.0 + x_0) : ((13.0 + x_2) > (8.0 + x_5)? (13.0 + x_2) : (8.0 + x_5))) > ((12.0 + x_6) > ((6.0 + x_7) > (1.0 + x_8)? (6.0 + x_7) : (1.0 + x_8))? (12.0 + x_6) : ((6.0 + x_7) > (1.0 + x_8)? (6.0 + x_7) : (1.0 + x_8)))? ((13.0 + x_0) > ((13.0 + x_2) > (8.0 + x_5)? (13.0 + x_2) : (8.0 + x_5))? (13.0 + x_0) : ((13.0 + x_2) > (8.0 + x_5)? (13.0 + x_2) : (8.0 + x_5))) : ((12.0 + x_6) > ((6.0 + x_7) > (1.0 + x_8)? (6.0 + x_7) : (1.0 + x_8))? (12.0 + x_6) : ((6.0 + x_7) > (1.0 + x_8)? (6.0 + x_7) : (1.0 + x_8)))) > (((10.0 + x_9) > ((7.0 + x_13) > (7.0 + x_14)? (7.0 + x_13) : (7.0 + x_14))? (10.0 + x_9) : ((7.0 + x_13) > (7.0 + x_14)? (7.0 + x_13) : (7.0 + x_14))) > ((20.0 + x_16) > ((1.0 + x_20) > (16.0 + x_21)? (1.0 + x_20) : (16.0 + x_21))? (20.0 + x_16) : ((1.0 + x_20) > (16.0 + x_21)? (1.0 + x_20) : (16.0 + x_21)))? ((10.0 + x_9) > ((7.0 + x_13) > (7.0 + x_14)? (7.0 + x_13) : (7.0 + x_14))? (10.0 + x_9) : ((7.0 + x_13) > (7.0 + x_14)? (7.0 + x_13) : (7.0 + x_14))) : ((20.0 + x_16) > ((1.0 + x_20) > (16.0 + x_21)? (1.0 + x_20) : (16.0 + x_21))? (20.0 + x_16) : ((1.0 + x_20) > (16.0 + x_21)? (1.0 + x_20) : (16.0 + x_21))))? (((13.0 + x_0) > ((13.0 + x_2) > (8.0 + x_5)? (13.0 + x_2) : (8.0 + x_5))? (13.0 + x_0) : ((13.0 + x_2) > (8.0 + x_5)? (13.0 + x_2) : (8.0 + x_5))) > ((12.0 + x_6) > ((6.0 + x_7) > (1.0 + x_8)? (6.0 + x_7) : (1.0 + x_8))? (12.0 + x_6) : ((6.0 + x_7) > (1.0 + x_8)? (6.0 + x_7) : (1.0 + x_8)))? ((13.0 + x_0) > ((13.0 + x_2) > (8.0 + x_5)? (13.0 + x_2) : (8.0 + x_5))? (13.0 + x_0) : ((13.0 + x_2) > (8.0 + x_5)? (13.0 + x_2) : (8.0 + x_5))) : ((12.0 + x_6) > ((6.0 + x_7) > (1.0 + x_8)? (6.0 + x_7) : (1.0 + x_8))? (12.0 + x_6) : ((6.0 + x_7) > (1.0 + x_8)? (6.0 + x_7) : (1.0 + x_8)))) : (((10.0 + x_9) > ((7.0 + x_13) > (7.0 + x_14)? (7.0 + x_13) : (7.0 + x_14))? (10.0 + x_9) : ((7.0 + x_13) > (7.0 + x_14)? (7.0 + x_13) : (7.0 + x_14))) > ((20.0 + x_16) > ((1.0 + x_20) > (16.0 + x_21)? (1.0 + x_20) : (16.0 + x_21))? (20.0 + x_16) : ((1.0 + x_20) > (16.0 + x_21)? (1.0 + x_20) : (16.0 + x_21)))? ((10.0 + x_9) > ((7.0 + x_13) > (7.0 + x_14)? (7.0 + x_13) : (7.0 + x_14))? (10.0 + x_9) : ((7.0 + x_13) > (7.0 + x_14)? (7.0 + x_13) : (7.0 + x_14))) : ((20.0 + x_16) > ((1.0 + x_20) > (16.0 + x_21)? (1.0 + x_20) : (16.0 + x_21))? (20.0 + x_16) : ((1.0 + x_20) > (16.0 + x_21)? (1.0 + x_20) : (16.0 + x_21)))));
  x_10_ = ((((16.0 + x_1) > ((15.0 + x_3) > (1.0 + x_5)? (15.0 + x_3) : (1.0 + x_5))? (16.0 + x_1) : ((15.0 + x_3) > (1.0 + x_5)? (15.0 + x_3) : (1.0 + x_5))) > ((8.0 + x_6) > ((9.0 + x_7) > (3.0 + x_9)? (9.0 + x_7) : (3.0 + x_9))? (8.0 + x_6) : ((9.0 + x_7) > (3.0 + x_9)? (9.0 + x_7) : (3.0 + x_9)))? ((16.0 + x_1) > ((15.0 + x_3) > (1.0 + x_5)? (15.0 + x_3) : (1.0 + x_5))? (16.0 + x_1) : ((15.0 + x_3) > (1.0 + x_5)? (15.0 + x_3) : (1.0 + x_5))) : ((8.0 + x_6) > ((9.0 + x_7) > (3.0 + x_9)? (9.0 + x_7) : (3.0 + x_9))? (8.0 + x_6) : ((9.0 + x_7) > (3.0 + x_9)? (9.0 + x_7) : (3.0 + x_9)))) > (((10.0 + x_10) > ((13.0 + x_11) > (12.0 + x_13)? (13.0 + x_11) : (12.0 + x_13))? (10.0 + x_10) : ((13.0 + x_11) > (12.0 + x_13)? (13.0 + x_11) : (12.0 + x_13))) > ((3.0 + x_14) > ((12.0 + x_19) > (19.0 + x_20)? (12.0 + x_19) : (19.0 + x_20))? (3.0 + x_14) : ((12.0 + x_19) > (19.0 + x_20)? (12.0 + x_19) : (19.0 + x_20)))? ((10.0 + x_10) > ((13.0 + x_11) > (12.0 + x_13)? (13.0 + x_11) : (12.0 + x_13))? (10.0 + x_10) : ((13.0 + x_11) > (12.0 + x_13)? (13.0 + x_11) : (12.0 + x_13))) : ((3.0 + x_14) > ((12.0 + x_19) > (19.0 + x_20)? (12.0 + x_19) : (19.0 + x_20))? (3.0 + x_14) : ((12.0 + x_19) > (19.0 + x_20)? (12.0 + x_19) : (19.0 + x_20))))? (((16.0 + x_1) > ((15.0 + x_3) > (1.0 + x_5)? (15.0 + x_3) : (1.0 + x_5))? (16.0 + x_1) : ((15.0 + x_3) > (1.0 + x_5)? (15.0 + x_3) : (1.0 + x_5))) > ((8.0 + x_6) > ((9.0 + x_7) > (3.0 + x_9)? (9.0 + x_7) : (3.0 + x_9))? (8.0 + x_6) : ((9.0 + x_7) > (3.0 + x_9)? (9.0 + x_7) : (3.0 + x_9)))? ((16.0 + x_1) > ((15.0 + x_3) > (1.0 + x_5)? (15.0 + x_3) : (1.0 + x_5))? (16.0 + x_1) : ((15.0 + x_3) > (1.0 + x_5)? (15.0 + x_3) : (1.0 + x_5))) : ((8.0 + x_6) > ((9.0 + x_7) > (3.0 + x_9)? (9.0 + x_7) : (3.0 + x_9))? (8.0 + x_6) : ((9.0 + x_7) > (3.0 + x_9)? (9.0 + x_7) : (3.0 + x_9)))) : (((10.0 + x_10) > ((13.0 + x_11) > (12.0 + x_13)? (13.0 + x_11) : (12.0 + x_13))? (10.0 + x_10) : ((13.0 + x_11) > (12.0 + x_13)? (13.0 + x_11) : (12.0 + x_13))) > ((3.0 + x_14) > ((12.0 + x_19) > (19.0 + x_20)? (12.0 + x_19) : (19.0 + x_20))? (3.0 + x_14) : ((12.0 + x_19) > (19.0 + x_20)? (12.0 + x_19) : (19.0 + x_20)))? ((10.0 + x_10) > ((13.0 + x_11) > (12.0 + x_13)? (13.0 + x_11) : (12.0 + x_13))? (10.0 + x_10) : ((13.0 + x_11) > (12.0 + x_13)? (13.0 + x_11) : (12.0 + x_13))) : ((3.0 + x_14) > ((12.0 + x_19) > (19.0 + x_20)? (12.0 + x_19) : (19.0 + x_20))? (3.0 + x_14) : ((12.0 + x_19) > (19.0 + x_20)? (12.0 + x_19) : (19.0 + x_20)))));
  x_11_ = ((((17.0 + x_1) > ((12.0 + x_4) > (13.0 + x_5)? (12.0 + x_4) : (13.0 + x_5))? (17.0 + x_1) : ((12.0 + x_4) > (13.0 + x_5)? (12.0 + x_4) : (13.0 + x_5))) > ((7.0 + x_10) > ((6.0 + x_11) > (12.0 + x_12)? (6.0 + x_11) : (12.0 + x_12))? (7.0 + x_10) : ((6.0 + x_11) > (12.0 + x_12)? (6.0 + x_11) : (12.0 + x_12)))? ((17.0 + x_1) > ((12.0 + x_4) > (13.0 + x_5)? (12.0 + x_4) : (13.0 + x_5))? (17.0 + x_1) : ((12.0 + x_4) > (13.0 + x_5)? (12.0 + x_4) : (13.0 + x_5))) : ((7.0 + x_10) > ((6.0 + x_11) > (12.0 + x_12)? (6.0 + x_11) : (12.0 + x_12))? (7.0 + x_10) : ((6.0 + x_11) > (12.0 + x_12)? (6.0 + x_11) : (12.0 + x_12)))) > (((4.0 + x_13) > ((18.0 + x_14) > (3.0 + x_17)? (18.0 + x_14) : (3.0 + x_17))? (4.0 + x_13) : ((18.0 + x_14) > (3.0 + x_17)? (18.0 + x_14) : (3.0 + x_17))) > ((16.0 + x_18) > ((16.0 + x_19) > (11.0 + x_20)? (16.0 + x_19) : (11.0 + x_20))? (16.0 + x_18) : ((16.0 + x_19) > (11.0 + x_20)? (16.0 + x_19) : (11.0 + x_20)))? ((4.0 + x_13) > ((18.0 + x_14) > (3.0 + x_17)? (18.0 + x_14) : (3.0 + x_17))? (4.0 + x_13) : ((18.0 + x_14) > (3.0 + x_17)? (18.0 + x_14) : (3.0 + x_17))) : ((16.0 + x_18) > ((16.0 + x_19) > (11.0 + x_20)? (16.0 + x_19) : (11.0 + x_20))? (16.0 + x_18) : ((16.0 + x_19) > (11.0 + x_20)? (16.0 + x_19) : (11.0 + x_20))))? (((17.0 + x_1) > ((12.0 + x_4) > (13.0 + x_5)? (12.0 + x_4) : (13.0 + x_5))? (17.0 + x_1) : ((12.0 + x_4) > (13.0 + x_5)? (12.0 + x_4) : (13.0 + x_5))) > ((7.0 + x_10) > ((6.0 + x_11) > (12.0 + x_12)? (6.0 + x_11) : (12.0 + x_12))? (7.0 + x_10) : ((6.0 + x_11) > (12.0 + x_12)? (6.0 + x_11) : (12.0 + x_12)))? ((17.0 + x_1) > ((12.0 + x_4) > (13.0 + x_5)? (12.0 + x_4) : (13.0 + x_5))? (17.0 + x_1) : ((12.0 + x_4) > (13.0 + x_5)? (12.0 + x_4) : (13.0 + x_5))) : ((7.0 + x_10) > ((6.0 + x_11) > (12.0 + x_12)? (6.0 + x_11) : (12.0 + x_12))? (7.0 + x_10) : ((6.0 + x_11) > (12.0 + x_12)? (6.0 + x_11) : (12.0 + x_12)))) : (((4.0 + x_13) > ((18.0 + x_14) > (3.0 + x_17)? (18.0 + x_14) : (3.0 + x_17))? (4.0 + x_13) : ((18.0 + x_14) > (3.0 + x_17)? (18.0 + x_14) : (3.0 + x_17))) > ((16.0 + x_18) > ((16.0 + x_19) > (11.0 + x_20)? (16.0 + x_19) : (11.0 + x_20))? (16.0 + x_18) : ((16.0 + x_19) > (11.0 + x_20)? (16.0 + x_19) : (11.0 + x_20)))? ((4.0 + x_13) > ((18.0 + x_14) > (3.0 + x_17)? (18.0 + x_14) : (3.0 + x_17))? (4.0 + x_13) : ((18.0 + x_14) > (3.0 + x_17)? (18.0 + x_14) : (3.0 + x_17))) : ((16.0 + x_18) > ((16.0 + x_19) > (11.0 + x_20)? (16.0 + x_19) : (11.0 + x_20))? (16.0 + x_18) : ((16.0 + x_19) > (11.0 + x_20)? (16.0 + x_19) : (11.0 + x_20)))));
  x_12_ = ((((20.0 + x_1) > ((16.0 + x_4) > (11.0 + x_7)? (16.0 + x_4) : (11.0 + x_7))? (20.0 + x_1) : ((16.0 + x_4) > (11.0 + x_7)? (16.0 + x_4) : (11.0 + x_7))) > ((16.0 + x_8) > ((12.0 + x_11) > (20.0 + x_12)? (12.0 + x_11) : (20.0 + x_12))? (16.0 + x_8) : ((12.0 + x_11) > (20.0 + x_12)? (12.0 + x_11) : (20.0 + x_12)))? ((20.0 + x_1) > ((16.0 + x_4) > (11.0 + x_7)? (16.0 + x_4) : (11.0 + x_7))? (20.0 + x_1) : ((16.0 + x_4) > (11.0 + x_7)? (16.0 + x_4) : (11.0 + x_7))) : ((16.0 + x_8) > ((12.0 + x_11) > (20.0 + x_12)? (12.0 + x_11) : (20.0 + x_12))? (16.0 + x_8) : ((12.0 + x_11) > (20.0 + x_12)? (12.0 + x_11) : (20.0 + x_12)))) > (((5.0 + x_14) > ((17.0 + x_16) > (18.0 + x_17)? (17.0 + x_16) : (18.0 + x_17))? (5.0 + x_14) : ((17.0 + x_16) > (18.0 + x_17)? (17.0 + x_16) : (18.0 + x_17))) > ((12.0 + x_18) > ((9.0 + x_20) > (2.0 + x_21)? (9.0 + x_20) : (2.0 + x_21))? (12.0 + x_18) : ((9.0 + x_20) > (2.0 + x_21)? (9.0 + x_20) : (2.0 + x_21)))? ((5.0 + x_14) > ((17.0 + x_16) > (18.0 + x_17)? (17.0 + x_16) : (18.0 + x_17))? (5.0 + x_14) : ((17.0 + x_16) > (18.0 + x_17)? (17.0 + x_16) : (18.0 + x_17))) : ((12.0 + x_18) > ((9.0 + x_20) > (2.0 + x_21)? (9.0 + x_20) : (2.0 + x_21))? (12.0 + x_18) : ((9.0 + x_20) > (2.0 + x_21)? (9.0 + x_20) : (2.0 + x_21))))? (((20.0 + x_1) > ((16.0 + x_4) > (11.0 + x_7)? (16.0 + x_4) : (11.0 + x_7))? (20.0 + x_1) : ((16.0 + x_4) > (11.0 + x_7)? (16.0 + x_4) : (11.0 + x_7))) > ((16.0 + x_8) > ((12.0 + x_11) > (20.0 + x_12)? (12.0 + x_11) : (20.0 + x_12))? (16.0 + x_8) : ((12.0 + x_11) > (20.0 + x_12)? (12.0 + x_11) : (20.0 + x_12)))? ((20.0 + x_1) > ((16.0 + x_4) > (11.0 + x_7)? (16.0 + x_4) : (11.0 + x_7))? (20.0 + x_1) : ((16.0 + x_4) > (11.0 + x_7)? (16.0 + x_4) : (11.0 + x_7))) : ((16.0 + x_8) > ((12.0 + x_11) > (20.0 + x_12)? (12.0 + x_11) : (20.0 + x_12))? (16.0 + x_8) : ((12.0 + x_11) > (20.0 + x_12)? (12.0 + x_11) : (20.0 + x_12)))) : (((5.0 + x_14) > ((17.0 + x_16) > (18.0 + x_17)? (17.0 + x_16) : (18.0 + x_17))? (5.0 + x_14) : ((17.0 + x_16) > (18.0 + x_17)? (17.0 + x_16) : (18.0 + x_17))) > ((12.0 + x_18) > ((9.0 + x_20) > (2.0 + x_21)? (9.0 + x_20) : (2.0 + x_21))? (12.0 + x_18) : ((9.0 + x_20) > (2.0 + x_21)? (9.0 + x_20) : (2.0 + x_21)))? ((5.0 + x_14) > ((17.0 + x_16) > (18.0 + x_17)? (17.0 + x_16) : (18.0 + x_17))? (5.0 + x_14) : ((17.0 + x_16) > (18.0 + x_17)? (17.0 + x_16) : (18.0 + x_17))) : ((12.0 + x_18) > ((9.0 + x_20) > (2.0 + x_21)? (9.0 + x_20) : (2.0 + x_21))? (12.0 + x_18) : ((9.0 + x_20) > (2.0 + x_21)? (9.0 + x_20) : (2.0 + x_21)))));
  x_13_ = ((((19.0 + x_2) > ((3.0 + x_3) > (14.0 + x_4)? (3.0 + x_3) : (14.0 + x_4))? (19.0 + x_2) : ((3.0 + x_3) > (14.0 + x_4)? (3.0 + x_3) : (14.0 + x_4))) > ((19.0 + x_6) > ((9.0 + x_7) > (10.0 + x_8)? (9.0 + x_7) : (10.0 + x_8))? (19.0 + x_6) : ((9.0 + x_7) > (10.0 + x_8)? (9.0 + x_7) : (10.0 + x_8)))? ((19.0 + x_2) > ((3.0 + x_3) > (14.0 + x_4)? (3.0 + x_3) : (14.0 + x_4))? (19.0 + x_2) : ((3.0 + x_3) > (14.0 + x_4)? (3.0 + x_3) : (14.0 + x_4))) : ((19.0 + x_6) > ((9.0 + x_7) > (10.0 + x_8)? (9.0 + x_7) : (10.0 + x_8))? (19.0 + x_6) : ((9.0 + x_7) > (10.0 + x_8)? (9.0 + x_7) : (10.0 + x_8)))) > (((13.0 + x_11) > ((18.0 + x_12) > (9.0 + x_13)? (18.0 + x_12) : (9.0 + x_13))? (13.0 + x_11) : ((18.0 + x_12) > (9.0 + x_13)? (18.0 + x_12) : (9.0 + x_13))) > ((3.0 + x_14) > ((16.0 + x_18) > (15.0 + x_23)? (16.0 + x_18) : (15.0 + x_23))? (3.0 + x_14) : ((16.0 + x_18) > (15.0 + x_23)? (16.0 + x_18) : (15.0 + x_23)))? ((13.0 + x_11) > ((18.0 + x_12) > (9.0 + x_13)? (18.0 + x_12) : (9.0 + x_13))? (13.0 + x_11) : ((18.0 + x_12) > (9.0 + x_13)? (18.0 + x_12) : (9.0 + x_13))) : ((3.0 + x_14) > ((16.0 + x_18) > (15.0 + x_23)? (16.0 + x_18) : (15.0 + x_23))? (3.0 + x_14) : ((16.0 + x_18) > (15.0 + x_23)? (16.0 + x_18) : (15.0 + x_23))))? (((19.0 + x_2) > ((3.0 + x_3) > (14.0 + x_4)? (3.0 + x_3) : (14.0 + x_4))? (19.0 + x_2) : ((3.0 + x_3) > (14.0 + x_4)? (3.0 + x_3) : (14.0 + x_4))) > ((19.0 + x_6) > ((9.0 + x_7) > (10.0 + x_8)? (9.0 + x_7) : (10.0 + x_8))? (19.0 + x_6) : ((9.0 + x_7) > (10.0 + x_8)? (9.0 + x_7) : (10.0 + x_8)))? ((19.0 + x_2) > ((3.0 + x_3) > (14.0 + x_4)? (3.0 + x_3) : (14.0 + x_4))? (19.0 + x_2) : ((3.0 + x_3) > (14.0 + x_4)? (3.0 + x_3) : (14.0 + x_4))) : ((19.0 + x_6) > ((9.0 + x_7) > (10.0 + x_8)? (9.0 + x_7) : (10.0 + x_8))? (19.0 + x_6) : ((9.0 + x_7) > (10.0 + x_8)? (9.0 + x_7) : (10.0 + x_8)))) : (((13.0 + x_11) > ((18.0 + x_12) > (9.0 + x_13)? (18.0 + x_12) : (9.0 + x_13))? (13.0 + x_11) : ((18.0 + x_12) > (9.0 + x_13)? (18.0 + x_12) : (9.0 + x_13))) > ((3.0 + x_14) > ((16.0 + x_18) > (15.0 + x_23)? (16.0 + x_18) : (15.0 + x_23))? (3.0 + x_14) : ((16.0 + x_18) > (15.0 + x_23)? (16.0 + x_18) : (15.0 + x_23)))? ((13.0 + x_11) > ((18.0 + x_12) > (9.0 + x_13)? (18.0 + x_12) : (9.0 + x_13))? (13.0 + x_11) : ((18.0 + x_12) > (9.0 + x_13)? (18.0 + x_12) : (9.0 + x_13))) : ((3.0 + x_14) > ((16.0 + x_18) > (15.0 + x_23)? (16.0 + x_18) : (15.0 + x_23))? (3.0 + x_14) : ((16.0 + x_18) > (15.0 + x_23)? (16.0 + x_18) : (15.0 + x_23)))));
  x_14_ = ((((3.0 + x_0) > ((5.0 + x_1) > (6.0 + x_2)? (5.0 + x_1) : (6.0 + x_2))? (3.0 + x_0) : ((5.0 + x_1) > (6.0 + x_2)? (5.0 + x_1) : (6.0 + x_2))) > ((7.0 + x_5) > ((12.0 + x_9) > (10.0 + x_10)? (12.0 + x_9) : (10.0 + x_10))? (7.0 + x_5) : ((12.0 + x_9) > (10.0 + x_10)? (12.0 + x_9) : (10.0 + x_10)))? ((3.0 + x_0) > ((5.0 + x_1) > (6.0 + x_2)? (5.0 + x_1) : (6.0 + x_2))? (3.0 + x_0) : ((5.0 + x_1) > (6.0 + x_2)? (5.0 + x_1) : (6.0 + x_2))) : ((7.0 + x_5) > ((12.0 + x_9) > (10.0 + x_10)? (12.0 + x_9) : (10.0 + x_10))? (7.0 + x_5) : ((12.0 + x_9) > (10.0 + x_10)? (12.0 + x_9) : (10.0 + x_10)))) > (((4.0 + x_11) > ((8.0 + x_12) > (11.0 + x_15)? (8.0 + x_12) : (11.0 + x_15))? (4.0 + x_11) : ((8.0 + x_12) > (11.0 + x_15)? (8.0 + x_12) : (11.0 + x_15))) > ((1.0 + x_20) > ((7.0 + x_22) > (18.0 + x_23)? (7.0 + x_22) : (18.0 + x_23))? (1.0 + x_20) : ((7.0 + x_22) > (18.0 + x_23)? (7.0 + x_22) : (18.0 + x_23)))? ((4.0 + x_11) > ((8.0 + x_12) > (11.0 + x_15)? (8.0 + x_12) : (11.0 + x_15))? (4.0 + x_11) : ((8.0 + x_12) > (11.0 + x_15)? (8.0 + x_12) : (11.0 + x_15))) : ((1.0 + x_20) > ((7.0 + x_22) > (18.0 + x_23)? (7.0 + x_22) : (18.0 + x_23))? (1.0 + x_20) : ((7.0 + x_22) > (18.0 + x_23)? (7.0 + x_22) : (18.0 + x_23))))? (((3.0 + x_0) > ((5.0 + x_1) > (6.0 + x_2)? (5.0 + x_1) : (6.0 + x_2))? (3.0 + x_0) : ((5.0 + x_1) > (6.0 + x_2)? (5.0 + x_1) : (6.0 + x_2))) > ((7.0 + x_5) > ((12.0 + x_9) > (10.0 + x_10)? (12.0 + x_9) : (10.0 + x_10))? (7.0 + x_5) : ((12.0 + x_9) > (10.0 + x_10)? (12.0 + x_9) : (10.0 + x_10)))? ((3.0 + x_0) > ((5.0 + x_1) > (6.0 + x_2)? (5.0 + x_1) : (6.0 + x_2))? (3.0 + x_0) : ((5.0 + x_1) > (6.0 + x_2)? (5.0 + x_1) : (6.0 + x_2))) : ((7.0 + x_5) > ((12.0 + x_9) > (10.0 + x_10)? (12.0 + x_9) : (10.0 + x_10))? (7.0 + x_5) : ((12.0 + x_9) > (10.0 + x_10)? (12.0 + x_9) : (10.0 + x_10)))) : (((4.0 + x_11) > ((8.0 + x_12) > (11.0 + x_15)? (8.0 + x_12) : (11.0 + x_15))? (4.0 + x_11) : ((8.0 + x_12) > (11.0 + x_15)? (8.0 + x_12) : (11.0 + x_15))) > ((1.0 + x_20) > ((7.0 + x_22) > (18.0 + x_23)? (7.0 + x_22) : (18.0 + x_23))? (1.0 + x_20) : ((7.0 + x_22) > (18.0 + x_23)? (7.0 + x_22) : (18.0 + x_23)))? ((4.0 + x_11) > ((8.0 + x_12) > (11.0 + x_15)? (8.0 + x_12) : (11.0 + x_15))? (4.0 + x_11) : ((8.0 + x_12) > (11.0 + x_15)? (8.0 + x_12) : (11.0 + x_15))) : ((1.0 + x_20) > ((7.0 + x_22) > (18.0 + x_23)? (7.0 + x_22) : (18.0 + x_23))? (1.0 + x_20) : ((7.0 + x_22) > (18.0 + x_23)? (7.0 + x_22) : (18.0 + x_23)))));
  x_15_ = ((((6.0 + x_0) > ((14.0 + x_4) > (10.0 + x_6)? (14.0 + x_4) : (10.0 + x_6))? (6.0 + x_0) : ((14.0 + x_4) > (10.0 + x_6)? (14.0 + x_4) : (10.0 + x_6))) > ((14.0 + x_8) > ((1.0 + x_9) > (8.0 + x_12)? (1.0 + x_9) : (8.0 + x_12))? (14.0 + x_8) : ((1.0 + x_9) > (8.0 + x_12)? (1.0 + x_9) : (8.0 + x_12)))? ((6.0 + x_0) > ((14.0 + x_4) > (10.0 + x_6)? (14.0 + x_4) : (10.0 + x_6))? (6.0 + x_0) : ((14.0 + x_4) > (10.0 + x_6)? (14.0 + x_4) : (10.0 + x_6))) : ((14.0 + x_8) > ((1.0 + x_9) > (8.0 + x_12)? (1.0 + x_9) : (8.0 + x_12))? (14.0 + x_8) : ((1.0 + x_9) > (8.0 + x_12)? (1.0 + x_9) : (8.0 + x_12)))) > (((11.0 + x_13) > ((18.0 + x_19) > (2.0 + x_20)? (18.0 + x_19) : (2.0 + x_20))? (11.0 + x_13) : ((18.0 + x_19) > (2.0 + x_20)? (18.0 + x_19) : (2.0 + x_20))) > ((8.0 + x_21) > ((3.0 + x_22) > (17.0 + x_23)? (3.0 + x_22) : (17.0 + x_23))? (8.0 + x_21) : ((3.0 + x_22) > (17.0 + x_23)? (3.0 + x_22) : (17.0 + x_23)))? ((11.0 + x_13) > ((18.0 + x_19) > (2.0 + x_20)? (18.0 + x_19) : (2.0 + x_20))? (11.0 + x_13) : ((18.0 + x_19) > (2.0 + x_20)? (18.0 + x_19) : (2.0 + x_20))) : ((8.0 + x_21) > ((3.0 + x_22) > (17.0 + x_23)? (3.0 + x_22) : (17.0 + x_23))? (8.0 + x_21) : ((3.0 + x_22) > (17.0 + x_23)? (3.0 + x_22) : (17.0 + x_23))))? (((6.0 + x_0) > ((14.0 + x_4) > (10.0 + x_6)? (14.0 + x_4) : (10.0 + x_6))? (6.0 + x_0) : ((14.0 + x_4) > (10.0 + x_6)? (14.0 + x_4) : (10.0 + x_6))) > ((14.0 + x_8) > ((1.0 + x_9) > (8.0 + x_12)? (1.0 + x_9) : (8.0 + x_12))? (14.0 + x_8) : ((1.0 + x_9) > (8.0 + x_12)? (1.0 + x_9) : (8.0 + x_12)))? ((6.0 + x_0) > ((14.0 + x_4) > (10.0 + x_6)? (14.0 + x_4) : (10.0 + x_6))? (6.0 + x_0) : ((14.0 + x_4) > (10.0 + x_6)? (14.0 + x_4) : (10.0 + x_6))) : ((14.0 + x_8) > ((1.0 + x_9) > (8.0 + x_12)? (1.0 + x_9) : (8.0 + x_12))? (14.0 + x_8) : ((1.0 + x_9) > (8.0 + x_12)? (1.0 + x_9) : (8.0 + x_12)))) : (((11.0 + x_13) > ((18.0 + x_19) > (2.0 + x_20)? (18.0 + x_19) : (2.0 + x_20))? (11.0 + x_13) : ((18.0 + x_19) > (2.0 + x_20)? (18.0 + x_19) : (2.0 + x_20))) > ((8.0 + x_21) > ((3.0 + x_22) > (17.0 + x_23)? (3.0 + x_22) : (17.0 + x_23))? (8.0 + x_21) : ((3.0 + x_22) > (17.0 + x_23)? (3.0 + x_22) : (17.0 + x_23)))? ((11.0 + x_13) > ((18.0 + x_19) > (2.0 + x_20)? (18.0 + x_19) : (2.0 + x_20))? (11.0 + x_13) : ((18.0 + x_19) > (2.0 + x_20)? (18.0 + x_19) : (2.0 + x_20))) : ((8.0 + x_21) > ((3.0 + x_22) > (17.0 + x_23)? (3.0 + x_22) : (17.0 + x_23))? (8.0 + x_21) : ((3.0 + x_22) > (17.0 + x_23)? (3.0 + x_22) : (17.0 + x_23)))));
  x_16_ = ((((18.0 + x_0) > ((19.0 + x_2) > (14.0 + x_5)? (19.0 + x_2) : (14.0 + x_5))? (18.0 + x_0) : ((19.0 + x_2) > (14.0 + x_5)? (19.0 + x_2) : (14.0 + x_5))) > ((18.0 + x_6) > ((9.0 + x_7) > (4.0 + x_14)? (9.0 + x_7) : (4.0 + x_14))? (18.0 + x_6) : ((9.0 + x_7) > (4.0 + x_14)? (9.0 + x_7) : (4.0 + x_14)))? ((18.0 + x_0) > ((19.0 + x_2) > (14.0 + x_5)? (19.0 + x_2) : (14.0 + x_5))? (18.0 + x_0) : ((19.0 + x_2) > (14.0 + x_5)? (19.0 + x_2) : (14.0 + x_5))) : ((18.0 + x_6) > ((9.0 + x_7) > (4.0 + x_14)? (9.0 + x_7) : (4.0 + x_14))? (18.0 + x_6) : ((9.0 + x_7) > (4.0 + x_14)? (9.0 + x_7) : (4.0 + x_14)))) > (((19.0 + x_16) > ((9.0 + x_17) > (2.0 + x_19)? (9.0 + x_17) : (2.0 + x_19))? (19.0 + x_16) : ((9.0 + x_17) > (2.0 + x_19)? (9.0 + x_17) : (2.0 + x_19))) > ((5.0 + x_20) > ((10.0 + x_21) > (1.0 + x_23)? (10.0 + x_21) : (1.0 + x_23))? (5.0 + x_20) : ((10.0 + x_21) > (1.0 + x_23)? (10.0 + x_21) : (1.0 + x_23)))? ((19.0 + x_16) > ((9.0 + x_17) > (2.0 + x_19)? (9.0 + x_17) : (2.0 + x_19))? (19.0 + x_16) : ((9.0 + x_17) > (2.0 + x_19)? (9.0 + x_17) : (2.0 + x_19))) : ((5.0 + x_20) > ((10.0 + x_21) > (1.0 + x_23)? (10.0 + x_21) : (1.0 + x_23))? (5.0 + x_20) : ((10.0 + x_21) > (1.0 + x_23)? (10.0 + x_21) : (1.0 + x_23))))? (((18.0 + x_0) > ((19.0 + x_2) > (14.0 + x_5)? (19.0 + x_2) : (14.0 + x_5))? (18.0 + x_0) : ((19.0 + x_2) > (14.0 + x_5)? (19.0 + x_2) : (14.0 + x_5))) > ((18.0 + x_6) > ((9.0 + x_7) > (4.0 + x_14)? (9.0 + x_7) : (4.0 + x_14))? (18.0 + x_6) : ((9.0 + x_7) > (4.0 + x_14)? (9.0 + x_7) : (4.0 + x_14)))? ((18.0 + x_0) > ((19.0 + x_2) > (14.0 + x_5)? (19.0 + x_2) : (14.0 + x_5))? (18.0 + x_0) : ((19.0 + x_2) > (14.0 + x_5)? (19.0 + x_2) : (14.0 + x_5))) : ((18.0 + x_6) > ((9.0 + x_7) > (4.0 + x_14)? (9.0 + x_7) : (4.0 + x_14))? (18.0 + x_6) : ((9.0 + x_7) > (4.0 + x_14)? (9.0 + x_7) : (4.0 + x_14)))) : (((19.0 + x_16) > ((9.0 + x_17) > (2.0 + x_19)? (9.0 + x_17) : (2.0 + x_19))? (19.0 + x_16) : ((9.0 + x_17) > (2.0 + x_19)? (9.0 + x_17) : (2.0 + x_19))) > ((5.0 + x_20) > ((10.0 + x_21) > (1.0 + x_23)? (10.0 + x_21) : (1.0 + x_23))? (5.0 + x_20) : ((10.0 + x_21) > (1.0 + x_23)? (10.0 + x_21) : (1.0 + x_23)))? ((19.0 + x_16) > ((9.0 + x_17) > (2.0 + x_19)? (9.0 + x_17) : (2.0 + x_19))? (19.0 + x_16) : ((9.0 + x_17) > (2.0 + x_19)? (9.0 + x_17) : (2.0 + x_19))) : ((5.0 + x_20) > ((10.0 + x_21) > (1.0 + x_23)? (10.0 + x_21) : (1.0 + x_23))? (5.0 + x_20) : ((10.0 + x_21) > (1.0 + x_23)? (10.0 + x_21) : (1.0 + x_23)))));
  x_17_ = ((((6.0 + x_2) > ((10.0 + x_3) > (6.0 + x_5)? (10.0 + x_3) : (6.0 + x_5))? (6.0 + x_2) : ((10.0 + x_3) > (6.0 + x_5)? (10.0 + x_3) : (6.0 + x_5))) > ((9.0 + x_7) > ((18.0 + x_8) > (19.0 + x_11)? (18.0 + x_8) : (19.0 + x_11))? (9.0 + x_7) : ((18.0 + x_8) > (19.0 + x_11)? (18.0 + x_8) : (19.0 + x_11)))? ((6.0 + x_2) > ((10.0 + x_3) > (6.0 + x_5)? (10.0 + x_3) : (6.0 + x_5))? (6.0 + x_2) : ((10.0 + x_3) > (6.0 + x_5)? (10.0 + x_3) : (6.0 + x_5))) : ((9.0 + x_7) > ((18.0 + x_8) > (19.0 + x_11)? (18.0 + x_8) : (19.0 + x_11))? (9.0 + x_7) : ((18.0 + x_8) > (19.0 + x_11)? (18.0 + x_8) : (19.0 + x_11)))) > (((10.0 + x_12) > ((12.0 + x_16) > (14.0 + x_20)? (12.0 + x_16) : (14.0 + x_20))? (10.0 + x_12) : ((12.0 + x_16) > (14.0 + x_20)? (12.0 + x_16) : (14.0 + x_20))) > ((6.0 + x_21) > ((7.0 + x_22) > (12.0 + x_23)? (7.0 + x_22) : (12.0 + x_23))? (6.0 + x_21) : ((7.0 + x_22) > (12.0 + x_23)? (7.0 + x_22) : (12.0 + x_23)))? ((10.0 + x_12) > ((12.0 + x_16) > (14.0 + x_20)? (12.0 + x_16) : (14.0 + x_20))? (10.0 + x_12) : ((12.0 + x_16) > (14.0 + x_20)? (12.0 + x_16) : (14.0 + x_20))) : ((6.0 + x_21) > ((7.0 + x_22) > (12.0 + x_23)? (7.0 + x_22) : (12.0 + x_23))? (6.0 + x_21) : ((7.0 + x_22) > (12.0 + x_23)? (7.0 + x_22) : (12.0 + x_23))))? (((6.0 + x_2) > ((10.0 + x_3) > (6.0 + x_5)? (10.0 + x_3) : (6.0 + x_5))? (6.0 + x_2) : ((10.0 + x_3) > (6.0 + x_5)? (10.0 + x_3) : (6.0 + x_5))) > ((9.0 + x_7) > ((18.0 + x_8) > (19.0 + x_11)? (18.0 + x_8) : (19.0 + x_11))? (9.0 + x_7) : ((18.0 + x_8) > (19.0 + x_11)? (18.0 + x_8) : (19.0 + x_11)))? ((6.0 + x_2) > ((10.0 + x_3) > (6.0 + x_5)? (10.0 + x_3) : (6.0 + x_5))? (6.0 + x_2) : ((10.0 + x_3) > (6.0 + x_5)? (10.0 + x_3) : (6.0 + x_5))) : ((9.0 + x_7) > ((18.0 + x_8) > (19.0 + x_11)? (18.0 + x_8) : (19.0 + x_11))? (9.0 + x_7) : ((18.0 + x_8) > (19.0 + x_11)? (18.0 + x_8) : (19.0 + x_11)))) : (((10.0 + x_12) > ((12.0 + x_16) > (14.0 + x_20)? (12.0 + x_16) : (14.0 + x_20))? (10.0 + x_12) : ((12.0 + x_16) > (14.0 + x_20)? (12.0 + x_16) : (14.0 + x_20))) > ((6.0 + x_21) > ((7.0 + x_22) > (12.0 + x_23)? (7.0 + x_22) : (12.0 + x_23))? (6.0 + x_21) : ((7.0 + x_22) > (12.0 + x_23)? (7.0 + x_22) : (12.0 + x_23)))? ((10.0 + x_12) > ((12.0 + x_16) > (14.0 + x_20)? (12.0 + x_16) : (14.0 + x_20))? (10.0 + x_12) : ((12.0 + x_16) > (14.0 + x_20)? (12.0 + x_16) : (14.0 + x_20))) : ((6.0 + x_21) > ((7.0 + x_22) > (12.0 + x_23)? (7.0 + x_22) : (12.0 + x_23))? (6.0 + x_21) : ((7.0 + x_22) > (12.0 + x_23)? (7.0 + x_22) : (12.0 + x_23)))));
  x_18_ = ((((8.0 + x_1) > ((8.0 + x_2) > (11.0 + x_3)? (8.0 + x_2) : (11.0 + x_3))? (8.0 + x_1) : ((8.0 + x_2) > (11.0 + x_3)? (8.0 + x_2) : (11.0 + x_3))) > ((1.0 + x_4) > ((4.0 + x_5) > (4.0 + x_7)? (4.0 + x_5) : (4.0 + x_7))? (1.0 + x_4) : ((4.0 + x_5) > (4.0 + x_7)? (4.0 + x_5) : (4.0 + x_7)))? ((8.0 + x_1) > ((8.0 + x_2) > (11.0 + x_3)? (8.0 + x_2) : (11.0 + x_3))? (8.0 + x_1) : ((8.0 + x_2) > (11.0 + x_3)? (8.0 + x_2) : (11.0 + x_3))) : ((1.0 + x_4) > ((4.0 + x_5) > (4.0 + x_7)? (4.0 + x_5) : (4.0 + x_7))? (1.0 + x_4) : ((4.0 + x_5) > (4.0 + x_7)? (4.0 + x_5) : (4.0 + x_7)))) > (((19.0 + x_9) > ((20.0 + x_10) > (16.0 + x_14)? (20.0 + x_10) : (16.0 + x_14))? (19.0 + x_9) : ((20.0 + x_10) > (16.0 + x_14)? (20.0 + x_10) : (16.0 + x_14))) > ((4.0 + x_16) > ((3.0 + x_20) > (14.0 + x_23)? (3.0 + x_20) : (14.0 + x_23))? (4.0 + x_16) : ((3.0 + x_20) > (14.0 + x_23)? (3.0 + x_20) : (14.0 + x_23)))? ((19.0 + x_9) > ((20.0 + x_10) > (16.0 + x_14)? (20.0 + x_10) : (16.0 + x_14))? (19.0 + x_9) : ((20.0 + x_10) > (16.0 + x_14)? (20.0 + x_10) : (16.0 + x_14))) : ((4.0 + x_16) > ((3.0 + x_20) > (14.0 + x_23)? (3.0 + x_20) : (14.0 + x_23))? (4.0 + x_16) : ((3.0 + x_20) > (14.0 + x_23)? (3.0 + x_20) : (14.0 + x_23))))? (((8.0 + x_1) > ((8.0 + x_2) > (11.0 + x_3)? (8.0 + x_2) : (11.0 + x_3))? (8.0 + x_1) : ((8.0 + x_2) > (11.0 + x_3)? (8.0 + x_2) : (11.0 + x_3))) > ((1.0 + x_4) > ((4.0 + x_5) > (4.0 + x_7)? (4.0 + x_5) : (4.0 + x_7))? (1.0 + x_4) : ((4.0 + x_5) > (4.0 + x_7)? (4.0 + x_5) : (4.0 + x_7)))? ((8.0 + x_1) > ((8.0 + x_2) > (11.0 + x_3)? (8.0 + x_2) : (11.0 + x_3))? (8.0 + x_1) : ((8.0 + x_2) > (11.0 + x_3)? (8.0 + x_2) : (11.0 + x_3))) : ((1.0 + x_4) > ((4.0 + x_5) > (4.0 + x_7)? (4.0 + x_5) : (4.0 + x_7))? (1.0 + x_4) : ((4.0 + x_5) > (4.0 + x_7)? (4.0 + x_5) : (4.0 + x_7)))) : (((19.0 + x_9) > ((20.0 + x_10) > (16.0 + x_14)? (20.0 + x_10) : (16.0 + x_14))? (19.0 + x_9) : ((20.0 + x_10) > (16.0 + x_14)? (20.0 + x_10) : (16.0 + x_14))) > ((4.0 + x_16) > ((3.0 + x_20) > (14.0 + x_23)? (3.0 + x_20) : (14.0 + x_23))? (4.0 + x_16) : ((3.0 + x_20) > (14.0 + x_23)? (3.0 + x_20) : (14.0 + x_23)))? ((19.0 + x_9) > ((20.0 + x_10) > (16.0 + x_14)? (20.0 + x_10) : (16.0 + x_14))? (19.0 + x_9) : ((20.0 + x_10) > (16.0 + x_14)? (20.0 + x_10) : (16.0 + x_14))) : ((4.0 + x_16) > ((3.0 + x_20) > (14.0 + x_23)? (3.0 + x_20) : (14.0 + x_23))? (4.0 + x_16) : ((3.0 + x_20) > (14.0 + x_23)? (3.0 + x_20) : (14.0 + x_23)))));
  x_19_ = ((((16.0 + x_1) > ((10.0 + x_3) > (18.0 + x_5)? (10.0 + x_3) : (18.0 + x_5))? (16.0 + x_1) : ((10.0 + x_3) > (18.0 + x_5)? (10.0 + x_3) : (18.0 + x_5))) > ((14.0 + x_7) > ((8.0 + x_9) > (12.0 + x_11)? (8.0 + x_9) : (12.0 + x_11))? (14.0 + x_7) : ((8.0 + x_9) > (12.0 + x_11)? (8.0 + x_9) : (12.0 + x_11)))? ((16.0 + x_1) > ((10.0 + x_3) > (18.0 + x_5)? (10.0 + x_3) : (18.0 + x_5))? (16.0 + x_1) : ((10.0 + x_3) > (18.0 + x_5)? (10.0 + x_3) : (18.0 + x_5))) : ((14.0 + x_7) > ((8.0 + x_9) > (12.0 + x_11)? (8.0 + x_9) : (12.0 + x_11))? (14.0 + x_7) : ((8.0 + x_9) > (12.0 + x_11)? (8.0 + x_9) : (12.0 + x_11)))) > (((20.0 + x_12) > ((16.0 + x_13) > (10.0 + x_14)? (16.0 + x_13) : (10.0 + x_14))? (20.0 + x_12) : ((16.0 + x_13) > (10.0 + x_14)? (16.0 + x_13) : (10.0 + x_14))) > ((4.0 + x_15) > ((15.0 + x_19) > (20.0 + x_23)? (15.0 + x_19) : (20.0 + x_23))? (4.0 + x_15) : ((15.0 + x_19) > (20.0 + x_23)? (15.0 + x_19) : (20.0 + x_23)))? ((20.0 + x_12) > ((16.0 + x_13) > (10.0 + x_14)? (16.0 + x_13) : (10.0 + x_14))? (20.0 + x_12) : ((16.0 + x_13) > (10.0 + x_14)? (16.0 + x_13) : (10.0 + x_14))) : ((4.0 + x_15) > ((15.0 + x_19) > (20.0 + x_23)? (15.0 + x_19) : (20.0 + x_23))? (4.0 + x_15) : ((15.0 + x_19) > (20.0 + x_23)? (15.0 + x_19) : (20.0 + x_23))))? (((16.0 + x_1) > ((10.0 + x_3) > (18.0 + x_5)? (10.0 + x_3) : (18.0 + x_5))? (16.0 + x_1) : ((10.0 + x_3) > (18.0 + x_5)? (10.0 + x_3) : (18.0 + x_5))) > ((14.0 + x_7) > ((8.0 + x_9) > (12.0 + x_11)? (8.0 + x_9) : (12.0 + x_11))? (14.0 + x_7) : ((8.0 + x_9) > (12.0 + x_11)? (8.0 + x_9) : (12.0 + x_11)))? ((16.0 + x_1) > ((10.0 + x_3) > (18.0 + x_5)? (10.0 + x_3) : (18.0 + x_5))? (16.0 + x_1) : ((10.0 + x_3) > (18.0 + x_5)? (10.0 + x_3) : (18.0 + x_5))) : ((14.0 + x_7) > ((8.0 + x_9) > (12.0 + x_11)? (8.0 + x_9) : (12.0 + x_11))? (14.0 + x_7) : ((8.0 + x_9) > (12.0 + x_11)? (8.0 + x_9) : (12.0 + x_11)))) : (((20.0 + x_12) > ((16.0 + x_13) > (10.0 + x_14)? (16.0 + x_13) : (10.0 + x_14))? (20.0 + x_12) : ((16.0 + x_13) > (10.0 + x_14)? (16.0 + x_13) : (10.0 + x_14))) > ((4.0 + x_15) > ((15.0 + x_19) > (20.0 + x_23)? (15.0 + x_19) : (20.0 + x_23))? (4.0 + x_15) : ((15.0 + x_19) > (20.0 + x_23)? (15.0 + x_19) : (20.0 + x_23)))? ((20.0 + x_12) > ((16.0 + x_13) > (10.0 + x_14)? (16.0 + x_13) : (10.0 + x_14))? (20.0 + x_12) : ((16.0 + x_13) > (10.0 + x_14)? (16.0 + x_13) : (10.0 + x_14))) : ((4.0 + x_15) > ((15.0 + x_19) > (20.0 + x_23)? (15.0 + x_19) : (20.0 + x_23))? (4.0 + x_15) : ((15.0 + x_19) > (20.0 + x_23)? (15.0 + x_19) : (20.0 + x_23)))));
  x_20_ = ((((3.0 + x_0) > ((7.0 + x_1) > (12.0 + x_2)? (7.0 + x_1) : (12.0 + x_2))? (3.0 + x_0) : ((7.0 + x_1) > (12.0 + x_2)? (7.0 + x_1) : (12.0 + x_2))) > ((1.0 + x_3) > ((18.0 + x_6) > (15.0 + x_11)? (18.0 + x_6) : (15.0 + x_11))? (1.0 + x_3) : ((18.0 + x_6) > (15.0 + x_11)? (18.0 + x_6) : (15.0 + x_11)))? ((3.0 + x_0) > ((7.0 + x_1) > (12.0 + x_2)? (7.0 + x_1) : (12.0 + x_2))? (3.0 + x_0) : ((7.0 + x_1) > (12.0 + x_2)? (7.0 + x_1) : (12.0 + x_2))) : ((1.0 + x_3) > ((18.0 + x_6) > (15.0 + x_11)? (18.0 + x_6) : (15.0 + x_11))? (1.0 + x_3) : ((18.0 + x_6) > (15.0 + x_11)? (18.0 + x_6) : (15.0 + x_11)))) > (((19.0 + x_14) > ((5.0 + x_16) > (17.0 + x_17)? (5.0 + x_16) : (17.0 + x_17))? (19.0 + x_14) : ((5.0 + x_16) > (17.0 + x_17)? (5.0 + x_16) : (17.0 + x_17))) > ((3.0 + x_20) > ((15.0 + x_21) > (2.0 + x_23)? (15.0 + x_21) : (2.0 + x_23))? (3.0 + x_20) : ((15.0 + x_21) > (2.0 + x_23)? (15.0 + x_21) : (2.0 + x_23)))? ((19.0 + x_14) > ((5.0 + x_16) > (17.0 + x_17)? (5.0 + x_16) : (17.0 + x_17))? (19.0 + x_14) : ((5.0 + x_16) > (17.0 + x_17)? (5.0 + x_16) : (17.0 + x_17))) : ((3.0 + x_20) > ((15.0 + x_21) > (2.0 + x_23)? (15.0 + x_21) : (2.0 + x_23))? (3.0 + x_20) : ((15.0 + x_21) > (2.0 + x_23)? (15.0 + x_21) : (2.0 + x_23))))? (((3.0 + x_0) > ((7.0 + x_1) > (12.0 + x_2)? (7.0 + x_1) : (12.0 + x_2))? (3.0 + x_0) : ((7.0 + x_1) > (12.0 + x_2)? (7.0 + x_1) : (12.0 + x_2))) > ((1.0 + x_3) > ((18.0 + x_6) > (15.0 + x_11)? (18.0 + x_6) : (15.0 + x_11))? (1.0 + x_3) : ((18.0 + x_6) > (15.0 + x_11)? (18.0 + x_6) : (15.0 + x_11)))? ((3.0 + x_0) > ((7.0 + x_1) > (12.0 + x_2)? (7.0 + x_1) : (12.0 + x_2))? (3.0 + x_0) : ((7.0 + x_1) > (12.0 + x_2)? (7.0 + x_1) : (12.0 + x_2))) : ((1.0 + x_3) > ((18.0 + x_6) > (15.0 + x_11)? (18.0 + x_6) : (15.0 + x_11))? (1.0 + x_3) : ((18.0 + x_6) > (15.0 + x_11)? (18.0 + x_6) : (15.0 + x_11)))) : (((19.0 + x_14) > ((5.0 + x_16) > (17.0 + x_17)? (5.0 + x_16) : (17.0 + x_17))? (19.0 + x_14) : ((5.0 + x_16) > (17.0 + x_17)? (5.0 + x_16) : (17.0 + x_17))) > ((3.0 + x_20) > ((15.0 + x_21) > (2.0 + x_23)? (15.0 + x_21) : (2.0 + x_23))? (3.0 + x_20) : ((15.0 + x_21) > (2.0 + x_23)? (15.0 + x_21) : (2.0 + x_23)))? ((19.0 + x_14) > ((5.0 + x_16) > (17.0 + x_17)? (5.0 + x_16) : (17.0 + x_17))? (19.0 + x_14) : ((5.0 + x_16) > (17.0 + x_17)? (5.0 + x_16) : (17.0 + x_17))) : ((3.0 + x_20) > ((15.0 + x_21) > (2.0 + x_23)? (15.0 + x_21) : (2.0 + x_23))? (3.0 + x_20) : ((15.0 + x_21) > (2.0 + x_23)? (15.0 + x_21) : (2.0 + x_23)))));
  x_21_ = ((((11.0 + x_0) > ((20.0 + x_1) > (3.0 + x_2)? (20.0 + x_1) : (3.0 + x_2))? (11.0 + x_0) : ((20.0 + x_1) > (3.0 + x_2)? (20.0 + x_1) : (3.0 + x_2))) > ((3.0 + x_5) > ((20.0 + x_6) > (5.0 + x_8)? (20.0 + x_6) : (5.0 + x_8))? (3.0 + x_5) : ((20.0 + x_6) > (5.0 + x_8)? (20.0 + x_6) : (5.0 + x_8)))? ((11.0 + x_0) > ((20.0 + x_1) > (3.0 + x_2)? (20.0 + x_1) : (3.0 + x_2))? (11.0 + x_0) : ((20.0 + x_1) > (3.0 + x_2)? (20.0 + x_1) : (3.0 + x_2))) : ((3.0 + x_5) > ((20.0 + x_6) > (5.0 + x_8)? (20.0 + x_6) : (5.0 + x_8))? (3.0 + x_5) : ((20.0 + x_6) > (5.0 + x_8)? (20.0 + x_6) : (5.0 + x_8)))) > (((5.0 + x_10) > ((17.0 + x_14) > (2.0 + x_16)? (17.0 + x_14) : (2.0 + x_16))? (5.0 + x_10) : ((17.0 + x_14) > (2.0 + x_16)? (17.0 + x_14) : (2.0 + x_16))) > ((11.0 + x_17) > ((7.0 + x_18) > (9.0 + x_20)? (7.0 + x_18) : (9.0 + x_20))? (11.0 + x_17) : ((7.0 + x_18) > (9.0 + x_20)? (7.0 + x_18) : (9.0 + x_20)))? ((5.0 + x_10) > ((17.0 + x_14) > (2.0 + x_16)? (17.0 + x_14) : (2.0 + x_16))? (5.0 + x_10) : ((17.0 + x_14) > (2.0 + x_16)? (17.0 + x_14) : (2.0 + x_16))) : ((11.0 + x_17) > ((7.0 + x_18) > (9.0 + x_20)? (7.0 + x_18) : (9.0 + x_20))? (11.0 + x_17) : ((7.0 + x_18) > (9.0 + x_20)? (7.0 + x_18) : (9.0 + x_20))))? (((11.0 + x_0) > ((20.0 + x_1) > (3.0 + x_2)? (20.0 + x_1) : (3.0 + x_2))? (11.0 + x_0) : ((20.0 + x_1) > (3.0 + x_2)? (20.0 + x_1) : (3.0 + x_2))) > ((3.0 + x_5) > ((20.0 + x_6) > (5.0 + x_8)? (20.0 + x_6) : (5.0 + x_8))? (3.0 + x_5) : ((20.0 + x_6) > (5.0 + x_8)? (20.0 + x_6) : (5.0 + x_8)))? ((11.0 + x_0) > ((20.0 + x_1) > (3.0 + x_2)? (20.0 + x_1) : (3.0 + x_2))? (11.0 + x_0) : ((20.0 + x_1) > (3.0 + x_2)? (20.0 + x_1) : (3.0 + x_2))) : ((3.0 + x_5) > ((20.0 + x_6) > (5.0 + x_8)? (20.0 + x_6) : (5.0 + x_8))? (3.0 + x_5) : ((20.0 + x_6) > (5.0 + x_8)? (20.0 + x_6) : (5.0 + x_8)))) : (((5.0 + x_10) > ((17.0 + x_14) > (2.0 + x_16)? (17.0 + x_14) : (2.0 + x_16))? (5.0 + x_10) : ((17.0 + x_14) > (2.0 + x_16)? (17.0 + x_14) : (2.0 + x_16))) > ((11.0 + x_17) > ((7.0 + x_18) > (9.0 + x_20)? (7.0 + x_18) : (9.0 + x_20))? (11.0 + x_17) : ((7.0 + x_18) > (9.0 + x_20)? (7.0 + x_18) : (9.0 + x_20)))? ((5.0 + x_10) > ((17.0 + x_14) > (2.0 + x_16)? (17.0 + x_14) : (2.0 + x_16))? (5.0 + x_10) : ((17.0 + x_14) > (2.0 + x_16)? (17.0 + x_14) : (2.0 + x_16))) : ((11.0 + x_17) > ((7.0 + x_18) > (9.0 + x_20)? (7.0 + x_18) : (9.0 + x_20))? (11.0 + x_17) : ((7.0 + x_18) > (9.0 + x_20)? (7.0 + x_18) : (9.0 + x_20)))));
  x_22_ = ((((15.0 + x_1) > ((7.0 + x_2) > (12.0 + x_3)? (7.0 + x_2) : (12.0 + x_3))? (15.0 + x_1) : ((7.0 + x_2) > (12.0 + x_3)? (7.0 + x_2) : (12.0 + x_3))) > ((11.0 + x_4) > ((11.0 + x_6) > (18.0 + x_8)? (11.0 + x_6) : (18.0 + x_8))? (11.0 + x_4) : ((11.0 + x_6) > (18.0 + x_8)? (11.0 + x_6) : (18.0 + x_8)))? ((15.0 + x_1) > ((7.0 + x_2) > (12.0 + x_3)? (7.0 + x_2) : (12.0 + x_3))? (15.0 + x_1) : ((7.0 + x_2) > (12.0 + x_3)? (7.0 + x_2) : (12.0 + x_3))) : ((11.0 + x_4) > ((11.0 + x_6) > (18.0 + x_8)? (11.0 + x_6) : (18.0 + x_8))? (11.0 + x_4) : ((11.0 + x_6) > (18.0 + x_8)? (11.0 + x_6) : (18.0 + x_8)))) > (((9.0 + x_9) > ((10.0 + x_11) > (11.0 + x_12)? (10.0 + x_11) : (11.0 + x_12))? (9.0 + x_9) : ((10.0 + x_11) > (11.0 + x_12)? (10.0 + x_11) : (11.0 + x_12))) > ((1.0 + x_16) > ((1.0 + x_18) > (13.0 + x_19)? (1.0 + x_18) : (13.0 + x_19))? (1.0 + x_16) : ((1.0 + x_18) > (13.0 + x_19)? (1.0 + x_18) : (13.0 + x_19)))? ((9.0 + x_9) > ((10.0 + x_11) > (11.0 + x_12)? (10.0 + x_11) : (11.0 + x_12))? (9.0 + x_9) : ((10.0 + x_11) > (11.0 + x_12)? (10.0 + x_11) : (11.0 + x_12))) : ((1.0 + x_16) > ((1.0 + x_18) > (13.0 + x_19)? (1.0 + x_18) : (13.0 + x_19))? (1.0 + x_16) : ((1.0 + x_18) > (13.0 + x_19)? (1.0 + x_18) : (13.0 + x_19))))? (((15.0 + x_1) > ((7.0 + x_2) > (12.0 + x_3)? (7.0 + x_2) : (12.0 + x_3))? (15.0 + x_1) : ((7.0 + x_2) > (12.0 + x_3)? (7.0 + x_2) : (12.0 + x_3))) > ((11.0 + x_4) > ((11.0 + x_6) > (18.0 + x_8)? (11.0 + x_6) : (18.0 + x_8))? (11.0 + x_4) : ((11.0 + x_6) > (18.0 + x_8)? (11.0 + x_6) : (18.0 + x_8)))? ((15.0 + x_1) > ((7.0 + x_2) > (12.0 + x_3)? (7.0 + x_2) : (12.0 + x_3))? (15.0 + x_1) : ((7.0 + x_2) > (12.0 + x_3)? (7.0 + x_2) : (12.0 + x_3))) : ((11.0 + x_4) > ((11.0 + x_6) > (18.0 + x_8)? (11.0 + x_6) : (18.0 + x_8))? (11.0 + x_4) : ((11.0 + x_6) > (18.0 + x_8)? (11.0 + x_6) : (18.0 + x_8)))) : (((9.0 + x_9) > ((10.0 + x_11) > (11.0 + x_12)? (10.0 + x_11) : (11.0 + x_12))? (9.0 + x_9) : ((10.0 + x_11) > (11.0 + x_12)? (10.0 + x_11) : (11.0 + x_12))) > ((1.0 + x_16) > ((1.0 + x_18) > (13.0 + x_19)? (1.0 + x_18) : (13.0 + x_19))? (1.0 + x_16) : ((1.0 + x_18) > (13.0 + x_19)? (1.0 + x_18) : (13.0 + x_19)))? ((9.0 + x_9) > ((10.0 + x_11) > (11.0 + x_12)? (10.0 + x_11) : (11.0 + x_12))? (9.0 + x_9) : ((10.0 + x_11) > (11.0 + x_12)? (10.0 + x_11) : (11.0 + x_12))) : ((1.0 + x_16) > ((1.0 + x_18) > (13.0 + x_19)? (1.0 + x_18) : (13.0 + x_19))? (1.0 + x_16) : ((1.0 + x_18) > (13.0 + x_19)? (1.0 + x_18) : (13.0 + x_19)))));
  x_23_ = ((((18.0 + x_0) > ((15.0 + x_1) > (9.0 + x_3)? (15.0 + x_1) : (9.0 + x_3))? (18.0 + x_0) : ((15.0 + x_1) > (9.0 + x_3)? (15.0 + x_1) : (9.0 + x_3))) > ((16.0 + x_4) > ((6.0 + x_6) > (5.0 + x_7)? (6.0 + x_6) : (5.0 + x_7))? (16.0 + x_4) : ((6.0 + x_6) > (5.0 + x_7)? (6.0 + x_6) : (5.0 + x_7)))? ((18.0 + x_0) > ((15.0 + x_1) > (9.0 + x_3)? (15.0 + x_1) : (9.0 + x_3))? (18.0 + x_0) : ((15.0 + x_1) > (9.0 + x_3)? (15.0 + x_1) : (9.0 + x_3))) : ((16.0 + x_4) > ((6.0 + x_6) > (5.0 + x_7)? (6.0 + x_6) : (5.0 + x_7))? (16.0 + x_4) : ((6.0 + x_6) > (5.0 + x_7)? (6.0 + x_6) : (5.0 + x_7)))) > (((14.0 + x_8) > ((2.0 + x_10) > (3.0 + x_14)? (2.0 + x_10) : (3.0 + x_14))? (14.0 + x_8) : ((2.0 + x_10) > (3.0 + x_14)? (2.0 + x_10) : (3.0 + x_14))) > ((11.0 + x_15) > ((20.0 + x_18) > (12.0 + x_22)? (20.0 + x_18) : (12.0 + x_22))? (11.0 + x_15) : ((20.0 + x_18) > (12.0 + x_22)? (20.0 + x_18) : (12.0 + x_22)))? ((14.0 + x_8) > ((2.0 + x_10) > (3.0 + x_14)? (2.0 + x_10) : (3.0 + x_14))? (14.0 + x_8) : ((2.0 + x_10) > (3.0 + x_14)? (2.0 + x_10) : (3.0 + x_14))) : ((11.0 + x_15) > ((20.0 + x_18) > (12.0 + x_22)? (20.0 + x_18) : (12.0 + x_22))? (11.0 + x_15) : ((20.0 + x_18) > (12.0 + x_22)? (20.0 + x_18) : (12.0 + x_22))))? (((18.0 + x_0) > ((15.0 + x_1) > (9.0 + x_3)? (15.0 + x_1) : (9.0 + x_3))? (18.0 + x_0) : ((15.0 + x_1) > (9.0 + x_3)? (15.0 + x_1) : (9.0 + x_3))) > ((16.0 + x_4) > ((6.0 + x_6) > (5.0 + x_7)? (6.0 + x_6) : (5.0 + x_7))? (16.0 + x_4) : ((6.0 + x_6) > (5.0 + x_7)? (6.0 + x_6) : (5.0 + x_7)))? ((18.0 + x_0) > ((15.0 + x_1) > (9.0 + x_3)? (15.0 + x_1) : (9.0 + x_3))? (18.0 + x_0) : ((15.0 + x_1) > (9.0 + x_3)? (15.0 + x_1) : (9.0 + x_3))) : ((16.0 + x_4) > ((6.0 + x_6) > (5.0 + x_7)? (6.0 + x_6) : (5.0 + x_7))? (16.0 + x_4) : ((6.0 + x_6) > (5.0 + x_7)? (6.0 + x_6) : (5.0 + x_7)))) : (((14.0 + x_8) > ((2.0 + x_10) > (3.0 + x_14)? (2.0 + x_10) : (3.0 + x_14))? (14.0 + x_8) : ((2.0 + x_10) > (3.0 + x_14)? (2.0 + x_10) : (3.0 + x_14))) > ((11.0 + x_15) > ((20.0 + x_18) > (12.0 + x_22)? (20.0 + x_18) : (12.0 + x_22))? (11.0 + x_15) : ((20.0 + x_18) > (12.0 + x_22)? (20.0 + x_18) : (12.0 + x_22)))? ((14.0 + x_8) > ((2.0 + x_10) > (3.0 + x_14)? (2.0 + x_10) : (3.0 + x_14))? (14.0 + x_8) : ((2.0 + x_10) > (3.0 + x_14)? (2.0 + x_10) : (3.0 + x_14))) : ((11.0 + x_15) > ((20.0 + x_18) > (12.0 + x_22)? (20.0 + x_18) : (12.0 + x_22))? (11.0 + x_15) : ((20.0 + x_18) > (12.0 + x_22)? (20.0 + x_18) : (12.0 + x_22)))));
  x_0 = x_0_;
  x_1 = x_1_;
  x_2 = x_2_;
  x_3 = x_3_;
  x_4 = x_4_;
  x_5 = x_5_;
  x_6 = x_6_;
  x_7 = x_7_;
  x_8 = x_8_;
  x_9 = x_9_;
  x_10 = x_10_;
  x_11 = x_11_;
  x_12 = x_12_;
  x_13 = x_13_;
  x_14 = x_14_;
  x_15 = x_15_;
  x_16 = x_16_;
  x_17 = x_17_;
  x_18 = x_18_;
  x_19 = x_19_;
  x_20 = x_20_;
  x_21 = x_21_;
  x_22 = x_22_;
  x_23 = x_23_;
    }
    return 0;
  }
  