text: //@ ltl invariant negative: (AP(x_4 - x_10 > -8) && (AP(x_2 - x_12 > 17) U AP(x_3 - x_14 > 10)));
  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;
  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_;
    while(1) {
  x_0_ = ((((8.0 + x_0) > (9.0 + x_4)? (8.0 + x_0) : (9.0 + x_4)) > ((9.0 + x_5) > ((12.0 + x_7) > (20.0 + x_11)? (12.0 + x_7) : (20.0 + x_11))? (9.0 + x_5) : ((12.0 + x_7) > (20.0 + x_11)? (12.0 + x_7) : (20.0 + x_11)))? ((8.0 + x_0) > (9.0 + x_4)? (8.0 + x_0) : (9.0 + x_4)) : ((9.0 + x_5) > ((12.0 + x_7) > (20.0 + x_11)? (12.0 + x_7) : (20.0 + x_11))? (9.0 + x_5) : ((12.0 + x_7) > (20.0 + x_11)? (12.0 + x_7) : (20.0 + x_11)))) > (((15.0 + x_12) > (12.0 + x_14)? (15.0 + x_12) : (12.0 + x_14)) > ((5.0 + x_15) > ((1.0 + x_18) > (5.0 + x_19)? (1.0 + x_18) : (5.0 + x_19))? (5.0 + x_15) : ((1.0 + x_18) > (5.0 + x_19)? (1.0 + x_18) : (5.0 + x_19)))? ((15.0 + x_12) > (12.0 + x_14)? (15.0 + x_12) : (12.0 + x_14)) : ((5.0 + x_15) > ((1.0 + x_18) > (5.0 + x_19)? (1.0 + x_18) : (5.0 + x_19))? (5.0 + x_15) : ((1.0 + x_18) > (5.0 + x_19)? (1.0 + x_18) : (5.0 + x_19))))? (((8.0 + x_0) > (9.0 + x_4)? (8.0 + x_0) : (9.0 + x_4)) > ((9.0 + x_5) > ((12.0 + x_7) > (20.0 + x_11)? (12.0 + x_7) : (20.0 + x_11))? (9.0 + x_5) : ((12.0 + x_7) > (20.0 + x_11)? (12.0 + x_7) : (20.0 + x_11)))? ((8.0 + x_0) > (9.0 + x_4)? (8.0 + x_0) : (9.0 + x_4)) : ((9.0 + x_5) > ((12.0 + x_7) > (20.0 + x_11)? (12.0 + x_7) : (20.0 + x_11))? (9.0 + x_5) : ((12.0 + x_7) > (20.0 + x_11)? (12.0 + x_7) : (20.0 + x_11)))) : (((15.0 + x_12) > (12.0 + x_14)? (15.0 + x_12) : (12.0 + x_14)) > ((5.0 + x_15) > ((1.0 + x_18) > (5.0 + x_19)? (1.0 + x_18) : (5.0 + x_19))? (5.0 + x_15) : ((1.0 + x_18) > (5.0 + x_19)? (1.0 + x_18) : (5.0 + x_19)))? ((15.0 + x_12) > (12.0 + x_14)? (15.0 + x_12) : (12.0 + x_14)) : ((5.0 + x_15) > ((1.0 + x_18) > (5.0 + x_19)? (1.0 + x_18) : (5.0 + x_19))? (5.0 + x_15) : ((1.0 + x_18) > (5.0 + x_19)? (1.0 + x_18) : (5.0 + x_19)))));
  x_1_ = ((((20.0 + x_1) > (16.0 + x_4)? (20.0 + x_1) : (16.0 + x_4)) > ((17.0 + x_5) > ((6.0 + x_6) > (19.0 + x_8)? (6.0 + x_6) : (19.0 + x_8))? (17.0 + x_5) : ((6.0 + x_6) > (19.0 + x_8)? (6.0 + x_6) : (19.0 + x_8)))? ((20.0 + x_1) > (16.0 + x_4)? (20.0 + x_1) : (16.0 + x_4)) : ((17.0 + x_5) > ((6.0 + x_6) > (19.0 + x_8)? (6.0 + x_6) : (19.0 + x_8))? (17.0 + x_5) : ((6.0 + x_6) > (19.0 + x_8)? (6.0 + x_6) : (19.0 + x_8)))) > (((13.0 + x_11) > (1.0 + x_12)? (13.0 + x_11) : (1.0 + x_12)) > ((5.0 + x_15) > ((1.0 + x_16) > (15.0 + x_18)? (1.0 + x_16) : (15.0 + x_18))? (5.0 + x_15) : ((1.0 + x_16) > (15.0 + x_18)? (1.0 + x_16) : (15.0 + x_18)))? ((13.0 + x_11) > (1.0 + x_12)? (13.0 + x_11) : (1.0 + x_12)) : ((5.0 + x_15) > ((1.0 + x_16) > (15.0 + x_18)? (1.0 + x_16) : (15.0 + x_18))? (5.0 + x_15) : ((1.0 + x_16) > (15.0 + x_18)? (1.0 + x_16) : (15.0 + x_18))))? (((20.0 + x_1) > (16.0 + x_4)? (20.0 + x_1) : (16.0 + x_4)) > ((17.0 + x_5) > ((6.0 + x_6) > (19.0 + x_8)? (6.0 + x_6) : (19.0 + x_8))? (17.0 + x_5) : ((6.0 + x_6) > (19.0 + x_8)? (6.0 + x_6) : (19.0 + x_8)))? ((20.0 + x_1) > (16.0 + x_4)? (20.0 + x_1) : (16.0 + x_4)) : ((17.0 + x_5) > ((6.0 + x_6) > (19.0 + x_8)? (6.0 + x_6) : (19.0 + x_8))? (17.0 + x_5) : ((6.0 + x_6) > (19.0 + x_8)? (6.0 + x_6) : (19.0 + x_8)))) : (((13.0 + x_11) > (1.0 + x_12)? (13.0 + x_11) : (1.0 + x_12)) > ((5.0 + x_15) > ((1.0 + x_16) > (15.0 + x_18)? (1.0 + x_16) : (15.0 + x_18))? (5.0 + x_15) : ((1.0 + x_16) > (15.0 + x_18)? (1.0 + x_16) : (15.0 + x_18)))? ((13.0 + x_11) > (1.0 + x_12)? (13.0 + x_11) : (1.0 + x_12)) : ((5.0 + x_15) > ((1.0 + x_16) > (15.0 + x_18)? (1.0 + x_16) : (15.0 + x_18))? (5.0 + x_15) : ((1.0 + x_16) > (15.0 + x_18)? (1.0 + x_16) : (15.0 + x_18)))));
  x_2_ = ((((4.0 + x_0) > (1.0 + x_1)? (4.0 + x_0) : (1.0 + x_1)) > ((12.0 + x_3) > ((18.0 + x_5) > (13.0 + x_7)? (18.0 + x_5) : (13.0 + x_7))? (12.0 + x_3) : ((18.0 + x_5) > (13.0 + x_7)? (18.0 + x_5) : (13.0 + x_7)))? ((4.0 + x_0) > (1.0 + x_1)? (4.0 + x_0) : (1.0 + x_1)) : ((12.0 + x_3) > ((18.0 + x_5) > (13.0 + x_7)? (18.0 + x_5) : (13.0 + x_7))? (12.0 + x_3) : ((18.0 + x_5) > (13.0 + x_7)? (18.0 + x_5) : (13.0 + x_7)))) > (((12.0 + x_8) > (17.0 + x_14)? (12.0 + x_8) : (17.0 + x_14)) > ((14.0 + x_16) > ((1.0 + x_17) > (16.0 + x_19)? (1.0 + x_17) : (16.0 + x_19))? (14.0 + x_16) : ((1.0 + x_17) > (16.0 + x_19)? (1.0 + x_17) : (16.0 + x_19)))? ((12.0 + x_8) > (17.0 + x_14)? (12.0 + x_8) : (17.0 + x_14)) : ((14.0 + x_16) > ((1.0 + x_17) > (16.0 + x_19)? (1.0 + x_17) : (16.0 + x_19))? (14.0 + x_16) : ((1.0 + x_17) > (16.0 + x_19)? (1.0 + x_17) : (16.0 + x_19))))? (((4.0 + x_0) > (1.0 + x_1)? (4.0 + x_0) : (1.0 + x_1)) > ((12.0 + x_3) > ((18.0 + x_5) > (13.0 + x_7)? (18.0 + x_5) : (13.0 + x_7))? (12.0 + x_3) : ((18.0 + x_5) > (13.0 + x_7)? (18.0 + x_5) : (13.0 + x_7)))? ((4.0 + x_0) > (1.0 + x_1)? (4.0 + x_0) : (1.0 + x_1)) : ((12.0 + x_3) > ((18.0 + x_5) > (13.0 + x_7)? (18.0 + x_5) : (13.0 + x_7))? (12.0 + x_3) : ((18.0 + x_5) > (13.0 + x_7)? (18.0 + x_5) : (13.0 + x_7)))) : (((12.0 + x_8) > (17.0 + x_14)? (12.0 + x_8) : (17.0 + x_14)) > ((14.0 + x_16) > ((1.0 + x_17) > (16.0 + x_19)? (1.0 + x_17) : (16.0 + x_19))? (14.0 + x_16) : ((1.0 + x_17) > (16.0 + x_19)? (1.0 + x_17) : (16.0 + x_19)))? ((12.0 + x_8) > (17.0 + x_14)? (12.0 + x_8) : (17.0 + x_14)) : ((14.0 + x_16) > ((1.0 + x_17) > (16.0 + x_19)? (1.0 + x_17) : (16.0 + x_19))? (14.0 + x_16) : ((1.0 + x_17) > (16.0 + x_19)? (1.0 + x_17) : (16.0 + x_19)))));
  x_3_ = ((((9.0 + x_2) > (17.0 + x_3)? (9.0 + x_2) : (17.0 + x_3)) > ((2.0 + x_5) > ((5.0 + x_7) > (20.0 + x_13)? (5.0 + x_7) : (20.0 + x_13))? (2.0 + x_5) : ((5.0 + x_7) > (20.0 + x_13)? (5.0 + x_7) : (20.0 + x_13)))? ((9.0 + x_2) > (17.0 + x_3)? (9.0 + x_2) : (17.0 + x_3)) : ((2.0 + x_5) > ((5.0 + x_7) > (20.0 + x_13)? (5.0 + x_7) : (20.0 + x_13))? (2.0 + x_5) : ((5.0 + x_7) > (20.0 + x_13)? (5.0 + x_7) : (20.0 + x_13)))) > (((4.0 + x_15) > (20.0 + x_16)? (4.0 + x_15) : (20.0 + x_16)) > ((7.0 + x_17) > ((11.0 + x_18) > (3.0 + x_19)? (11.0 + x_18) : (3.0 + x_19))? (7.0 + x_17) : ((11.0 + x_18) > (3.0 + x_19)? (11.0 + x_18) : (3.0 + x_19)))? ((4.0 + x_15) > (20.0 + x_16)? (4.0 + x_15) : (20.0 + x_16)) : ((7.0 + x_17) > ((11.0 + x_18) > (3.0 + x_19)? (11.0 + x_18) : (3.0 + x_19))? (7.0 + x_17) : ((11.0 + x_18) > (3.0 + x_19)? (11.0 + x_18) : (3.0 + x_19))))? (((9.0 + x_2) > (17.0 + x_3)? (9.0 + x_2) : (17.0 + x_3)) > ((2.0 + x_5) > ((5.0 + x_7) > (20.0 + x_13)? (5.0 + x_7) : (20.0 + x_13))? (2.0 + x_5) : ((5.0 + x_7) > (20.0 + x_13)? (5.0 + x_7) : (20.0 + x_13)))? ((9.0 + x_2) > (17.0 + x_3)? (9.0 + x_2) : (17.0 + x_3)) : ((2.0 + x_5) > ((5.0 + x_7) > (20.0 + x_13)? (5.0 + x_7) : (20.0 + x_13))? (2.0 + x_5) : ((5.0 + x_7) > (20.0 + x_13)? (5.0 + x_7) : (20.0 + x_13)))) : (((4.0 + x_15) > (20.0 + x_16)? (4.0 + x_15) : (20.0 + x_16)) > ((7.0 + x_17) > ((11.0 + x_18) > (3.0 + x_19)? (11.0 + x_18) : (3.0 + x_19))? (7.0 + x_17) : ((11.0 + x_18) > (3.0 + x_19)? (11.0 + x_18) : (3.0 + x_19)))? ((4.0 + x_15) > (20.0 + x_16)? (4.0 + x_15) : (20.0 + x_16)) : ((7.0 + x_17) > ((11.0 + x_18) > (3.0 + x_19)? (11.0 + x_18) : (3.0 + x_19))? (7.0 + x_17) : ((11.0 + x_18) > (3.0 + x_19)? (11.0 + x_18) : (3.0 + x_19)))));
  x_4_ = ((((14.0 + x_0) > (2.0 + x_2)? (14.0 + x_0) : (2.0 + x_2)) > ((13.0 + x_4) > ((4.0 + x_5) > (5.0 + x_6)? (4.0 + x_5) : (5.0 + x_6))? (13.0 + x_4) : ((4.0 + x_5) > (5.0 + x_6)? (4.0 + x_5) : (5.0 + x_6)))? ((14.0 + x_0) > (2.0 + x_2)? (14.0 + x_0) : (2.0 + x_2)) : ((13.0 + x_4) > ((4.0 + x_5) > (5.0 + x_6)? (4.0 + x_5) : (5.0 + x_6))? (13.0 + x_4) : ((4.0 + x_5) > (5.0 + x_6)? (4.0 + x_5) : (5.0 + x_6)))) > (((17.0 + x_10) > (16.0 + x_12)? (17.0 + x_10) : (16.0 + x_12)) > ((15.0 + x_14) > ((15.0 + x_15) > (9.0 + x_18)? (15.0 + x_15) : (9.0 + x_18))? (15.0 + x_14) : ((15.0 + x_15) > (9.0 + x_18)? (15.0 + x_15) : (9.0 + x_18)))? ((17.0 + x_10) > (16.0 + x_12)? (17.0 + x_10) : (16.0 + x_12)) : ((15.0 + x_14) > ((15.0 + x_15) > (9.0 + x_18)? (15.0 + x_15) : (9.0 + x_18))? (15.0 + x_14) : ((15.0 + x_15) > (9.0 + x_18)? (15.0 + x_15) : (9.0 + x_18))))? (((14.0 + x_0) > (2.0 + x_2)? (14.0 + x_0) : (2.0 + x_2)) > ((13.0 + x_4) > ((4.0 + x_5) > (5.0 + x_6)? (4.0 + x_5) : (5.0 + x_6))? (13.0 + x_4) : ((4.0 + x_5) > (5.0 + x_6)? (4.0 + x_5) : (5.0 + x_6)))? ((14.0 + x_0) > (2.0 + x_2)? (14.0 + x_0) : (2.0 + x_2)) : ((13.0 + x_4) > ((4.0 + x_5) > (5.0 + x_6)? (4.0 + x_5) : (5.0 + x_6))? (13.0 + x_4) : ((4.0 + x_5) > (5.0 + x_6)? (4.0 + x_5) : (5.0 + x_6)))) : (((17.0 + x_10) > (16.0 + x_12)? (17.0 + x_10) : (16.0 + x_12)) > ((15.0 + x_14) > ((15.0 + x_15) > (9.0 + x_18)? (15.0 + x_15) : (9.0 + x_18))? (15.0 + x_14) : ((15.0 + x_15) > (9.0 + x_18)? (15.0 + x_15) : (9.0 + x_18)))? ((17.0 + x_10) > (16.0 + x_12)? (17.0 + x_10) : (16.0 + x_12)) : ((15.0 + x_14) > ((15.0 + x_15) > (9.0 + x_18)? (15.0 + x_15) : (9.0 + x_18))? (15.0 + x_14) : ((15.0 + x_15) > (9.0 + x_18)? (15.0 + x_15) : (9.0 + x_18)))));
  x_5_ = ((((17.0 + x_2) > (2.0 + x_4)? (17.0 + x_2) : (2.0 + x_4)) > ((18.0 + x_5) > ((17.0 + x_6) > (20.0 + x_8)? (17.0 + x_6) : (20.0 + x_8))? (18.0 + x_5) : ((17.0 + x_6) > (20.0 + x_8)? (17.0 + x_6) : (20.0 + x_8)))? ((17.0 + x_2) > (2.0 + x_4)? (17.0 + x_2) : (2.0 + x_4)) : ((18.0 + x_5) > ((17.0 + x_6) > (20.0 + x_8)? (17.0 + x_6) : (20.0 + x_8))? (18.0 + x_5) : ((17.0 + x_6) > (20.0 + x_8)? (17.0 + x_6) : (20.0 + x_8)))) > (((7.0 + x_10) > (2.0 + x_14)? (7.0 + x_10) : (2.0 + x_14)) > ((19.0 + x_16) > ((12.0 + x_17) > (13.0 + x_18)? (12.0 + x_17) : (13.0 + x_18))? (19.0 + x_16) : ((12.0 + x_17) > (13.0 + x_18)? (12.0 + x_17) : (13.0 + x_18)))? ((7.0 + x_10) > (2.0 + x_14)? (7.0 + x_10) : (2.0 + x_14)) : ((19.0 + x_16) > ((12.0 + x_17) > (13.0 + x_18)? (12.0 + x_17) : (13.0 + x_18))? (19.0 + x_16) : ((12.0 + x_17) > (13.0 + x_18)? (12.0 + x_17) : (13.0 + x_18))))? (((17.0 + x_2) > (2.0 + x_4)? (17.0 + x_2) : (2.0 + x_4)) > ((18.0 + x_5) > ((17.0 + x_6) > (20.0 + x_8)? (17.0 + x_6) : (20.0 + x_8))? (18.0 + x_5) : ((17.0 + x_6) > (20.0 + x_8)? (17.0 + x_6) : (20.0 + x_8)))? ((17.0 + x_2) > (2.0 + x_4)? (17.0 + x_2) : (2.0 + x_4)) : ((18.0 + x_5) > ((17.0 + x_6) > (20.0 + x_8)? (17.0 + x_6) : (20.0 + x_8))? (18.0 + x_5) : ((17.0 + x_6) > (20.0 + x_8)? (17.0 + x_6) : (20.0 + x_8)))) : (((7.0 + x_10) > (2.0 + x_14)? (7.0 + x_10) : (2.0 + x_14)) > ((19.0 + x_16) > ((12.0 + x_17) > (13.0 + x_18)? (12.0 + x_17) : (13.0 + x_18))? (19.0 + x_16) : ((12.0 + x_17) > (13.0 + x_18)? (12.0 + x_17) : (13.0 + x_18)))? ((7.0 + x_10) > (2.0 + x_14)? (7.0 + x_10) : (2.0 + x_14)) : ((19.0 + x_16) > ((12.0 + x_17) > (13.0 + x_18)? (12.0 + x_17) : (13.0 + x_18))? (19.0 + x_16) : ((12.0 + x_17) > (13.0 + x_18)? (12.0 + x_17) : (13.0 + x_18)))));
  x_6_ = ((((8.0 + x_2) > (2.0 + x_3)? (8.0 + x_2) : (2.0 + x_3)) > ((13.0 + x_5) > ((15.0 + x_9) > (12.0 + x_11)? (15.0 + x_9) : (12.0 + x_11))? (13.0 + x_5) : ((15.0 + x_9) > (12.0 + x_11)? (15.0 + x_9) : (12.0 + x_11)))? ((8.0 + x_2) > (2.0 + x_3)? (8.0 + x_2) : (2.0 + x_3)) : ((13.0 + x_5) > ((15.0 + x_9) > (12.0 + x_11)? (15.0 + x_9) : (12.0 + x_11))? (13.0 + x_5) : ((15.0 + x_9) > (12.0 + x_11)? (15.0 + x_9) : (12.0 + x_11)))) > (((2.0 + x_13) > (18.0 + x_14)? (2.0 + x_13) : (18.0 + x_14)) > ((17.0 + x_16) > ((7.0 + x_17) > (11.0 + x_18)? (7.0 + x_17) : (11.0 + x_18))? (17.0 + x_16) : ((7.0 + x_17) > (11.0 + x_18)? (7.0 + x_17) : (11.0 + x_18)))? ((2.0 + x_13) > (18.0 + x_14)? (2.0 + x_13) : (18.0 + x_14)) : ((17.0 + x_16) > ((7.0 + x_17) > (11.0 + x_18)? (7.0 + x_17) : (11.0 + x_18))? (17.0 + x_16) : ((7.0 + x_17) > (11.0 + x_18)? (7.0 + x_17) : (11.0 + x_18))))? (((8.0 + x_2) > (2.0 + x_3)? (8.0 + x_2) : (2.0 + x_3)) > ((13.0 + x_5) > ((15.0 + x_9) > (12.0 + x_11)? (15.0 + x_9) : (12.0 + x_11))? (13.0 + x_5) : ((15.0 + x_9) > (12.0 + x_11)? (15.0 + x_9) : (12.0 + x_11)))? ((8.0 + x_2) > (2.0 + x_3)? (8.0 + x_2) : (2.0 + x_3)) : ((13.0 + x_5) > ((15.0 + x_9) > (12.0 + x_11)? (15.0 + x_9) : (12.0 + x_11))? (13.0 + x_5) : ((15.0 + x_9) > (12.0 + x_11)? (15.0 + x_9) : (12.0 + x_11)))) : (((2.0 + x_13) > (18.0 + x_14)? (2.0 + x_13) : (18.0 + x_14)) > ((17.0 + x_16) > ((7.0 + x_17) > (11.0 + x_18)? (7.0 + x_17) : (11.0 + x_18))? (17.0 + x_16) : ((7.0 + x_17) > (11.0 + x_18)? (7.0 + x_17) : (11.0 + x_18)))? ((2.0 + x_13) > (18.0 + x_14)? (2.0 + x_13) : (18.0 + x_14)) : ((17.0 + x_16) > ((7.0 + x_17) > (11.0 + x_18)? (7.0 + x_17) : (11.0 + x_18))? (17.0 + x_16) : ((7.0 + x_17) > (11.0 + x_18)? (7.0 + x_17) : (11.0 + x_18)))));
  x_7_ = ((((3.0 + x_0) > (11.0 + x_3)? (3.0 + x_0) : (11.0 + x_3)) > ((12.0 + x_5) > ((3.0 + x_7) > (5.0 + x_10)? (3.0 + x_7) : (5.0 + x_10))? (12.0 + x_5) : ((3.0 + x_7) > (5.0 + x_10)? (3.0 + x_7) : (5.0 + x_10)))? ((3.0 + x_0) > (11.0 + x_3)? (3.0 + x_0) : (11.0 + x_3)) : ((12.0 + x_5) > ((3.0 + x_7) > (5.0 + x_10)? (3.0 + x_7) : (5.0 + x_10))? (12.0 + x_5) : ((3.0 + x_7) > (5.0 + x_10)? (3.0 + x_7) : (5.0 + x_10)))) > (((5.0 + x_11) > (5.0 + x_14)? (5.0 + x_11) : (5.0 + x_14)) > ((20.0 + x_17) > ((14.0 + x_18) > (10.0 + x_19)? (14.0 + x_18) : (10.0 + x_19))? (20.0 + x_17) : ((14.0 + x_18) > (10.0 + x_19)? (14.0 + x_18) : (10.0 + x_19)))? ((5.0 + x_11) > (5.0 + x_14)? (5.0 + x_11) : (5.0 + x_14)) : ((20.0 + x_17) > ((14.0 + x_18) > (10.0 + x_19)? (14.0 + x_18) : (10.0 + x_19))? (20.0 + x_17) : ((14.0 + x_18) > (10.0 + x_19)? (14.0 + x_18) : (10.0 + x_19))))? (((3.0 + x_0) > (11.0 + x_3)? (3.0 + x_0) : (11.0 + x_3)) > ((12.0 + x_5) > ((3.0 + x_7) > (5.0 + x_10)? (3.0 + x_7) : (5.0 + x_10))? (12.0 + x_5) : ((3.0 + x_7) > (5.0 + x_10)? (3.0 + x_7) : (5.0 + x_10)))? ((3.0 + x_0) > (11.0 + x_3)? (3.0 + x_0) : (11.0 + x_3)) : ((12.0 + x_5) > ((3.0 + x_7) > (5.0 + x_10)? (3.0 + x_7) : (5.0 + x_10))? (12.0 + x_5) : ((3.0 + x_7) > (5.0 + x_10)? (3.0 + x_7) : (5.0 + x_10)))) : (((5.0 + x_11) > (5.0 + x_14)? (5.0 + x_11) : (5.0 + x_14)) > ((20.0 + x_17) > ((14.0 + x_18) > (10.0 + x_19)? (14.0 + x_18) : (10.0 + x_19))? (20.0 + x_17) : ((14.0 + x_18) > (10.0 + x_19)? (14.0 + x_18) : (10.0 + x_19)))? ((5.0 + x_11) > (5.0 + x_14)? (5.0 + x_11) : (5.0 + x_14)) : ((20.0 + x_17) > ((14.0 + x_18) > (10.0 + x_19)? (14.0 + x_18) : (10.0 + x_19))? (20.0 + x_17) : ((14.0 + x_18) > (10.0 + x_19)? (14.0 + x_18) : (10.0 + x_19)))));
  x_8_ = ((((15.0 + x_0) > (9.0 + x_3)? (15.0 + x_0) : (9.0 + x_3)) > ((4.0 + x_5) > ((16.0 + x_6) > (3.0 + x_9)? (16.0 + x_6) : (3.0 + x_9))? (4.0 + x_5) : ((16.0 + x_6) > (3.0 + x_9)? (16.0 + x_6) : (3.0 + x_9)))? ((15.0 + x_0) > (9.0 + x_3)? (15.0 + x_0) : (9.0 + x_3)) : ((4.0 + x_5) > ((16.0 + x_6) > (3.0 + x_9)? (16.0 + x_6) : (3.0 + x_9))? (4.0 + x_5) : ((16.0 + x_6) > (3.0 + x_9)? (16.0 + x_6) : (3.0 + x_9)))) > (((18.0 + x_10) > (1.0 + x_12)? (18.0 + x_10) : (1.0 + x_12)) > ((7.0 + x_16) > ((14.0 + x_17) > (10.0 + x_19)? (14.0 + x_17) : (10.0 + x_19))? (7.0 + x_16) : ((14.0 + x_17) > (10.0 + x_19)? (14.0 + x_17) : (10.0 + x_19)))? ((18.0 + x_10) > (1.0 + x_12)? (18.0 + x_10) : (1.0 + x_12)) : ((7.0 + x_16) > ((14.0 + x_17) > (10.0 + x_19)? (14.0 + x_17) : (10.0 + x_19))? (7.0 + x_16) : ((14.0 + x_17) > (10.0 + x_19)? (14.0 + x_17) : (10.0 + x_19))))? (((15.0 + x_0) > (9.0 + x_3)? (15.0 + x_0) : (9.0 + x_3)) > ((4.0 + x_5) > ((16.0 + x_6) > (3.0 + x_9)? (16.0 + x_6) : (3.0 + x_9))? (4.0 + x_5) : ((16.0 + x_6) > (3.0 + x_9)? (16.0 + x_6) : (3.0 + x_9)))? ((15.0 + x_0) > (9.0 + x_3)? (15.0 + x_0) : (9.0 + x_3)) : ((4.0 + x_5) > ((16.0 + x_6) > (3.0 + x_9)? (16.0 + x_6) : (3.0 + x_9))? (4.0 + x_5) : ((16.0 + x_6) > (3.0 + x_9)? (16.0 + x_6) : (3.0 + x_9)))) : (((18.0 + x_10) > (1.0 + x_12)? (18.0 + x_10) : (1.0 + x_12)) > ((7.0 + x_16) > ((14.0 + x_17) > (10.0 + x_19)? (14.0 + x_17) : (10.0 + x_19))? (7.0 + x_16) : ((14.0 + x_17) > (10.0 + x_19)? (14.0 + x_17) : (10.0 + x_19)))? ((18.0 + x_10) > (1.0 + x_12)? (18.0 + x_10) : (1.0 + x_12)) : ((7.0 + x_16) > ((14.0 + x_17) > (10.0 + x_19)? (14.0 + x_17) : (10.0 + x_19))? (7.0 + x_16) : ((14.0 + x_17) > (10.0 + x_19)? (14.0 + x_17) : (10.0 + x_19)))));
  x_9_ = ((((5.0 + x_3) > (4.0 + x_4)? (5.0 + x_3) : (4.0 + x_4)) > ((19.0 + x_5) > ((9.0 + x_6) > (5.0 + x_10)? (9.0 + x_6) : (5.0 + x_10))? (19.0 + x_5) : ((9.0 + x_6) > (5.0 + x_10)? (9.0 + x_6) : (5.0 + x_10)))? ((5.0 + x_3) > (4.0 + x_4)? (5.0 + x_3) : (4.0 + x_4)) : ((19.0 + x_5) > ((9.0 + x_6) > (5.0 + x_10)? (9.0 + x_6) : (5.0 + x_10))? (19.0 + x_5) : ((9.0 + x_6) > (5.0 + x_10)? (9.0 + x_6) : (5.0 + x_10)))) > (((12.0 + x_12) > (7.0 + x_14)? (12.0 + x_12) : (7.0 + x_14)) > ((12.0 + x_15) > ((20.0 + x_16) > (3.0 + x_17)? (20.0 + x_16) : (3.0 + x_17))? (12.0 + x_15) : ((20.0 + x_16) > (3.0 + x_17)? (20.0 + x_16) : (3.0 + x_17)))? ((12.0 + x_12) > (7.0 + x_14)? (12.0 + x_12) : (7.0 + x_14)) : ((12.0 + x_15) > ((20.0 + x_16) > (3.0 + x_17)? (20.0 + x_16) : (3.0 + x_17))? (12.0 + x_15) : ((20.0 + x_16) > (3.0 + x_17)? (20.0 + x_16) : (3.0 + x_17))))? (((5.0 + x_3) > (4.0 + x_4)? (5.0 + x_3) : (4.0 + x_4)) > ((19.0 + x_5) > ((9.0 + x_6) > (5.0 + x_10)? (9.0 + x_6) : (5.0 + x_10))? (19.0 + x_5) : ((9.0 + x_6) > (5.0 + x_10)? (9.0 + x_6) : (5.0 + x_10)))? ((5.0 + x_3) > (4.0 + x_4)? (5.0 + x_3) : (4.0 + x_4)) : ((19.0 + x_5) > ((9.0 + x_6) > (5.0 + x_10)? (9.0 + x_6) : (5.0 + x_10))? (19.0 + x_5) : ((9.0 + x_6) > (5.0 + x_10)? (9.0 + x_6) : (5.0 + x_10)))) : (((12.0 + x_12) > (7.0 + x_14)? (12.0 + x_12) : (7.0 + x_14)) > ((12.0 + x_15) > ((20.0 + x_16) > (3.0 + x_17)? (20.0 + x_16) : (3.0 + x_17))? (12.0 + x_15) : ((20.0 + x_16) > (3.0 + x_17)? (20.0 + x_16) : (3.0 + x_17)))? ((12.0 + x_12) > (7.0 + x_14)? (12.0 + x_12) : (7.0 + x_14)) : ((12.0 + x_15) > ((20.0 + x_16) > (3.0 + x_17)? (20.0 + x_16) : (3.0 + x_17))? (12.0 + x_15) : ((20.0 + x_16) > (3.0 + x_17)? (20.0 + x_16) : (3.0 + x_17)))));
  x_10_ = ((((20.0 + x_0) > (12.0 + x_3)? (20.0 + x_0) : (12.0 + x_3)) > ((18.0 + x_6) > ((8.0 + x_8) > (8.0 + x_9)? (8.0 + x_8) : (8.0 + x_9))? (18.0 + x_6) : ((8.0 + x_8) > (8.0 + x_9)? (8.0 + x_8) : (8.0 + x_9)))? ((20.0 + x_0) > (12.0 + x_3)? (20.0 + x_0) : (12.0 + x_3)) : ((18.0 + x_6) > ((8.0 + x_8) > (8.0 + x_9)? (8.0 + x_8) : (8.0 + x_9))? (18.0 + x_6) : ((8.0 + x_8) > (8.0 + x_9)? (8.0 + x_8) : (8.0 + x_9)))) > (((2.0 + x_10) > (16.0 + x_11)? (2.0 + x_10) : (16.0 + x_11)) > ((18.0 + x_16) > ((20.0 + x_17) > (11.0 + x_19)? (20.0 + x_17) : (11.0 + x_19))? (18.0 + x_16) : ((20.0 + x_17) > (11.0 + x_19)? (20.0 + x_17) : (11.0 + x_19)))? ((2.0 + x_10) > (16.0 + x_11)? (2.0 + x_10) : (16.0 + x_11)) : ((18.0 + x_16) > ((20.0 + x_17) > (11.0 + x_19)? (20.0 + x_17) : (11.0 + x_19))? (18.0 + x_16) : ((20.0 + x_17) > (11.0 + x_19)? (20.0 + x_17) : (11.0 + x_19))))? (((20.0 + x_0) > (12.0 + x_3)? (20.0 + x_0) : (12.0 + x_3)) > ((18.0 + x_6) > ((8.0 + x_8) > (8.0 + x_9)? (8.0 + x_8) : (8.0 + x_9))? (18.0 + x_6) : ((8.0 + x_8) > (8.0 + x_9)? (8.0 + x_8) : (8.0 + x_9)))? ((20.0 + x_0) > (12.0 + x_3)? (20.0 + x_0) : (12.0 + x_3)) : ((18.0 + x_6) > ((8.0 + x_8) > (8.0 + x_9)? (8.0 + x_8) : (8.0 + x_9))? (18.0 + x_6) : ((8.0 + x_8) > (8.0 + x_9)? (8.0 + x_8) : (8.0 + x_9)))) : (((2.0 + x_10) > (16.0 + x_11)? (2.0 + x_10) : (16.0 + x_11)) > ((18.0 + x_16) > ((20.0 + x_17) > (11.0 + x_19)? (20.0 + x_17) : (11.0 + x_19))? (18.0 + x_16) : ((20.0 + x_17) > (11.0 + x_19)? (20.0 + x_17) : (11.0 + x_19)))? ((2.0 + x_10) > (16.0 + x_11)? (2.0 + x_10) : (16.0 + x_11)) : ((18.0 + x_16) > ((20.0 + x_17) > (11.0 + x_19)? (20.0 + x_17) : (11.0 + x_19))? (18.0 + x_16) : ((20.0 + x_17) > (11.0 + x_19)? (20.0 + x_17) : (11.0 + x_19)))));
  x_11_ = ((((8.0 + x_0) > (4.0 + x_4)? (8.0 + x_0) : (4.0 + x_4)) > ((2.0 + x_7) > ((12.0 + x_8) > (17.0 + x_10)? (12.0 + x_8) : (17.0 + x_10))? (2.0 + x_7) : ((12.0 + x_8) > (17.0 + x_10)? (12.0 + x_8) : (17.0 + x_10)))? ((8.0 + x_0) > (4.0 + x_4)? (8.0 + x_0) : (4.0 + x_4)) : ((2.0 + x_7) > ((12.0 + x_8) > (17.0 + x_10)? (12.0 + x_8) : (17.0 + x_10))? (2.0 + x_7) : ((12.0 + x_8) > (17.0 + x_10)? (12.0 + x_8) : (17.0 + x_10)))) > (((17.0 + x_11) > (19.0 + x_12)? (17.0 + x_11) : (19.0 + x_12)) > ((9.0 + x_15) > ((20.0 + x_18) > (11.0 + x_19)? (20.0 + x_18) : (11.0 + x_19))? (9.0 + x_15) : ((20.0 + x_18) > (11.0 + x_19)? (20.0 + x_18) : (11.0 + x_19)))? ((17.0 + x_11) > (19.0 + x_12)? (17.0 + x_11) : (19.0 + x_12)) : ((9.0 + x_15) > ((20.0 + x_18) > (11.0 + x_19)? (20.0 + x_18) : (11.0 + x_19))? (9.0 + x_15) : ((20.0 + x_18) > (11.0 + x_19)? (20.0 + x_18) : (11.0 + x_19))))? (((8.0 + x_0) > (4.0 + x_4)? (8.0 + x_0) : (4.0 + x_4)) > ((2.0 + x_7) > ((12.0 + x_8) > (17.0 + x_10)? (12.0 + x_8) : (17.0 + x_10))? (2.0 + x_7) : ((12.0 + x_8) > (17.0 + x_10)? (12.0 + x_8) : (17.0 + x_10)))? ((8.0 + x_0) > (4.0 + x_4)? (8.0 + x_0) : (4.0 + x_4)) : ((2.0 + x_7) > ((12.0 + x_8) > (17.0 + x_10)? (12.0 + x_8) : (17.0 + x_10))? (2.0 + x_7) : ((12.0 + x_8) > (17.0 + x_10)? (12.0 + x_8) : (17.0 + x_10)))) : (((17.0 + x_11) > (19.0 + x_12)? (17.0 + x_11) : (19.0 + x_12)) > ((9.0 + x_15) > ((20.0 + x_18) > (11.0 + x_19)? (20.0 + x_18) : (11.0 + x_19))? (9.0 + x_15) : ((20.0 + x_18) > (11.0 + x_19)? (20.0 + x_18) : (11.0 + x_19)))? ((17.0 + x_11) > (19.0 + x_12)? (17.0 + x_11) : (19.0 + x_12)) : ((9.0 + x_15) > ((20.0 + x_18) > (11.0 + x_19)? (20.0 + x_18) : (11.0 + x_19))? (9.0 + x_15) : ((20.0 + x_18) > (11.0 + x_19)? (20.0 + x_18) : (11.0 + x_19)))));
  x_12_ = ((((20.0 + x_1) > (1.0 + x_5)? (20.0 + x_1) : (1.0 + x_5)) > ((18.0 + x_6) > ((14.0 + x_7) > (13.0 + x_8)? (14.0 + x_7) : (13.0 + x_8))? (18.0 + x_6) : ((14.0 + x_7) > (13.0 + x_8)? (14.0 + x_7) : (13.0 + x_8)))? ((20.0 + x_1) > (1.0 + x_5)? (20.0 + x_1) : (1.0 + x_5)) : ((18.0 + x_6) > ((14.0 + x_7) > (13.0 + x_8)? (14.0 + x_7) : (13.0 + x_8))? (18.0 + x_6) : ((14.0 + x_7) > (13.0 + x_8)? (14.0 + x_7) : (13.0 + x_8)))) > (((17.0 + x_10) > (9.0 + x_11)? (17.0 + x_10) : (9.0 + x_11)) > ((8.0 + x_12) > ((14.0 + x_13) > (12.0 + x_18)? (14.0 + x_13) : (12.0 + x_18))? (8.0 + x_12) : ((14.0 + x_13) > (12.0 + x_18)? (14.0 + x_13) : (12.0 + x_18)))? ((17.0 + x_10) > (9.0 + x_11)? (17.0 + x_10) : (9.0 + x_11)) : ((8.0 + x_12) > ((14.0 + x_13) > (12.0 + x_18)? (14.0 + x_13) : (12.0 + x_18))? (8.0 + x_12) : ((14.0 + x_13) > (12.0 + x_18)? (14.0 + x_13) : (12.0 + x_18))))? (((20.0 + x_1) > (1.0 + x_5)? (20.0 + x_1) : (1.0 + x_5)) > ((18.0 + x_6) > ((14.0 + x_7) > (13.0 + x_8)? (14.0 + x_7) : (13.0 + x_8))? (18.0 + x_6) : ((14.0 + x_7) > (13.0 + x_8)? (14.0 + x_7) : (13.0 + x_8)))? ((20.0 + x_1) > (1.0 + x_5)? (20.0 + x_1) : (1.0 + x_5)) : ((18.0 + x_6) > ((14.0 + x_7) > (13.0 + x_8)? (14.0 + x_7) : (13.0 + x_8))? (18.0 + x_6) : ((14.0 + x_7) > (13.0 + x_8)? (14.0 + x_7) : (13.0 + x_8)))) : (((17.0 + x_10) > (9.0 + x_11)? (17.0 + x_10) : (9.0 + x_11)) > ((8.0 + x_12) > ((14.0 + x_13) > (12.0 + x_18)? (14.0 + x_13) : (12.0 + x_18))? (8.0 + x_12) : ((14.0 + x_13) > (12.0 + x_18)? (14.0 + x_13) : (12.0 + x_18)))? ((17.0 + x_10) > (9.0 + x_11)? (17.0 + x_10) : (9.0 + x_11)) : ((8.0 + x_12) > ((14.0 + x_13) > (12.0 + x_18)? (14.0 + x_13) : (12.0 + x_18))? (8.0 + x_12) : ((14.0 + x_13) > (12.0 + x_18)? (14.0 + x_13) : (12.0 + x_18)))));
  x_13_ = ((((10.0 + x_0) > (15.0 + x_1)? (10.0 + x_0) : (15.0 + x_1)) > ((4.0 + x_2) > ((13.0 + x_7) > (15.0 + x_10)? (13.0 + x_7) : (15.0 + x_10))? (4.0 + x_2) : ((13.0 + x_7) > (15.0 + x_10)? (13.0 + x_7) : (15.0 + x_10)))? ((10.0 + x_0) > (15.0 + x_1)? (10.0 + x_0) : (15.0 + x_1)) : ((4.0 + x_2) > ((13.0 + x_7) > (15.0 + x_10)? (13.0 + x_7) : (15.0 + x_10))? (4.0 + x_2) : ((13.0 + x_7) > (15.0 + x_10)? (13.0 + x_7) : (15.0 + x_10)))) > (((17.0 + x_12) > (19.0 + x_13)? (17.0 + x_12) : (19.0 + x_13)) > ((7.0 + x_14) > ((3.0 + x_15) > (15.0 + x_18)? (3.0 + x_15) : (15.0 + x_18))? (7.0 + x_14) : ((3.0 + x_15) > (15.0 + x_18)? (3.0 + x_15) : (15.0 + x_18)))? ((17.0 + x_12) > (19.0 + x_13)? (17.0 + x_12) : (19.0 + x_13)) : ((7.0 + x_14) > ((3.0 + x_15) > (15.0 + x_18)? (3.0 + x_15) : (15.0 + x_18))? (7.0 + x_14) : ((3.0 + x_15) > (15.0 + x_18)? (3.0 + x_15) : (15.0 + x_18))))? (((10.0 + x_0) > (15.0 + x_1)? (10.0 + x_0) : (15.0 + x_1)) > ((4.0 + x_2) > ((13.0 + x_7) > (15.0 + x_10)? (13.0 + x_7) : (15.0 + x_10))? (4.0 + x_2) : ((13.0 + x_7) > (15.0 + x_10)? (13.0 + x_7) : (15.0 + x_10)))? ((10.0 + x_0) > (15.0 + x_1)? (10.0 + x_0) : (15.0 + x_1)) : ((4.0 + x_2) > ((13.0 + x_7) > (15.0 + x_10)? (13.0 + x_7) : (15.0 + x_10))? (4.0 + x_2) : ((13.0 + x_7) > (15.0 + x_10)? (13.0 + x_7) : (15.0 + x_10)))) : (((17.0 + x_12) > (19.0 + x_13)? (17.0 + x_12) : (19.0 + x_13)) > ((7.0 + x_14) > ((3.0 + x_15) > (15.0 + x_18)? (3.0 + x_15) : (15.0 + x_18))? (7.0 + x_14) : ((3.0 + x_15) > (15.0 + x_18)? (3.0 + x_15) : (15.0 + x_18)))? ((17.0 + x_12) > (19.0 + x_13)? (17.0 + x_12) : (19.0 + x_13)) : ((7.0 + x_14) > ((3.0 + x_15) > (15.0 + x_18)? (3.0 + x_15) : (15.0 + x_18))? (7.0 + x_14) : ((3.0 + x_15) > (15.0 + x_18)? (3.0 + x_15) : (15.0 + x_18)))));
  x_14_ = ((((1.0 + x_0) > (1.0 + x_1)? (1.0 + x_0) : (1.0 + x_1)) > ((16.0 + x_4) > ((20.0 + x_8) > (12.0 + x_9)? (20.0 + x_8) : (12.0 + x_9))? (16.0 + x_4) : ((20.0 + x_8) > (12.0 + x_9)? (20.0 + x_8) : (12.0 + x_9)))? ((1.0 + x_0) > (1.0 + x_1)? (1.0 + x_0) : (1.0 + x_1)) : ((16.0 + x_4) > ((20.0 + x_8) > (12.0 + x_9)? (20.0 + x_8) : (12.0 + x_9))? (16.0 + x_4) : ((20.0 + x_8) > (12.0 + x_9)? (20.0 + x_8) : (12.0 + x_9)))) > (((9.0 + x_10) > (15.0 + x_11)? (9.0 + x_10) : (15.0 + x_11)) > ((11.0 + x_14) > ((9.0 + x_18) > (7.0 + x_19)? (9.0 + x_18) : (7.0 + x_19))? (11.0 + x_14) : ((9.0 + x_18) > (7.0 + x_19)? (9.0 + x_18) : (7.0 + x_19)))? ((9.0 + x_10) > (15.0 + x_11)? (9.0 + x_10) : (15.0 + x_11)) : ((11.0 + x_14) > ((9.0 + x_18) > (7.0 + x_19)? (9.0 + x_18) : (7.0 + x_19))? (11.0 + x_14) : ((9.0 + x_18) > (7.0 + x_19)? (9.0 + x_18) : (7.0 + x_19))))? (((1.0 + x_0) > (1.0 + x_1)? (1.0 + x_0) : (1.0 + x_1)) > ((16.0 + x_4) > ((20.0 + x_8) > (12.0 + x_9)? (20.0 + x_8) : (12.0 + x_9))? (16.0 + x_4) : ((20.0 + x_8) > (12.0 + x_9)? (20.0 + x_8) : (12.0 + x_9)))? ((1.0 + x_0) > (1.0 + x_1)? (1.0 + x_0) : (1.0 + x_1)) : ((16.0 + x_4) > ((20.0 + x_8) > (12.0 + x_9)? (20.0 + x_8) : (12.0 + x_9))? (16.0 + x_4) : ((20.0 + x_8) > (12.0 + x_9)? (20.0 + x_8) : (12.0 + x_9)))) : (((9.0 + x_10) > (15.0 + x_11)? (9.0 + x_10) : (15.0 + x_11)) > ((11.0 + x_14) > ((9.0 + x_18) > (7.0 + x_19)? (9.0 + x_18) : (7.0 + x_19))? (11.0 + x_14) : ((9.0 + x_18) > (7.0 + x_19)? (9.0 + x_18) : (7.0 + x_19)))? ((9.0 + x_10) > (15.0 + x_11)? (9.0 + x_10) : (15.0 + x_11)) : ((11.0 + x_14) > ((9.0 + x_18) > (7.0 + x_19)? (9.0 + x_18) : (7.0 + x_19))? (11.0 + x_14) : ((9.0 + x_18) > (7.0 + x_19)? (9.0 + x_18) : (7.0 + x_19)))));
  x_15_ = ((((17.0 + x_1) > (18.0 + x_3)? (17.0 + x_1) : (18.0 + x_3)) > ((18.0 + x_6) > ((5.0 + x_9) > (16.0 + x_10)? (5.0 + x_9) : (16.0 + x_10))? (18.0 + x_6) : ((5.0 + x_9) > (16.0 + x_10)? (5.0 + x_9) : (16.0 + x_10)))? ((17.0 + x_1) > (18.0 + x_3)? (17.0 + x_1) : (18.0 + x_3)) : ((18.0 + x_6) > ((5.0 + x_9) > (16.0 + x_10)? (5.0 + x_9) : (16.0 + x_10))? (18.0 + x_6) : ((5.0 + x_9) > (16.0 + x_10)? (5.0 + x_9) : (16.0 + x_10)))) > (((5.0 + x_13) > (14.0 + x_14)? (5.0 + x_13) : (14.0 + x_14)) > ((10.0 + x_17) > ((13.0 + x_18) > (9.0 + x_19)? (13.0 + x_18) : (9.0 + x_19))? (10.0 + x_17) : ((13.0 + x_18) > (9.0 + x_19)? (13.0 + x_18) : (9.0 + x_19)))? ((5.0 + x_13) > (14.0 + x_14)? (5.0 + x_13) : (14.0 + x_14)) : ((10.0 + x_17) > ((13.0 + x_18) > (9.0 + x_19)? (13.0 + x_18) : (9.0 + x_19))? (10.0 + x_17) : ((13.0 + x_18) > (9.0 + x_19)? (13.0 + x_18) : (9.0 + x_19))))? (((17.0 + x_1) > (18.0 + x_3)? (17.0 + x_1) : (18.0 + x_3)) > ((18.0 + x_6) > ((5.0 + x_9) > (16.0 + x_10)? (5.0 + x_9) : (16.0 + x_10))? (18.0 + x_6) : ((5.0 + x_9) > (16.0 + x_10)? (5.0 + x_9) : (16.0 + x_10)))? ((17.0 + x_1) > (18.0 + x_3)? (17.0 + x_1) : (18.0 + x_3)) : ((18.0 + x_6) > ((5.0 + x_9) > (16.0 + x_10)? (5.0 + x_9) : (16.0 + x_10))? (18.0 + x_6) : ((5.0 + x_9) > (16.0 + x_10)? (5.0 + x_9) : (16.0 + x_10)))) : (((5.0 + x_13) > (14.0 + x_14)? (5.0 + x_13) : (14.0 + x_14)) > ((10.0 + x_17) > ((13.0 + x_18) > (9.0 + x_19)? (13.0 + x_18) : (9.0 + x_19))? (10.0 + x_17) : ((13.0 + x_18) > (9.0 + x_19)? (13.0 + x_18) : (9.0 + x_19)))? ((5.0 + x_13) > (14.0 + x_14)? (5.0 + x_13) : (14.0 + x_14)) : ((10.0 + x_17) > ((13.0 + x_18) > (9.0 + x_19)? (13.0 + x_18) : (9.0 + x_19))? (10.0 + x_17) : ((13.0 + x_18) > (9.0 + x_19)? (13.0 + x_18) : (9.0 + x_19)))));
  x_16_ = ((((14.0 + x_0) > (2.0 + x_1)? (14.0 + x_0) : (2.0 + x_1)) > ((3.0 + x_4) > ((18.0 + x_5) > (8.0 + x_6)? (18.0 + x_5) : (8.0 + x_6))? (3.0 + x_4) : ((18.0 + x_5) > (8.0 + x_6)? (18.0 + x_5) : (8.0 + x_6)))? ((14.0 + x_0) > (2.0 + x_1)? (14.0 + x_0) : (2.0 + x_1)) : ((3.0 + x_4) > ((18.0 + x_5) > (8.0 + x_6)? (18.0 + x_5) : (8.0 + x_6))? (3.0 + x_4) : ((18.0 + x_5) > (8.0 + x_6)? (18.0 + x_5) : (8.0 + x_6)))) > (((17.0 + x_9) > (17.0 + x_12)? (17.0 + x_9) : (17.0 + x_12)) > ((2.0 + x_13) > ((4.0 + x_15) > (1.0 + x_17)? (4.0 + x_15) : (1.0 + x_17))? (2.0 + x_13) : ((4.0 + x_15) > (1.0 + x_17)? (4.0 + x_15) : (1.0 + x_17)))? ((17.0 + x_9) > (17.0 + x_12)? (17.0 + x_9) : (17.0 + x_12)) : ((2.0 + x_13) > ((4.0 + x_15) > (1.0 + x_17)? (4.0 + x_15) : (1.0 + x_17))? (2.0 + x_13) : ((4.0 + x_15) > (1.0 + x_17)? (4.0 + x_15) : (1.0 + x_17))))? (((14.0 + x_0) > (2.0 + x_1)? (14.0 + x_0) : (2.0 + x_1)) > ((3.0 + x_4) > ((18.0 + x_5) > (8.0 + x_6)? (18.0 + x_5) : (8.0 + x_6))? (3.0 + x_4) : ((18.0 + x_5) > (8.0 + x_6)? (18.0 + x_5) : (8.0 + x_6)))? ((14.0 + x_0) > (2.0 + x_1)? (14.0 + x_0) : (2.0 + x_1)) : ((3.0 + x_4) > ((18.0 + x_5) > (8.0 + x_6)? (18.0 + x_5) : (8.0 + x_6))? (3.0 + x_4) : ((18.0 + x_5) > (8.0 + x_6)? (18.0 + x_5) : (8.0 + x_6)))) : (((17.0 + x_9) > (17.0 + x_12)? (17.0 + x_9) : (17.0 + x_12)) > ((2.0 + x_13) > ((4.0 + x_15) > (1.0 + x_17)? (4.0 + x_15) : (1.0 + x_17))? (2.0 + x_13) : ((4.0 + x_15) > (1.0 + x_17)? (4.0 + x_15) : (1.0 + x_17)))? ((17.0 + x_9) > (17.0 + x_12)? (17.0 + x_9) : (17.0 + x_12)) : ((2.0 + x_13) > ((4.0 + x_15) > (1.0 + x_17)? (4.0 + x_15) : (1.0 + x_17))? (2.0 + x_13) : ((4.0 + x_15) > (1.0 + x_17)? (4.0 + x_15) : (1.0 + x_17)))));
  x_17_ = ((((16.0 + x_0) > (14.0 + x_4)? (16.0 + x_0) : (14.0 + x_4)) > ((20.0 + x_6) > ((15.0 + x_7) > (2.0 + x_8)? (15.0 + x_7) : (2.0 + x_8))? (20.0 + x_6) : ((15.0 + x_7) > (2.0 + x_8)? (15.0 + x_7) : (2.0 + x_8)))? ((16.0 + x_0) > (14.0 + x_4)? (16.0 + x_0) : (14.0 + x_4)) : ((20.0 + x_6) > ((15.0 + x_7) > (2.0 + x_8)? (15.0 + x_7) : (2.0 + x_8))? (20.0 + x_6) : ((15.0 + x_7) > (2.0 + x_8)? (15.0 + x_7) : (2.0 + x_8)))) > (((5.0 + x_11) > (13.0 + x_14)? (5.0 + x_11) : (13.0 + x_14)) > ((10.0 + x_16) > ((4.0 + x_18) > (1.0 + x_19)? (4.0 + x_18) : (1.0 + x_19))? (10.0 + x_16) : ((4.0 + x_18) > (1.0 + x_19)? (4.0 + x_18) : (1.0 + x_19)))? ((5.0 + x_11) > (13.0 + x_14)? (5.0 + x_11) : (13.0 + x_14)) : ((10.0 + x_16) > ((4.0 + x_18) > (1.0 + x_19)? (4.0 + x_18) : (1.0 + x_19))? (10.0 + x_16) : ((4.0 + x_18) > (1.0 + x_19)? (4.0 + x_18) : (1.0 + x_19))))? (((16.0 + x_0) > (14.0 + x_4)? (16.0 + x_0) : (14.0 + x_4)) > ((20.0 + x_6) > ((15.0 + x_7) > (2.0 + x_8)? (15.0 + x_7) : (2.0 + x_8))? (20.0 + x_6) : ((15.0 + x_7) > (2.0 + x_8)? (15.0 + x_7) : (2.0 + x_8)))? ((16.0 + x_0) > (14.0 + x_4)? (16.0 + x_0) : (14.0 + x_4)) : ((20.0 + x_6) > ((15.0 + x_7) > (2.0 + x_8)? (15.0 + x_7) : (2.0 + x_8))? (20.0 + x_6) : ((15.0 + x_7) > (2.0 + x_8)? (15.0 + x_7) : (2.0 + x_8)))) : (((5.0 + x_11) > (13.0 + x_14)? (5.0 + x_11) : (13.0 + x_14)) > ((10.0 + x_16) > ((4.0 + x_18) > (1.0 + x_19)? (4.0 + x_18) : (1.0 + x_19))? (10.0 + x_16) : ((4.0 + x_18) > (1.0 + x_19)? (4.0 + x_18) : (1.0 + x_19)))? ((5.0 + x_11) > (13.0 + x_14)? (5.0 + x_11) : (13.0 + x_14)) : ((10.0 + x_16) > ((4.0 + x_18) > (1.0 + x_19)? (4.0 + x_18) : (1.0 + x_19))? (10.0 + x_16) : ((4.0 + x_18) > (1.0 + x_19)? (4.0 + x_18) : (1.0 + x_19)))));
  x_18_ = ((((9.0 + x_0) > (12.0 + x_5)? (9.0 + x_0) : (12.0 + x_5)) > ((19.0 + x_6) > ((11.0 + x_7) > (9.0 + x_9)? (11.0 + x_7) : (9.0 + x_9))? (19.0 + x_6) : ((11.0 + x_7) > (9.0 + x_9)? (11.0 + x_7) : (9.0 + x_9)))? ((9.0 + x_0) > (12.0 + x_5)? (9.0 + x_0) : (12.0 + x_5)) : ((19.0 + x_6) > ((11.0 + x_7) > (9.0 + x_9)? (11.0 + x_7) : (9.0 + x_9))? (19.0 + x_6) : ((11.0 + x_7) > (9.0 + x_9)? (11.0 + x_7) : (9.0 + x_9)))) > (((19.0 + x_10) > (20.0 + x_11)? (19.0 + x_10) : (20.0 + x_11)) > ((2.0 + x_12) > ((17.0 + x_13) > (7.0 + x_15)? (17.0 + x_13) : (7.0 + x_15))? (2.0 + x_12) : ((17.0 + x_13) > (7.0 + x_15)? (17.0 + x_13) : (7.0 + x_15)))? ((19.0 + x_10) > (20.0 + x_11)? (19.0 + x_10) : (20.0 + x_11)) : ((2.0 + x_12) > ((17.0 + x_13) > (7.0 + x_15)? (17.0 + x_13) : (7.0 + x_15))? (2.0 + x_12) : ((17.0 + x_13) > (7.0 + x_15)? (17.0 + x_13) : (7.0 + x_15))))? (((9.0 + x_0) > (12.0 + x_5)? (9.0 + x_0) : (12.0 + x_5)) > ((19.0 + x_6) > ((11.0 + x_7) > (9.0 + x_9)? (11.0 + x_7) : (9.0 + x_9))? (19.0 + x_6) : ((11.0 + x_7) > (9.0 + x_9)? (11.0 + x_7) : (9.0 + x_9)))? ((9.0 + x_0) > (12.0 + x_5)? (9.0 + x_0) : (12.0 + x_5)) : ((19.0 + x_6) > ((11.0 + x_7) > (9.0 + x_9)? (11.0 + x_7) : (9.0 + x_9))? (19.0 + x_6) : ((11.0 + x_7) > (9.0 + x_9)? (11.0 + x_7) : (9.0 + x_9)))) : (((19.0 + x_10) > (20.0 + x_11)? (19.0 + x_10) : (20.0 + x_11)) > ((2.0 + x_12) > ((17.0 + x_13) > (7.0 + x_15)? (17.0 + x_13) : (7.0 + x_15))? (2.0 + x_12) : ((17.0 + x_13) > (7.0 + x_15)? (17.0 + x_13) : (7.0 + x_15)))? ((19.0 + x_10) > (20.0 + x_11)? (19.0 + x_10) : (20.0 + x_11)) : ((2.0 + x_12) > ((17.0 + x_13) > (7.0 + x_15)? (17.0 + x_13) : (7.0 + x_15))? (2.0 + x_12) : ((17.0 + x_13) > (7.0 + x_15)? (17.0 + x_13) : (7.0 + x_15)))));
  x_19_ = ((((6.0 + x_0) > (18.0 + x_1)? (6.0 + x_0) : (18.0 + x_1)) > ((2.0 + x_3) > ((4.0 + x_7) > (1.0 + x_9)? (4.0 + x_7) : (1.0 + x_9))? (2.0 + x_3) : ((4.0 + x_7) > (1.0 + x_9)? (4.0 + x_7) : (1.0 + x_9)))? ((6.0 + x_0) > (18.0 + x_1)? (6.0 + x_0) : (18.0 + x_1)) : ((2.0 + x_3) > ((4.0 + x_7) > (1.0 + x_9)? (4.0 + x_7) : (1.0 + x_9))? (2.0 + x_3) : ((4.0 + x_7) > (1.0 + x_9)? (4.0 + x_7) : (1.0 + x_9)))) > (((2.0 + x_10) > (11.0 + x_14)? (2.0 + x_10) : (11.0 + x_14)) > ((2.0 + x_16) > ((16.0 + x_17) > (5.0 + x_19)? (16.0 + x_17) : (5.0 + x_19))? (2.0 + x_16) : ((16.0 + x_17) > (5.0 + x_19)? (16.0 + x_17) : (5.0 + x_19)))? ((2.0 + x_10) > (11.0 + x_14)? (2.0 + x_10) : (11.0 + x_14)) : ((2.0 + x_16) > ((16.0 + x_17) > (5.0 + x_19)? (16.0 + x_17) : (5.0 + x_19))? (2.0 + x_16) : ((16.0 + x_17) > (5.0 + x_19)? (16.0 + x_17) : (5.0 + x_19))))? (((6.0 + x_0) > (18.0 + x_1)? (6.0 + x_0) : (18.0 + x_1)) > ((2.0 + x_3) > ((4.0 + x_7) > (1.0 + x_9)? (4.0 + x_7) : (1.0 + x_9))? (2.0 + x_3) : ((4.0 + x_7) > (1.0 + x_9)? (4.0 + x_7) : (1.0 + x_9)))? ((6.0 + x_0) > (18.0 + x_1)? (6.0 + x_0) : (18.0 + x_1)) : ((2.0 + x_3) > ((4.0 + x_7) > (1.0 + x_9)? (4.0 + x_7) : (1.0 + x_9))? (2.0 + x_3) : ((4.0 + x_7) > (1.0 + x_9)? (4.0 + x_7) : (1.0 + x_9)))) : (((2.0 + x_10) > (11.0 + x_14)? (2.0 + x_10) : (11.0 + x_14)) > ((2.0 + x_16) > ((16.0 + x_17) > (5.0 + x_19)? (16.0 + x_17) : (5.0 + x_19))? (2.0 + x_16) : ((16.0 + x_17) > (5.0 + x_19)? (16.0 + x_17) : (5.0 + x_19)))? ((2.0 + x_10) > (11.0 + x_14)? (2.0 + x_10) : (11.0 + x_14)) : ((2.0 + x_16) > ((16.0 + x_17) > (5.0 + x_19)? (16.0 + x_17) : (5.0 + x_19))? (2.0 + x_16) : ((16.0 + x_17) > (5.0 + x_19)? (16.0 + x_17) : (5.0 + x_19)))));
  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_;
    }
    return 0;
  }
  