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