Probably true things that the Halide simplifier can't prove

gistfile1.txt

 (max(((17 - (v0 % 4))/4), ((max(((min((v1*2), ((v0 % 2) + 5)) + (v0/2))/2), ((v0/4) + v1)) - (((v0 + -6)/4) + v1)) + 2)) <= 1024)
 (max(((17 - (v0 % 4))/4), ((((min((v1*2), ((v0 % 2) + 20)) + (v0/2))/2) - (((v0 + -6)/4) + v1)) + 2)) <= 1024)
 (max(((8 - (((v0*161) + v1) % 2))/2), ((((min((v2*2), 159) + ((v0*161) + v1))/2) - (((((v0*161) + v1) + -3)/2) + v2)) + 2)) <= 1024)
 (max(max(min(v0, 12), (min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(((v1 + -15)/16), (v2 + -1)), ((v1 + -14)/16)), ((v1 + -13)/16)), ((v1 + -2)/16)), ((v1 + -1)/16)), ((v1 + 1)/16)), ((v3 + -2)/16)), ((v3 + -1)/16)), ((v4 + -2)/16)), ((v4 + -1)/16)), ((v5 + -2)/16)), ((v5 + -1)/16)), ((v6 + -2)/16)), ((v6 + -1)/16)), 11) + 1)), 0) <= max(min(v0, 12), 0))
 (max(max(min(((v0 + 131)/144), 2), (min(((min((min(min(min(min(min(min((min((((v1 + v2) + 25)/2), v3) - ((v4*288) + v5)), v6), (min((((v1 + v2) + 29)/2), v3) - ((v4*288) + v5))), (v7 + 13)), v8), v9), (v7 + 15)) + 128), v8) + -140)/144), 1) + 1)), 0) <= max(min(((v0 + 131)/144), 2), 0))
 (max(max(min(v0, 24), (min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(((v1 + -15)/16), (v2 + -1)), ((v1 + -14)/16)), ((v1 + -13)/16)), ((v1 + -2)/16)), ((v1 + -1)/16)), ((v1 + 1)/16)), ((v3 + -2)/16)), ((v3 + -1)/16)), ((v4 + -2)/16)), ((v4 + -1)/16)), ((v5 + -2)/16)), ((v5 + -1)/16)), ((v6 + -2)/16)), ((v6 + -1)/16)), 23) + 1)), 0) <= max(min(v0, 24), 0))
 (max(max(min(v0, 2), (min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min((min(min(min(v1, v2), v3), v4) + -1), v2), ((v5 + -208)/192)), ((v5 + -207)/192)), ((v5 + -206)/192)), ((v5 + -205)/192)), ((v5 + -191)/192)), ((v5 + -4)/192)), ((v5 + -3)/192)), ((v5 + -2)/192)), ((v5 + -1)/192)), ((v6 + -210)/192)), ((v6 + -209)/192)), ((v6 + -208)/192)), ((v6 + -207)/192)), ((v6 + -206)/192)), ((v6 + -205)/192)), ((v6 + -204)/192)), ((v6 + -203)/192)), ((v6 + -194)/192)), ((v6 + -193)/192)), ((v6 + -191)/192)), ((v6 + -190)/192)), ((v6 + -189)/192)), ((v6 + -4)/192)), ((v6 + -3)/192)), ((v6 + -2)/192)), ((v6 + -1)/192)), ((v6 + 1)/192)), ((v6 + 2)/192)), ((v6 + 3)/192)), (((((((v7 + v8) + -209)/2)*2) - ((v9*384) + v10)) + -1)/192)), ((v11 + -1)/192)), ((v12 + -1)/192)), (((((((v7 + v8) + -203)/2)*2) - ((v9*384) + v10)) + -1)/192)), ((v13 + -1)/192)), ((v14 + -1)/192)), ((v15 + -1)/192)), (((((((v7 + v8) + -31)/2)*2) - ((v9*384) + v10)) + -178)/192)), ((v16 + -178)/192)), ((v17 + -184)/192)), ((v17 + -182)/192)), ((v17 + -178)/192)), ((v18 + -184)/192)), ((v18 + -182)/192)), ((v19 + -178)/192)), ((v20 + -182)/192)), ((v20 + -178)/192)), ((v21 + -182)/192)), ((v22 + -2)/192)), ((v22 + -1)/192)), ((v23 + -2)/192)), ((v23 + -1)/192)), ((v24 + -4)/192)), ((v24 + -2)/192)), ((v24 + -1)/192)), ((v25 + -4)/192)), ((v25 + -2)/192)), ((v25 + -1)/192)), 1) + 1)), 0) <= max(min(v0, 2), 0))
 (max(max(min(v0, 2), (min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min((min(min(min(v1, v2), v3), v4) + -1), v2), ((v5 + -191)/192)), ((v5 + -2)/192)), ((v5 + -1)/192)), ((v6 + -210)/192)), ((v6 + -209)/192)), ((v6 + -208)/192)), ((v6 + -207)/192)), ((v6 + -206)/192)), ((v6 + -205)/192)), ((v6 + -204)/192)), ((v6 + -203)/192)), ((v6 + -194)/192)), ((v6 + -193)/192)), ((v6 + -191)/192)), ((v6 + -190)/192)), ((v6 + -189)/192)), ((v6 + -4)/192)), ((v6 + -3)/192)), ((v6 + -2)/192)), ((v6 + -1)/192)), ((v6 + 1)/192)), ((v6 + 2)/192)), ((v6 + 3)/192)), (((((((v7 + v8) + -209)/2)*2) - ((v9*384) + v10)) + -1)/192)), ((v11 + -1)/192)), ((v12 + -1)/192)), (((((((v7 + v8) + -203)/2)*2) - ((v9*384) + v10)) + -1)/192)), ((v13 + -1)/192)), ((v14 + -1)/192)), ((v15 + -1)/192)), (((((((v7 + v8) + -31)/2)*2) - ((v9*384) + v10)) + -178)/192)), ((v16 + -178)/192)), ((v17 + -184)/192)), ((v17 + -182)/192)), ((v17 + -178)/192)), ((v18 + -184)/192)), ((v18 + -182)/192)), ((v19 + -178)/192)), ((v20 + -182)/192)), ((v20 + -178)/192)), ((v21 + -182)/192)), ((v22 + -2)/192)), ((v22 + -1)/192)), ((v23 + -2)/192)), ((v23 + -1)/192)), ((v24 + -4)/192)), ((v24 + -2)/192)), ((v24 + -1)/192)), ((v25 + -4)/192)), ((v25 + -2)/192)), ((v25 + -1)/192)), 1) + 1)), 0) <= max(min(v0, 2), 0))
 (max(max(min(v0, 2), (min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min(min((min(v1, v2) + -1), v2), ((v3 + -191)/192)), ((v3 + -2)/192)), ((v3 + -1)/192)), ((v4 + -194)/192)), ((v4 + -193)/192)), ((v4 + -191)/192)), ((v4 + -190)/192)), ((v4 + -189)/192)), ((v4 + -2)/192)), ((v4 + -1)/192)), ((v4 + 1)/192)), ((v4 + 2)/192)), ((v4 + 3)/192)), (((((((v5 + v6) + -193)/2)*2) - ((v7*384) + v8)) + -1)/192)), ((v9 + -1)/192)), (((((((v5 + v6) + -189)/2)*2) - ((v7*384) + v8)) + -1)/192)), (((((((v5 + v6) + -15)/2)*2) - ((v7*384) + v8)) + -178)/192)), ((v10 + -182)/192)), ((v10 + -178)/192)), (((((((v5 + v6) + -11)/2)*2) - ((v7*384) + v8)) + -182)/192)), ((v11 + -2)/192)), ((v11 + -1)/192)), ((v12 + -2)/192)), ((v12 + -1)/192)), ((v13 + -2)/192)), ((v13 + -1)/192)), 1) + 1)), 0) <= max(min(v0, 2), 0))
 (max(min(min(v0, int32((select((float32((v1 + -1)) < 0.000000f), (float32((v1 + -1))*64.000000f), 0.000000f)*0.015625f))), (v1 + -2)), 0) <= max(min((v1 + -2), v0), 0))
 ((max(min((v0 + -2), int32(min(float32((v0 + -1)), 0.000000f))), 0) + -1) <= max((max(v1, 0) + 1), v1))
 (max(min(((v0 + v1) + -1), v2), v1) <= max(min((v0 + v1), v2), (v1 + 1)))
 (max(((v0 + -1)/2), (((v0 + -3)/2) + (((v0 + 1) % 2)*2))) <= ((v0 + 1)/2))
 (max((((((v0*161) + v1) + v2) + -1)/2), ((((((v0*161) + v1) + v2) + -3)/2) + ((((((v0*161) + v1) + v2) + 1) % 2)*2))) <= (((((v0*161) + v1) + v2) + 1)/2))
 ((max((v0/2), -2) + 1) <= max(((v0 + 3)/2), 0))
 (max((((((v0*41) + v1) + v2) + -1)/2), ((((((v0*41) + v1) + v2) + -3)/2) + ((((((v0*41) + v1) + v2) + 1) % 2)*2))) <= (((((v0*41) + v1) + v2) + 1)/2))
 (max((((((v0*81) + v1) + v2) + -1)/2), ((((((v0*81) + v1) + v2) + -3)/2) + ((((((v0*81) + v1) + v2) + 1) % 2)*2))) <= (((((v0*81) + v1) + v2) + 1)/2))
 (max(((v0 - v1)/2), -1) <= max((((v0 - v1) + 1)/2), 0))
 (min(min(min(min(((v0 - ((v1*144) + v2)) + 2), v3), (v3 + 1)), (min(min(min(min(min(min(min(min(min(min(v4, v5), v6), v7), v8), v9), v10), v11), v12), ((((v13 + v14) + -55)/4) - ((v1*144) + v2))), ((((v13 + v14) + -54)/4) - ((v1*144) + v2))) + 16)), (v15 + 17)) <= 12)
 (min(min(min((min((v0 - ((v1*144) + v2)), v3) + 1), v3), (v3 + 2)), (min(min(min(v4, v5), ((((v6 + v7) + -29)/2) - ((v1*144) + v2))), v8) + 16)) <= 14)
 (((min(((((min(v0, 101) + v1) + -163)/32) + (((v2 + -1)/8)*8)), (v3 + -8)) + -15)/2) <= ((v4/2) + ((((((min(((((min(v0, 101) + v1) + -163)/32) + (((v2 + 7)/8)*8)), v3) + 1)/2) - (v4/2)) + 1)/14)*14)))
 ((min(((((min(v0, 101) + v1) + -163)/32) + (((v2 + -1)/8)*8)), (v3 + -8)) + -18) <= (((((min(((((min(v0, 101) + v1) + -163)/32) + (((v2 + 7)/8)*8)), v3) - v4) + -1)/26)*26) + v4))
 (((min(((((min(v0, 101) + v1) + -163)/32) + (((v2 + -1)/8)*8)), (v3 + -8)) + 5)/2) <= ((v4/2) + ((((((min(((((min(v0, 101) + v1) + -163)/32) + (((v2 + 7)/8)*8)), v3) + 1)/2) - (v4/2)) + 1)/4)*4)))
 (((min((((min(v0, 101) + v1) + -227)/64), ((v2 + -29)/2)) + 1) <= (min((((min(v0, 101) + v1) + -163)/32), (v2 + -8))/2)) && (((min(((((min(v0, 101) + v1) + -163)/32) + ((((v2 - (((min(v0, 101) + v1) + -163)/32)) + -1)/8)*8)), (v2 + -8)) + -21)/2) <= min(((v2 + -29)/2), ((((min(v0, 101) + v1) + -227)/64) + (((((v2 + 1)/2) - (((min(v0, 101) + v1) + -227)/64))/16)*16)))))
 (((min((((min(v0, 11) + v1) + -25)/8), ((v2 + -23)/4)) + 1) <= (min((((min(v0, 11) + v1) + -17)/4), ((v2 + -13)/2))/2)) && (((min(((v2 + -13)/2), ((((min(v0, 11) + v1) + -17)/4) + ((((min((((v0 + v1) + 5)/2), v3)/2) - (((min(v0, 11) + v1) + -17)/4))/8)*8))) + -5)/2) <= min(((v2 + -23)/4), ((((min(v0, 11) + v1) + -25)/8) + (((((v2 + 5)/4) - (((min(v0, 11) + v1) + -25)/8))/8)*8)))))
 ((((min((((min(v0, 11) + v1) + -25)/8), ((v2 + -23)/4)) + 1) <= (min((((min(v0, 11) + v1) + -17)/4), ((v2 + -13)/2))/2)) && (((min(((v2 + -13)/2), ((((min(v0, 11) + v1) + -17)/4) + ((((min((((v0 + v1) + 5)/2), v3)/2) - (((min(v0, 11) + v1) + -17)/4))/8)*8))) + -5)/2) <= min(((v2 + -23)/4), ((((min(v0, 11) + v1) + -25)/8) + (((((v2 + 5)/4) - (((min(v0, 11) + v1) + -25)/8))/8)*8))))) && (((v4 + 1)/4) <= ((((((v4 + 5)/4) - v5)/2)*2) + v5)))
 (((min((((min(v0, 11) + v1) + -41)/16), ((v2 + -43)/8)) + 1) <= (min((((min(v0, 11) + v1) + -25)/8), ((v2 + -23)/4))/2)) && (((min(((v2 + -23)/4), ((((min(v0, 11) + v1) + -25)/8) + (((((v2 + 5)/4) - (((min(v0, 11) + v1) + -25)/8))/8)*8))) + -5)/2) <= min(((v2 + -43)/8), ((((min(v0, 11) + v1) + -41)/16) + (((((v2 + 13)/8) - (((min(v0, 11) + v1) + -41)/16))/8)*8)))))
 (((min(((((min(v0, 17) + v1) + -23)/4) + (((v2 + -1)/8)*8)), (v3 + -8)) + -183)/2) <= ((v4/2) + ((((((min(((((min(v0, 17) + v1) + -23)/4) + (((v2 + 7)/8)*8)), v3) + 1)/2) - (v4/2)) + 1)/98)*98)))
 (((min((((min(v0, 17) + v1) + -31)/8), ((v2 + -13)/2)) + 1) <= (min((((min(v0, 17) + v1) + -23)/4), (v2 + -8))/2)) && (((min(((((min(v0, 17) + v1) + -23)/4) + ((((v2 - (((min(v0, 17) + v1) + -23)/4)) + -1)/8)*8)), (v2 + -8)) + -5)/2) <= min(((v2 + -13)/2), ((((min(v0, 17) + v1) + -31)/8) + (((((v2 + 1)/2) - (((min(v0, 17) + v1) + -31)/8))/8)*8)))))
 (((min((((min(v0, 17) + v1) + -47)/16), ((v2 + -23)/4)) + 1) <= (min((((min(v0, 17) + v1) + -31)/8), ((v2 + -13)/2))/2)) && (((min(((v2 + -13)/2), ((((min(v0, 17) + v1) + -31)/8) + (((((v2 + 1)/2) - (((min(v0, 17) + v1) + -31)/8))/8)*8))) + -5)/2) <= min(((v2 + -23)/4), ((((min(v0, 17) + v1) + -47)/16) + (((((v2 + 5)/4) - (((min(v0, 17) + v1) + -47)/16))/8)*8)))))
 (((min(((((min(v0, 29) + v1) + -43)/8) + (((v2 + -1)/8)*8)), (v3 + -8)) + -87)/2) <= ((v4/2) + ((((((min(((((min(v0, 29) + v1) + -43)/8) + (((v2 + 7)/8)*8)), v3) + 1)/2) - (v4/2)) + 1)/50)*50)))
 (((min((((min(v0, 29) + v1) + -59)/16), ((v2 + -13)/2)) + 1) <= (min((((min(v0, 29) + v1) + -43)/8), (v2 + -8))/2)) && (((min(((((min(v0, 29) + v1) + -43)/8) + ((((v2 - (((min(v0, 29) + v1) + -43)/8)) + -1)/8)*8)), (v2 + -8)) + -5)/2) <= min(((v2 + -13)/2), ((((min(v0, 29) + v1) + -59)/16) + (((((v2 + 1)/2) - (((min(v0, 29) + v1) + -59)/16))/8)*8)))))
 (((min((((min(v0, 29) + v1) + -91)/32), ((v2 + -23)/4)) + 1) <= (min((((min(v0, 29) + v1) + -59)/16), ((v2 + -13)/2))/2)) && (((min(((v2 + -13)/2), ((((min(v0, 29) + v1) + -59)/16) + (((((v2 + 1)/2) - (((min(v0, 29) + v1) + -59)/16))/8)*8))) + -5)/2) <= min(((v2 + -23)/4), ((((min(v0, 29) + v1) + -91)/32) + (((((v2 + 5)/4) - (((min(v0, 29) + v1) + -91)/32))/8)*8)))))
 ((min((min((v0*4), 3) + v1), v2) <= ((v0*4) + v1)) && ((min((v0*4), 3) + v1) <= ((((((min((v0*4), 3) + v1) - v2) + 3)/4)*4) + v2)))
 (((min((((min(v0, 53) + v1) + -115)/32), ((v2 + -13)/2)) + 1) <= (min((((min(v0, 53) + v1) + -83)/16), (v2 + -8))/2)) && (((min(((((min(v0, 53) + v1) + -83)/16) + ((((v2 - (((min(v0, 53) + v1) + -83)/16)) + -1)/8)*8)), (v2 + -8)) + -5)/2) <= min(((v2 + -13)/2), ((((min(v0, 53) + v1) + -115)/32) + (((((v2 + 1)/2) - (((min(v0, 53) + v1) + -115)/32))/8)*8)))))
 (((min((((min(v0, 53) + v1) + -179)/64), ((v2 + -55)/4)) + 1) <= (min((((min(v0, 53) + v1) + -115)/32), ((v2 + -13)/2))/2)) && (((min(((v2 + -13)/2), ((((min(v0, 53) + v1) + -115)/32) + (((((v2 + 1)/2) - (((min(v0, 53) + v1) + -115)/32))/8)*8))) + -21)/2) <= min(((v2 + -55)/4), ((((min(v0, 53) + v1) + -179)/64) + (((((v2 + 5)/4) - (((min(v0, 53) + v1) + -179)/64))/16)*16)))))
 ((min(((((min(v0, 53) + v1) + -83)/16) + (((v2 + -1)/8)*8)), (v3 + -8)) + -42) <= (((((min(((((min(v0, 53) + v1) + -83)/16) + (((v2 + 7)/8)*8)), v3) - v4) + -1)/50)*50) + v4))
 ((min(min((v0 - (v1*117)), v2), 116) + (min(((v0 - v2)/117), v1)*117)) <= v3)
 ((min(min((v0 - (v1*161)), v2), 160) + (min(((v0 - v2)/161), v1)*161)) <= v3)
 ((((min((v0 + 10), v1)/2) + -5) <= (v0/2)) && (((v1/2) + -5) <= ((v0/2) + (((((v1/2) - (v0/2)) + 2)/8)*8))))
 (((min((v0 + 11), v1) + -13)/2) <= ((v1 + -13)/2))
 (((min((v0 + -11), v1)/2) <= (min((v0 + -8), v1)/2)) && (((min((((((v0 - v1) + -1)/8)*8) + v1), (v0 + -8)) + -5)/2) <= min(((v0 + -13)/2), (((v1/2) + ((((((v0 + 1)/2) - (v1/2)) + 1)/8)*8)) + -1))))
 (((((min(v0, 11) + v1) + 367)/4) + ((v2/97)*97)) <= ((((min(v0, 11) + v1) + 755)/4) + (((((((min(v0, 11) + v1) + 367)/4) + ((v2/97)*97)) - (((min(v0, 11) + v1) + -17)/4))/194)*194)))
 ((min(((v0 + -13)/2), ((((min(v1, 11) + v2) + -17)/4) + ((v3/8)*8))) + -186) <= (((((min(((v0 + 3)/2), ((((min(v1, 11) + v2) + 15)/4) + ((v3/8)*8))) - v4) + -1)/194)*194) + v4))
 (((min(((v0 + -13)/2), ((((min(v1, 17) + v2) + -31)/8) + ((v3/8)*8))) + -87)/2) <= ((v4/2) + ((((((min(((v0 + 3)/2), ((((min(v1, 17) + v2) + 33)/8) + ((v3/8)*8))) + 1)/2) - (v4/2)) + 1)/50)*50)))
 ((min(((v0 + -13)/2), ((((min(v1, 17) + v2) + -31)/8) + ((v3/8)*8))) + -90) <= (((((min(((v0 + 3)/2), ((((min(v1, 17) + v2) + 33)/8) + ((v3/8)*8))) - v4) + -1)/98)*98) + v4))
 (((min(((v0 + -13)/2), ((((min(v1, 29) + v2) + -59)/16) + ((v3/8)*8))) + -39)/2) <= ((v4/2) + ((((((min(((v0 + 3)/2), ((((min(v1, 29) + v2) + 69)/16) + ((v3/8)*8))) + 1)/2) - (v4/2)) + 1)/26)*26)))
 (((min(((v0 + -13)/2), ((((min(v1, 53) + v2) + -115)/32) + ((v3/8)*8))) + -15)/2) <= ((v4/2) + ((((((min(((v0 + 3)/2), ((((min(v1, 53) + v2) + 141)/32) + ((v3/8)*8))) + 1)/2) - (v4/2)) + 1)/14)*14)))
 ((min(((v0 + -13)/2), ((((min(v1, 53) + v2) + -115)/32) + ((v3/8)*8))) + -18) <= (((((min(((v0 + 3)/2), ((((min(v1, 53) + v2) + 141)/32) + ((v3/8)*8))) - v4) + -1)/26)*26) + v4))
 (min((((v0*144) + v1) + 128), v2) <= min(((min(((min((v2 - ((v0*144) + v1)), 128) + 15)/16), 8)*16) + ((v0*144) + v1)), v2))
 ((min((((v0*144) + v1) + 136), v2) + -8) <= ((((min((v2 - ((v0*144) + v1)), 136) + 7)/16)*16) + ((v0*144) + v1)))
 ((min((((v0*144) + v1) + 139), v2) + -11) <= ((((min((v2 - ((v0*144) + v1)), 139) + 4)/16)*16) + ((v0*144) + v1)))
 ((min((((v0*144) + v1) + 140), v2) + -12) <= ((((min((v2 - ((v0*144) + v1)), 140) + 3)/16)*16) + ((v0*144) + v1)))
 ((min((((v0*144) + v1) + 142), v2) + -14) <= ((((min((v2 - ((v0*144) + v1)), 142) + 1)/16)*16) + ((v0*144) + v1)))
 ((min((((v0*144) + v1) + 142), v2) + -70) <= ((((min((v2 - ((v0*144) + v1)), 142) + 1)/72)*72) + ((v0*144) + v1)))
 (((min(((v0 + -14)/8), (((((v0 + -10)/4) + v1)/2) + -6)) + 1) <= (min(((v0 + -6)/4), (((v0 + -38)/4) + v1))/2)) && (((min((((v0 + -6)/4) + ((((((v0 + -10)/4) + v1) - ((v0 + -6)/4))/8)*8)), (((v0 + -38)/4) + v1)) + -5)/2) <= min((((v0 + -14)/8) + ((((((((v0 + -10)/4) + v1)/2) - ((v0 + -14)/8)) + 1)/8)*8)), (((((v0 + -10)/4) + v1)/2) + -6))))
 ((((min((v0 + 17), v1) + -23)/4) <= ((min((v0 + 11), v1) + -17)/4)) && (((min(((v1 + -13)/2), (((v0/2) + ((((((v1 + 1)/2) - (v0/2)) + 1)/8)*8)) + -1)) + -5)/2) <= min(((v1 + -23)/4), (((v0 + -6)/4) + (((((v1 + 5)/4) - ((v0 + -6)/4))/8)*8)))))
 (((((min(((v0*193) + 10), v1) + (v2/2)) + -3)/2) <= ((min(((v0*193) + 7), v1) + (v2/2))/2)) && (((min(((((min((v1 - (v0*193)), 192)/8)*8) + v3) + 7), v4) + -13)/2) <= min(((v4 + -13)/2), (((v3 + -3)/2) + (((((v4 + 1)/2) - ((v3 + -3)/2))/8)*8)))))
 (((min((((v0/2) % 2)*2), 1) + ((v0/4) + v1)) + -1) <= (((v0 + 6)/4) + v1))
 ((min((((v0 + 22)/4) + ((v1/8)*8)), v2) + -193) <= ((((min((((v0 + 22)/4) + ((v1/8)*8)), v2) - v3)/194)*194) + v3))
 (((min(((v0 + -23)/4), ((((min(v1, 17) + v2) + -47)/16) + ((v3/8)*8))) + -39)/2) <= ((v4/2) + ((((((min(((v0 + 9)/4), ((((min(v1, 17) + v2) + 81)/16) + ((v3/8)*8))) + 1)/2) - (v4/2)) + 1)/26)*26)))
 ((min(((v0 + -23)/4), ((((min(v1, 29) + v2) + -91)/32) + ((v3/8)*8))) + -18) <= (((((min(((v0 + 9)/4), ((((min(v1, 29) + v2) + 165)/32) + ((v3/8)*8))) - v4) + -1)/26)*26) + v4))
 (((min(((v0 + -23)/4), ((v1/8) + -3)) + 1) <= (min(((v0 + -13)/2), ((v1/4) + -4))/2)) && (((min(((v0 + -13)/2), (((v1/4) + ((((((v0 + 1)/2) - (v1/4)) + 4)/8)*8)) + -4)) + -5)/2) <= min(((v0 + -23)/4), (((v1/8) + ((((((v0 + 5)/4) - (v1/8)) + 3)/8)*8)) + -3))))
 (((min(((v0 + -25)/8), ((v1 + -55)/4)) + 1) <= (min(((v0 + -17)/4), ((v1 + -13)/2))/2)) && (((min(((v1 + -13)/2), (((v0 + -17)/4) + (((((v1 + 1)/2) - ((v0 + -17)/4))/8)*8))) + -21)/2) <= min(((v1 + -55)/4), (((v0 + -25)/8) + (((((v1 + 5)/4) - ((v0 + -25)/8))/16)*16)))))
 (((min((v0 + 27), v1) + -29)/2) <= ((v1 + -29)/2))
 (((min((v0 + -27), v1)/2) <= (min((v0 + -16), v1)/2)) && (((min((((((v0 - v1) + -1)/16)*16) + v1), (v0 + -16)) + -13)/2) <= min(((v0 + -29)/2), (((v1/2) + ((((((v0 + 1)/2) - (v1/2)) + 1)/16)*16)) + -1))))
 (((min((v0 + -27), v1)/2) <= (min((v0 + -8), v1)/2)) && (((min((((((v0 - v1) + -1)/8)*8) + v1), (v0 + -8)) + -21)/2) <= min(((v0 + -29)/2), (((v1/2) + ((((((v0 + 1)/2) - (v1/2)) + 1)/16)*16)) + -1))))
 ((min(((v0 + -29)/2), ((((min(v1, 101) + v2) + -227)/64) + ((v3/16)*16))) + 2) <= (((((min(((v0 + 3)/2), ((((min(v1, 101) + v2) + 797)/64) + ((v3/16)*16))) - v4) + -1)/14)*14) + v4))
 (((min(((v0 + -29)/2), ((((min(v1, 101) + v2) + -227)/64) + ((v3/16)*16))) + 5)/2) <= ((v4/2) + ((((((min(((v0 + 3)/2), ((((min(v1, 101) + v2) + 797)/64) + ((v3/16)*16))) + 1)/2) - (v4/2)) + 1)/8)*8)))
 (min((v0 + -2), int32(min(float32((v0 + -1)), 0.000000f))) <= 0)
 ((min((((((v0*2) + v1)*144) + v2) + 140), v3) + -12) <= ((((min((v3 - ((((v0*2) + v1)*144) + v2)), 140) + 3)/16)*16) + ((((v0*2) + v1)*144) + v2)))
 ((min((((((v0*2) + v1)*144) + v2) + 142), v3) + -14) <= ((((min((v3 - ((((v0*2) + v1)*144) + v2)), 142) + 1)/16)*16) + ((((v0*2) + v1)*144) + v2)))
 (((min(((v0/2) + (v1*161)), v2) + -3)/2) <= ((v2 + -3)/2))
 (((min((((v0/2) + (((v1 + 1)/8)*8)) + 6), v2)/2) + 1) <= (((v3 + 377)/2) + (((((min((((v0/2) + (((v1 + 9)/8)*8)) + -2), v2)/2) - ((v3 + -9)/2)) + 1)/194)*194)))
 ((((min((v0 + 2), v1)/2) + -1) <= (v0/2)) && (((v1/2) + -1) <= ((v0/2) + (((((v1/2) - (v0/2)) + 2)/4)*4))))
 (((min(((v0/2) + (v1*321)), v2) + -3)/2) <= ((v2 + -3)/2))
 (((min(((v0/2) + (v1*41)), v2) + -3)/2) <= ((v2 + -3)/2))
 (((min(((v0/2) + (v1*81)), v2) + -3)/2) <= ((v2 + -3)/2))
 ((min(((v0*31) + ((v1*4) + v2)), (v3 + -1)) + ((v4 + -6)/4)) < (((v4 + -2)/4) + ((v0*31) + ((v1*4) + v2))))
 ((min((((v0 + -3)/2) + (((v1 + 1)/8)*8)), ((v2/2) + -6)) + -36) <= ((v3/2) + ((((min((((v0 + -3)/2) + (((v1 + 9)/8)*8)), ((v2/2) + 2)) - (v3/2)) + 5)/50)*50)))
 ((min((v0 + 3), v1)/2) <= (v1/2))
 ((((min((v0 + 41), v1) + -38)/4) <= (min((v0 + 3), v1)/4)) && (((min((((v0 + -9)/2) + (((((v1/2) - ((v0 + -9)/2)) + 1)/8)*8)), ((v1/2) + -6)) + -21)/2) <= min(((v1 + -54)/4), (((v0 + -13)/4) + (((((v1 + 6)/4) - ((v0 + -13)/4))/16)*16)))))
 ((((min((v0 + 49), v1) + -55)/4) <= ((min((v0 + 11), v1) + -17)/4)) && (((min(((v1 + -13)/2), (((v0/2) + ((((((v1 + 1)/2) - (v0/2)) + 1)/8)*8)) + -1)) + -21)/2) <= min(((v1 + -55)/4), (((v0 + -6)/4) + (((((v1 + 5)/4) - ((v0 + -6)/4))/16)*16)))))
 ((min((((v0 + 5)/2) + v1), ((((((((v0 + 3)/2) + v1) - v2)/2)*2) + v2) + 2)) + -1) <= (((v0 + 3)/2) + v1))
 (min(((v0 + -6)/4), (min(v1, 49) + ((v0 + -38)/4))) <= min(((v0 + -6)/4), (((v0 + -38)/4) + v1)))
 (min(((v0 + -6)/4), (((v0 + -38)/4) + v1)) <= min(((v0 + -6)/4), (min(v1, 49) + ((v0 + -38)/4))))
 (((min((((v0 + -6)/4) + (((v1 + 1)/8)*8)), ((v2/2) + -6)) + -85)/2) <= ((v3/2) + ((((((min((((v0 + -6)/4) + (((v1 + 9)/8)*8)), ((v2/2) + 2)) + 1)/2) - (v3/2)) + 1)/49)*49)))
 (min((((v0 + -6)/4) + ((v1/8)*8)), (((v0 + -38)/4) + v2)) <= min((((v1/8)*8) + (((v0 + -6)/4) + (max((v3/49), 0)*49))), (((v0 + -38)/4) + v2)))
 (((min((((v0 + -6)/4) + v1), (v2 + 6))/2) + -3) <= (v2/2))
 (((min((v0 + 6), ((v1/2) + v2)) + -3)/2) <= ((v0 + 3)/2))
 ((min(((v0*81) + ((v1*41) + v2)), (v3 + -1)) + ((v4 + -6)/4)) < (((v4 + -2)/4) + ((v0*81) + ((v1*41) + v2))))
 ((min(((v0*81) + ((v1*8) + v2)), (v3 + -1)) + ((v4 + -6)/4)) < (((v4 + -2)/4) + ((v0*81) + ((v1*8) + v2))))
 ((((min((v0 + 9), v1) + -6)/4) <= (min((v0 + 3), v1)/4)) && (((min((((v0 + -9)/2) + (((((v1/2) - ((v0 + -9)/2)) + 1)/8)*8)), ((v1/2) + -6)) + -5)/2) <= min(((v1 + -22)/4), (((v0 + -13)/4) + (((((v1 + 6)/4) - ((v0 + -13)/4))/8)*8)))))
 (min((((v0 + v1)*117) + (min(((v2*59) + (((v3*4) + v4) + v5)), v6) + v7)), v8) <= (((v0 + v1)*117) + (((v2*59) + (((v3*4) + v4) + v5)) + v7)))
 (((min((((v0 + v1) + -13)/2), (((v1/2) + (((v2 + 1)/8)*8)) + -1)) + 9)/2) <= ((((min(v0, 11) + v1) + 367)/4) + ((((min((((v0 + v1) + 5)/2), ((v1/2) + (((v2 + 9)/8)*8)))/2) - (((min(v0, 11) + v1) + -17)/4))/97)*97)))
 (((min((((v0 + v1) + -13)/2), (((v1/2) + (((v2 + 1)/8)*8)) + -1)) + 9)/2) <= ((((min(v0, 11) + v1) + 755)/4) + ((((min((((v0 + v1) + 5)/2), ((v1/2) + (((v2 + 9)/8)*8)))/2) - (((min(v0, 11) + v1) + -17)/4))/194)*194)))
 ((min((((((v0 - v1)/16)*16) + v1) + 15), v0) + -142) <= ((((min((((((v0 - v1)/16)*16) + v1) + 15), v0) - v2)/143)*143) + v2))
 ((min((((((v0 - v1)/16)*16) + v1) + 15), v0) + -70) <= ((((min((((((v0 - v1)/16)*16) + v1) + 15), v0) - v2)/71)*71) + v2))
 (min((((v0 + v1)*161) + (min(((v2*81) + (((v3*2) + v4) + v5)), v6) + v7)), v8) <= (((v0 + v1)*161) + (((v2*81) + (((v3*2) + v4) + v5)) + v7)))
 (min((((v0 + v1)*161) + (min(((v2*81) + (((v3*4) + v4) + v5)), v6) + v7)), v8) <= (((v0 + v1)*161) + (((v2*81) + (((v3*4) + v4) + v5)) + v7)))
 (min((((v0 + v1)*161) + (min(v2, v3) + v4)), v5) <= (((v0 + v1)*161) + (v2 + v4)))
 ((min((((v0 + v1) + -163)/32), (((v1 + -62)/32) + ((v2/8)*8))) + 7) <= ((((min(v0, 101) + v1) + 221)/32) + ((((min((((v0 + v1) + 93)/32), (((v1 + 194)/32) + ((v2/8)*8))) - (((min(v0, 101) + v1) + -163)/32)) + -1)/13)*13)))
 ((min((((v0 + v1) + -163)/32), (((v1 + -62)/32) + ((v2/8)*8))) + 7) <= ((((min(v0, 101) + v1) + 637)/32) + ((((min((((v0 + v1) + 93)/32), (((v1 + 194)/32) + ((v2/8)*8))) - (((min(v0, 101) + v1) + -163)/32)) + -1)/26)*26)))
 (((min((((v0 + v1) + -163)/32), (((v1 + -62)/32) + ((v2/8)*8))) + 9)/2) <= ((((min(v0, 101) + v1) + -35)/64) + (((((min((((v0 + v1) + 93)/32), (((v1 + 194)/32) + ((v2/8)*8))) + 1)/2) - (((min(v0, 101) + v1) + -227)/64))/4)*4)))
 (((min((((v0 + v1) + -163)/32), (((v1 + -62)/32) + ((v2/8)*8))) + 9)/2) <= ((((min(v0, 101) + v1) + 605)/64) + (((((min((((v0 + v1) + 93)/32), (((v1 + 194)/32) + ((v2/8)*8))) + 1)/2) - (((min(v0, 101) + v1) + -227)/64))/14)*14)))
 ((min((((v0 + v1) + -1667)/128), (((v1 + -254)/128) + ((v2/16)*16))) + 15) <= ((((min(v0, 1413) + v1) + -1539)/128) + ((((min((((v0 + v1) + 381)/128), (((v1 + 1794)/128) + ((v2/16)*16))) - (((min(v0, 1413) + v1) + -1667)/128)) + -1)/2)*2)))
 ((min((((v0 + v1) + -1667)/128), (((v1 + -254)/128) + ((v2/16)*16))) + 15) <= ((((min(v0, 1413) + v1) + -771)/128) + ((((min((((v0 + v1) + 381)/128), (((v1 + 1794)/128) + ((v2/16)*16))) - (((min(v0, 1413) + v1) + -1667)/128)) + -1)/8)*8)))
 (((min(((v0 - v1)/16), v2)*16) + v1) <= (max(((v2*16) + (v1 - v0)), -15) + min((((v2*16) + v1) + 15), v0)))
 (((min(((((((v0 - v1) + 1)/8)*8) + v1) + 6), v0)/2) + 1) <= (((v2 + 89)/2) + (((((min(((((((v0 - v1) + 9)/8)*8) + v1) + -2), v0)/2) - ((v2 + -9)/2)) + 1)/50)*50)))
 ((min(((((((v0 - v1) + 1)/8)*8) + v1) + 6), v0) + -41) <= (((((min(((((((v0 - v1) + 9)/8)*8) + v1) + -2), v0) - v2) + 7)/49)*49) + v2))
 ((min(((((((v0 - v1) + 1)/8)*8) + v1) + 6), v0) + -89) <= (((((min(((((((v0 - v1) + 9)/8)*8) + v1) + -2), v0) - v2) + 7)/97)*97) + v2))
 (((min((((((v0 - v1) + 191)/16)*16) + v1), (v0 + 176)) + -77)/2) <= ((v2/2) + ((((((min((((((v0 - v1) + 207)/16)*16) + v1), (v0 + 192)) + 1)/2) - (v2/2)) + 1)/49)*49)))
 ((min(((((((v0 - v1) + 2)/16)*16) + v1) + 13), v0) + 3) <= min((min((((((min((((((v0 - v1) + 18)/16)*16) + v1), (v0 + 3)) - v2) + 12)/16)*16) + v2), v0) + 3), (((((v0 - v1) + 18)/16)*16) + v1)))
 ((min((((v0 + v1) + -23)/4), (((v1 + -6)/4) + ((v2/8)*8))) + 7) <= ((((min(v0, 17) + v1) + 749)/4) + ((((min((((v0 + v1) + 9)/4), (((v1 + 26)/4) + ((v2/8)*8))) - (((min(v0, 17) + v1) + -23)/4)) + -1)/194)*194)))
 (((min((((v0 + v1) + -23)/4), (((v1 + -6)/4) + ((v2/8)*8))) + 9)/2) <= ((((min(v0, 17) + v1) + 353)/8) + (((((min((((v0 + v1) + 9)/4), (((v1 + 26)/4) + ((v2/8)*8))) + 1)/2) - (((min(v0, 17) + v1) + -31)/8))/49)*49)))
 (((min((((v0 + v1) + -23)/4), (((v1 + -6)/4) + ((v2/8)*8))) + 9)/2) <= ((((min(v0, 17) + v1) + 745)/8) + (((((min((((v0 + v1) + 9)/4), (((v1 + 26)/4) + ((v2/8)*8))) + 1)/2) - (((min(v0, 17) + v1) + -31)/8))/98)*98)))
 (((min((((v0 + v1) + -23)/4), (((v1 + -6)/4) + ((v2/8)*8))) + 9)/2) <= ((((min(v0, 17) + v1) + -7)/8) + (((((min((((v0 + v1) + 9)/4), (((v1 + 26)/4) + ((v2/8)*8))) + 1)/2) - (((min(v0, 17) + v1) + -31)/8))/4)*4)))
 (((min((v0 - ((v1*26) + v2)), 25) + (v1*26)) + v2) <= min((((v1*26) + v2) + 25), v0))
 (((min(((v0 - v1)/26), v2)*26) + v1) <= (max(((v2*26) + (v1 - v0)), -25) + min((((v2*26) + v1) + 25), v0)))
 ((min(((((((v0 - v1) + 2)/8)*8) + v1) + 5), v0) + 3) <= min((min((((((min((((((v0 - v1) + 10)/8)*8) + v1), (v0 + 3)) - v2) + 4)/8)*8) + v2), v0) + 3), (((((v0 - v1) + 10)/8)*8) + v1)))
 (((min(((((((v0 - v1) + 2)/8)*8) + v1) + 5), v0) + 3) <= min((min((((((min((((((v0 - v1) + 10)/8)*8) + v1), (v0 + 3)) - v2) + 4)/8)*8) + v2), v0) + 3), (((((v0 - v1) + 10)/8)*8) + v1))) && (((min(((v3 - v4)/13), v5)*13) + v4) <= (max(((v5*13) + (v4 - v3)), -12) + min((((v5*13) + v4) + 12), v3))))
 ((min(((((((v0 - v1) + 2)/8)*8) + v1) + 5), v0) + -9) <= (((((min((((((v0 - v1) + 10)/8)*8) + v1), (v0 + 3)) - v2) + 4)/17)*17) + v2))
 ((min(((((((v0 - v1) + 4)/16)*16) + v1) + 11), v0) + 5) <= min((min((((((min((((((v0 - v1) + 20)/16)*16) + v1), (v0 + 5)) - v2) + 10)/16)*16) + v2), v0) + 5), (((((v0 - v1) + 20)/16)*16) + v1)))
 (((min(((((((v0 - v1) + 4)/16)*16) + v1) + 11), v0) + 5) <= min((min((((((min((((((v0 - v1) + 20)/16)*16) + v1), (v0 + 5)) - v2) + 10)/16)*16) + v2), v0) + 5), (((((v0 - v1) + 20)/16)*16) + v1))) && (((min(((v3 - v4)/26), v5)*26) + v4) <= (max(((v5*26) + (v4 - v3)), -25) + min((((v5*26) + v4) + 25), v3))))
 (((min(((((((v0 - v1) + 4)/16)*16) + v1) + 11), v0) + 5) <= min((min((((((min((((((v0 - v1) + 20)/16)*16) + v1), (v0 + 5)) - v2) + 10)/16)*16) + v2), v0) + 5), (((((v0 - v1) + 20)/16)*16) + v1))) && (((min((((v3 - v4) + 4)/26), v5)*26) + v4) <= (max(((v5*26) + (v4 - v3)), -21) + min((((v5*26) + v4) + 21), v3))))
 ((min((((v0 + v1) + -43)/8), (((v1 + -14)/8) + ((v2/8)*8))) + 7) <= ((((min(v0, 29) + v1) + 733)/8) + ((((min((((v0 + v1) + 21)/8), (((v1 + 50)/8) + ((v2/8)*8))) - (((min(v0, 29) + v1) + -43)/8)) + -1)/98)*98)))
 (((min((((v0 + v1) + -43)/8), (((v1 + -14)/8) + ((v2/8)*8))) + 9)/2) <= ((((min(v0, 29) + v1) + 325)/16) + (((((min((((v0 + v1) + 21)/8), (((v1 + 50)/8) + ((v2/8)*8))) + 1)/2) - (((min(v0, 29) + v1) + -59)/16))/25)*25)))
 (((min((((v0 + v1) + -43)/8), (((v1 + -14)/8) + ((v2/8)*8))) + 9)/2) <= ((((min(v0, 29) + v1) + 725)/16) + (((((min((((v0 + v1) + 21)/8), (((v1 + 50)/8) + ((v2/8)*8))) + 1)/2) - (((min(v0, 29) + v1) + -59)/16))/50)*50)))
 ((min(((((((v0 - v1) + 4)/8)*8) + v1) + 3), v0) + 5) <= min((min((((((min((((((v0 - v1) + 12)/8)*8) + v1), (v0 + 5)) - v2) + 2)/8)*8) + v2), v0) + 5), (((((v0 - v1) + 12)/8)*8) + v1)))
 (((min(((v0 - v1)/52), v2)*52) + v1) <= (max(((v2*52) + (v1 - v0)), -51) + min((((v2*52) + v1) + 51), v0)))
 ((min(((((((v0 - v1) + 8)/16)*16) + v1) + 7), v0) + 9) <= min((min((((((min((((((v0 - v1) + 24)/16)*16) + v1), (v0 + 9)) - v2) + 6)/16)*16) + v2), v0) + 9), (((((v0 - v1) + 24)/16)*16) + v1)))
 (((min(((((((v0 - v1) + 8)/16)*16) + v1) + 7), v0) + 9) <= min((min((((((min((((((v0 - v1) + 24)/16)*16) + v1), (v0 + 9)) - v2) + 6)/16)*16) + v2), v0) + 9), (((((v0 - v1) + 24)/16)*16) + v1))) && (((min(((v3 - v4)/26), v5)*26) + v4) <= (max(((v5*26) + (v4 - v3)), -25) + min((((v5*26) + v4) + 25), v3))))
 (min((((v0 + v1)*81) + (min(((v2*41) + (((v3*2) + v4) + v5)), v6) + v7)), v8) <= (((v0 + v1)*81) + (((v2*41) + (((v3*2) + v4) + v5)) + v7)))
 ((min((((v0 + v1) + -83)/16), (((v1 + -30)/16) + ((v2/8)*8))) + 7) <= ((((min(v0, 53) + v1) + 301)/16) + ((((min((((v0 + v1) + 45)/16), (((v1 + 98)/16) + ((v2/8)*8))) - (((min(v0, 53) + v1) + -83)/16)) + -1)/25)*25)))
 (((min((((v0 + v1) + -83)/16), (((v1 + -30)/16) + ((v2/8)*8))) + 9)/2) <= ((((min(v0, 53) + v1) + -19)/32) + (((((min((((v0 + v1) + 45)/16), (((v1 + 98)/16) + ((v2/8)*8))) + 1)/2) - (((min(v0, 53) + v1) + -115)/32))/4)*4)))
 (((min((((v0 + v1) + -83)/16), (((v1 + -30)/16) + ((v2/8)*8))) + 9)/2) <= ((((min(v0, 53) + v1) + 269)/32) + (((((min((((v0 + v1) + 45)/16), (((v1 + 98)/16) + ((v2/8)*8))) + 1)/2) - (((min(v0, 53) + v1) + -115)/32))/13)*13)))
 (((min((((v0 + v1) + -83)/16), (((v1 + -30)/16) + ((v2/8)*8))) + 9)/2) <= ((((min(v0, 53) + v1) + 685)/32) + (((((min((((v0 + v1) + 45)/16), (((v1 + 98)/16) + ((v2/8)*8))) + 1)/2) - (((min(v0, 53) + v1) + -115)/32))/26)*26)))
 (((min((((v0 + v1) + -83)/16), (((v1 + -30)/16) + ((v2/8)*8))) + 9)/2) <= ((((min(v0, 53) + v1) + -83)/32) + (((((min((((v0 + v1) + 45)/16), (((v1 + 98)/16) + ((v2/8)*8))) + 1)/2) - (((min(v0, 53) + v1) + -115)/32))/2)*2)))
 ((min((((v0 + v1) + -835)/64), (((v1 + -126)/64) + ((v2/16)*16))) + 15) <= ((((min(v0, 709) + v1) + -3)/64) + ((((min((((v0 + v1) + 189)/64), (((v1 + 898)/64) + ((v2/16)*16))) - (((min(v0, 709) + v1) + -835)/64)) + -1)/14)*14)))
 ((min((((v0 + v1) + -835)/64), (((v1 + -126)/64) + ((v2/16)*16))) + 15) <= ((((min(v0, 709) + v1) + -387)/64) + ((((min((((v0 + v1) + 189)/64), (((v1 + 898)/64) + ((v2/16)*16))) - (((min(v0, 709) + v1) + -835)/64)) + -1)/7)*7)))
 ((min((((v0 + v1) + -835)/64), (((v1 + -126)/64) + ((v2/16)*16))) + 15) <= ((((min(v0, 709) + v1) + -643)/64) + ((((min((((v0 + v1) + 189)/64), (((v1 + 898)/64) + ((v2/16)*16))) - (((min(v0, 709) + v1) + -835)/64)) + -1)/4)*4)))
 ((min((((((v0 - v1)/8)*8) + v1) + 7), v0) + -16) <= ((((min((((((v0 - v1)/8)*8) + v1) + 7), v0) - v2)/17)*17) + v2))
 ((min((((((v0 - v1)/8)*8) + v1) + 7), v0) + -34) <= ((((min((((((v0 - v1)/8)*8) + v1) + 7), v0) - v2)/35)*35) + v2))
 (((min((v0 - ((v1*8) + v2)), 7) + (v1*8)) + v2) <= min((((v1*8) + v2) + 7), v0))
 (((min(((((v0 - v1) + 98)/97)*97), 8) + v1) + -8) <= v1)
 (select((v0 < v1), (((v1 + v2) + 21)/8), (((v1 + v2) + -14)/8)) <= (((v1 + v2) + 22)/8))
 ((select((v0 < v1), (((v1 + v2) + 3)/2), (((v1 + v2)/2) + -1)) + -2) <= ((v1 + v2)/2))
 (select((v0 < v1), (((v1 + v2) + 9)/4), (((v1 + v2) + -6)/4)) <= (((v1 + v2) + 10)/4))
 ((select((v0 < v1), ((((v1 + v2) + v3) + 3)/2), ((((v1 + v2) + v3)/2) + -1)) + -2) <= (((v1 + v2) + v3)/2))
 (select((v0 < v1), ((((v1 + v2) + v3) + 9)/4), ((((v1 + v2) + v3) + -6)/4)) <= ((((v1 + v2) + v3) + 10)/4))
 ((select((v0 < v1), (((((v1 + v2) + v3) + v4) + 3)/2), (((((v1 + v2) + v3) + v4)/2) + -1)) + -2) <= ((((v1 + v2) + v3) + v4)/2))
 ((v0 + -11) <= ((((v0 - v1)/12)*12) + v1))
 ((((v0*1280) + v1) + v2) <= select((v3 < ((v4 + v3) + -1)), ((((v0*1280) + v1) + v2) + 1), (((v0*1280) + v1) + v2)))
 ((((((v0 + 129)/2) - v1)/4) + -1) <= max(((((v0 + 123)/2) - v1)/4), -1))
 (((v0 + -1)/2) <= ((((((v0 + 1)/2) - v1)/2)*2) + v1))
 (((v0 + 1)/2) <= ((v0/2) + ((((v0 % 2) + 3)/4)*4)))
 ((((((v0 + 1)/2) - v1)/2) + -1) <= max(((((v0 + -1)/2) - v1)/2), -1))
 ((((((v0 + 1)/2) - v1)/5) + -1) <= max(((((v0 + -7)/2) - v1)/5), -1))
 (((v0 + -15) <= (((((v0 - v1)/16) - (v2*9))*16) + ((v2*144) + v1))) && (((min(((v3 - v4)/104), v5)*104) + v4) <= (max(((v5*104) + (v4 - v3)), -103) + min((((v5*104) + v4) + 103), v3))))
 (((v0 + -15) <= (((((v0 - v1)/16) - (v2*9))*16) + ((v2*144) + v1))) && (((min((v3 - ((v4*16) + v5)), 15) + (v4*16)) + v5) <= min((((v4*16) + v5) + 15), v3)))
 (((v0 + -15) <= (((((v0 - v1)/16) - (v2*9))*16) + ((v2*144) + v1))) && (((min(((v3 - v4)/16), v5)*16) + v4) <= (max(((v5*16) + (v4 - v3)), -15) + min((((v5*16) + v4) + 15), v3))))
 (((v0 + -15) <= (((((v0 - v1)/16) - (v2*9))*16) + ((v2*144) + v1))) && (((min((v3 - ((v4*32) + v5)), 16) + (v4*32)) + v5) <= min((((v4*32) + v5) + 16), v3)))
 (((v0 + -15) <= (((((v0 - v1)/16) - (v2*9))*16) + ((v2*144) + v1))) && (((min((v3 - ((v4*52) + v5)), 51) + (v4*52)) + v5) <= min((((v4*52) + v5) + 51), v3)))
 (((v0 + -15) <= (((((v0 - v1)/16) - (v2*9))*16) + ((v2*144) + v1))) && (((min(((v3 - v4)/52), v5)*52) + v4) <= (max(((v5*52) + (v4 - v3)), -51) + min((((v5*52) + v4) + 51), v3))))
 (((v0 + -15) <= (((((v0 - v1)/16) - (v2*9))*16) + ((v2*144) + v1))) && (((min((v3 - (((v4 + v5)*16) + v6)), 15) + ((v4 + v5)*16)) + v6) <= min(((((v4 + v5)*16) + v6) + 15), v3)))
 ((((v0*160) + v1) + v2) <= select((v3 < ((v4 + v3) + -1)), ((((v0*160) + v1) + v2) + 1), (((v0*160) + v1) + v2)))
 ((((((v0 + 161)/2) - v1)/4) + -1) <= max(((((v0 + 155)/2) - v1)/4), -1))
 ((((((((v0*161) + v1) + 161)/2) - v2)/4) + -1) <= max(((((((v0*161) + v1) + 155)/2) - v2)/4), -1))
 ((((((((v0*161) + v1) + 161)/2) - v2)/42) + -1) <= max(((((((v0*161) + v1) + 79)/2) - v2)/42), -1))
 ((((((v0 + 163)/2) - v1)/4) + -1) <= max(((((v0 + 157)/2) - v1)/4), -1))
 ((v0 + -17) <= ((((v0 - v1)/18)*18) + v1))
 ((((((v0 + 193)/2) - v1)/8) + -1) <= max(((((v0 + 179)/2) - v1)/8), -1))
 ((v0 + -1) <= (max(v1, 0) + (((v0 - max(v1, 0))/2)*2)))
 ((v0 + -1) <= ((((v0 - v1)/2)*2) + v1))
 (((v0/2) + -1022) <= select((((v1*161) + v2) < (v0 + 1)), ((v0 + 3)/2), ((v0/2) + -1)))
 (((v0/2) + -1022) <= select(((v1/2) < (v0 + 1)), ((v0 + 3)/2), ((v0/2) + -1)))
 (((v0/2) + -1022) <= select((v1 < (v0 + 1)), ((v0 + 3)/2), ((v0/2) + -1)))
 (((v0/2) + -14) <= (((v1 + -126)/64) + (((((v0/2) - ((v1 + -126)/64)) + 1)/16)*16)))
 (((v0/2) + 1) <= max(((v0 + 3)/2), 0))
 (((v0/2) <= (min(((v0 % 2)*2), 1) + (v0/2))) && (((max(((v0 % 2)*2), 1) + (v0/2)) + -2) <= (v0/2)))
 (((((v0/2) + (min((v1 - (v2*161)), 160) + (min((v1/161), v2)*161))) + 1)/2) <= (((min(((v2*161) + 160), v1) + (v0/2)) + 1)/2))
 (((((v0/2) + (min((v1 - (v2*81)), 80) + (min((v1/81), v2)*81))) + 1)/2) <= (((min(((v2*81) + 80), v1) + (v0/2)) + 1)/2))
 ((v0 + -2) <= ((((v0 - v1)/3)*3) + v1))
 (((v0/2) + (v1*320)) <= (select(v2, (((v1*640) + v0) + 1), ((v1*640) + v0))/2))
 (((v0/2) + (v1*640)) <= (select(v2, (((v1*1280) + v0) + 1), ((v1*1280) + v0))/2))
 ((((v0*320) + v1) + v2) <= select((v3 < ((v4 + v3) + -1)), ((((v0*320) + v1) + v2) + 1), (((v0*320) + v1) + v2)))
 ((((((v0 + 321)/2) - v1)/41) + -1) <= max(((((v0 + 241)/2) - v1)/41), -1))
 ((((((v0 + 321)/2) - v1)/4) + -1) <= max(((((v0 + 315)/2) - v1)/4), -1))
 ((((((v0 + 321)/2) - v1)/8) + -1) <= max(((((v0 + 307)/2) - v1)/8), -1))
 ((((((((v0*321) + v1) + 321)/2) - v2)/82) + -1) <= max(((((((v0*321) + v1) + 159)/2) - v2)/82), -1))
 ((((((v0*321) + v1) - v2)/2) + 160) <= max((((((v0*321) + v1) - v2) + 321)/2), 0))
 ((((((v0 + 3)/2) - v1)/2) + -1) <= max(((((v0 + 1)/2) - v1)/2), -1))
 ((v0 + -3) <= (max(v1, 0) + (((v0 - max(v1, 0))/4)*4)))
 (((v0 + -4086)/4) <= min(select(v1, ((v0 + 9)/4), ((v0 + -6)/4)), ((select(v1, ((v0 + 3)/2), ((v0/2) + -1))/2) + -1)))
 ((v0 + -40) <= ((((v0 - v1)/41)*41) + v1))
 ((((v0*40) + (((v1 + 165)/4) + (v2*160))) + -3) <= ((((v0*10) + (((((v1 + 165)/4) - v3)/4) + (v2*40)))*4) + v3))
 ((((((v0*4) + ((((min(v1, 53) + v2) + -115)/64) + (v3*2))) + -1) <= ((((min(v1, 53) + v2) + -179)/64) + (((v0*2) + v3)*2))) && ((v4/2) <= (min(((v4 % 2)*2), 1) + (v4/2)))) && (((max(((v4 % 2)*2), 1) + (v4/2)) + -2) <= (v4/2)))
 ((v0 + -4) <= ((((v0 - v1)/5)*5) + v1))
 ((((v0*4) + (((v1 + 9)/2) + (v2*640))) + -1) <= ((((v0*2) + (((((v1 + 9)/2) - v3)/2) + (v2*320)))*2) + v3))
 ((((((v0 + 51)/2) - v1)/16) + -1) <= max(((((v0 + 21)/2) - v1)/16), -1))
 ((v0 + -5) <= ((((v0 - v1)/6)*6) + v1))
 ((((v0*640) + v1) + v2) <= select((v3 < ((v4 + v3) + -1)), ((((v0*640) + v1) + v2) + 1), (((v0*640) + v1) + v2)))
 ((((((v0 + 641)/2) - v1)/4) + -1) <= max(((((v0 + 635)/2) - v1)/4), -1))
 ((v0 + -70) <= ((((v0 - v1)/71)*71) + v1))
 ((((v0 + 738)/32) + ((v1/26)*26)) <= (((v0 + 34)/32) + ((((((v0 + 738)/32) + ((v1/26)*26)) - ((v0 + -62)/32))/4)*4)))
 ((((((v0 + 81)/2) - v1)/11) + -1) <= max(((((v0 + 61)/2) - v1)/11), -1))
 ((((((((v0*81) + v1) + 81)/2) - v2)/11) + -1) <= max(((((((v0*81) + v1) + 61)/2) - v2)/11), -1))
 ((v0 + -8) <= ((((v0 - v1)/9)*9) + v1))
 ((((v0*8) + (((v1 + 17)/2) + (v2*640))) + -1) <= ((((v0*4) + (((((v1 + 17)/2) - v3)/2) + (v2*320)))*2) + v3))
 (v0 <= max(max(v0, v1), (max(v1, 0) + 1)))
 (v0 < (select((v1 < v2), 2, 1) + v0))
 ((((v0 + v1)/2) <= (min((((v0 + v1) % 2)*2), 1) + ((v0 + v1)/2))) && (((max((((v0 + v1) % 2)*2), 1) + ((v0 + v1)/2)) + -2) <= ((v0 + v1)/2)))
 (((((v0 + v1)/2) + ((v2 + v3)*4)) + -2) <= select((v4 < v1), ((((v0 + v1) + 3)/2) + ((v2 + v3)*4)), ((((v0 + v1)/2) + ((v2 + v3)*4)) + -1)))
 ((((v0 - v1)/4) + 1) <= max((((v0 - v1) + 5)/4), 0))
 ((((v0 - v1)/8) + 1) <= max((((v0 - v1) + 9)/8), 0))
 ((((v0 - v1)/8) + 32) <= max((((v0 - v1) + 257)/8), 0))
 ((((v0 - v1)/8) + 96) <= max((((v0 - v1) + 769)/8), 0))
 (((((v0 - v1) + 98)/97)*97) <= (min(((((v0 - v1) + 98)/97)*97), 8) + (((max(((((v0 - v1) + 98)/97)*97), 8) + -1)/8)*8)))