gistfile1.txt

Attempting to disprove: (((1 == 1) && ((7 == 7) && ((4 == 4) && (g.s0.y.y > g.s0.y.y$8)))) && (((((uint1)1 && (f.s0.x == g.s0.x$1)) && (f.s0.y == (((g.s0.y.y$8*5) + g.min.1) + g.s0.y.v10$1))) && (let f.s0.x.loop_extent = max((100 - g.min.0), g.extent.0) in (((((((uint1)1 && (g.s0.y.y >= 0)) && (g.s0.y.y < (0 + ((g.extent.1 + 4)/5)))) && (f.s0.y >= ((g.s0.y.y*5) + g.min.1))) && (f.s0.y < (((g.s0.y.y*5) + g.min.1) + 5))) && (f.s0.x >= g.min.0)) && (f.s0.x < (g.min.0 + f.s0.x.loop_extent))))) && (((((((((((((uint1)1 && (g.s0.y.y$8 >= 0)) && (g.s0.y.y$8 < (0 + ((g.extent.1 + 4)/5)))) && (f.s0.y >= ((g.s0.y.y$8*5) + g.min.1))) && (f.s0.y < (((g.s0.y.y$8*5) + g.min.1) + 5))) && (f.s1.y >= ((g.s0.y.y$8*5) + g.min.1))) && (f.s1.y < (((g.s0.y.y$8*5) + g.min.1) + 5))) && (f.s2.y >= ((g.s0.y.y$8*5) + g.min.1))) && (f.s2.y < (((g.s0.y.y$8*5) + g.min.1) + 5))) && (g.s0.y.v10$1 >= 0)) && (g.s0.y.v10$1 < (0 + 5))) && (g.s0.x$1 >= g.min.0)) && (g.s0.x$1 < (g.min.0 + g.extent.0)))))
Expr: (((((((((0 <= g.s0.y.y) && (g.s0.y.y < ((g.extent.1 + 4)/5))) && (t23 <= f.s0.y)) && (f.s0.y < (t23 + 5))) && (g.min.0 <= f.s0.x)) && (f.s0.x < (max((100 - g.min.0), g.extent.0) + g.min.0))) && ((f.s0.x == g.s0.x$1) && (f.s0.y == (t24 + g.s0.y.v10$1)))) && ((((((((((((0 <= g.s0.y.y$8) && (g.s0.y.y$8 < ((g.extent.1 + 4)/5))) && (t24 <= f.s0.y)) && (f.s0.y < (t24 + 5))) && (t24 <= f.s1.y)) && (f.s1.y < (t24 + 5))) && (t24 <= f.s2.y)) && (f.s2.y < (t24 + 5))) && (0 <= g.s0.y.v10$1)) && (g.s0.y.v10$1 < 5)) && (g.min.0 <= g.s0.x$1)) && (g.s0.x$1 < (g.extent.0 + g.min.0)))) && (g.s0.y.y$8 < g.s0.y.y))
Attempting to disprove conjunction:
 ((g.s0.y.y$8 + max(k18, 1)) == g.s0.y.y)
 ((g.s0.x$1 + max(k19, 1)) == (g.extent.0 + g.min.0))
 ((g.min.0 + max(k20, 0)) == g.s0.x$1)
 ((g.s0.y.v10$1 + max(k21, 1)) == 5)
 ((0 + max(k22, 0)) == g.s0.y.v10$1)
 ((f.s2.y + max(k23, 1)) == (5 + t24))
 ((t24 + max(k24, 0)) == f.s2.y)
 ((f.s1.y + max(k25, 1)) == (5 + t24))
 ((t24 + max(k26, 0)) == f.s1.y)
 ((f.s0.y + max(k27, 1)) == (5 + t24))
 ((t24 + max(k28, 0)) == f.s0.y)
 ((g.s0.y.y$8 + max(k29, 1)) == ((g.extent.1 + 4)/5))
 ((0 + max(k30, 0)) == g.s0.y.y$8)
 (f.s0.y == (g.s0.y.v10$1 + t24))
 (f.s0.x == g.s0.x$1)
 ((f.s0.x + max(k31, 1)) == (g.min.0 + max((100 - g.min.0), g.extent.0)))
 ((g.min.0 + max(k32, 0)) == f.s0.x)
 ((f.s0.y + max(k33, 1)) == (5 + t23))
 ((t23 + max(k34, 0)) == f.s0.y)
 ((g.s0.y.y + max(k35, 1)) == ((g.extent.1 + 4)/5))
 ((0 + max(k36, 0)) == g.s0.y.y)
Substituting...
Substituting out f.s0.x = g.s0.x$1
 ((max(k18, 1) + g.s0.y.y$8) == g.s0.y.y)
 ((max(k19, 1) + g.s0.x$1) == (g.extent.0 + g.min.0))
 ((max(k20, 0) + g.min.0) == g.s0.x$1)
 ((max(k21, 1) + g.s0.y.v10$1) == 5)
 (max(k22, 0) == g.s0.y.v10$1)
 ((max(k23, 1) + f.s2.y) == (t24 + 5))
 ((max(k24, 0) + t24) == f.s2.y)
 ((max(k25, 1) + f.s1.y) == (t24 + 5))
 ((max(k26, 0) + t24) == f.s1.y)
 ((max(k27, 1) + f.s0.y) == (t24 + 5))
 ((max(k28, 0) + t24) == f.s0.y)
 ((max(k29, 1) + g.s0.y.y$8) == ((g.extent.1 + 4)/5))
 (max(k30, 0) == g.s0.y.y$8)
 (f.s0.y == (g.s0.y.v10$1 + t24))
 ((max(k31, 1) + g.s0.x$1) == max((g.extent.0 + g.min.0), 100))
 ((max(k32, 0) + g.min.0) == g.s0.x$1)
 ((max(k33, 1) + f.s0.y) == (t23 + 5))
 ((max(k34, 0) + t23) == f.s0.y)
 ((max(k35, 1) + g.s0.y.y) == ((g.extent.1 + 4)/5))
 (max(k36, 0) == g.s0.y.y)
 (uint1)1
Substituting out g.s0.y.y$8 = (g.s0.y.y - max(k18, 1))
 ((max(k19, 1) + g.s0.x$1) == (g.extent.0 + g.min.0))
 ((max(k20, 0) + g.min.0) == g.s0.x$1)
 ((max(k21, 1) + g.s0.y.v10$1) == 5)
 (max(k22, 0) == g.s0.y.v10$1)
 ((max(k23, 1) + f.s2.y) == (t24 + 5))
 ((max(k24, 0) + t24) == f.s2.y)
 ((max(k25, 1) + f.s1.y) == (t24 + 5))
 ((max(k26, 0) + t24) == f.s1.y)
 ((max(k27, 1) + f.s0.y) == (t24 + 5))
 ((max(k28, 0) + t24) == f.s0.y)
 ((max(k29, 1) + (g.s0.y.y - max(k18, 1))) == ((g.extent.1 + 4)/5))
 ((max(k30, 0) + (max(k18, 1) - g.s0.y.y)) == 0)
 (f.s0.y == (g.s0.y.v10$1 + t24))
 ((max(k31, 1) + g.s0.x$1) == max((g.extent.0 + g.min.0), 100))
 ((max(k32, 0) + g.min.0) == g.s0.x$1)
 ((max(k33, 1) + f.s0.y) == (t23 + 5))
 ((max(k34, 0) + t23) == f.s0.y)
 ((max(k35, 1) + g.s0.y.y) == ((g.extent.1 + 4)/5))
 (max(k36, 0) == g.s0.y.y)
 (uint1)1
Substituting out g.s0.x$1 = ((g.extent.0 + g.min.0) - max(k19, 1))
 (((max(k19, 1) - (g.extent.0 + g.min.0)) + (max(k20, 0) + g.min.0)) == 0)
 ((max(k21, 1) + g.s0.y.v10$1) == 5)
 (max(k22, 0) == g.s0.y.v10$1)
 ((max(k23, 1) + f.s2.y) == (t24 + 5))
 ((max(k24, 0) + t24) == f.s2.y)
 ((max(k25, 1) + f.s1.y) == (t24 + 5))
 ((max(k26, 0) + t24) == f.s1.y)
 ((max(k27, 1) + f.s0.y) == (t24 + 5))
 ((max(k28, 0) + t24) == f.s0.y)
 ((max(k29, 1) + g.s0.y.y) == (max(k18, 1) + ((g.extent.1 + 4)/5)))
 ((max(k18, 1) + max(k30, 0)) == g.s0.y.y)
 (f.s0.y == (g.s0.y.v10$1 + t24))
 ((max(k31, 1) + ((g.extent.0 + g.min.0) - max(k19, 1))) == max((g.extent.0 + g.min.0), 100))
 (((max(k19, 1) - (g.extent.0 + g.min.0)) + (max(k32, 0) + g.min.0)) == 0)
 ((max(k33, 1) + f.s0.y) == (t23 + 5))
 ((max(k34, 0) + t23) == f.s0.y)
 ((max(k35, 1) + g.s0.y.y) == ((g.extent.1 + 4)/5))
 (max(k36, 0) == g.s0.y.y)
 (uint1)1
Substituting out g.extent.0 = (max(k19, 1) + max(k20, 0))
 ((max(k21, 1) + g.s0.y.v10$1) == 5)
 (max(k22, 0) == g.s0.y.v10$1)
 ((max(k23, 1) + f.s2.y) == (t24 + 5))
 ((max(k24, 0) + t24) == f.s2.y)
 ((max(k25, 1) + f.s1.y) == (t24 + 5))
 ((max(k26, 0) + t24) == f.s1.y)
 ((max(k27, 1) + f.s0.y) == (t24 + 5))
 ((max(k28, 0) + t24) == f.s0.y)
 ((max(k29, 1) + g.s0.y.y) == (max(k18, 1) + ((g.extent.1 + 4)/5)))
 ((max(k18, 1) + max(k30, 0)) == g.s0.y.y)
 (f.s0.y == (g.s0.y.v10$1 + t24))
 ((max(k31, 1) + ((max(k19, 1) + max(k20, 0)) + g.min.0)) == (max(k19, 1) + max(((max(k19, 1) + max(k20, 0)) + g.min.0), 100)))
 (max(k32, 0) == max(k20, 0))
 ((max(k33, 1) + f.s0.y) == (t23 + 5))
 ((max(k34, 0) + t23) == f.s0.y)
 ((max(k35, 1) + g.s0.y.y) == ((g.extent.1 + 4)/5))
 (max(k36, 0) == g.s0.y.y)
 (uint1)1
Substituting out g.s0.y.v10$1 = ((max(k21, 1)*-1) + 5)
 ((max(k22, 0) + max(k21, 1)) == 5)
 ((max(k23, 1) + f.s2.y) == (t24 + 5))
 ((max(k24, 0) + t24) == f.s2.y)
 ((max(k25, 1) + f.s1.y) == (t24 + 5))
 ((max(k26, 0) + t24) == f.s1.y)
 ((max(k27, 1) + f.s0.y) == (t24 + 5))
 ((max(k28, 0) + t24) == f.s0.y)
 ((max(k29, 1) + g.s0.y.y) == (max(k18, 1) + ((g.extent.1 + 4)/5)))
 ((max(k18, 1) + max(k30, 0)) == g.s0.y.y)
 (((max(k21, 1) - t24) + f.s0.y) == 5)
 ((max(k31, 1) + (max(k20, 0) + g.min.0)) == max(((max(k19, 1) + max(k20, 0)) + g.min.0), 100))
 (max(k32, 0) == max(k20, 0))
 ((max(k33, 1) + f.s0.y) == (t23 + 5))
 ((max(k34, 0) + t23) == f.s0.y)
 ((max(k35, 1) + g.s0.y.y) == ((g.extent.1 + 4)/5))
 (max(k36, 0) == g.s0.y.y)
 (uint1)1
Substituting out t24 = ((max(k23, 1) + f.s2.y) + -5)
 ((max(k21, 1) + max(k22, 0)) == 5)
 ((max(k24, 0) + max(k23, 1)) == 5)
 ((max(k25, 1) + f.s1.y) == (max(k23, 1) + f.s2.y))
 ((max(k26, 0) + (max(k23, 1) + f.s2.y)) == (f.s1.y + 5))
 ((max(k27, 1) + f.s0.y) == (max(k23, 1) + f.s2.y))
 ((max(k28, 0) + (max(k23, 1) + f.s2.y)) == (f.s0.y + 5))
 ((max(k29, 1) + g.s0.y.y) == (max(k18, 1) + ((g.extent.1 + 4)/5)))
 ((max(k18, 1) + max(k30, 0)) == g.s0.y.y)
 ((max(k21, 1) + f.s0.y) == (max(k23, 1) + f.s2.y))
 ((max(k31, 1) + (max(k20, 0) + g.min.0)) == max(((max(k19, 1) + max(k20, 0)) + g.min.0), 100))
 (max(k32, 0) == max(k20, 0))
 ((max(k33, 1) + f.s0.y) == (t23 + 5))
 ((max(k34, 0) + t23) == f.s0.y)
 ((max(k35, 1) + g.s0.y.y) == ((g.extent.1 + 4)/5))
 (max(k36, 0) == g.s0.y.y)
 (uint1)1
Substituting out f.s2.y = (max(k25, 1) + (f.s1.y - max(k23, 1)))
 ((max(k21, 1) + max(k22, 0)) == 5)
 ((max(k23, 1) + max(k24, 0)) == 5)
 ((max(k26, 0) + (max(k23, 1) + (max(k25, 1) + (f.s1.y - max(k23, 1))))) == (f.s1.y + 5))
 ((max(k27, 1) + f.s0.y) == (max(k23, 1) + (max(k25, 1) + (f.s1.y - max(k23, 1)))))
 ((max(k28, 0) + (max(k23, 1) + (max(k25, 1) + (f.s1.y - max(k23, 1))))) == (f.s0.y + 5))
 ((max(k29, 1) + g.s0.y.y) == (max(k18, 1) + ((g.extent.1 + 4)/5)))
 ((max(k18, 1) + max(k30, 0)) == g.s0.y.y)
 ((max(k21, 1) + f.s0.y) == (max(k23, 1) + (max(k25, 1) + (f.s1.y - max(k23, 1)))))
 ((max(k31, 1) + (max(k20, 0) + g.min.0)) == max(((max(k19, 1) + max(k20, 0)) + g.min.0), 100))
 (max(k32, 0) == max(k20, 0))
 ((max(k33, 1) + f.s0.y) == (t23 + 5))
 ((max(k34, 0) + t23) == f.s0.y)
 ((max(k35, 1) + g.s0.y.y) == ((g.extent.1 + 4)/5))
 (max(k36, 0) == g.s0.y.y)
 (uint1)1
Substituting out f.s1.y = (max(k27, 1) + (f.s0.y - max(k25, 1)))
 ((max(k21, 1) + max(k22, 0)) == 5)
 ((max(k23, 1) + max(k24, 0)) == 5)
 ((max(k25, 1) + max(k26, 0)) == 5)
 ((max(k28, 0) + (max(k25, 1) + (max(k27, 1) + (f.s0.y - max(k25, 1))))) == (f.s0.y + 5))
 ((max(k29, 1) + g.s0.y.y) == (max(k18, 1) + ((g.extent.1 + 4)/5)))
 ((max(k18, 1) + max(k30, 0)) == g.s0.y.y)
 ((max(k21, 1) + f.s0.y) == (max(k25, 1) + (max(k27, 1) + (f.s0.y - max(k25, 1)))))
 ((max(k31, 1) + (max(k20, 0) + g.min.0)) == max(((max(k19, 1) + max(k20, 0)) + g.min.0), 100))
 (max(k32, 0) == max(k20, 0))
 ((max(k33, 1) + f.s0.y) == (t23 + 5))
 ((max(k34, 0) + t23) == f.s0.y)
 ((max(k35, 1) + g.s0.y.y) == ((g.extent.1 + 4)/5))
 (max(k36, 0) == g.s0.y.y)
 (uint1)1
Substituting out g.s0.y.y = ((max(k18, 1) + ((g.extent.1 + 4)/5)) - max(k29, 1))
 ((max(k21, 1) + max(k22, 0)) == 5)
 ((max(k23, 1) + max(k24, 0)) == 5)
 ((max(k25, 1) + max(k26, 0)) == 5)
 ((max(k27, 1) + max(k28, 0)) == 5)
 (((max(k29, 1) - (max(k18, 1) + ((g.extent.1 + 4)/5))) + (max(k18, 1) + max(k30, 0))) == 0)
 (max(k21, 1) == max(k27, 1))
 ((max(k31, 1) + (max(k20, 0) + g.min.0)) == max(((max(k19, 1) + max(k20, 0)) + g.min.0), 100))
 (max(k32, 0) == max(k20, 0))
 ((max(k33, 1) + f.s0.y) == (t23 + 5))
 ((max(k34, 0) + t23) == f.s0.y)
 ((max(k35, 1) + ((max(k18, 1) + ((g.extent.1 + 4)/5)) - max(k29, 1))) == ((g.extent.1 + 4)/5))
 ((max(k36, 0) + (max(k29, 1) - (max(k18, 1) + ((g.extent.1 + 4)/5)))) == 0)
 (uint1)1
Substituting out g.min.0 = (max(((max(k19, 1) + max(k20, 0)) + g.min.0), 100) + ((max(k20, 0)*-1) - max(k31, 1)))
 ((max(k21, 1) + max(k22, 0)) == 5)
 ((max(k23, 1) + max(k24, 0)) == 5)
 ((max(k25, 1) + max(k26, 0)) == 5)
 ((max(k27, 1) + max(k28, 0)) == 5)
 ((max(k29, 1) + max(k30, 0)) == ((g.extent.1 + 4)/5))
 (max(k21, 1) == max(k27, 1))
 (max(k32, 0) == max(k20, 0))
 ((max(k33, 1) + f.s0.y) == (t23 + 5))
 ((max(k34, 0) + t23) == f.s0.y)
 ((max(k18, 1) + max(k35, 1)) == max(k29, 1))
 ((max(k29, 1) + max(k36, 0)) == (max(k18, 1) + ((g.extent.1 + 4)/5)))
 (uint1)1
Substituting out t23 = ((max(k33, 1) + f.s0.y) + -5)
 ((max(k21, 1) + max(k22, 0)) == 5)
 ((max(k23, 1) + max(k24, 0)) == 5)
 ((max(k25, 1) + max(k26, 0)) == 5)
 ((max(k27, 1) + max(k28, 0)) == 5)
 ((max(k29, 1) + max(k30, 0)) == ((g.extent.1 + 4)/5))
 (max(k21, 1) == max(k27, 1))
 (max(k32, 0) == max(k20, 0))
 ((max(k34, 0) + max(k33, 1)) == 5)
 ((max(k18, 1) + max(k35, 1)) == max(k29, 1))
 ((max(k29, 1) + max(k36, 0)) == (max(k18, 1) + ((g.extent.1 + 4)/5)))
 (uint1)1
Failed to disprove (((((((((((((((((((((max(k21, 1) + max(k22, 0)) == 5) && ((max(k23, 1) + max(k24, 0)) == 5)) && ((max(k25, 1) + max(k26, 0)) == 5)) && ((max(k27, 1) + max(k28, 0)) == 5)) && ((max(k29, 1) + max(k30, 0)) == ((g.extent.1 + 4)/5))) && (max(k21, 1) == max(k27, 1))) && (max(k32, 0) == max(k20, 0))) && ((max(k33, 1) + max(k34, 0)) == 5)) && ((max(k18, 1) + max(k35, 1)) == max(k29, 1))) && ((max(k29, 1) + max(k36, 0)) == (max(k18, 1) + ((g.extent.1 + 4)/5)))) && ((max(k21, 1) + max(k22, 0)) == 5)) && ((max(k23, 1) + max(k24, 0)) == 5)) && ((max(k25, 1) + max(k26, 0)) == 5)) && ((max(k27, 1) + max(k28, 0)) == 5)) && ((max(k29, 1) + max(k30, 0)) == ((g.extent.1 + 4)/5))) && (max(k21, 1) == max(k27, 1))) && (max(k32, 0) == max(k20, 0))) && ((max(k33, 1) + max(k34, 0)) == 5)) && ((max(k18, 1) + max(k35, 1)) == max(k29, 1))) && ((max(k29, 1) + max(k36, 0)) == (max(k18, 1) + ((g.extent.1 + 4)/5))))
Failure!