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